theorem ReplaceValue2: :: RVSUM_3:30

for f being FinSequence
for i, j being Nat
for a, b being object st i in dom f & j in dom f & i <> j holds
(Replace (f,i,j,a,b)) . j = b