let X be set ; :: thesis: for S being Field_Subset of X

for M being Measure of S

for A, B being Element of S st A c= B & M . A < +infty holds

M . (B \ A) = (M . B) - (M . A)

let S be Field_Subset of X; :: thesis: for M being Measure of S

for A, B being Element of S st A c= B & M . A < +infty holds

M . (B \ A) = (M . B) - (M . A)

let M be Measure of S; :: thesis: for A, B being Element of S st A c= B & M . A < +infty holds

M . (B \ A) = (M . B) - (M . A)

let A, B be Element of S; :: thesis: ( A c= B & M . A < +infty implies M . (B \ A) = (M . B) - (M . A) )

set C = B \ A;

assume that

A1: A c= B and

A2: M . A < +infty ; :: thesis: M . (B \ A) = (M . B) - (M . A)

A3: 0. <= M . A by Def2;

A misses B \ A by XBOOLE_1:79;

then M . (A \/ (B \ A)) = (M . A) + (M . (B \ A)) by Def3;

then M . B = (M . A) + (M . (B \ A)) by A1, XBOOLE_1:45;

hence M . (B \ A) = (M . B) - (M . A) by A2, A3, XXREAL_3:28; :: thesis: verum

for M being Measure of S

for A, B being Element of S st A c= B & M . A < +infty holds

M . (B \ A) = (M . B) - (M . A)

let S be Field_Subset of X; :: thesis: for M being Measure of S

for A, B being Element of S st A c= B & M . A < +infty holds

M . (B \ A) = (M . B) - (M . A)

let M be Measure of S; :: thesis: for A, B being Element of S st A c= B & M . A < +infty holds

M . (B \ A) = (M . B) - (M . A)

let A, B be Element of S; :: thesis: ( A c= B & M . A < +infty implies M . (B \ A) = (M . B) - (M . A) )

set C = B \ A;

assume that

A1: A c= B and

A2: M . A < +infty ; :: thesis: M . (B \ A) = (M . B) - (M . A)

A3: 0. <= M . A by Def2;

A misses B \ A by XBOOLE_1:79;

then M . (A \/ (B \ A)) = (M . A) + (M . (B \ A)) by Def3;

then M . B = (M . A) + (M . (B \ A)) by A1, XBOOLE_1:45;

hence M . (B \ A) = (M . B) - (M . A) by A2, A3, XXREAL_3:28; :: thesis: verum