let x1, x2 be set ; :: thesis: 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 )
let A be non empty set ; :: thesis: ( x1 <> x2 implies for y1, y2 being Element of A holds
( ((x1,x2) --> (y1,y2)) /. x1 = y1 & ((x1,x2) --> (y1,y2)) /. x2 = y2 ) )
assume A1: x1 <> x2 ; :: thesis: for y1, y2 being Element of A holds
( ((x1,x2) --> (y1,y2)) /. x1 = y1 & ((x1,x2) --> (y1,y2)) /. x2 = y2 )
let y1, y2 be Element of A; :: thesis: ( ((x1,x2) --> (y1,y2)) /. x1 = y1 & ((x1,x2) --> (y1,y2)) /. x2 = y2 )
set h = (x1,x2) --> (y1,y2);
A2: ( ((x1,x2) --> (y1,y2)) . x2 = y2 & x1 in {x1,x2} ) by FUNCT_4:63, TARSKI:def 2;
A3: x2 in {x1,x2} by TARSKI:def 2;
((x1,x2) --> (y1,y2)) . x1 = y1 by A1, FUNCT_4:63;
hence ( ((x1,x2) --> (y1,y2)) /. x1 = y1 & ((x1,x2) --> (y1,y2)) /. x2 = y2 ) by A2, A3, FUNCT_2:def 13; :: thesis: verum