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