let f be Function of REAL,REAL; :: thesis: f is Function of R^1,(R^1 | (R^1 (rng f)))
REAL = dom f by FUNCT_2:def 1;
then R^1 | (R^1 (dom f)) = R^1 by Th6;
then R^1 f is Function of R^1,(R^1 | (R^1 (rng f))) ;
hence f is Function of R^1,(R^1 | (R^1 (rng f))) ; :: thesis: verum