let seq be Complex_Sequence; :: thesis: for n being Element of NAT st ( for i being Element of NAT holds
( (Re seq) . i >= 0 & (Im seq) . i = 0 ) ) holds
|.(Partial_Sums seq).| . n = (Partial_Sums |.seq.|) . n
let n be Element of NAT ; :: thesis: ( ( for i being Element of NAT holds
( (Re seq) . i >= 0 & (Im seq) . i = 0 ) ) implies |.(Partial_Sums seq).| . n = (Partial_Sums |.seq.|) . n )
assume A1: for i being Element of NAT holds
( (Re seq) . i >= 0 & (Im seq) . i = 0 ) ; :: thesis: |.(Partial_Sums seq).| . n = (Partial_Sums |.seq.|) . n
defpred S₁[ Element of NAT ] means |.(Partial_Sums seq).| . $1 = (Partial_Sums |.seq.|) . $1;
A2: S₁[ 0 ]

proof

|.(Partial_Sums seq).| . 0 = |.((Partial_Sums seq) . 0 ).| by VALUED_1:18
.= |.(seq . 0 ).| by COMSEQ_3:def 7
.= |.seq.| . 0 by VALUED_1:18 ;
hence S₁[ 0 ] by SERIES_1:def 1; :: thesis: verum

end;

A3: now

let m be Element of NAT ; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A4: S₁[m] ; :: thesis: S₁[m + 1]
thus S₁[m + 1] :: thesis: verum

proof

A5: for i being Element of NAT holds (Partial_Sums (Re seq)) . i >= 0

proof

let i be Element of NAT ; :: thesis: (Partial_Sums (Re seq)) . i >= 0
defpred S₂[ Element of NAT ] means (Partial_Sums (Re seq)) . $1 >= 0 ;
A6: S₂[ 0 ]

proof

(Partial_Sums (Re seq)) . 0 = (Re seq) . 0 by SERIES_1:def 1;
hence S₂[ 0 ] by A1; :: thesis: verum

end;

A7: now

let k be Element of NAT ; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume A8: S₂[k] ; :: thesis: S₂[k + 1]
thus S₂[k + 1] :: thesis: verum

proof

A9: (Partial_Sums (Re seq)) . (k + 1) = ((Partial_Sums (Re seq)) . k) + ((Re seq) . (k + 1)) by SERIES_1:def 1;
( (Partial_Sums (Re seq)) . k >= 0 & (Re seq) . (k + 1) >= 0 ) by A1, A8;
then (Partial_Sums (Re seq)) . (k + 1) >= 0 + 0 by A9, XREAL_1:9;
hence S₂[k + 1] ; :: thesis: verum

end;

end;

for i being Element of NAT holds S₂[i] from NAT_1:sch 1(A6, A7);
hence (Partial_Sums (Re seq)) . i >= 0 ; :: thesis: verum

end;

A10: for i being Element of NAT holds (Partial_Sums (Im seq)) . i = 0

proof

let i be Element of NAT ; :: thesis: (Partial_Sums (Im seq)) . i = 0
defpred S₂[ Element of NAT ] means (Partial_Sums (Im seq)) . $1 = 0 ;
A11: S₂[ 0 ]

proof

(Partial_Sums (Im seq)) . 0 = (Im seq) . 0 by SERIES_1:def 1;
hence S₂[ 0 ] by A1; :: thesis: verum

end;

A12: now

let k be Element of NAT ; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume A13: S₂[k] ; :: thesis: S₂[k + 1]
thus S₂[k + 1] :: thesis: verum

proof

(Partial_Sums (Im seq)) . (k + 1) = ((Partial_Sums (Im seq)) . k) + ((Im seq) . (k + 1)) by SERIES_1:def 1;
hence S₂[k + 1] by A1, A13; :: thesis: verum

end;

end;

for i being Element of NAT holds S₂[i] from NAT_1:sch 1(A11, A12);
hence (Partial_Sums (Im seq)) . i = 0 ; :: thesis: verum

end;

A14: |.(Partial_Sums seq).| . (m + 1) = |.((Partial_Sums seq) . (m + 1)).| by VALUED_1:18
.= |.(((Partial_Sums seq) . m) + (seq . (m + 1))).| by COMSEQ_3:def 7 ;
( (Partial_Sums (Re seq)) . m >= 0 & (Partial_Sums (Im seq)) . m = 0 ) by A5, A10;
then ( (Re (Partial_Sums seq)) . m >= 0 & (Im (Partial_Sums seq)) . m = 0 ) by COMSEQ_3:26;
then A15: ( Re ((Partial_Sums seq) . m) >= 0 & Im ((Partial_Sums seq) . m) = 0 ) by COMSEQ_3:def 3, COMSEQ_3:def 4;
( (Re seq) . (m + 1) >= 0 & (Im seq) . (m + 1) = 0 ) by A1;
then A16: ( Re (seq . (m + 1)) >= 0 & Im (seq . (m + 1)) = 0 ) by COMSEQ_3:def 3, COMSEQ_3:def 4;
set z1 = (Partial_Sums seq) . m;
set z2 = seq . (m + 1);
A17: (Re ((Partial_Sums seq) . m)) * (Im (seq . (m + 1))) = (Re (seq . (m + 1))) * (Im ((Partial_Sums seq) . m)) by A15, A16;
((Re ((Partial_Sums seq) . m)) * (Re (seq . (m + 1)))) + ((Im ((Partial_Sums seq) . m)) * (Im (seq . (m + 1)))) >= 0 by A15, A16, XREAL_1:129;
then |.(Partial_Sums seq).| . (m + 1) = |.((Partial_Sums seq) . m).| + |.(seq . (m + 1)).| by A14, A17, Lm4
.= (|.(Partial_Sums seq).| . m) + |.(seq . (m + 1)).| by VALUED_1:18
.= ((Partial_Sums |.seq.|) . m) + (|.seq.| . (m + 1)) by A4, VALUED_1:18 ;
hence S₁[m + 1] by SERIES_1:def 1; :: thesis: verum

end;

end;

for m being Element of NAT holds S₁[m] from NAT_1:sch 1(A2, A3);
hence |.(Partial_Sums seq).| . n = (Partial_Sums |.seq.|) . n ; :: thesis: verum