let z be Element of COMPLEX ; :: thesis: for k being Element of 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 Element of 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₁[ Element of NAT ] means |.((Partial_Sums (z ExpSeq )) . $1).| <= (Partial_Sums (|.z.| rExpSeq )) . $1;
A1: |.((Partial_Sums (z ExpSeq )) . 0 ).| = |.((z ExpSeq ) . 0 ).| by COMSEQ_3:def 7
.= |.((z |^ 0 ) / (0 !c )).| by Def8
.= 1 by Th1, COMPLEX1:134, COMSEQ_3:def 1 ;
A2: (Partial_Sums (|.z.| rExpSeq )) . 0 = (|.z.| rExpSeq ) . 0 by SERIES_1:def 1
.= (|.z.| |^ 0 ) / (0 ! ) by Def9
.= 1 by NEWTON:9, NEWTON:18 ;
A3: S₁[ 0 ] by A1, A2;
A4: 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 A5: |.((Partial_Sums (z ExpSeq )) . k).| <= (Partial_Sums (|.z.| rExpSeq )) . k ; :: thesis: S₁[k + 1]
A6: ( |.((Partial_Sums (z ExpSeq )) . (k + 1)).| = |.(((Partial_Sums (z ExpSeq )) . k) + ((z ExpSeq ) . (k + 1))).| & |.(((Partial_Sums (z ExpSeq )) . k) + ((z ExpSeq ) . (k + 1))).| <= |.((Partial_Sums (z ExpSeq )) . k).| + |.((z ExpSeq ) . (k + 1)).| ) by COMPLEX1:142, COMSEQ_3:def 7;
A7: |.((Partial_Sums (z ExpSeq )) . (k + 1)).| <= |.((Partial_Sums (z ExpSeq )) . k).| + ((|.z.| rExpSeq ) . (k + 1)) by A6, Th4;
A8: |.((Partial_Sums (z ExpSeq )) . k).| + ((|.z.| rExpSeq ) . (k + 1)) <= ((Partial_Sums (|.z.| rExpSeq )) . k) + ((|.z.| rExpSeq ) . (k + 1)) by A5, XREAL_1:8;
A9: ((Partial_Sums (|.z.| rExpSeq )) . k) + ((|.z.| rExpSeq ) . (k + 1)) = (Partial_Sums (|.z.| rExpSeq )) . (k + 1) by SERIES_1:def 1;
thus S₁[k + 1] by A7, A8, A9, XXREAL_0:2; :: thesis: verum

end;

A10: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A3, A4);
thus |.((Partial_Sums (z ExpSeq )) . k).| <= (Partial_Sums (|.z.| rExpSeq )) . k by A10; :: thesis: ( (Partial_Sums (|.z.| rExpSeq )) . k <= Sum (|.z.| rExpSeq ) & |.((Partial_Sums (z ExpSeq )) . k).| <= Sum (|.z.| rExpSeq ) )

A11: now

let k be set ; :: thesis: ( k in NAT implies |.(z ExpSeq ).| . k = (|.z.| rExpSeq ) . k )
assume A12: k in NAT ; :: thesis: |.(z ExpSeq ).| . k = (|.z.| rExpSeq ) . k
thus |.(z ExpSeq ).| . k = |.((z ExpSeq ) . k).| by VALUED_1:18
.= (|.z.| rExpSeq ) . k by A12, Th4 ; :: thesis: verum

end;

A13: |.(z ExpSeq ).| = |.z.| rExpSeq by A11, FUNCT_2:18;
A14: (Partial_Sums (|.z.| rExpSeq )) . k <= lim (Partial_Sums (|.z.| rExpSeq )) by A13, SEQ_4:54;
thus (Partial_Sums (|.z.| rExpSeq )) . k <= Sum (|.z.| rExpSeq ) by A14, SERIES_1:def 3; :: thesis: |.((Partial_Sums (z ExpSeq )) . k).| <= Sum (|.z.| rExpSeq )

A15: now

let k be Element of NAT ; :: thesis: (Partial_Sums (|.z.| rExpSeq )) . k <= Sum (|.z.| rExpSeq )
A16: lim (Partial_Sums (|.z.| rExpSeq )) = Sum (|.z.| rExpSeq ) by SERIES_1:def 3;
thus (Partial_Sums (|.z.| rExpSeq )) . k <= Sum (|.z.| rExpSeq ) by A13, A16, SEQ_4:54; :: thesis: verum

end;

A17: |.((Partial_Sums (z ExpSeq )) . k).| <= (Partial_Sums (|.z.| rExpSeq )) . k by A10;
A18: (Partial_Sums (|.z.| rExpSeq )) . k <= Sum (|.z.| rExpSeq ) by A15;
thus |.((Partial_Sums (z ExpSeq )) . k).| <= Sum (|.z.| rExpSeq ) by A17, A18, XXREAL_0:2; :: thesis: verum