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