let x1, x2, y1, y2 be object ; ( ( x1 <> x2 implies ((x1,x2) --> (y1,y2)) . x1 = y1 ) & ((x1,x2) --> (y1,y2)) . x2 = y2 )
set f = {x1} --> y1;
set g = {x2} --> y2;
set h = (x1,x2) --> (y1,y2);
A1:
x2 in {x2}
by TARSKI:def 1;
A2:
x1 in {x1}
by TARSKI:def 1;
hereby ((x1,x2) --> (y1,y2)) . x2 = y2
end;
{x2} = dom ({x2} --> y2)
;
then
((x1,x2) --> (y1,y2)) . x2 = ({x2} --> y2) . x2
by A1, Th13;
hence
((x1,x2) --> (y1,y2)) . x2 = y2
by A1, FUNCOP_1:7; verum