theorem Th17: :: GRAPHSP:17

for i, k being Nat
for f being Element of REAL *
for r being Real st i <> k & i in dom f holds
((f,i) := (k,r)) . i = k