set f = x,y --> a,b;
set g = w,z --> c,d;
set h = x,y,w,z --> a,b,c,d;
A1: rng (x,y,w,z --> a,b,c,d) c= (rng (x,y --> a,b)) \/ (rng (w,z --> c,d)) by FUNCT_4:18;
A2: dom (x,y,w,z --> a,b,c,d) = {x,y,w,z} by Th1;
rng (x,y,w,z --> a,b,c,d) c= A by A1, XBOOLE_1:1;
hence x,y,w,z --> a,b,c,d is Function of {x,y,w,z},A by A2, FUNCT_2:def 1, RELSET_1:11; :: thesis: verum