let X be set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for A, B being Element of S st A misses B holds
M . (A \/ B) = (M . A) + (M . B)
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for A, B being Element of S st A misses B holds
M . (A \/ B) = (M . A) + (M . B)
let M be sigma_Measure of S; :: thesis: for A, B being Element of S st A misses B holds
M . (A \/ B) = (M . A) + (M . B)
let A, B be Element of S; :: thesis: ( A misses B implies M . (A \/ B) = (M . A) + (M . B) )
assume A1: A misses B ; :: thesis: M . (A \/ B) = (M . A) + (M . B)
M is Measure of S by Th60;
hence M . (A \/ B) = (M . A) + (M . B) by A1, Def5; :: thesis: verum