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:66, TARSKI:def 2;
A3: x2 in {x1,x2} by TARSKI:def 2;
(x1,x2 --> y1,y2) . x1 = y1 by A1, FUNCT_4:66;
hence ( (x1,x2 --> y1,y2) /. x1 = y1 & (x1,x2 --> y1,y2) /. x2 = y2 ) by A2, A3, FUNCT_2:def 14; :: thesis: verum