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}

(max+ f) " {-infty} misses (max- f) " {-infty}

(max+ f) " {+infty} misses (max- f) " {-infty}

(max+ f) " {-infty} misses (max- f) " {+infty}

dom ((max+ f) - (max- f)) = ((dom f) /\ (dom f)) \ ({} \/ {}) by A1, A7, A9, MESFUNC1:def 4;

hence ( dom f = dom ((max+ f) - (max- f)) & dom f = dom ((max+ f) + (max- f)) ) by A1, A12, A14, MESFUNC1:def 3; :: thesis: verum

( 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

then A7:
((max+ f) " {+infty}) /\ ((max- f) " {+infty}) = {}
;
assume
not (max+ f) " {+infty} misses (max- f) " {+infty}
; :: thesis: contradiction

then consider x1 being object such that

A2: x1 in (max+ f) " {+infty} and

A3: x1 in (max- f) " {+infty} by XBOOLE_0:3;

reconsider x1 = x1 as Element of C by A2;

A4: (max+ f) . x1 in {+infty} by A2, FUNCT_1:def 7;

A5: (max- f) . x1 in {+infty} by A3, FUNCT_1:def 7;

A6: (max+ f) . x1 = +infty by A4, TARSKI:def 1;

(max- f) . x1 = +infty by A5, TARSKI:def 1;

hence contradiction by A6, Th15; :: thesis: verum

end;then consider x1 being object such that

A2: x1 in (max+ f) " {+infty} and

A3: x1 in (max- f) " {+infty} by XBOOLE_0:3;

reconsider x1 = x1 as Element of C by A2;

A4: (max+ f) . x1 in {+infty} by A2, FUNCT_1:def 7;

A5: (max- f) . x1 in {+infty} by A3, FUNCT_1:def 7;

A6: (max+ f) . x1 = +infty by A4, TARSKI:def 1;

(max- f) . x1 = +infty by A5, TARSKI:def 1;

hence contradiction by A6, Th15; :: thesis: verum

(max+ f) " {-infty} misses (max- f) " {-infty}

proof

then A9:
((max+ f) " {-infty}) /\ ((max- f) " {-infty}) = {}
;
assume
not (max+ f) " {-infty} misses (max- f) " {-infty}
; :: thesis: contradiction

then consider x1 being object such that

A8: x1 in (max+ f) " {-infty} and

x1 in (max- f) " {-infty} by XBOOLE_0:3;

reconsider x1 = x1 as Element of C by A8;

(max+ f) . x1 in {-infty} by A8, FUNCT_1:def 7;

then (max+ f) . x1 = -infty by TARSKI:def 1;

hence contradiction by Th12; :: thesis: verum

end;then consider x1 being object such that

A8: x1 in (max+ f) " {-infty} and

x1 in (max- f) " {-infty} by XBOOLE_0:3;

reconsider x1 = x1 as Element of C by A8;

(max+ f) . x1 in {-infty} by A8, FUNCT_1:def 7;

then (max+ f) . x1 = -infty by TARSKI:def 1;

hence contradiction by Th12; :: thesis: verum

(max+ f) " {+infty} misses (max- f) " {-infty}

proof

then A12:
((max+ f) " {+infty}) /\ ((max- f) " {-infty}) = {}
;
assume
not (max+ f) " {+infty} misses (max- f) " {-infty}
; :: thesis: contradiction

then consider x1 being object such that

A10: x1 in (max+ f) " {+infty} and

A11: x1 in (max- f) " {-infty} by XBOOLE_0:3;

reconsider x1 = x1 as Element of C by A10;

(max- f) . x1 in {-infty} by A11, FUNCT_1:def 7;

then (max- f) . x1 = -infty by TARSKI:def 1;

hence contradiction by Th13; :: thesis: verum

end;then consider x1 being object such that

A10: x1 in (max+ f) " {+infty} and

A11: x1 in (max- f) " {-infty} by XBOOLE_0:3;

reconsider x1 = x1 as Element of C by A10;

(max- f) . x1 in {-infty} by A11, FUNCT_1:def 7;

then (max- f) . x1 = -infty by TARSKI:def 1;

hence contradiction by Th13; :: thesis: verum

(max+ f) " {-infty} misses (max- f) " {+infty}

proof

then A14:
((max+ f) " {-infty}) /\ ((max- f) " {+infty}) = {}
;
assume
not (max+ f) " {-infty} misses (max- f) " {+infty}
; :: thesis: contradiction

then consider x1 being object 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 7;

then (max+ f) . x1 = -infty by TARSKI:def 1;

hence contradiction by Th12; :: thesis: verum

end;then consider x1 being object 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 7;

then (max+ f) . x1 = -infty by TARSKI:def 1;

hence contradiction by Th12; :: thesis: verum

dom ((max+ f) - (max- f)) = ((dom f) /\ (dom f)) \ ({} \/ {}) by A1, A7, A9, MESFUNC1:def 4;

hence ( dom f = dom ((max+ f) - (max- f)) & dom f = dom ((max+ f) + (max- f)) ) by A1, A12, A14, MESFUNC1:def 3; :: thesis: verum