let X be set ; :: thesis: for C being C_Measure of X
for W, Z being Subset of X st W in sigma_Field C & Z misses W holds
C . (W \/ Z) = (C . W) + (C . Z)
let C be C_Measure of X; :: thesis: for W, Z being Subset of X st W in sigma_Field C & Z misses W holds
C . (W \/ Z) = (C . W) + (C . Z)
let W, Z be Subset of X; :: thesis: ( W in sigma_Field C & Z misses W implies C . (W \/ Z) = (C . W) + (C . Z) )
assume that
A1: W in sigma_Field C and
A2: Z misses W ; :: thesis: C . (W \/ Z) = (C . W) + (C . Z)
Z \ W c= X \ W by XBOOLE_1:33;
then Z c= X \ W by A2, XBOOLE_1:83;
hence C . (W \/ Z) = (C . W) + (C . Z) by A1, Th5; :: thesis: verum