set f = {x1} --> y1;
set g = {x2} --> y2;
set h = x1,x2 --> y1,y2;

now

thus dom (x1,x2 --> y1,y2) = {x1,x2} by Th65; :: thesis: rng (x1,x2 --> y1,y2) c= A
( (rng ({x1} --> y1)) \/ (rng ({x2} --> y2)) c= A & rng (x1,x2 --> y1,y2) c= (rng ({x1} --> y1)) \/ (rng ({x2} --> y2)) ) by Th18;
hence rng (x1,x2 --> y1,y2) c= A by XBOOLE_1:1; :: thesis: verum

end;

hence x1,x2 --> y1,y2 is Function of {x1,x2},A by FUNCT_2:def 1, RELSET_1:11; :: thesis: verum