theorem :: FUNCT_4:64

for x1, x2, y1, y2 being object st x1 <> x2 holds
rng ((x1,x2) --> (y1,y2)) = {y1,y2}