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.

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

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

M * F is V92()
by MEASURE1:25;
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;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

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