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) )

A2: 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) )

A4: not +infty in rng f by A3;
A5: f " {+infty } = {} by A4, FUNCT_1:142;
A6: not -infty in rng f by A3;
A7: f " {-infty } = {} by A6, FUNCT_1:142;
A8: ((f " {+infty }) /\ (g " {-infty })) \/ ((f " {-infty }) /\ (g " {+infty })) = {} by A5, A7;
A9: ((f " {+infty }) /\ (g " {+infty })) \/ ((f " {-infty }) /\ (g " {-infty })) = {} by A5, A7;
A10: dom (f + g) = ((dom f) /\ (dom g)) \ {} by A8, MESFUNC1:def 3;
thus ( dom (f + g) = (dom f) /\ (dom g) & dom (f - g) = (dom f) /\ (dom g) ) by A9, A10, 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) )

A12: not +infty in rng g by A11;
A13: g " {+infty } = {} by A12, FUNCT_1:142;
A14: not -infty in rng g by A11;
A15: g " {-infty } = {} by A14, FUNCT_1:142;
A16: ((f " {+infty }) /\ (g " {-infty })) \/ ((f " {-infty }) /\ (g " {+infty })) = {} by A13, A15;
A17: ((f " {+infty }) /\ (g " {+infty })) \/ ((f " {-infty }) /\ (g " {-infty })) = {} by A13, A15;
A18: dom (f + g) = ((dom f) /\ (dom g)) \ {} by A16, MESFUNC1:def 3;
thus ( dom (f + g) = (dom f) /\ (dom g) & dom (f - g) = (dom f) /\ (dom g) ) by A17, A18, MESFUNC1:def 4; :: thesis: verum

end;

end;

end;

thus ( dom (f + g) = (dom f) /\ (dom g) & dom (f - g) = (dom f) /\ (dom g) ) by A2; :: thesis: verum