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:17;
A2: dom ((x,y,w,z) --> (a,b,c,d)) = {x,y,w,z} by FUNCT_4:137;
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:4; :: thesis: verum