dom (r (#) f) = dom f by MESFUNC1:def 6;
then dom (r (#) f) = X by FUNCT_2:def 1;
hence r (#) f is Function of X,ExtREAL by FUNCT_2:def 1; :: thesis: verum