theorem :: RVSUM_4:68

for f being XFinSequence of COMPLEX
for g being FinSequence of COMPLEX holds
( Sum (f ^ g) = (Sum f) + (Sum g) & Sum (g ^ f) = (Sum g) + (Sum f) )