let a, b, c, x, y, z be object ; :: thesis: rng ((a,b,c) --> (x,y,z)) c= {x,y,z}
A1: {x,y} \/ {z} = {x,y,z} by ENUMSET1:3;
A2: rng ((a,b,c) --> (x,y,z)) c= (rng ((a,b) --> (x,y))) \/ (rng (c .--> z)) by Th17;
A3: rng (c .--> z) = {z} by FUNCOP_1:8;
rng ((a,b) --> (x,y)) c= {x,y} by Th62;
then (rng ((a,b) --> (x,y))) \/ (rng (c .--> z)) c= {x,y} \/ {z} by A3, XBOOLE_1:13;
hence rng ((a,b,c) --> (x,y,z)) c= {x,y,z} by A2, A1; :: thesis: verum