dom (f / g) = (dom f) /\ (dom g) by Th3
.= X /\ (dom g) by FUNCT_2:def 1
.= X /\ X by FUNCT_2:def 1 ;
hence f / g is Function of X,REAL by FUNCT_2:def 1; :: thesis: verum