set f = {x1} --> y1;
set g = {x2} --> y2;
set h = x1,x2 --> y1,y2;
rng (x1,x2 --> y1,y2) c= (rng ({x1} --> y1)) \/ (rng ({x2} --> y2)) by Th18;
then A1: rng (x1,x2 --> y1,y2) c= A by XBOOLE_1:1;
dom (x1,x2 --> y1,y2) = {x1,x2} by Th65;
hence x1,x2 --> y1,y2 is Function of {x1,x2},A by A1, FUNCT_2:def 1, RELSET_1:11; :: thesis: verum