let X be set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for T being N_Measure_fam of S st ( for A being set st A in T holds
A is measure_zero of M ) holds
union T is measure_zero of M
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for T being N_Measure_fam of S st ( for A being set st A in T holds
A is measure_zero of M ) holds
union T is measure_zero of M
let M be sigma_Measure of S; :: thesis: for T being N_Measure_fam of S st ( for A being set st A in T holds
A is measure_zero of M ) holds
union T is measure_zero of M
let T be N_Measure_fam of S; :: thesis: ( ( for A being set st A in T holds
A is measure_zero of M ) implies union T is measure_zero of M )
assume A1: for A being set st A in T holds
A is measure_zero of M ; :: thesis: union T is measure_zero of M
consider F being Function of NAT ,S such that
A2: T = rng F by Th14;
set G = M * F;
A3: M * F is nonnegative by Th1;
A4: for r being Element of NAT st 0 <= r holds
(M * F) . r = 0.

proof

let r be Element of NAT ; :: thesis: ( 0 <= r implies (M * F) . r = 0. )
F . r is measure_zero of M by A1, A2, FUNCT_2:6;
then M . (F . r) = 0. by MEASURE1:def 13;
hence ( 0 <= r implies (M * F) . r = 0. ) by FUNCT_2:21; :: thesis: verum

end;

then SUM (M * F) = (Ser (M * F)) . 0 by A3, SUPINF_2:67;
then SUM (M * F) = (M * F) . 0 by SUPINF_2:63;
then SUM (M * F) = 0. by A4;
then A5: M . (union T) <= 0. by A2, Th13;
0. <= M . (union T) by MEASURE1:def 4;
then M . (union T) = 0. by A5, XXREAL_0:1;
hence union T is measure_zero of M by MEASURE1:def 13; :: thesis: verum