let X be set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for A being Element of S
for B being measure_zero of M holds
( M . (A \/ B) = M . A & M . (A /\ B) = 0. & M . (A \ B) = M . A )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for A being Element of S
for B being measure_zero of M holds
( M . (A \/ B) = M . A & M . (A /\ B) = 0. & M . (A \ B) = M . A )
let M be sigma_Measure of S; :: thesis: for A being Element of S
for B being measure_zero of M holds
( M . (A \/ B) = M . A & M . (A /\ B) = 0. & M . (A \ B) = M . A )
let A be Element of S; :: thesis: for B being measure_zero of M holds
( M . (A \/ B) = M . A & M . (A /\ B) = 0. & M . (A \ B) = M . A )
let B be measure_zero of M; :: thesis: ( M . (A \/ B) = M . A & M . (A /\ B) = 0. & M . (A \ B) = M . A )
A1: M . B = 0. by Def13;
A2: ( 0. <= M . (A \/ B) & 0. <= M . (A /\ B) & 0. <= M . (A \ B) ) by Def4;
M . (A \/ B) <= (M . A) + 0. by A1, Th64;
then A3: M . (A \/ B) <= M . A by XXREAL_3:4;
A4: M . A <= M . (A \/ B) by Th62, XBOOLE_1:7;
A5: M . (A /\ B) <= 0. by A1, Th62, XBOOLE_1:17;
then A6: M . (A /\ B) = 0. by A2, XXREAL_0:1;
A7: M . (A \ B) <= M . A by Th62, XBOOLE_1:36;
M . A = M . ((A /\ B) \/ (A \ B)) by XBOOLE_1:51;
then M . A <= 0. + (M . (A \ B)) by A6, Th64;
then M . A <= M . (A \ B) by XXREAL_3:4;
hence ( M . (A \/ B) = M . A & M . (A /\ B) = 0. & M . (A \ B) = M . A ) by A2, A3, A4, A5, A7, XXREAL_0:1; :: thesis: verum