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