let x, y, w, z, a, b, c, d be set ; :: thesis: rng ((x,y,w,z) --> (a,b,c,d)) c= {a,b,c,d}
set f = (x,y) --> (a,b);
set g = (w,z) --> (c,d);
set h = ((x,y) --> (a,b)) +* ((w,z) --> (c,d));
A1: rng ((x,y) --> (a,b)) c= {a,b} by FUNCT_4:62;
rng ((w,z) --> (c,d)) c= {c,d} by FUNCT_4:62;
then (rng ((x,y) --> (a,b))) \/ (rng ((w,z) --> (c,d))) c= {a,b} \/ {c,d} by A1, XBOOLE_1:13;
then A2: (rng ((x,y) --> (a,b))) \/ (rng ((w,z) --> (c,d))) c= {a,b,c,d} by ENUMSET1:5;
rng (((x,y) --> (a,b)) +* ((w,z) --> (c,d))) c= (rng ((x,y) --> (a,b))) \/ (rng ((w,z) --> (c,d))) by FUNCT_4:17;
hence rng ((x,y,w,z) --> (a,b,c,d)) c= {a,b,c,d} by A2, XBOOLE_1:1; :: thesis: verum