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 " = {} by FUNCT_1:72;
not -infty in rng f by A2;
then A4: f " = {} by FUNCT_1:72;
then A5: ((f " ) /\ ()) \/ (() /\ ()) = {} by A3;
A6: ((f " ) /\ ()) \/ (() /\ ()) = {} by A3, A4;
dom (f + g) = ((dom f) /\ (dom g)) \ {} by ;
hence ( dom (f + g) = (dom f) /\ (dom g) & dom (f - g) = (dom f) /\ (dom g) ) by ; :: 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 " = {} by FUNCT_1:72;
not -infty in rng g by A7;
then A9: g " = {} by FUNCT_1:72;
then A10: ((f " ) /\ ()) \/ (() /\ ()) = {} by A8;
A11: ((f " ) /\ ()) \/ (() /\ ()) = {} by A8, A9;
dom (f + g) = ((dom f) /\ (dom g)) \ {} by ;
hence ( dom (f + g) = (dom f) /\ (dom g) & dom (f - g) = (dom f) /\ (dom g) ) by ; :: thesis: verum
end;
end;
end;
hence ( dom (f + g) = (dom f) /\ (dom g) & dom (f - g) = (dom f) /\ (dom g) ) ; :: thesis: verum