let f be real-valued XFinSequence; :: thesis: Sum f = Sum (Sequel f)
reconsider g = Re (Sequel f) as summable Real_Sequence ;
reconsider n = len f as Nat ;
A2: Sum (Sequel f) = (Sum g) + ((Sum (Im (Sequel f))) * <i>) by COMSEQ_3:53
.= (Sum g) + (0 * <i>)
.= Sum g ;

per cases ( n = 0 or n > 0 ) ;

suppose n = 0 ; :: thesis: Sum f = Sum (Sequel f)

then f is empty ;
then ( Sum f = 0 & Sum (Sequel f) = 0 ) ;
hence Sum f = Sum (Sequel f) ; :: thesis: verum

end;

suppose n > 0 ; :: thesis: Sum f = Sum (Sequel f)

then reconsider k = n - 1 as Nat ;
Sum g = ((Partial_Sums g) . k) + (Sum (g ^\ (k + 1))) by SERIES_1:15
.= ((Partial_Sums g) . k) + 0
.= Sum (g | (k + 1)) by AFINSQ_2:56
.= Sum f ;
hence Sum f = Sum (Sequel f) by A2; :: thesis: verum

end;

end;