theorem :: RVSUM_4:67

for f being complex-valued XFinSequence holds Sum f = Sum (Sequel f)