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:
assume that
A1: f is_simple_func_in S and
A2: f is nonnegative ; :: thesis:
deffunc H₁( Nat) -> PartFunc of X,ExtREAL = f;
consider F being Functional_Sequence of X,ExtREAL such that
A3: for n being Nat holds F . n = H₁(n) from SEQFUNC:sch 1();
A4: for n, m being Nat st n <= m holds
for x being Element of X st x in dom f holds
(F . n) . x <= (F . m) . x

let n, m be Nat; :: thesis:
assume n <= m ; :: thesis:
let x be Element of X; :: thesis:
assume x in dom f ; :: thesis:
(F . n) . x = f . x by A3;
hence (F . n) . x <= (F . m) . x by A3; :: thesis:

end;

deffunc H₂( Nat) -> Element of ExtREAL = integral' M,(F . $1);
consider K being Function of NAT ,ExtREAL such that
A5: for n being Element of NAT holds K . n = H₂(n) from FUNCT_2:sch 4();

end;

let n be Nat; :: thesis:
thus K . n = integral' M,(F . n) by A6
.= integral' M,f by A3 ; :: thesis:

end;

then A8: lim K = integral' M,f by Th66;
ex GF being Finite_Sep_Sequence of S st
( dom f = union (rng GF) & ( for n being Nat
for x, y being Element of X st n in dom GF & x in GF . n & y in GF . n holds
f . x = f . y ) ) by A1, MESFUNC2:def 5;
then reconsider A = dom f as Element of S by MESFUNC2:34;
A9: f is_measurable_on A by A1, MESFUNC2:37;
A10: for x being Element of X st x in dom f holds
( F # x is convergent & lim (F # x) = f . x )

let x be Element of X; :: thesis:
assume x in dom f ; :: thesis:

let n be Nat; :: thesis:
thus (F # x) . n = (F . n) . x by Def13
.= f . x by A3 ; :: thesis:

end;

hence ( F # x is convergent & lim (F # x) = f . x ) by Th66; :: thesis:

end;