let a, b, c, x, y, z, w, d be object ; :: 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 Th62;
rng ((w,z) --> (c,d)) c= {c,d} by Th62;
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 Th17;
hence rng ((x,y,w,z) --> (a,b,c,d)) c= {a,b,c,d} by A2; :: thesis: verum