let x1, x2, y1, y2 be object ; :: thesis: ( ( 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 :: thesis: ((x1,x2) --> (y1,y2)) . x2 = y2

assume x1 <> x2 ; :: thesis: ((x1,x2) --> (y1,y2)) . x1 = y1
then not x1 in dom ({x2} --> y2) by TARSKI:def 1;
then ((x1,x2) --> (y1,y2)) . x1 = ({x1} --> y1) . x1 by Th11;
hence ((x1,x2) --> (y1,y2)) . x1 = y1 by A2, FUNCOP_1:7; :: thesis: verum

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; :: thesis: verum