let x1, x2, y be set ; :: 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

thus A1: ( dom ((x1,x2) --> (y,y)) = {x1,x2} & dom ({x1,x2} --> y) = {x1,x2} ) by Th65, FUNCOP_1:19; :: thesis: for x being set st x in {x1,x2} holds
((x1,x2) --> (y,y)) . x = ({x1,x2} --> y) . x
let x be set ; :: 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

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

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 Th12;
hence ( ((x1,x2) --> (y,y)) . x = y & ({x1,x2} --> y) . x = y ) by A2, A3, FUNCOP_1:13; :: 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 Th14;
hence ( ((x1,x2) --> (y,y)) . x = y & ({x1,x2} --> y) . x = y ) by A2, A4, FUNCOP_1:13; :: 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 by FUNCT_1:9; :: thesis: verum