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 . A = M . ((A /\ B) \/ (A \ B)) by XBOOLE_1:51;
A2: M . B = 0. by Def7;
then A3: M . (A /\ B) <= 0. by ;
A4: 0. <= M . (A /\ B) by Def2;
then M . (A /\ B) = 0. by A3;
then M . A <= 0. + (M . (A \ B)) by ;
then A5: M . A <= M . (A \ B) by XXREAL_3:4;
M . (A \/ B) <= (M . A) + 0. by ;
then A6: M . (A \/ B) <= M . A by XXREAL_3:4;
( M . A <= M . (A \/ B) & M . (A \ B) <= M . A ) by ;
hence ( M . (A \/ B) = M . A & M . (A /\ B) = 0. & M . (A \ B) = M . A ) by ; :: thesis: verum