let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let f be PartFunc of X,ExtREAL; :: thesis:
let E be Element of S; :: thesis:
assume that
A1: E = dom f and
A2: f is nonnegative and
A3: f is E -measurable and
A4: Integral (M,f) = 0 ; :: thesis:
defpred S₁[ 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₁[n,y]

let n be Element of NAT ; :: thesis:
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₁[n,y] ; :: thesis:

end;

consider F being Function of NAT,S such that
A6: for n being Element of NAT holds S₁[n,F . n] from FUNCT_2:sch 3(A5);
A7: for n being Element of NAT holds (M * F) . n = 0

let n be Element of NAT ; :: thesis:
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:

end;