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 ;
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 V92() by MEASURE1:25;
then SUM (M * F) = (Ser (M * F)) . 0 by ;
then SUM (M * F) = (M * F) . 0 by SUPINF_2:def 11;
then SUM (M * F) = 0. by A3;
then A4: M . () <= 0. by ;
0. <= M . () by MEASURE1:def 2;
then M . () = 0. by ;
hence union T is measure_zero of M by MEASURE1:def 7; :: thesis: verum