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

for n being Nat st E = dom f & f is nonnegative & f is E -measurable & Integral (M,f) = 0 holds

M . (E /\ (great_eq_dom (f,(1 / (n + 1))))) = 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

for n being Nat st E = dom f & f is nonnegative & f is E -measurable & Integral (M,f) = 0 holds

M . (E /\ (great_eq_dom (f,(1 / (n + 1))))) = 0

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL

for E being Element of S

for n being Nat st E = dom f & f is nonnegative & f is E -measurable & Integral (M,f) = 0 holds

M . (E /\ (great_eq_dom (f,(1 / (n + 1))))) = 0

let f be PartFunc of X,ExtREAL; :: thesis: for E being Element of S

for n being Nat st E = dom f & f is nonnegative & f is E -measurable & Integral (M,f) = 0 holds

M . (E /\ (great_eq_dom (f,(1 / (n + 1))))) = 0

let E be Element of S; :: thesis: for n being Nat st E = dom f & f is nonnegative & f is E -measurable & Integral (M,f) = 0 holds

M . (E /\ (great_eq_dom (f,(1 / (n + 1))))) = 0

let n be Nat; :: thesis: ( E = dom f & f is nonnegative & f is E -measurable & Integral (M,f) = 0 implies M . (E /\ (great_eq_dom (f,(1 / (n + 1))))) = 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_eq_dom (f,(1 / (n + 1))))) = 0

assume A5: M . (E /\ (great_eq_dom (f,(1 / (n + 1))))) <> 0 ; :: thesis: contradiction

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

then A6: M . (E /\ (great_eq_dom (f,(1 / (n + 1))))) > 0 by A5, MEASURE1:def 2;

great_eq_dom (f,(1 / (n + 1))) c= E by A1, MESFUNC1:def 14;

then A7: M . (great_eq_dom (f,(1 / (n + 1)))) > 0 by A6, XBOOLE_1:28;

1 / (n + 1) > 0 by XREAL_1:139;

then (1 / (n + 1)) * (M . (great_eq_dom (f,(1 / (n + 1))))) > 0 by A7;

hence contradiction by A3, A1, A2, A4, MESFUN13:16; :: thesis: verum

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for E being Element of S

for n being Nat st E = dom f & f is nonnegative & f is E -measurable & Integral (M,f) = 0 holds

M . (E /\ (great_eq_dom (f,(1 / (n + 1))))) = 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

for n being Nat st E = dom f & f is nonnegative & f is E -measurable & Integral (M,f) = 0 holds

M . (E /\ (great_eq_dom (f,(1 / (n + 1))))) = 0

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL

for E being Element of S

for n being Nat st E = dom f & f is nonnegative & f is E -measurable & Integral (M,f) = 0 holds

M . (E /\ (great_eq_dom (f,(1 / (n + 1))))) = 0

let f be PartFunc of X,ExtREAL; :: thesis: for E being Element of S

for n being Nat st E = dom f & f is nonnegative & f is E -measurable & Integral (M,f) = 0 holds

M . (E /\ (great_eq_dom (f,(1 / (n + 1))))) = 0

let E be Element of S; :: thesis: for n being Nat st E = dom f & f is nonnegative & f is E -measurable & Integral (M,f) = 0 holds

M . (E /\ (great_eq_dom (f,(1 / (n + 1))))) = 0

let n be Nat; :: thesis: ( E = dom f & f is nonnegative & f is E -measurable & Integral (M,f) = 0 implies M . (E /\ (great_eq_dom (f,(1 / (n + 1))))) = 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_eq_dom (f,(1 / (n + 1))))) = 0

assume A5: M . (E /\ (great_eq_dom (f,(1 / (n + 1))))) <> 0 ; :: thesis: contradiction

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

then A6: M . (E /\ (great_eq_dom (f,(1 / (n + 1))))) > 0 by A5, MEASURE1:def 2;

great_eq_dom (f,(1 / (n + 1))) c= E by A1, MESFUNC1:def 14;

then A7: M . (great_eq_dom (f,(1 / (n + 1)))) > 0 by A6, XBOOLE_1:28;

1 / (n + 1) > 0 by XREAL_1:139;

then (1 / (n + 1)) * (M . (great_eq_dom (f,(1 / (n + 1))))) > 0 by A7;

hence contradiction by A3, A1, A2, A4, MESFUN13:16; :: thesis: verum