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 that
A1: f is without+infty and
A2: g is without-infty ; :: thesis: dom (f - g) = (dom f) /\ (dom g)
not +infty in rng f by A1;
then A3: f " {+infty} = {} by FUNCT_1:72;
not -infty in rng g by A2;
then g " {-infty} = {} by FUNCT_1:72;
then ((g " {+infty}) /\ (f " {+infty})) \/ ((g " {-infty}) /\ (f " {-infty})) = {} by A3;
then dom (f - g) = ((dom f) /\ (dom g)) \ {} by MESFUNC1:def 4;
hence dom (f - g) = (dom f) /\ (dom g) ; :: thesis: verum