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

now

per cases ( f is real-valued or g is real-valued ) by A1;

suppose A3: f is real-valued ; :: thesis: ( dom (f + g) = (dom f) /\ (dom g) & dom (f - g) = (dom f) /\ (dom g) )

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

end;

suppose A11: g is real-valued ; :: thesis: ( dom (f + g) = (dom f) /\ (dom g) & dom (f - g) = (dom f) /\ (dom g) )

then not +infty in rng g ;
then A13: g " {+infty} = {} by FUNCT_1:142;
not -infty in rng g by A11;
then A15: g " {-infty} = {} by FUNCT_1:142;
then A16: ((f " {+infty}) /\ (g " {-infty})) \/ ((f " {-infty}) /\ (g " {+infty})) = {} by A13;
A17: ((f " {+infty}) /\ (g " {+infty})) \/ ((f " {-infty}) /\ (g " {-infty})) = {} by A13, A15;
dom (f + g) = ((dom f) /\ (dom g)) \ {} by A16, MESFUNC1:def 3;
hence ( dom (f + g) = (dom f) /\ (dom g) & dom (f - g) = (dom f) /\ (dom g) ) by A17, 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