let seq be Complex_Sequence; :: thesis: for n being Nat st ( for i being Nat holds

( (Re seq) . i >= 0 & (Im seq) . i = 0 ) ) holds

|.(Partial_Sums seq).| . n = (Partial_Sums |.seq.|) . n

let n be Nat; :: thesis: ( ( for i being Nat holds

( (Re seq) . i >= 0 & (Im seq) . i = 0 ) ) implies |.(Partial_Sums seq).| . n = (Partial_Sums |.seq.|) . n )

defpred S_{1}[ Nat] means |.(Partial_Sums seq).| . $1 = (Partial_Sums |.seq.|) . $1;

assume A1: for i being Nat holds

( (Re seq) . i >= 0 & (Im seq) . i = 0 ) ; :: thesis: |.(Partial_Sums seq).| . n = (Partial_Sums |.seq.|) . n

.= |.(seq . 0).| by SERIES_1:def 1

.= |.seq.| . 0 by VALUED_1:18 ;

then A14: S_{1}[ 0 ]
by SERIES_1:def 1;

for m being Nat holds S_{1}[m]
from NAT_1:sch 2(A14, A2);

hence |.(Partial_Sums seq).| . n = (Partial_Sums |.seq.|) . n ; :: thesis: verum

( (Re seq) . i >= 0 & (Im seq) . i = 0 ) ) holds

|.(Partial_Sums seq).| . n = (Partial_Sums |.seq.|) . n

let n be Nat; :: thesis: ( ( for i being Nat holds

( (Re seq) . i >= 0 & (Im seq) . i = 0 ) ) implies |.(Partial_Sums seq).| . n = (Partial_Sums |.seq.|) . n )

defpred S

assume A1: for i being Nat holds

( (Re seq) . i >= 0 & (Im seq) . i = 0 ) ; :: thesis: |.(Partial_Sums seq).| . n = (Partial_Sums |.seq.|) . n

A2: now :: thesis: for m being Nat st S_{1}[m] holds

S_{1}[m + 1]

|.(Partial_Sums seq).| . 0 =
|.((Partial_Sums seq) . 0).|
by VALUED_1:18
S

let m be Nat; :: thesis: ( S_{1}[m] implies S_{1}[m + 1] )

assume A3: S_{1}[m]
; :: thesis: S_{1}[m + 1]

thus S_{1}[m + 1]
:: thesis: verum

end;assume A3: S

thus S

proof

for i being Nat holds (Partial_Sums (Re seq)) . i >= 0

then (Re (Partial_Sums seq)) . m >= 0 by COMSEQ_3:26;

then A7: Re ((Partial_Sums seq) . m) >= 0 by COMSEQ_3:def 5;

set z2 = seq . (m + 1);

set z1 = (Partial_Sums seq) . m;

A8: |.(Partial_Sums seq).| . (m + 1) = |.((Partial_Sums seq) . (m + 1)).| by VALUED_1:18

.= |.(((Partial_Sums seq) . m) + (seq . (m + 1))).| by SERIES_1:def 1 ;

for i being Nat holds (Partial_Sums (Im seq)) . i = 0

then (Im (Partial_Sums seq)) . m = 0 by COMSEQ_3:26;

then A12: Im ((Partial_Sums seq) . m) = 0 by COMSEQ_3:def 6;

(Im seq) . (m + 1) = 0 by A1;

then Im (seq . (m + 1)) = 0 by COMSEQ_3:def 6;

then A13: (Re ((Partial_Sums seq) . m)) * (Im (seq . (m + 1))) = (Re (seq . (m + 1))) * (Im ((Partial_Sums seq) . m)) by A12;

(Re seq) . (m + 1) >= 0 by A1;

then Re (seq . (m + 1)) >= 0 by COMSEQ_3:def 5;

then ((Re ((Partial_Sums seq) . m)) * (Re (seq . (m + 1)))) + ((Im ((Partial_Sums seq) . m)) * (Im (seq . (m + 1)))) >= 0 by A7, A12;

then |.(Partial_Sums seq).| . (m + 1) = |.((Partial_Sums seq) . m).| + |.(seq . (m + 1)).| by A8, A13, Lm3

.= (|.(Partial_Sums seq).| . m) + |.(seq . (m + 1)).| by VALUED_1:18

.= ((Partial_Sums |.seq.|) . m) + (|.seq.| . (m + 1)) by A3, VALUED_1:18 ;

hence S_{1}[m + 1]
by SERIES_1:def 1; :: thesis: verum

end;proof

then
(Partial_Sums (Re seq)) . m >= 0
;
defpred S_{2}[ Nat] means (Partial_Sums (Re seq)) . $1 >= 0 ;

let i be Nat; :: thesis: (Partial_Sums (Re seq)) . i >= 0

then A6: S_{2}[ 0 ]
by A1;

for i being Nat holds S_{2}[i]
from NAT_1:sch 2(A6, A4);

hence (Partial_Sums (Re seq)) . i >= 0 ; :: thesis: verum

end;let i be Nat; :: thesis: (Partial_Sums (Re seq)) . i >= 0

