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);
( rng (x,y --> a,b) c= {a,b} & rng (w,z --> c,d) c= {c,d} ) by FUNCT_4:65;
then (rng (x,y --> a,b)) \/ (rng (w,z --> c,d)) c= {a,b} \/ {c,d} by XBOOLE_1:13;
then A1: (rng (x,y --> a,b)) \/ (rng (w,z --> c,d)) c= {a,b,c,d} by ENUMSET1:45;
rng ((x,y --> a,b) +* (w,z --> 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,b,c,d} by A1, XBOOLE_1:1; :: thesis: verum