let seq be Complex_Sequence; :: thesis: ( Partial_Sums (Re seq) = Re (Partial_Sums seq) & Partial_Sums (Im seq) = Im (Partial_Sums seq) )
defpred S1[ Nat] means (Partial_Sums (Re seq)) . $1 = (Re (Partial_Sums seq)) . $1;
defpred S2[ Nat] means (Partial_Sums (Im seq)) . $1 = (Im (Partial_Sums seq)) . $1;
A1: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume S1[k] ; :: thesis: S1[k + 1]
then (Partial_Sums (Re seq)) . (k + 1) = ((Re (Partial_Sums seq)) . k) + ((Re seq) . (k + 1)) by SERIES_1:def 1
.= ((Re (Partial_Sums seq)) . k) + (Re (seq . (k + 1))) by Def5
.= (Re ((Partial_Sums seq) . k)) + (Re (seq . (k + 1))) by Def5
.= Re (((Partial_Sums seq) . k) + (seq . (k + 1))) by COMPLEX1:8
.= Re ((Partial_Sums seq) . (k + 1)) by SERIES_1:def 1
.= (Re (Partial_Sums seq)) . (k + 1) by Def5 ;
hence S1[k + 1] ; :: thesis: verum
end;
A2: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume S2[k] ; :: thesis: S2[k + 1]
then (Partial_Sums (Im seq)) . (k + 1) = ((Im (Partial_Sums seq)) . k) + ((Im seq) . (k + 1)) by SERIES_1:def 1
.= ((Im (Partial_Sums seq)) . k) + (Im (seq . (k + 1))) by Def6
.= (Im ((Partial_Sums seq) . k)) + (Im (seq . (k + 1))) by Def6
.= Im (((Partial_Sums seq) . k) + (seq . (k + 1))) by COMPLEX1:8
.= Im ((Partial_Sums seq) . (k + 1)) by SERIES_1:def 1
.= (Im (Partial_Sums seq)) . (k + 1) by Def6 ;
hence S2[k + 1] ; :: thesis: verum
end;
(Partial_Sums (Im seq)) . 0 = (Im seq) . 0 by SERIES_1:def 1
.= Im (seq . 0) by Def6
.= Im ((Partial_Sums seq) . 0) by SERIES_1:def 1
.= (Im (Partial_Sums seq)) . 0 by Def6 ;
then A3: S2[ 0 ] ;
A4: for n being Nat holds S2[n] from NAT_1:sch 2(A3, A2);
 (Partial_Sums (Re seq)) . 0 = (Re seq) . 0 by SERIES_1:def 1
.= Re (seq . 0) by Def5
.= Re ((Partial_Sums seq) . 0) by SERIES_1:def 1
.= (Re (Partial_Sums seq)) . 0 by Def5 ;
then A5: S1[ 0 ] ;
for n being Nat holds S1[n] from NAT_1:sch 2(A5, A1);
 hence ( Partial_Sums (Re seq) = Re (Partial_Sums seq) & Partial_Sums (Im seq) = Im (Partial_Sums seq) ) by A4; :: thesis: verum