for f being Function
for x, y being set holds
( [x,y] in graph f iff ( x is finite & x in dom f & y in f . x ) )