let X be Complex_Banach_Algebra; :: thesis: for z being Element of X
for n being Element of NAT holds 0 <= (||.z.|| rExpSeq ) . n
let z be Element of X; :: thesis: for n being Element of NAT holds 0 <= (||.z.|| rExpSeq ) . n
let n be Element of NAT ; :: thesis: 0 <= (||.z.|| rExpSeq ) . n
defpred S₁[ Element of NAT ] means 0 <= ||.z.|| |^ $1;
A1: n ! > 0 by NEWTON:23;
A2: S₁[ 0 ] by NEWTON:9;
A3: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
A5: ||.z.|| |^ (k + 1) = (||.z.|| |^ k) * ||.z.|| by NEWTON:11;
0 <= ||.z.|| by CLVECT_1:106;
hence S₁[k + 1] by A4, A5; :: thesis: verum

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A2, A3);
then A6: 0 <= ||.z.|| |^ n ;
A7: (||.z.|| |^ n) / (n ! ) = (||.z.|| |^ n) * ((n ! ) " ) by XCMPLX_0:def 9;
0 < (n ! ) " by A1;
then 0 <= (||.z.|| |^ n) * ((n ! ) " ) by A6;
hence 0 <= (||.z.|| rExpSeq ) . n by A7, SIN_COS:def 9; :: thesis: verum