let C be non empty set ; :: thesis: for f being PartFunc of C,ExtREAL holds
( dom f = dom ((max+ f) - (max- f)) & dom f = dom ((max+ f) + (max- f)) )
let f be PartFunc of C,ExtREAL; :: thesis: ( dom f = dom ((max+ f) - (max- f)) & dom f = dom ((max+ f) + (max- f)) )
A1: ( dom (max+ f) = dom f & dom (max- f) = dom f ) by Def2, Def3;
(max+ f) " {+infty} misses (max- f) " {+infty}

proof

assume not (max+ f) " {+infty} misses (max- f) " {+infty} ; :: thesis: contradiction
then consider x1 being set such that
A4: x1 in (max+ f) " {+infty} and
A5: x1 in (max- f) " {+infty} by XBOOLE_0:3;
reconsider x1 = x1 as Element of C by A4;
A6: (max+ f) . x1 in {+infty} by A4, FUNCT_1:def 13;
A7: (max- f) . x1 in {+infty} by A5, FUNCT_1:def 13;
A8: (max+ f) . x1 = +infty by A6, TARSKI:def 1;
(max- f) . x1 = +infty by A7, TARSKI:def 1;
hence contradiction by A8, Th17; :: thesis: verum

end;

then A10: ((max+ f) " {+infty}) /\ ((max- f) " {+infty}) = {} by XBOOLE_0:def 7;
(max+ f) " {-infty} misses (max- f) " {-infty}

proof

assume not (max+ f) " {-infty} misses (max- f) " {-infty} ; :: thesis: contradiction
then consider x1 being set such that
A13: x1 in (max+ f) " {-infty} and
x1 in (max- f) " {-infty} by XBOOLE_0:3;
reconsider x1 = x1 as Element of C by A13;
(max+ f) . x1 in {-infty} by A13, FUNCT_1:def 13;
then (max+ f) . x1 = -infty by TARSKI:def 1;
hence contradiction by Th14; :: thesis: verum

end;

then A16: ((max+ f) " {-infty}) /\ ((max- f) " {-infty}) = {} by XBOOLE_0:def 7;
(max+ f) " {+infty} misses (max- f) " {-infty}

proof

assume not (max+ f) " {+infty} misses (max- f) " {-infty} ; :: thesis: contradiction
then consider x1 being set such that
A19: x1 in (max+ f) " {+infty} and
A20: x1 in (max- f) " {-infty} by XBOOLE_0:3;
reconsider x1 = x1 as Element of C by A19;
(max- f) . x1 in {-infty} by A20, FUNCT_1:def 13;
then (max- f) . x1 = -infty by TARSKI:def 1;
hence contradiction by Th15; :: thesis: verum

end;

then A23: ((max+ f) " {+infty}) /\ ((max- f) " {-infty}) = {} by XBOOLE_0:def 7;
(max+ f) " {-infty} misses (max- f) " {+infty}

proof

assume not (max+ f) " {-infty} misses (max- f) " {+infty} ; :: thesis: contradiction
then consider x1 being set such that
A26: x1 in (max+ f) " {-infty} and
x1 in (max- f) " {+infty} by XBOOLE_0:3;
reconsider x1 = x1 as Element of C by A26;
(max+ f) . x1 in {-infty} by A26, FUNCT_1:def 13;
then (max+ f) . x1 = -infty by TARSKI:def 1;
hence contradiction by Th14; :: thesis: verum

end;

then A29: ((max+ f) " {-infty}) /\ ((max- f) " {+infty}) = {} by XBOOLE_0:def 7;
dom ((max+ f) - (max- f)) = ((dom f) /\ (dom f)) \ ({} \/ {}) by A1, A10, A16, MESFUNC1:def 4;
hence ( dom f = dom ((max+ f) - (max- f)) & dom f = dom ((max+ f) + (max- f)) ) by A1, A23, A29, MESFUNC1:def 3; :: thesis: verum