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;
A2: (max+ f) " {+infty } misses (max- f) " {+infty }

proof

assume A3: not (max+ f) " {+infty } misses (max- f) " {+infty } ; :: thesis: contradiction
consider x1 being set such that
A4: x1 in (max+ f) " {+infty } and
A5: x1 in (max- f) " {+infty } by A3, 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;
A9: (max- f) . x1 = +infty by A7, TARSKI:def 1;
thus contradiction by A8, A9, Th17; :: thesis: verum

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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