>>511
横レスだが、f ' (x)＝ f(x), f(0)＝1 なる関数の
存在性・一意性に限って言えば、そこまで高級な議論は必要ない。

存在性：f(x)＝Σ[k＝0〜∞](x^k)/k! と置けばよい。
任意の x∈R に対して右辺が収束していることは簡単に出る。
f(0)＝1 は簡単に出る。f ' (x)＝f(x) は次の補題から簡単に出る。

補題：実数列 { f_n(k) }_k (n∈N)と実数列 { f(k) }_k, { g(k) }_k は次を満たすとする。
・lim[n→∞]f_n(k)＝f(k) (∀n).
・|f_n(k)|≦g(k) (∀k, ∀n).
・Σ[k＝1〜∞]g(k)＜∞.
このとき Σ[k＝1〜∞]f_n(k) (n∈N) 及び Σ[k＝1〜∞]f(k)が存在して、しかも
lim[n→∞]Σ[k＝1〜∞]f_n(k)＝Σ[k＝1〜∞]f(k)
が成り立つ。

上記の補題は簡単なε−δ論法で証明できる。