let X be non empty 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 4
.= (dom f) /\ (dom g) ; :: thesis: verum