dom (R_EAL f) = X by FUNCT_2:def 1;
hence R_EAL f is total by PARTFUN1:def 4; :: thesis: verum