let x1, x2, y1, y2 be set ; :: 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: ( x1 in {x1} & x2 in {x2} ) by TARSKI:def 1;
A2: ( {x1} = dom ({x1} --> y1) & {x2} = dom ({x2} --> y2) ) by FUNCOP_1:19;

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 Th12;
hence (x1,x2 --> y1,y2) . x1 = y1 by A1, FUNCOP_1:13; :: thesis: verum

end;

(x1,x2 --> y1,y2) . x2 = ({x2} --> y2) . x2 by A1, A2, Th14;
hence (x1,x2 --> y1,y2) . x2 = y2 by A1, FUNCOP_1:13; :: thesis: verum