let X be Complex_Banach_Algebra; :: thesis: for z being Element of X
for k being Nat holds
( ||.((Partial_Sums (z ExpSeq)) . k).|| <= (Partial_Sums (||.z.|| rExpSeq)) . k & (Partial_Sums (||.z.|| rExpSeq)) . k <= Sum (||.z.|| rExpSeq) & ||.((Partial_Sums (z ExpSeq)) . k).|| <= Sum (||.z.|| rExpSeq) )
let z be Element of X; :: thesis: for k being Nat holds
( ||.((Partial_Sums (z ExpSeq)) . k).|| <= (Partial_Sums (||.z.|| rExpSeq)) . k & (Partial_Sums (||.z.|| rExpSeq)) . k <= Sum (||.z.|| rExpSeq) & ||.((Partial_Sums (z ExpSeq)) . k).|| <= Sum (||.z.|| rExpSeq) )
let k be Nat; :: thesis: ( ||.((Partial_Sums (z ExpSeq)) . k).|| <= (Partial_Sums (||.z.|| rExpSeq)) . k & (Partial_Sums (||.z.|| rExpSeq)) . k <= Sum (||.z.|| rExpSeq) & ||.((Partial_Sums (z ExpSeq)) . k).|| <= Sum (||.z.|| rExpSeq) )
defpred S₁[ Nat] means ||.((Partial_Sums (z ExpSeq)) . $1).|| <= (Partial_Sums (||.z.|| rExpSeq)) . $1;
A1: (Partial_Sums (||.z.|| rExpSeq)) . 0 = (||.z.|| rExpSeq) . 0 by SERIES_1:def 1
.= (||.z.|| |^ 0) / (0 !) by SIN_COS:def 5
.= 1 by NEWTON:4, NEWTON:12 ;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume ||.((Partial_Sums (z ExpSeq)) . k).|| <= (Partial_Sums (||.z.|| rExpSeq)) . k ; :: thesis: S₁[k + 1]
then A3: ||.((Partial_Sums (z ExpSeq)) . k).|| + ((||.z.|| rExpSeq) . (k + 1)) <= ((Partial_Sums (||.z.|| rExpSeq)) . k) + ((||.z.|| rExpSeq) . (k + 1)) by XREAL_1:6;
A4: ||.(((Partial_Sums (z ExpSeq)) . k) + ((z ExpSeq) . (k + 1))).|| <= ||.((Partial_Sums (z ExpSeq)) . k).|| + ||.((z ExpSeq) . (k + 1)).|| by CLOPBAN3:38;
||.((z ExpSeq) . (k + 1)).|| <= (||.z.|| rExpSeq) . (k + 1) by Th13;
then A5: ||.((Partial_Sums (z ExpSeq)) . k).|| + ||.((z ExpSeq) . (k + 1)).|| <= ||.((Partial_Sums (z ExpSeq)) . k).|| + ((||.z.|| rExpSeq) . (k + 1)) by XREAL_1:7;
A6: ((Partial_Sums (||.z.|| rExpSeq)) . k) + ((||.z.|| rExpSeq) . (k + 1)) = (Partial_Sums (||.z.|| rExpSeq)) . (k + 1) by SERIES_1:def 1;
||.((Partial_Sums (z ExpSeq)) . (k + 1)).|| = ||.(((Partial_Sums (z ExpSeq)) . k) + ((z ExpSeq) . (k + 1))).|| by BHSP_4:def 1;
then ||.((Partial_Sums (z ExpSeq)) . (k + 1)).|| <= ||.((Partial_Sums (z ExpSeq)) . k).|| + ((||.z.|| rExpSeq) . (k + 1)) by A4, A5, XXREAL_0:2;
hence S₁[k + 1] by A3, A6, XXREAL_0:2; :: thesis: verum

end;

||.((Partial_Sums (z ExpSeq)) . 0).|| = ||.((z ExpSeq) . 0).|| by BHSP_4:def 1
.= ||.((1r / (0 !)) * (z #N 0)).|| by Def1
.= ||.((1r / (0 !)) * ((z GeoSeq) . 0)).|| by CLOPBAN3:def 8
.= ||.(1r * (1. X)).|| by CLOPBAN3:def 7, SIN_COS:1
.= ||.(1. X).|| by CLVECT_1:def 5
.= 1 by CLOPBAN3:38 ;
then A7: S₁[ 0 ] by A1;
A8: for k being Nat holds S₁[k] from NAT_1:sch 2(A7, A2);
hence ||.((Partial_Sums (z ExpSeq)) . k).|| <= (Partial_Sums (||.z.|| rExpSeq)) . k ; :: thesis: ( (Partial_Sums (||.z.|| rExpSeq)) . k <= Sum (||.z.|| rExpSeq) & ||.((Partial_Sums (z ExpSeq)) . k).|| <= Sum (||.z.|| rExpSeq) )
A9: for n being Nat holds 0 <= (||.z.|| rExpSeq) . n by Th26;
||.z.|| rExpSeq is summable by SIN_COS:45;
then A10: Partial_Sums (||.z.|| rExpSeq) is bounded_above by A9, SERIES_1:17;
then (Partial_Sums (||.z.|| rExpSeq)) . k <= lim (Partial_Sums (||.z.|| rExpSeq)) by A9, SEQ_4:37, SERIES_1:16;
hence (Partial_Sums (||.z.|| rExpSeq)) . k <= Sum (||.z.|| rExpSeq) by SERIES_1:def 3; :: thesis: ||.((Partial_Sums (z ExpSeq)) . k).|| <= Sum (||.z.|| rExpSeq)

now :: thesis: for k being Nat holds (Partial_Sums (||.z.|| rExpSeq)) . k <= Sum (||.z.|| rExpSeq)

let k be Nat; :: thesis: (Partial_Sums (||.z.|| rExpSeq)) . k <= Sum (||.z.|| rExpSeq)
lim (Partial_Sums (||.z.|| rExpSeq)) = Sum (||.z.|| rExpSeq) by SERIES_1:def 3;
hence (Partial_Sums (||.z.|| rExpSeq)) . k <= Sum (||.z.|| rExpSeq) by A9, A10, SEQ_4:37, SERIES_1:16; :: thesis: verum

end;

then A11: (Partial_Sums (||.z.|| rExpSeq)) . k <= Sum (||.z.|| rExpSeq) ;
||.((Partial_Sums (z ExpSeq)) . k).|| <= (Partial_Sums (||.z.|| rExpSeq)) . k by A8;
hence ||.((Partial_Sums (z ExpSeq)) . k).|| <= Sum (||.z.|| rExpSeq) by A11, XXREAL_0:2; :: thesis: verum