theorem Th62: :: FUNCT_4:62

for x1, x2, y1, y2 being object holds
( dom ((x1,x2) --> (y1,y2)) = {x1,x2} & rng ((x1,x2) --> (y1,y2)) c= {y1,y2} )