let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for E being Element of S st E = dom f & f is nonnegative & f is E -measurable & Integral (M,f) = 0 holds
M . (E /\ (great_dom (f,0))) = 0

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for E being Element of S st E = dom f & f is nonnegative & f is E -measurable & Integral (M,f) = 0 holds
M . (E /\ (great_dom (f,0))) = 0

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL
for E being Element of S st E = dom f & f is nonnegative & f is E -measurable & Integral (M,f) = 0 holds
M . (E /\ (great_dom (f,0))) = 0

let f be PartFunc of X,ExtREAL; :: thesis: for E being Element of S st E = dom f & f is nonnegative & f is E -measurable & Integral (M,f) = 0 holds
M . (E /\ (great_dom (f,0))) = 0

let E be Element of S; :: thesis: ( E = dom f & f is nonnegative & f is E -measurable & Integral (M,f) = 0 implies M . (E /\ (great_dom (f,0))) = 0 )
assume that
A1: E = dom f and
A2: f is nonnegative and
A3: f is E -measurable and
A4: Integral (M,f) = 0 ; :: thesis: M . (E /\ (great_dom (f,0))) = 0
defpred S1[ Nat, object ] means \$2 = E /\ (great_eq_dom (f,(1 / (\$1 + 1))));
A5: for n being Element of NAT ex y being Element of S st S1[n,y]
proof
let n be Element of NAT ; :: thesis: ex y being Element of S st S1[n,y]
E /\ (great_eq_dom (f,(1 / (n + 1)))) is Element of S by ;
hence ex y being Element of S st S1[n,y] ; :: thesis: verum
end;
consider F being Function of NAT,S such that
A6: for n being Element of NAT holds S1[n,F . n] from A7: for n being Element of NAT holds (M * F) . n = 0
proof
let n be Element of NAT ; :: thesis: (M * F) . n = 0
dom F = NAT by FUNCT_2:def 1;
then (M * F) . n = M . (F . n) by FUNCT_1:13
.= M . (E /\ (great_eq_dom (f,(1 / (n + 1))))) by A6 ;
hence (M * F) . n = 0 by A1, A2, A3, A4, Th23; :: thesis: verum
end;
( rng F is N_Sub_set_fam of X & rng F c= S ) by ;
then reconsider T = rng F as N_Measure_fam of S by MEASURE2:def 1;
for n being Element of NAT holds F . n = E /\ (great_eq_dom (f,(0 + (1 / (n + 1))))) by A6;
then E /\ (great_dom (f,0)) = union T by MESFUNC1:22;
then M . (E /\ (great_dom (f,0))) <= SUM (M * F) by MEASURE2:11;
then M . (E /\ (great_dom (f,0))) <= 0 by ;
hence M . (E /\ (great_dom (f,0))) = 0 by SUPINF_2:51; :: thesis: verum