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:41;
( dom ({x1} --> y1) = {x1} & dom ({x2} --> y2) = {x2} ) by FUNCOP_1:19;
then (dom ({x1} --> y1)) \/ (dom ({x2} --> y2)) = {x1,x2} by ENUMSET1:41;
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