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