let X be set ; :: thesis: for S being Field_Subset of X
for M being 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 Field_Subset of X; :: thesis: for M being 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 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 . A = M . ((A /\ B) \/ (A \ B)) by XBOOLE_1:51;
A2: M . B = 0. by Def7;
then A3: M . (A /\ B) <= 0. by Th25, XBOOLE_1:17;
A4: 0. <= M . (A /\ B) by Def4;
then M . (A /\ B) = 0. by A3, XXREAL_0:1;
then M . A <= 0. + (M . (A \ B)) by A1, Th27;
then A5: M . A <= M . (A \ B) by XXREAL_3:4;
M . (A \/ B) <= (M . A) + 0. by A2, Th27;
then A6: M . (A \/ B) <= M . A by XXREAL_3:4;
( M . A <= M . (A \/ B) & M . (A \ B) <= M . A ) by Th25, XBOOLE_1:7, XBOOLE_1:36;
hence ( M . (A \/ B) = M . A & M . (A /\ B) = 0. & M . (A \ B) = M . A ) by A4, A6, A3, A5, XXREAL_0:1; :: thesis: verum