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

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