let X be set ; :: thesis: for f being PartFunc of X,REAL
for g being non-empty PartFunc of X,REAL holds dom (f / g) = (dom f) /\ (dom g)
let f be PartFunc of X,REAL; :: thesis: for g being non-empty PartFunc of X,REAL holds dom (f / g) = (dom f) /\ (dom g)
let g be non-empty PartFunc of X,REAL; :: thesis: dom (f / g) = (dom f) /\ (dom g)
thus dom (f / g) = (dom f) /\ ((dom g) \ (g " {0})) by RFUNCT_1:def 1
.= (dom f) /\ (dom g) ; :: thesis: verum