let f be XFinSequence of COMPLEX ; :: thesis: for g being FinSequence of COMPLEX holds
( Sum (f ^ g) = (Sum f) + (Sum g) & Sum (g ^ f) = (Sum g) + (Sum f) )
let g be FinSequence of COMPLEX ; :: thesis: ( Sum (f ^ g) = (Sum f) + (Sum g) & Sum (g ^ f) = (Sum g) + (Sum f) )
A1: Sum (f ^ g) = Sum (f ^ (XFS2FS (FS2XFS g)))
.= Sum (f ^ (FS2XFS g)) by XFX
.= (Sum f) + (Sum (FS2XFS g)) by AFINSQ_2:55
.= (Sum f) + (Sum g) by FSS ;
Sum (g ^ f) = Sum (g ^ (FS2XFS (XFS2FS f)))
.= Sum (g ^ (XFS2FS f)) by FXF
.= (Sum g) + (Sum (XFS2FS f)) by RVSUM_2:32
.= (Sum g) + (Sum f) by XSS ;
hence ( Sum (f ^ g) = (Sum f) + (Sum g) & Sum (g ^ f) = (Sum g) + (Sum f) ) by A1; :: thesis: verum