let X be Complex_Banach_Algebra; :: thesis: for z being Element of X
for n being Element of 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 Element of 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 Element of 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 !c )) * (z #N 0 ) by Def2
.= (1r / (0 !c )) * ((z GeoSeq ) . 0 ) by CLOPBAN3:def 13
.= 1r * (1. X) by CLOPBAN3:def 12, SIN_COS:1
.= 1. X by CLVECT_1:def 2 ;

A2: now

let n be Element of NAT ; :: thesis: (z ExpSeq ) . (n + 1) = ((1r / (n + 1)) * z) * ((z ExpSeq ) . n)
thus (z ExpSeq ) . (n + 1) = (1r / ((n + 1) !c )) * (z #N (n + 1)) by Def2
.= (1r / ((n + 1) !c )) * ((z GeoSeq ) . (n + 1)) by CLOPBAN3:def 13
.= (1r / ((n + 1) !c )) * (((z GeoSeq ) . n) * z) by CLOPBAN3:def 12
.= (1r / ((n + 1) !c )) * ((z #N n) * z) by CLOPBAN3:def 13
.= (1r / ((n !c ) * (n + 1))) * ((z #N n) * z) by SIN_COS:1
.= ((1r * 1r ) / ((n !c ) * (n + 1))) * (z * (z #N n)) by Lm1, COMPLEX1:def 7
.= ((1r / (n !c )) * (1r / (n + 1))) * (z * (z #N n)) by XCMPLX_1:77
.= ((1r / (n + 1)) * z) * ((1r / (n !c )) * (z #N n)) by CLOPBAN3:42
.= ((1r / (n + 1)) * z) * ((z ExpSeq ) . n) by Def2 ; :: thesis: verum

end;

A3: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
0 <= ||.((1r / (n + 1)) * z).|| by CLVECT_1:106;
then A5: ||.((1r / (n + 1)) * z).|| * ||.((z ExpSeq ) . n).|| <= ||.((1r / (n + 1)) * z).|| * ((||.z.|| rExpSeq ) . n) by A4, XREAL_1:66;
A6: ||.(((1r / (n + 1)) * z) * ((z ExpSeq ) . n)).|| <= ||.((1r / (n + 1)) * z).|| * ||.((z ExpSeq ) . n).|| by CLOPBAN3:42;
0 <= n + 1 by NAT_1:2;
then |.(n + 1).| = n + 1 by ABSVALUE:def 1;
then |.(1r / (n + 1)).| = 1 / (n + 1) by COMPLEX1:134, COMPLEX1:153;
then A7: ||.((1r / (n + 1)) * z).|| = (1 / (n + 1)) * ||.z.|| by CLVECT_1:def 11;
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 9
.= (1 / (n + 1)) * (((||.z.|| |^ n) * ||.z.||) / (n ! )) by XCMPLX_1:75
.= (1 / (n + 1)) * ((||.z.|| |^ (n + 1)) / (n ! )) by NEWTON:11
.= (||.z.|| |^ (n + 1)) / ((n ! ) * (n + 1)) by XCMPLX_1:104
.= (||.z.|| |^ (n + 1)) / ((n + 1) ! ) by NEWTON:21
.= (||.z.|| rExpSeq ) . (n + 1) by SIN_COS:def 9 ;
||.((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 9
.= 1 / (0 ! ) by NEWTON:9
.= 1 / (Prod_real_n . 0 ) by SIN_COS:def 7
.= 1 / 1 by SIN_COS:def 5
.= 1 ;
then A9: S₁[ 0 ] by A1, CLOPBAN3:42;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(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