let X be Complex_Banach_Algebra; :: thesis: for z being Element of X

for n being Nat holds 0 <= (||.z.|| rExpSeq) . n

let z be Element of X; :: thesis: for n being Nat holds 0 <= (||.z.|| rExpSeq) . n

let n be Nat; :: thesis: 0 <= (||.z.|| rExpSeq) . n

defpred S_{1}[ Nat] means 0 <= ||.z.|| |^ $1;

A1: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
by NEWTON:4;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A4, A1);

then A5: 0 <= ||.z.|| |^ n ;

A6: (||.z.|| |^ n) / (n !) = (||.z.|| |^ n) * ((n !) ") by XCMPLX_0:def 9;

thus 0 <= (||.z.|| rExpSeq) . n by A5, A6, SIN_COS:def 5; :: thesis: verum

for n being Nat holds 0 <= (||.z.|| rExpSeq) . n

let z be Element of X; :: thesis: for n being Nat holds 0 <= (||.z.|| rExpSeq) . n

let n be Nat; :: thesis: 0 <= (||.z.|| rExpSeq) . n

defpred S

A1: for k being Nat st S

S

proof

A4:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A2: S_{1}[k]
; :: thesis: S_{1}[k + 1]

A3: 0 <= ||.z.|| by CLVECT_1:105;

||.z.|| |^ (k + 1) = (||.z.|| |^ k) * ||.z.|| by NEWTON:6;

hence S_{1}[k + 1]
by A2, A3; :: thesis: verum

end;assume A2: S

A3: 0 <= ||.z.|| by CLVECT_1:105;

||.z.|| |^ (k + 1) = (||.z.|| |^ k) * ||.z.|| by NEWTON:6;

hence S

for k being Nat holds S

then A5: 0 <= ||.z.|| |^ n ;

A6: (||.z.|| |^ n) / (n !) = (||.z.|| |^ n) * ((n !) ") by XCMPLX_0:def 9;

thus 0 <= (||.z.|| rExpSeq) . n by A5, A6, SIN_COS:def 5; :: thesis: verum