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