let X be Banach_Algebra; :: thesis: for z being Element of X
for k being Element of NAT holds
( ||.((Partial_Sums (z rExpSeq )) . k).|| <= (Partial_Sums (||.z.|| rExpSeq )) . k & (Partial_Sums (||.z.|| rExpSeq )) . k <= Sum (||.z.|| rExpSeq ) & ||.((Partial_Sums (z rExpSeq )) . k).|| <= Sum (||.z.|| rExpSeq ) )
let z be Element of X; :: thesis: for k being Element of NAT holds
( ||.((Partial_Sums (z rExpSeq )) . k).|| <= (Partial_Sums (||.z.|| rExpSeq )) . k & (Partial_Sums (||.z.|| rExpSeq )) . k <= Sum (||.z.|| rExpSeq ) & ||.((Partial_Sums (z rExpSeq )) . k).|| <= Sum (||.z.|| rExpSeq ) )
let k be Element of NAT ; :: thesis: ( ||.((Partial_Sums (z rExpSeq )) . k).|| <= (Partial_Sums (||.z.|| rExpSeq )) . k & (Partial_Sums (||.z.|| rExpSeq )) . k <= Sum (||.z.|| rExpSeq ) & ||.((Partial_Sums (z rExpSeq )) . k).|| <= Sum (||.z.|| rExpSeq ) )
defpred S₁[ Element of NAT ] means ||.((Partial_Sums (z rExpSeq )) . $1).|| <= (Partial_Sums (||.z.|| rExpSeq )) . $1;
A1: ||.((Partial_Sums (z rExpSeq )) . 0 ).|| = ||.((z rExpSeq ) . 0 ).|| by BHSP_4:def 1
.= ||.((1 / (0 ! )) * (z #N 0 )).|| by Def2
.= ||.((1 / 1) * (1. X)).|| by LOPBAN_3:def 13, NEWTON:18
.= ||.(1. X).|| by LOPBAN_3:43
.= 1 by LOPBAN_3:43 ;
(Partial_Sums (||.z.|| rExpSeq )) . 0 = (||.z.|| rExpSeq ) . 0 by SERIES_1:def 1
.= (||.z.|| |^ 0 ) / (0 ! ) by SIN_COS:def 9
.= 1 by NEWTON:9, NEWTON:18 ;
then A2: S₁[ 0 ] by A1;
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: ||.((Partial_Sums (z rExpSeq )) . k).|| <= (Partial_Sums (||.z.|| rExpSeq )) . k ; :: thesis: S₁[k + 1]
A5: ||.((Partial_Sums (z rExpSeq )) . (k + 1)).|| = ||.(((Partial_Sums (z rExpSeq )) . k) + ((z rExpSeq ) . (k + 1))).|| by BHSP_4:def 1;
A6: ||.(((Partial_Sums (z rExpSeq )) . k) + ((z rExpSeq ) . (k + 1))).|| <= ||.((Partial_Sums (z rExpSeq )) . k).|| + ||.((z rExpSeq ) . (k + 1)).|| by LOPBAN_3:43;
||.((z rExpSeq ) . (k + 1)).|| <= (||.z.|| rExpSeq ) . (k + 1) by Th14;
then ||.((Partial_Sums (z rExpSeq )) . k).|| + ||.((z rExpSeq ) . (k + 1)).|| <= ||.((Partial_Sums (z rExpSeq )) . k).|| + ((||.z.|| rExpSeq ) . (k + 1)) by XREAL_1:9;
then A7: ||.((Partial_Sums (z rExpSeq )) . (k + 1)).|| <= ||.((Partial_Sums (z rExpSeq )) . k).|| + ((||.z.|| rExpSeq ) . (k + 1)) by A5, A6, XXREAL_0:2;
A8: ||.((Partial_Sums (z rExpSeq )) . k).|| + ((||.z.|| rExpSeq ) . (k + 1)) <= ((Partial_Sums (||.z.|| rExpSeq )) . k) + ((||.z.|| rExpSeq ) . (k + 1)) by A4, XREAL_1:8;
((Partial_Sums (||.z.|| rExpSeq )) . k) + ((||.z.|| rExpSeq ) . (k + 1)) = (Partial_Sums (||.z.|| rExpSeq )) . (k + 1) by SERIES_1:def 1;
hence S₁[k + 1] by A7, A8, XXREAL_0:2; :: thesis: verum

end;

A9: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A2, A3);
hence ||.((Partial_Sums (z rExpSeq )) . k).|| <= (Partial_Sums (||.z.|| rExpSeq )) . k ; :: thesis: ( (Partial_Sums (||.z.|| rExpSeq )) . k <= Sum (||.z.|| rExpSeq ) & ||.((Partial_Sums (z rExpSeq )) . k).|| <= Sum (||.z.|| rExpSeq ) )
A10: for n being Element of NAT holds 0 <= (||.z.|| rExpSeq ) . n by Th27;
then A11: Partial_Sums (||.z.|| rExpSeq ) is non-decreasing by SERIES_1:19;
||.z.|| rExpSeq is summable by SIN_COS:49;
then A12: Partial_Sums (||.z.|| rExpSeq ) is bounded_above by A10, SERIES_1:20;
then (Partial_Sums (||.z.|| rExpSeq )) . k <= lim (Partial_Sums (||.z.|| rExpSeq )) by A11, SEQ_4:54;
hence (Partial_Sums (||.z.|| rExpSeq )) . k <= Sum (||.z.|| rExpSeq ) by SERIES_1:def 3; :: thesis: ||.((Partial_Sums (z rExpSeq )) . k).|| <= Sum (||.z.|| rExpSeq )

A13: now

let k be Element of 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 A11, A12, SEQ_4:54; :: thesis: verum

end;

A14: ||.((Partial_Sums (z rExpSeq )) . k).|| <= (Partial_Sums (||.z.|| rExpSeq )) . k by A9;
(Partial_Sums (||.z.|| rExpSeq )) . k <= Sum (||.z.|| rExpSeq ) by A13;
hence ||.((Partial_Sums (z rExpSeq )) . k).|| <= Sum (||.z.|| rExpSeq ) by A14, XXREAL_0:2; :: thesis: verum