let X be non empty set ; :: thesis: for F being Functional_Sequence of X,COMPLEX holds

( Partial_Sums (Re F) = Re (Partial_Sums F) & Partial_Sums (Im F) = Im (Partial_Sums F) )

let F be Functional_Sequence of X,COMPLEX; :: thesis: ( Partial_Sums (Re F) = Re (Partial_Sums F) & Partial_Sums (Im F) = Im (Partial_Sums F) )

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

defpred S_{2}[ Nat] means (Partial_Sums (Im F)) . $1 = (Im (Partial_Sums F)) . $1;

A1: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{2}[k] holds

S_{2}[k + 1]

.= Im (F . 0) by MESFUN7C:24

.= Im ((Partial_Sums F) . 0) by Def3 ;

then A3: S_{2}[ 0 ]
by MESFUN7C:24;

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

(Partial_Sums (Re F)) . 0 = (Re F) . 0 by Def2

.= Re (F . 0) by MESFUN7C:24

.= Re ((Partial_Sums F) . 0) by Def3 ;

then A5: S_{1}[ 0 ]
by MESFUN7C:24;

for i being Nat holds S_{1}[i]
from NAT_1:sch 2(A5, A1);

hence ( Partial_Sums (Re F) = Re (Partial_Sums F) & Partial_Sums (Im F) = Im (Partial_Sums F) ) by A4; :: thesis: verum

( Partial_Sums (Re F) = Re (Partial_Sums F) & Partial_Sums (Im F) = Im (Partial_Sums F) )

let F be Functional_Sequence of X,COMPLEX; :: thesis: ( Partial_Sums (Re F) = Re (Partial_Sums F) & Partial_Sums (Im F) = Im (Partial_Sums F) )

defpred S

defpred S

A1: for k being Nat st S

S

proof

A2:
for k being Nat st S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

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

then (Partial_Sums (Re F)) . (k + 1) = ((Re (Partial_Sums F)) . k) + ((Re F) . (k + 1)) by Def2

.= ((Re (Partial_Sums F)) . k) + (Re (F . (k + 1))) by MESFUN7C:24

.= (Re ((Partial_Sums F) . k)) + (Re (F . (k + 1))) by MESFUN7C:24

.= Re (((Partial_Sums F) . k) + (F . (k + 1))) by MESFUN6C:5

.= Re ((Partial_Sums F) . (k + 1)) by Def3 ;

hence S_{1}[k + 1]
by MESFUN7C:24; :: thesis: verum

end;assume S

then (Partial_Sums (Re F)) . (k + 1) = ((Re (Partial_Sums F)) . k) + ((Re F) . (k + 1)) by Def2

.= ((Re (Partial_Sums F)) . k) + (Re (F . (k + 1))) by MESFUN7C:24

.= (Re ((Partial_Sums F) . k)) + (Re (F . (k + 1))) by MESFUN7C:24

.= Re (((Partial_Sums F) . k) + (F . (k + 1))) by MESFUN6C:5

.= Re ((Partial_Sums F) . (k + 1)) by Def3 ;

hence S

S

proof

(Partial_Sums (Im F)) . 0 =
(Im F) . 0
by Def2
let k be Nat; :: thesis: ( S_{2}[k] implies S_{2}[k + 1] )

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

then (Partial_Sums (Im F)) . (k + 1) = ((Im (Partial_Sums F)) . k) + ((Im F) . (k + 1)) by Def2

.= ((Im (Partial_Sums F)) . k) + (Im (F . (k + 1))) by MESFUN7C:24

.= (Im ((Partial_Sums F) . k)) + (Im (F . (k + 1))) by MESFUN7C:24

.= Im (((Partial_Sums F) . k) + (F . (k + 1))) by MESFUN6C:5

.= Im ((Partial_Sums F) . (k + 1)) by Def3 ;

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

end;assume S

then (Partial_Sums (Im F)) . (k + 1) = ((Im (Partial_Sums F)) . k) + ((Im F) . (k + 1)) by Def2

.= ((Im (Partial_Sums F)) . k) + (Im (F . (k + 1))) by MESFUN7C:24

.= (Im ((Partial_Sums F) . k)) + (Im (F . (k + 1))) by MESFUN7C:24

.= Im (((Partial_Sums F) . k) + (F . (k + 1))) by MESFUN6C:5

.= Im ((Partial_Sums F) . (k + 1)) by Def3 ;

hence S

.= Im (F . 0) by MESFUN7C:24

.= Im ((Partial_Sums F) . 0) by Def3 ;

then A3: S

A4: for i being Nat holds S

(Partial_Sums (Re F)) . 0 = (Re F) . 0 by Def2

.= Re (F . 0) by MESFUN7C:24

.= Re ((Partial_Sums F) . 0) by Def3 ;

then A5: S

for i being Nat holds S

hence ( Partial_Sums (Re F) = Re (Partial_Sums F) & Partial_Sums (Im F) = Im (Partial_Sums F) ) by A4; :: thesis: verum