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

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