let r be Real; :: thesis: rng (REAL --> r) c= REAL
rng (REAL --> r) c= {r} by FUNCOP_1:13;
hence rng (REAL --> r) c= REAL by XBOOLE_1:1; :: thesis: verum