let x1, x2, y be object ; :: thesis: (x1,x2) --> (y,y) = {x1,x2} --> y
set F = (x1,x2) --> (y,y);
set f = {x1} --> y;
set g = {x2} --> y;
set F9 = {x1,x2} --> y;

now :: thesis: ( dom ((x1,x2) --> (y,y)) = {x1,x2} & dom ({x1,x2} --> y) = {x1,x2} & ( for x being object st x in {x1,x2} holds
((x1,x2) --> (y,y)) . x = ({x1,x2} --> y) . x ) )

thus A1: ( dom ((x1,x2) --> (y,y)) = {x1,x2} & dom ({x1,x2} --> y) = {x1,x2} ) by Th62; :: thesis: for x being object st x in {x1,x2} holds
((x1,x2) --> (y,y)) . x = ({x1,x2} --> y) . x
let x be object ; :: thesis: ( x in {x1,x2} implies ((x1,x2) --> (y,y)) . x = ({x1,x2} --> y) . x )
assume A2: x in {x1,x2} ; :: thesis: ((x1,x2) --> (y,y)) . x = ({x1,x2} --> y) . x

now :: thesis: ( ((x1,x2) --> (y,y)) . x = y & ({x1,x2} --> y) . x = y )

per cases ( ( x in dom ({x1} --> y) & not x in dom ({x2} --> y) ) or x in dom ({x2} --> y) ) by A1, A2, Th12;

suppose A3: ( x in dom ({x1} --> y) & not x in dom ({x2} --> y) ) ; :: thesis: ( ((x1,x2) --> (y,y)) . x = y & ({x1,x2} --> y) . x = y )

then ((x1,x2) --> (y,y)) . x = ({x1} --> y) . x by Th11;
hence ( ((x1,x2) --> (y,y)) . x = y & ({x1,x2} --> y) . x = y ) by A2, A3, FUNCOP_1:7; :: thesis: verum

end;

suppose A4: x in dom ({x2} --> y) ; :: thesis: ( ((x1,x2) --> (y,y)) . x = y & ({x1,x2} --> y) . x = y )

then ((x1,x2) --> (y,y)) . x = ({x2} --> y) . x by Th13;
hence ( ((x1,x2) --> (y,y)) . x = y & ({x1,x2} --> y) . x = y ) by A2, A4, FUNCOP_1:7; :: thesis: verum

end;

end;

end;

hence ((x1,x2) --> (y,y)) . x = ({x1,x2} --> y) . x ; :: thesis: verum

end;

hence (x1,x2) --> (y,y) = {x1,x2} --> y ; :: thesis: verum