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 Th17;
then A1: rng ((x1,x2) --> (y1,y2)) c= A by XBOOLE_1:1;
dom ((x1,x2) --> (y1,y2)) = {x1,x2} by Th62;
hence (x1,x2) --> (y1,y2) is Function of {x1,x2},A by A1, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum