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

( 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) )end;

hence
( dom (f + g) = (dom f) /\ (dom g) & dom (f - g) = (dom f) /\ (dom g) )
; :: thesis: verumper cases
( not f is V82() or not g is V82() )
by A1;

end;

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

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