theorem Th19: :: GRAPHSP:19

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