theorem :: GRFUNC_1:5

for x, y being object holds {[x,y]} is Function ;