theorem SumA: :: RVSUM_3:24

for f being real-valued FinSequence
for i being Nat
for a being Real st i in dom f holds
Sum (f +* (i,a)) = ((Sum f) - (f . i)) + a