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