let a, b, c, x, y, z, w, d be object ; 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; verum