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

.= 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