let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for E1, E2 being Element of S st M . E1 = 0 & M . E2 = 0 holds
M . (E1 \/ E2) = 0
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for E1, E2 being Element of S st M . E1 = 0 & M . E2 = 0 holds
M . (E1 \/ E2) = 0
let M be sigma_Measure of S; :: thesis: for E1, E2 being Element of S st M . E1 = 0 & M . E2 = 0 holds
M . (E1 \/ E2) = 0
let E1, E2 be Element of S; :: thesis: ( M . E1 = 0 & M . E2 = 0 implies M . (E1 \/ E2) = 0 )
assume ( M . E1 = 0 & M . E2 = 0 ) ; :: thesis: M . (E1 \/ E2) = 0
then ( E1 is measure_zero of M & E2 is measure_zero of M ) by MEASURE1:def 7;
hence M . (E1 \/ E2) = 0 by MEASURE1:37, MEASURE1:def 7; :: thesis: verum