let X be Complex_Banach_Algebra; :: thesis: for z being Element of X
for n being Nat holds
( (z ExpSeq) . (n + 1) = ((1r / (n + 1)) * z) * ((z ExpSeq) . n) & (z ExpSeq) . 0 = 1. X & ||.((z ExpSeq) . n).|| <= (||.z.|| rExpSeq) . n )
let z be Element of X; :: thesis: for n being Nat holds
( (z ExpSeq) . (n + 1) = ((1r / (n + 1)) * z) * ((z ExpSeq) . n) & (z ExpSeq) . 0 = 1. X & ||.((z ExpSeq) . n).|| <= (||.z.|| rExpSeq) . n )
let n be Nat; :: thesis: ( (z ExpSeq) . (n + 1) = ((1r / (n + 1)) * z) * ((z ExpSeq) . n) & (z ExpSeq) . 0 = 1. X & ||.((z ExpSeq) . n).|| <= (||.z.|| rExpSeq) . n )
defpred S₁[ Nat] means ||.((z ExpSeq) . $1).|| <= (||.z.|| rExpSeq) . $1;
A1: (z ExpSeq) . 0 = (1r / (0 !)) * (z #N 0) by Def1
.= (1r / (0 !)) * ((z GeoSeq) . 0) by CLOPBAN3:def 8
.= 1r * (1. X) by CLOPBAN3:def 7, SIN_COS:1
.= 1. X by CLVECT_1:def 5 ;

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

let n be Nat; :: thesis: (z ExpSeq) . (n + 1) = ((1r / (n + 1)) * z) * ((z ExpSeq) . n)
thus (z ExpSeq) . (n + 1) = (1r / ((n + 1) !)) * (z #N (n + 1)) by Def1
.= (1r / ((n + 1) !)) * ((z GeoSeq) . (n + 1)) by CLOPBAN3:def 8
.= (1r / ((n + 1) !)) * (((z GeoSeq) . n) * z) by CLOPBAN3:def 7
.= (1r / ((n + 1) !)) * ((z #N n) * z) by CLOPBAN3:def 8
.= (1r / ((n !) * (n + 1))) * ((z #N n) * z) by SIN_COS:1
.= ((1r * 1r) / ((n !) * (n + 1))) * (z * (z #N n)) by Lm1, COMPLEX1:def 4
.= ((1r / (n !)) * (1r / (n + 1))) * (z * (z #N n)) by XCMPLX_1:76
.= ((1r / (n + 1)) * z) * ((1r / (n !)) * (z #N n)) by CLOPBAN3:38
.= ((1r / (n + 1)) * z) * ((z ExpSeq) . n) by Def1 ; :: 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 <= ||.((1r / (n + 1)) * z).|| by CLVECT_1:105;
then A5: ||.((1r / (n + 1)) * z).|| * ||.((z ExpSeq) . n).|| <= ||.((1r / (n + 1)) * z).|| * ((||.z.|| rExpSeq) . n) by A4, XREAL_1:64;
A6: ||.(((1r / (n + 1)) * z) * ((z ExpSeq) . n)).|| <= ||.((1r / (n + 1)) * z).|| * ||.((z ExpSeq) . n).|| by CLOPBAN3:38;
|.(n + 1).| = n + 1 by ABSVALUE:def 1;
then |.(1r / (n + 1)).| = 1 / (n + 1) by COMPLEX1:48, COMPLEX1:67;
then A7: ||.((1r / (n + 1)) * z).|| = (1 / (n + 1)) * ||.z.|| by CLVECT_1:def 13;
A8: ((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 ;
||.((z ExpSeq) . (n + 1)).|| = ||.(((1r / (n + 1)) * z) * ((z ExpSeq) . n)).|| by A2;
hence S₁[n + 1] by A6, A7, A5, A8, 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, CLOPBAN3:38;
for n being Nat holds S₁[n] from NAT_1:sch 2(A9, A3);
hence ( (z ExpSeq) . (n + 1) = ((1r / (n + 1)) * z) * ((z ExpSeq) . n) & (z ExpSeq) . 0 = 1. X & ||.((z ExpSeq) . n).|| <= (||.z.|| rExpSeq) . n ) by A2, A1; :: thesis: verum