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 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 A7: ((max+ f) " {+infty}) /\ ((max- f) " {+infty}) = {} ;
(max+ f) " {-infty} misses (max- f) " {-infty}
proof
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 A9: ((max+ f) " {-infty}) /\ ((max- f) " {-infty}) = {} ;
(max+ f) " {+infty} misses (max- f) " {-infty}
proof
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 A12: ((max+ f) " {+infty}) /\ ((max- f) " {-infty}) = {} ;
(max+ f) " {-infty} misses (max- f) " {+infty}
proof
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 A14: ((max+ f) " {-infty}) /\ ((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