let x1, x2, y1, y2 be set ; :: thesis: ( 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) = {x1} & dom ({x2} --> y2) = {x2} ) by FUNCOP_1:13;
then (dom ({x1} --> y1)) \/ (dom ({x2} --> y2)) = {x1,x2} by ENUMSET1:1;
hence dom ((x1,x2) --> (y1,y2)) = {x1,x2} by Def1; :: thesis: rng ((x1,x2) --> (y1,y2)) c= {y1,y2}
rng ((x1,x2) --> (y1,y2)) c= (rng ({x1} --> y1)) \/ (rng ({x2} --> y2)) by Th18;
hence rng ((x1,x2) --> (y1,y2)) c= {y1,y2} by A1, XBOOLE_1:1; :: thesis: verum