let f be Function of REAL,REAL; :: thesis: f is Function of R^1,R^1
dom f = REAL by FUNCT_2:def 1;
then reconsider B = rng f as non empty Subset of REAL by RELAT_1:42;
f is Function of R^1,(R^1 | (R^1 B)) by Th7;
hence f is Function of R^1,R^1 by TOPREALA:7; :: thesis: verum