theorem ReplaceValue: :: RVSUM_3:29

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