let X be Banach_Algebra; :: thesis: for z being Element of X
for n being Nat holds
( (z rExpSeq) . (n + 1) = ((1 / (n + 1)) * z) * ((z rExpSeq) . n) & (z rExpSeq) . 0 = 1. X & ||.((z rExpSeq) . n).|| <= (||.z.|| rExpSeq) . n )
let z be Element of X; :: thesis: for n being Nat holds
( (z rExpSeq) . (n + 1) = ((1 / (n + 1)) * z) * ((z rExpSeq) . n) & (z rExpSeq) . 0 = 1. X & ||.((z rExpSeq) . n).|| <= (||.z.|| rExpSeq) . n )
let n be Nat; :: thesis: ( (z rExpSeq) . (n + 1) = ((1 / (n + 1)) * z) * ((z rExpSeq) . n) & (z rExpSeq) . 0 = 1. X & ||.((z rExpSeq) . n).|| <= (||.z.|| rExpSeq) . n )
defpred S₁[ Nat] means ||.((z rExpSeq) . $1).|| <= (||.z.|| rExpSeq) . $1;
A1: (z rExpSeq) . 0 = (1 / (0 !)) * (z #N 0) by Def2
.= (1 / 1) * (1. X) by LOPBAN_3:def 9, NEWTON:12
.= 1. X by RLVECT_1:def 8 ;

A2: now :: thesis: for n being Nat holds (z rExpSeq) . (n + 1) = ((1 / (n + 1)) * z) * ((z rExpSeq) . n)

let n be Nat; :: thesis: (z rExpSeq) . (n + 1) = ((1 / (n + 1)) * z) * ((z rExpSeq) . n)
thus (z rExpSeq) . (n + 1) = (1 / ((n + 1) !)) * (z #N (n + 1)) by Def2
.= (1 / ((n + 1) !)) * (((z GeoSeq) . n) * z) by LOPBAN_3:def 9
.= (1 / ((n !) * (n + 1))) * ((z #N n) * z) by NEWTON:15
.= ((1 * 1) / ((n !) * (n + 1))) * (z * (z #N n)) by Lm1
.= ((1 / (n !)) * (1 / (n + 1))) * (z * (z #N n)) by XCMPLX_1:76
.= ((1 / (n + 1)) * z) * ((1 / (n !)) * (z #N n)) by LOPBAN_3:38
.= ((1 / (n + 1)) * z) * ((z rExpSeq) . n) by Def2 ; :: thesis: verum

end;

A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
0 <= ||.((1 / (n + 1)) * z).|| by NORMSP_1:4;
then A5: ||.((1 / (n + 1)) * z).|| * ||.((z rExpSeq) . n).|| <= ||.((1 / (n + 1)) * z).|| * ((||.z.|| rExpSeq) . n) by A4, XREAL_1:64;
A6: ||.(((1 / (n + 1)) * z) * ((z rExpSeq) . n)).|| <= ||.((1 / (n + 1)) * z).|| * ||.((z rExpSeq) . n).|| by LOPBAN_3:38;
A7: ((1 / (n + 1)) * ||.z.||) * ((||.z.|| rExpSeq) . n) = (1 / (n + 1)) * (((||.z.|| rExpSeq) . n) * ||.z.||)
.= (1 / (n + 1)) * (((||.z.|| |^ n) / (n !)) * ||.z.||) by SIN_COS:def 5
.= (1 / (n + 1)) * (((||.z.|| |^ n) * ||.z.||) / (n !)) by XCMPLX_1:74
.= (1 / (n + 1)) * ((||.z.|| |^ (n + 1)) / (n !)) by NEWTON:6
.= (||.z.|| |^ (n + 1)) / ((n !) * (n + 1)) by XCMPLX_1:103
.= (||.z.|| |^ (n + 1)) / ((n + 1) !) by NEWTON:15
.= (||.z.|| rExpSeq) . (n + 1) by SIN_COS:def 5 ;
A8: ||.((1 / (n + 1)) * z).|| = |.(1 / (n + 1)).| * ||.z.|| by NORMSP_1:def 1
.= (1 / (n + 1)) * ||.z.|| by ABSVALUE:def 1 ;
||.((z rExpSeq) . (n + 1)).|| = ||.(((1 / (n + 1)) * z) * ((z rExpSeq) . n)).|| by A2;
hence S₁[n + 1] by A6, A8, A5, A7, XXREAL_0:2; :: thesis: verum

end;

(||.z.|| rExpSeq) . 0 = (||.z.|| |^ 0) / (0 !) by SIN_COS:def 5
.= 1 / (0 !) by NEWTON:4
.= 1 / (Prod_real_n . 0) by SIN_COS:def 3
.= 1 / 1 by SIN_COS:def 2
.= 1 ;
then A9: S₁[ 0 ] by A1, LOPBAN_3:38;
for n being Nat holds S₁[n] from NAT_1:sch 2(A9, A3);
hence ( (z rExpSeq) . (n + 1) = ((1 / (n + 1)) * z) * ((z rExpSeq) . n) & (z rExpSeq) . 0 = 1. X & ||.((z rExpSeq) . n).|| <= (||.z.|| rExpSeq) . n ) by A2, A1; :: thesis: verum