let a, b, x, y, z be set ; :: thesis: for c being complex number holds rng ((a,b,c) --> (x,y,z)) c= {x,y,z}
let c be complex number ; :: 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 FUNCT_4:17;
A3: rng (c .--> z) = {z} by FUNCOP_1:8;
rng ((a,b) --> (x,y)) c= {x,y} by FUNCT_4:62;
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, XBOOLE_1:1; :: thesis: verum