dom f = A by FUNCT_2:def 1;
then dom (Im f) = A by MESFUN6C:def 2;
hence Im f is Function of A,REAL by FUNCT_2:def 1; :: thesis: verum