let X be non empty set ; :: thesis: for f being PartFunc of ,
for g being non-empty PartFunc of , holds dom (f / g) = (dom f) /\ (dom g)
let f be PartFunc of ,; :: thesis: for g being non-empty PartFunc of , holds dom (f / g) = (dom f) /\ (dom g)
let g be non-empty PartFunc of ,; :: 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