theorem Th3: :: CAT_3:3

for x1, x2 being set
for A being non empty set st x1 <> x2 holds
for y1, y2 being Element of A holds
( ((x1,x2) --> (y1,y2)) /. x1 = y1 & ((x1,x2) --> (y1,y2)) /. x2 = y2 )