theorem Th20: :: GRAPHSP:20

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