let f be XFinSequence of REAL ; :: thesis: Sum (XFS2FS f) = Sum f

per cases ( not f is empty or f is empty ) ;

suppose not f is empty ; :: thesis: Sum (XFS2FS f) = Sum f

then reconsider k = len f as non zero Nat ;
reconsider n = k - 1 as Nat ;
reconsider g = Sequel f as Real_Sequence by RSC;
Sum (XFS2FS f) = Sum (Shift ((g | (Segm (n + 1))),1))
.= (Partial_Sums g) . n by DBLSEQ_2:49
.= Sum (g | (n + 1)) by AFINSQ_2:56 ;
hence Sum (XFS2FS f) = Sum f ; :: thesis: verum

end;

suppose f is empty ; :: thesis: Sum (XFS2FS f) = Sum f

then ( Sum f = 0 & Sum (XFS2FS f) = 0 ) ;
hence Sum (XFS2FS f) = Sum f ; :: thesis: verum

end;

end;