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 A2: f is real-valued ; :: thesis: ( dom (f + g) = (dom f) /\ (dom g) & dom (f - g) = (dom f) /\ (dom g) )

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

end;

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

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

end;

end;

end;

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