let x1, x2, y1, y2 be object ; ( dom ((x1,x2) --> (y1,y2)) = {x1,x2} & rng ((x1,x2) --> (y1,y2)) c= {y1,y2} )
set f = {x1} --> y1;
set g = {x2} --> y2;
set h = (x1,x2) --> (y1,y2);
(rng ({x1} --> y1)) \/ (rng ({x2} --> y2)) c= {y1} \/ {y2}
by XBOOLE_1:13;
then A1:
(rng ({x1} --> y1)) \/ (rng ({x2} --> y2)) c= {y1,y2}
by ENUMSET1:1;
(dom ({x1} --> y1)) \/ (dom ({x2} --> y2)) = {x1,x2}
by ENUMSET1:1;
hence
dom ((x1,x2) --> (y1,y2)) = {x1,x2}
by Def1; rng ((x1,x2) --> (y1,y2)) c= {y1,y2}
rng ((x1,x2) --> (y1,y2)) c= (rng ({x1} --> y1)) \/ (rng ({x2} --> y2))
by Th17;
hence
rng ((x1,x2) --> (y1,y2)) c= {y1,y2}
by A1; verum