let X be 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
defpred S₁[ Nat] means 0 <= ||.z.|| |^ $1;
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[k + 1]
A3: 0 <= ||.z.|| by NORMSP_1:4;
||.z.|| |^ (k + 1) = (||.z.|| |^ k) * ||.z.|| by NEWTON:6;
hence S₁[k + 1] by A2, A3; :: thesis: verum

end;

A4: S₁[ 0 ] by NEWTON:4;
let n be Nat; :: thesis: 0 <= (||.z.|| rExpSeq) . n
for k being Nat holds S₁[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