let X be non empty set ; :: thesis: for f, g being PartFunc of X,ExtREAL st ( not f is V82() or not g is V82() ) holds
( dom (f + g) = (dom f) /\ (dom g) & dom (f - g) = (dom f) /\ (dom g) )
let f, g be PartFunc of X,ExtREAL; :: thesis: ( ( not f is V82() or not g is V82() ) implies ( dom (f + g) = (dom f) /\ (dom g) & dom (f - g) = (dom f) /\ (dom g) ) )
assume A1: ( not f is V82() or not g is V82() ) ; :: thesis: ( dom (f + g) = (dom f) /\ (dom g) & dom (f - g) = (dom f) /\ (dom g) )

now :: thesis: ( dom (f + g) = (dom f) /\ (dom g) & dom (f - g) = (dom f) /\ (dom g) )

per cases ( not f is V82() or not g is V82() ) by A1;

suppose A2: f is V82() ; :: thesis: ( dom (f + g) = (dom f) /\ (dom g) & dom (f - g) = (dom f) /\ (dom g) )

then not +infty in rng f ;
then A3: f " {+infty} = {} by FUNCT_1:72;
not -infty in rng f by A2;
then A4: f " {-infty} = {} by FUNCT_1:72;
then A5: ((f " {+infty}) /\ (g " {-infty})) \/ ((f " {-infty}) /\ (g " {+infty})) = {} by A3;
A6: ((f " {+infty}) /\ (g " {+infty})) \/ ((f " {-infty}) /\ (g " {-infty})) = {} by A3, A4;
dom (f + g) = ((dom f) /\ (dom g)) \ {} by A5, MESFUNC1:def 3;
hence ( dom (f + g) = (dom f) /\ (dom g) & dom (f - g) = (dom f) /\ (dom g) ) by A6, MESFUNC1:def 4; :: thesis: verum

end;

suppose A7: g is V82() ; :: thesis: ( dom (f + g) = (dom f) /\ (dom g) & dom (f - g) = (dom f) /\ (dom g) )

then not +infty in rng g ;
then A8: g " {+infty} = {} by FUNCT_1:72;
not -infty in rng g by A7;
then A9: g " {-infty} = {} by FUNCT_1:72;
then A10: ((f " {+infty}) /\ (g " {-infty})) \/ ((f " {-infty}) /\ (g " {+infty})) = {} by A8;
A11: ((f " {+infty}) /\ (g " {+infty})) \/ ((f " {-infty}) /\ (g " {-infty})) = {} by A8, A9;
dom (f + g) = ((dom f) /\ (dom g)) \ {} by A10, MESFUNC1:def 3;
hence ( dom (f + g) = (dom f) /\ (dom g) & dom (f - g) = (dom f) /\ (dom g) ) by A11, MESFUNC1:def 4; :: thesis: verum

end;

end;

end;

hence ( dom (f + g) = (dom f) /\ (dom g) & dom (f - g) = (dom f) /\ (dom g) ) ; :: thesis: verum