let f be complex-valued XFinSequence; :: thesis: Sum (XFS2FS f) = Sum f
dom (Re (XFS2FS f)) = dom (XFS2FS f) by COMSEQ_3:def 3;
then len (Re (XFS2FS f)) = len (XFS2FS f) by FINSEQ_3:29
.= len f by AFINSQ_1:def 9 ;
then reconsider g = Re (XFS2FS f) as len f -element FinSequence of COMPLEX by CARD_1:def 7, NEWTON02:103;
dom (<i> (#) (Im (XFS2FS f))) = dom (Im (XFS2FS f)) by VALUED_1:def 5
.= dom (XFS2FS f) by COMSEQ_3:def 4 ;
then len (<i> (#) (Im (XFS2FS f))) = len (XFS2FS f) by FINSEQ_3:29
.= len f by AFINSQ_1:def 9 ;
then reconsider h = <i> (#) (Im (XFS2FS f)) as len f -element FinSequence of COMPLEX by CARD_1:def 7, NEWTON02:103;
Sum f = (Sum (Re f)) + (<i> * (Sum (Im f))) by RSI
.= (Sum (XFS2FS (Re f))) + (<i> * (Sum (Im f))) by XSF
.= (Sum (XFS2FS (Re f))) + (<i> * (Sum (XFS2FS (Im f)))) by XSF
.= (Sum (XFS2FS (Re f))) + (<i> * (Sum (Im (XFS2FS f)))) by RSH
.= (Sum (Re (XFS2FS f))) + (<i> * (Sum (Im (XFS2FS f)))) by RSH
.= (Sum (Re (XFS2FS f))) + (Sum h) by RVSUM_2:38
.= Sum (g + h) by RVSUM_2:40
.= Sum (XFS2FS f) ;
hence Sum (XFS2FS f) = Sum f ; :: thesis: verum