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