theorem Th63: :: FUNCT_4:63

for x1, x2, y1, y2 being object holds
( ( x1 <> x2 implies ((x1,x2) --> (y1,y2)) . x1 = y1 ) & ((x1,x2) --> (y1,y2)) . x2 = y2 )