theorem Th38: :: WAYBEL26:38

for x, y being object
for f being Function holds
( [x,y] in *graph f iff ( x in dom f & y in f . x ) )