theorem :: GRFUNC_1:6

for x, y being object
for f being Function st f = {[x,y]} holds
f . x = y