let r be Real; :: thesis: rng (REAL --> r) c= REAL
A1: rng (REAL --> r) c= {r} by FUNCOP_1:19;
thus rng (REAL --> r) c= REAL by A1, XBOOLE_1:1; :: thesis: verum