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