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 F' = {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 ( 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 & x in {x1} ) by Th12;
hence ( (x1,x2 --> y,y) . x = y & ({x1,x2} --> y) . x = y ) by A2, FUNCOP_1:13; :: thesis: verum

end;

suppose 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 & x in {x2} ) by Th14;
hence ( (x1,x2 --> y,y) . x = y & ({x1,x2} --> y) . x = y ) by A2, 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