theorem :: GRFUNC_1:8

for x1, x2, y1, y2 being object holds
( {[x1,y1],[x2,y2]} is Function iff ( x1 = x2 implies y1 = y2 ) )