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
A2: ( x1 in (max+ f) " {+infty } & x1 in (max- f) " {+infty } ) by XBOOLE_0:3;
reconsider x1 = x1 as Element of C by A2;
( x1 in dom (max+ f) & (max+ f) . x1 in {+infty } & x1 in dom (max- f) & (max- f) . x1 in {+infty } ) by A2, FUNCT_1:def 13;
then ( x1 in dom f & (max+ f) . x1 = +infty & (max- f) . x1 = +infty ) by Def2, TARSKI:def 1;
hence contradiction by Th17; :: thesis: verum

end;

then A3: ((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
A4: ( x1 in (max+ f) " {-infty } & x1 in (max- f) " {-infty } ) by XBOOLE_0:3;
reconsider x1 = x1 as Element of C by A4;
( x1 in dom (max+ f) & (max+ f) . x1 in {-infty } & x1 in dom (max- f) & (max- f) . x1 in {-infty } ) by A4, FUNCT_1:def 13;
then ( x1 in dom f & (max+ f) . x1 = -infty & (max- f) . x1 = -infty ) by Def2, TARSKI:def 1;
hence contradiction by Th14; :: thesis: verum

end;

then A5: ((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
A6: ( x1 in (max+ f) " {+infty } & x1 in (max- f) " {-infty } ) by XBOOLE_0:3;
reconsider x1 = x1 as Element of C by A6;
( x1 in dom (max- f) & (max- f) . x1 in {-infty } ) by A6, FUNCT_1:def 13;
then ( x1 in dom f & (max- f) . x1 = -infty ) by Def3, TARSKI:def 1;
hence contradiction by Th15; :: thesis: verum

end;

then A7: ((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
A8: ( x1 in (max+ f) " {-infty } & x1 in (max- f) " {+infty } ) by XBOOLE_0:3;
reconsider x1 = x1 as Element of C by A8;
( x1 in dom (max+ f) & (max+ f) . x1 in {-infty } ) by A8, FUNCT_1:def 13;
then ( x1 in dom f & (max+ f) . x1 = -infty ) by Def2, TARSKI:def 1;
hence contradiction by Th14; :: thesis: verum

end;

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