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 )
consider F being sequence of S such that
A1: T = rng F by Th12;
set G = M * F;
assume A2: for A being set st A in T holds
A is measure_zero of M ; :: thesis: union T is measure_zero of M
A3: 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 A2, A1, FUNCT_2:4;
then M . (F . r) = 0. by MEASURE1:def 7;
hence ( 0 <= r implies (M * F) . r = 0. ) by FUNCT_2:15; :: thesis: verum

end;

M * F is nonnegative by MEASURE1:25;
then SUM (M * F) = (Ser (M * F)) . 0 by A3, SUPINF_2:48;
then SUM (M * F) = (M * F) . 0 by SUPINF_2:def 11;
then SUM (M * F) = 0. by A3;
then A4: M . (union T) <= 0. by A1, Th11;
0. <= M . (union T) by MEASURE1:def 2;
then M . (union T) = 0. by A4, XXREAL_0:1;
hence union T is measure_zero of M by MEASURE1:def 7; :: thesis: verum