let f be FinSequence of COMPLEX ; :: thesis: Sum (FS2XFS f) = Sum f
reconsider g = FS2XFS f as XFinSequence of COMPLEX ;
Sum g = Sum (XFS2FS g) by XSS
.= Sum f ;
hence Sum (FS2XFS f) = Sum f ; :: thesis: verum