dom f = REAL by FUNCT_2:def 1;
then f is_differentiable_on REAL by FDIFF_1:def 8;
then dom (f `| REAL) = REAL by FDIFF_1:def 7;
hence f `| REAL is Function of REAL,REAL by FUNCT_2:67; :: thesis: verum