let X be Banach_Algebra; :: thesis: for z being Element of X
for n being Element of 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 Element of 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 Element of 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₁[ Element of 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 13, NEWTON:18
.= 1. X by RLVECT_1:def 9 ;

A2: now

let n be Element of 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 13
.= (1 / ((n ! ) * (n + 1))) * ((z #N n) * z) by NEWTON:21
.= ((1 * 1) / ((n ! ) * (n + 1))) * (z * (z #N n)) by Lm1
.= ((1 / (n ! )) * (1 / (n + 1))) * (z * (z #N n)) by XCMPLX_1:77
.= ((1 / (n + 1)) * z) * ((1 / (n ! )) * (z #N n)) by LOPBAN_3:43
.= ((1 / (n + 1)) * z) * ((z rExpSeq ) . 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 <= ||.((1 / (n + 1)) * z).|| by NORMSP_1:8;
then A5: ||.((1 / (n + 1)) * z).|| * ||.((z rExpSeq ) . n).|| <= ||.((1 / (n + 1)) * z).|| * ((||.z.|| rExpSeq ) . n) by A4, XREAL_1:66;
A6: ||.(((1 / (n + 1)) * z) * ((z rExpSeq ) . n)).|| <= ||.((1 / (n + 1)) * z).|| * ||.((z rExpSeq ) . n).|| by LOPBAN_3:43;
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 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 ;
A8: ||.((1 / (n + 1)) * z).|| = (abs (1 / (n + 1))) * ||.z.|| by NORMSP_1:def 2
.= (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 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, LOPBAN_3:43;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(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