theorem SumReplace: :: RVSUM_3:26

for f being real-valued FinSequence
for i, j being Nat
for a, b being Real st i in dom f & j in dom f & i <> j holds
Sum (Replace (f,i,j,a,b)) = ((((Sum f) - (f . i)) - (f . j)) + a) + b