Proof of Power Series: the Sequence of Terms, the Coefficients 1/(k-1)!, and the Sum as a Map on the Set of Convergence

$\mathbb{R}$, with $+$, $\cdot$, $0$ and $1$, is a field by The Structure of ℝ as a Field and an Ordered Ring (i), hence a commutative ring by Fields (i). Sequences in $\mathbb{R}$ are maps $\mathbb{N}\to\mathbb{R}$ by Sequences (i), so two of them with the same $k$-th term for every $k\in\mathbb{N}$ are equal by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv); this gives the uniqueness in (i) and (ii), and only existence is shown below.

Proof of (i). Let $u\in\mathbb{R}$. By Maps Given by Iterated Operations: Partial Iterates, Images of Natural Numbers, Powers and Operations over a Finite Set (iv) there is a map $P:\mathbb{N}_{0}\to\mathbb{R}$ with $P(n)=u^{n}$ for every $n\in\mathbb{N}_{0}$. By Sequences of Real Numbers Built from Given Ones: Partial Sums, Index Shifts, Predecessor Reindexing, Absolute Values and Termwise Operations (iii), with $q=P$, there is a sequence $(r_{k})$ in $\mathbb{R}$ with $r_{k}=P(k-1)=u^{k-1}$ for every $k\in\mathbb{N}$. By Sequences of Real Numbers Built from Given Ones: Partial Sums, Index Shifts, Predecessor Reindexing, Absolute Values and Termwise Operations (v), applied to $(c_{k})$ and $(r_{k})$, there is a sequence in $\mathbb{R}$ whose $k$-th term is $c_{k}r_{k}=c_{k}u^{k-1}$ for every $k\in\mathbb{N}$.

Proof of (ii). By The Factorial as a Map on the Natural Numbers with Zero (i) there is a map $F:\mathbb{N}_{0}\to\mathbb{N}_{0}$ with $F(n)=n!$, and by Maps Given by Iterated Operations: Partial Iterates, Images of Natural Numbers, Powers and Operations over a Finite Set (ii), with $R=\mathbb{R}$, a map $\nu:\mathbb{N}_{0}\to\mathbb{R}$ with $\nu(n)=n_{\mathbb{R}}$, for every $n\in\mathbb{N}_{0}$. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (ii), $\chi=\nu\circ F$ is a map $\mathbb{N}_{0}\to\mathbb{R}$ with $\chi(n)=\nu(n!)=(n!)_{\mathbb{R}}$, which is $n!$ read in $\mathbb{R}$; it is nonzero by Natural Numbers and Factorials Read in the Reals: the Order Carries Over, One Is Least, and Factorials Are Positive, Recursive and Nondecreasing (iii). By The Reciprocal and the Quotient of Real-Valued Maps with a Nonvanishing Denominator Are Maps (i), with $E=\mathbb{N}_{0}$, there is a map $\rho:\mathbb{N}_{0}\to\mathbb{R}$ with $\rho(n)=1/\chi(n)=1/n!$ for every $n\in\mathbb{N}_{0}$. By Sequences of Real Numbers Built from Given Ones: Partial Sums, Index Shifts, Predecessor Reindexing, Absolute Values and Termwise Operations (iii), with $q=\rho$, there is a sequence in $\mathbb{R}$ whose $k$-th term is $\rho(k-1)=1/(k-1)!$ for every $k\in\mathbb{N}$.

Proof of (iii). The term maps. Let $k\in\mathbb{N}$. For $u\in\mathbb{R}$, $c_{k}\in\mathbb{R}$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (ii), and $c_{k}u^{k-1}\in\mathbb{R}$. The expression $c(k)\cdot u^{k-1}$ is built from variables and defined set symbols used properly for $k\in\mathbb{N}$ and $u\in\mathbb{R}$, with no class abstraction written in it: the value $c(k)$ and the product, eliminated as in Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (x) and Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (xi); the difference $k-1$, defined as $1\le k$ by Arithmetic and Order of the Natural Numbers (x), the only $j\in\mathbb{N}_{0}$ with $((1,j),k)\in{+}$ for the addition of $\mathbb{N}_{0}$, a predicative condition by Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (iv); and the power $u^{k-1}$, the only $p$ with $p=u^{k-1}$, a condition expressed by a predicative formula by Predicative Formulas for the Derivative Condition and for Powers (ii), its variables $t$, $m$ and $z$ renamed to $u$, $j$ and $p$ by Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (i); the last two are eliminated as in Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (ii). So Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (v) applies, with $\mathbb{R}$ for its $A$ and $B$, the single variable $k$ for $v_{1}$, the guard $k\in\mathbb{N}$ for $\gamma$, and $c(k)\cdot u^{k-1}$ for $t(u,k)$: the map $g_{k}:\mathbb{R}\to\mathbb{R}$, $u\mapsto c_{k}u^{k-1}$, of Sets and Maps: Ordinary Notation (v) is the only set satisfying the predicative formula $\theta$ there, and is thus a defined set symbol with argument $k$, used properly where $k\in\mathbb{N}$. It lies in $\mathbb{R}^{\mathbb{R}}$ by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i). By Maps and Relations Given by Formulas (i), with $\mathbb{N}$ and $\mathbb{R}^{\mathbb{R}}$ for its $a$ and $b$, $\mathbb{R}^{\mathbb{R}}$ being a set by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (ii), $k\mapsto g_{k}$ is a map $\mathbb{N}\to\mathbb{R}^{\mathbb{R}}$, a sequence $(g_{k})_{k\in\mathbb{N}}$ in $\mathbb{R}^{\mathbb{R}}$ by Sequences (i).

The sum. By Sequences of Real-Valued Maps: the Map of Pointwise Limits on a Subset, and the Sequence of Pointwise Partial Sums (ii), with $D=\mathbb{R}$, there is a sequence $(s_{n})_{n\in\mathbb{N}}$ in $\mathbb{R}^{\mathbb{R}}$ such that, for every $u\in\mathbb{R}$, $(s_{n}(u))_{n}$ is the sequence of partial sums of $(g_{k}(u))_{k}$. Let $u\in E$. The sequence $(g_{k}(u))_{k}$ of The Sequences k ↦ f_k(p) of a Sequence in ℝ^I, and the Map of Their Limits (i) has $k$-th term $g_{k}(u)=c_{k}u^{k-1}$ for every $k\in\mathbb{N}$, so it is the sequence of (i) for this $u$, by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv). By hypothesis its series converges, so by Series of Real Numbers: Partial Sums, Convergence, the Sum and Absolute Convergence (ii) $(s_{n}(u))_{n}$ is convergent, with limit $\lim_{n\to\infty}s_{n}(u)=\sum_{k=1}^{\infty}c_{k}u^{k-1}$. $E$ is a set, being a subclass of $\mathbb{R}$ (Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper (i)). By Sequences of Real-Valued Maps: the Map of Pointwise Limits on a Subset, and the Sequence of Pointwise Partial Sums (i), with $D=\mathbb{R}$, $E$ for its $S$ and $(s_{n})$ for $(f_{k})$, there is exactly one map $h:E\to\mathbb{R}$ with $h(u)=\lim_{n\to\infty}s_{n}(u)$ for every $u\in E$, that is, with $h(u)=\sum_{k=1}^{\infty}c_{k}u^{k-1}$ for every $u\in E$.