theorem ReplaceValue3: :: RVSUM_3:31

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)) . i = a