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₁[ Element of NAT ] means (Partial_Sums (Re F)) . $1 = (Re (Partial_Sums F)) . $1;
(Partial_Sums (Re F)) . 0 = (Re F) . 0 by Def0
.= Re (F . 0 ) by MESFUN7C:24
.= Re ((Partial_Sums F) . 0 ) by Def0c ;
then A1: S₁[ 0 ] by MESFUN7C:24;
A2: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of 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 Def0
.= ((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 Def0c ;
hence S₁[k + 1] by MESFUN7C:24; :: thesis: verum

end;

A3: for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A1, A2);
defpred S₂[ Element of NAT ] means (Partial_Sums (Im F)) . $1 = (Im (Partial_Sums F)) . $1;
(Partial_Sums (Im F)) . 0 = (Im F) . 0 by Def0
.= Im (F . 0 ) by MESFUN7C:24
.= Im ((Partial_Sums F) . 0 ) by Def0c ;
then A4: S₂[ 0 ] by MESFUN7C:24;
A5: for k being Element of NAT st S₂[k] holds
S₂[k + 1]

proof

let k be Element of 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 Def0
.= ((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 Def0c ;
hence S₂[k + 1] by MESFUN7C:24; :: thesis: verum

end;

for i being Element of NAT holds S₂[i] from NAT_1:sch 1(A4, A5);
hence ( Partial_Sums (Re F) = Re (Partial_Sums F) & Partial_Sums (Im F) = Im (Partial_Sums F) ) by A3, FUNCT_2:113; :: thesis: verum