theorem Th1: :: FUNCT_1:1

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