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 Def4;

then A3: M . (A /\ B) <= 0. by Th8, XBOOLE_1:17;

A4: 0. <= M . (A /\ B) by Def2;

then M . (A /\ B) = 0. by A3;

then M . A <= 0. + (M . (A \ B)) by A1, Th10;

then A5: M . A <= M . (A \ B) by XXREAL_3:4;

M . (A \/ B) <= (M . A) + 0. by A2, Th10;

then A6: M . (A \/ B) <= M . A by XXREAL_3:4;

( M . A <= M . (A \/ B) & M . (A \ B) <= M . A ) by Th8, 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

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 Def4;

then A3: M . (A /\ B) <= 0. by Th8, XBOOLE_1:17;

A4: 0. <= M . (A /\ B) by Def2;

then M . (A /\ B) = 0. by A3;

then M . A <= 0. + (M . (A \ B)) by A1, Th10;

then A5: M . A <= M . (A \ B) by XXREAL_3:4;

M . (A \/ B) <= (M . A) + 0. by A2, Th10;

then A6: M . (A \/ B) <= M . A by XXREAL_3:4;

( M . A <= M . (A \/ B) & M . (A \ B) <= M . A ) by Th8, 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