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₁[ Nat] means (Partial_Sums (Re F)) . $1 = (Re (Partial_Sums F)) . $1;
defpred S₂[ Nat] means (Partial_Sums (Im F)) . $1 = (Im (Partial_Sums F)) . $1;
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[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₁[k + 1] by MESFUN7C:24; :: thesis: verum

end;

A2: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume S₂[k] ; :: thesis: S₂[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₂[k + 1] by MESFUN7C:24; :: thesis: verum

end;

(Partial_Sums (Im F)) . 0 = (Im F) . 0 by Def2
.= Im (F . 0) by MESFUN7C:24
.= Im ((Partial_Sums F) . 0) by Def3 ;
then A3: S₂[ 0 ] by MESFUN7C:24;
A4: for i being Nat holds S₂[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₁[ 0 ] by MESFUN7C:24;
for i being Nat holds S₁[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