let z be Complex; :: 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 ExpSeq)) . 0).| = |.((z ExpSeq) . 0).| by SERIES_1:def 1
.= |.((z |^ 0) / (0 !)).| by Def4
.= 1 by Th1, COMPLEX1:48, COMSEQ_3:def 1 ;
(Partial_Sums (|.z.| rExpSeq)) . 0 = (|.z.| rExpSeq) . 0 by SERIES_1:def 1
.= (|.z.| |^ 0) / (0 !) by Def5
.= 1 by NEWTON:4, NEWTON:12 ;
then A2: S₁[ 0 ] by A1;
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: |.((Partial_Sums (z ExpSeq)) . k).| <= (Partial_Sums (|.z.| rExpSeq)) . k ; :: thesis: S₁[k + 1]
( |.((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:56, SERIES_1:def 1;
then A5: |.((Partial_Sums (z ExpSeq)) . (k + 1)).| <= |.((Partial_Sums (z ExpSeq)) . k).| + ((|.z.| rExpSeq) . (k + 1)) by Th3;
A6: |.((Partial_Sums (z ExpSeq)) . k).| + ((|.z.| rExpSeq) . (k + 1)) <= ((Partial_Sums (|.z.| rExpSeq)) . k) + ((|.z.| rExpSeq) . (k + 1)) by A4, XREAL_1:6;
((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 A5, A6, XXREAL_0:2; :: thesis: verum

end;

A7: for k being Nat holds S₁[k] from NAT_1:sch 2(A2, A3);
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) )

now :: thesis: for k being object st k in NAT holds
|.(z ExpSeq).| . k = (|.z.| rExpSeq) . k

let k be object ; :: thesis: ( k in NAT implies |.(z ExpSeq).| . k = (|.z.| rExpSeq) . k )
assume A8: 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 A8, Th3 ; :: thesis: verum

end;

then A9: |.(z ExpSeq).| = |.z.| rExpSeq ;
then (Partial_Sums (|.z.| rExpSeq)) . k <= lim (Partial_Sums (|.z.| rExpSeq)) by SEQ_4:37;
hence (Partial_Sums (|.z.| rExpSeq)) . k <= Sum (|.z.| rExpSeq) by SERIES_1:def 3; :: thesis: |.((Partial_Sums (z ExpSeq)) . k).| <= Sum (|.z.| rExpSeq)

A10: 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, SEQ_4:37; :: thesis: verum

end;

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