let Z be open Subset of REAL; :: thesis: for n being Nat holds (diff (exp_R,Z)) . n = exp_R | Z

let n be Nat; :: thesis: (diff (exp_R,Z)) . n = exp_R | Z

defpred S_{1}[ Nat] means (diff (exp_R,Z)) . $1 = exp_R | Z;

A1: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
by TAYLOR_1:def 5;

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A4, A1);

hence (diff (exp_R,Z)) . n = exp_R | Z ; :: thesis: verum

let n be Nat; :: thesis: (diff (exp_R,Z)) . n = exp_R | Z

defpred S

A1: for k being Nat st S

S

proof

A4:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A2: S_{1}[k]
; :: thesis: S_{1}[k + 1]

A3: exp_R is_differentiable_on Z by FDIFF_1:26, TAYLOR_1:16;

(diff (exp_R,Z)) . (k + 1) = ((diff (exp_R,Z)) . k) `| Z by TAYLOR_1:def 5

.= exp_R `| Z by A2, A3, FDIFF_2:16

.= exp_R | Z by Th5 ;

hence S_{1}[k + 1]
; :: thesis: verum

end;assume A2: S

A3: exp_R is_differentiable_on Z by FDIFF_1:26, TAYLOR_1:16;

(diff (exp_R,Z)) . (k + 1) = ((diff (exp_R,Z)) . k) `| Z by TAYLOR_1:def 5

.= exp_R `| Z by A2, A3, FDIFF_2:16

.= exp_R | Z by Th5 ;

hence S

for n being Nat holds S

hence (diff (exp_R,Z)) . n = exp_R | Z ; :: thesis: verum