let X be non empty set ; :: thesis: for f, g being PartFunc of X,ExtREAL st f is without+infty & g is without-infty holds
dom (f - g) = (dom f) /\ (dom g)
let f, g be PartFunc of X,ExtREAL ; :: thesis: ( f is without+infty & g is without-infty implies dom (f - g) = (dom f) /\ (dom g) )
assume ( f is without+infty & g is without-infty ) ; :: thesis: dom (f - g) = (dom f) /\ (dom g)
then ( not -infty in rng g & not +infty in rng f ) by MESFUNC5:def 3, MESFUNC5:def 4;
then ( g " {-infty } = {} & f " {+infty } = {} ) by FUNCT_1:142;
then ((g " {+infty }) /\ (f " {+infty })) \/ ((g " {-infty }) /\ (f " {-infty })) = {} ;
then dom (f - g) = ((dom f) /\ (dom g)) \ {} by MESFUNC1:def 4;
hence dom (f - g) = (dom f) /\ (dom g) ; :: thesis: verum