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 S_{1}[ 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 S_{1}[n,y]

A6: for n being Element of NAT holds S_{1}[n,F . n]
from FUNCT_2:sch 3(A5);

A7: for n being Element of NAT holds (M * F) . n = 0

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 A7, MEASURE7:1;

hence M . (E /\ (great_dom (f,0))) = 0 by SUPINF_2:51; :: thesis: verum

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 S

A5: for n being Element of NAT ex y being Element of S st S

proof

consider F being Function of NAT,S such that
let n be Element of NAT ; :: thesis: ex y being Element of S st S_{1}[n,y]

E /\ (great_eq_dom (f,(1 / (n + 1)))) is Element of S by A1, A3, MESFUNC1:27;

hence ex y being Element of S st S_{1}[n,y]
; :: thesis: verum

end;E /\ (great_eq_dom (f,(1 / (n + 1)))) is Element of S by A1, A3, MESFUNC1:27;

hence ex y being Element of S st S

A6: for n being Element of NAT holds S

A7: for n being Element of NAT holds (M * F) . n = 0

proof

( rng F is N_Sub_set_fam of X & rng F c= S )
by MEASURE1:23, RELAT_1:def 19;
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;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

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 A7, MEASURE7:1;

hence M . (E /\ (great_dom (f,0))) = 0 by SUPINF_2:51; :: thesis: verum