A4: now :: thesis: for k being Nat st S_{2}[k] holds

S_{2}[k + 1]

(Partial_Sums (Re seq)) . 0 = (Re seq) . 0
by SERIES_1:def 1;S

let k be Nat; :: thesis: ( S_{2}[k] implies S_{2}[k + 1] )

assume A5: S_{2}[k]
; :: thesis: S_{2}[k + 1]

( (Partial_Sums (Re seq)) . (k + 1) = ((Partial_Sums (Re seq)) . k) + ((Re seq) . (k + 1)) & (Re seq) . (k + 1) >= 0 ) by A1, SERIES_1:def 1;

then (Partial_Sums (Re seq)) . (k + 1) >= 0 + 0 by A5;

hence S_{2}[k + 1]
; :: thesis: verum

end;assume A5: S

( (Partial_Sums (Re seq)) . (k + 1) = ((Partial_Sums (Re seq)) . k) + ((Re seq) . (k + 1)) & (Re seq) . (k + 1) >= 0 ) by A1, SERIES_1:def 1;

then (Partial_Sums (Re seq)) . (k + 1) >= 0 + 0 by A5;

hence S

then A6: S

for i being Nat holds S

hence (Partial_Sums (Re seq)) . i >= 0 ; :: thesis: verum

then (Re (Partial_Sums seq)) . m >= 0 by COMSEQ_3:26;

then A7: Re ((Partial_Sums seq) . m) >= 0 by COMSEQ_3:def 5;

set z2 = seq . (m + 1);

set z1 = (Partial_Sums seq) . m;

A8: |.(Partial_Sums seq).| . (m + 1) = |.((Partial_Sums seq) . (m + 1)).| by VALUED_1:18

.= |.(((Partial_Sums seq) . m) + (seq . (m + 1))).| by SERIES_1:def 1 ;

for i being Nat holds (Partial_Sums (Im seq)) . i = 0

proof

then
(Partial_Sums (Im seq)) . m = 0
;
defpred S_{2}[ Nat] means (Partial_Sums (Im seq)) . $1 = 0 ;

let i be Nat; :: thesis: (Partial_Sums (Im seq)) . i = 0

then A11: S_{2}[ 0 ]
by A1;

for i being Nat holds S_{2}[i]
from NAT_1:sch 2(A11, A9);

hence (Partial_Sums (Im seq)) . i = 0 ; :: thesis: verum

end;let i be Nat; :: thesis: (Partial_Sums (Im seq)) . i = 0

A9: now :: thesis: for k being Nat st S_{2}[k] holds

S_{2}[k + 1]

(Partial_Sums (Im seq)) . 0 = (Im seq) . 0
by SERIES_1:def 1;S

let k be Nat; :: thesis: ( S_{2}[k] implies S_{2}[k + 1] )

A10: (Partial_Sums (Im seq)) . (k + 1) = ((Partial_Sums (Im seq)) . k) + ((Im seq) . (k + 1)) by SERIES_1:def 1;

assume S_{2}[k]
; :: thesis: S_{2}[k + 1]

hence S_{2}[k + 1]
by A1, A10; :: thesis: verum

end;A10: (Partial_Sums (Im seq)) . (k + 1) = ((Partial_Sums (Im seq)) . k) + ((Im seq) . (k + 1)) by SERIES_1:def 1;

assume S

hence S

then A11: S

for i being Nat holds S

hence (Partial_Sums (Im seq)) . i = 0 ; :: thesis: verum

then (Im (Partial_Sums seq)) . m = 0 by COMSEQ_3:26;

then A12: Im ((Partial_Sums seq) . m) = 0 by COMSEQ_3:def 6;

(Im seq) . (m + 1) = 0 by A1;

then Im (seq . (m + 1)) = 0 by COMSEQ_3:def 6;

then A13: (Re ((Partial_Sums seq) . m)) * (Im (seq . (m + 1))) = (Re (seq . (m + 1))) * (Im ((Partial_Sums seq) . m)) by A12;

(Re seq) . (m + 1) >= 0 by A1;

then Re (seq . (m + 1)) >= 0 by COMSEQ_3:def 5;

then ((Re ((Partial_Sums seq) . m)) * (Re (seq . (m + 1)))) + ((Im ((Partial_Sums seq) . m)) * (Im (seq . (m + 1)))) >= 0 by A7, A12;

then |.(Partial_Sums seq).| . (m + 1) = |.((Partial_Sums seq) . m).| + |.(seq . (m + 1)).| by A8, A13, Lm3

.= (|.(Partial_Sums seq).| . m) + |.(seq . (m + 1)).| by VALUED_1:18

.= ((Partial_Sums |.seq.|) . m) + (|.seq.| . (m + 1)) by A3, VALUED_1:18 ;

hence S

.= |.(seq . 0).| by SERIES_1:def 1

.= |.seq.| . 0 by VALUED_1:18 ;

then A14: S

for m being Nat holds S

hence |.(Partial_Sums seq).| . n = (Partial_Sums |.seq.|) . n ; :: thesis: verum