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 st f is_simple_func_in S & f is nonnegative holds
integral+ M,f = integral' M,f
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st f is_simple_func_in S & f is nonnegative holds
integral+ M,f = integral' M,f
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL st f is_simple_func_in S & f is nonnegative holds
integral+ M,f = integral' M,f
let f be PartFunc of X,ExtREAL ; :: thesis: ( f is_simple_func_in S & f is nonnegative implies integral+ M,f = integral' M,f )
assume A1: ( f is_simple_func_in S & f is nonnegative ) ; :: thesis: integral+ M,f = integral' M,f
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;
A2: f is_measurable_on A by A1, MESFUNC2:37;
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();
deffunc H₂( Nat) -> Element of ExtREAL = integral' M,(F . $1);
consider K being Function of NAT ,ExtREAL such that
A4: for n being Element of NAT holds K . n = H₂(n) from FUNCT_2:sch 4();

A5: now

let n be Nat; :: thesis: K . n = H₂(n)
n in NAT by ORDINAL1:def 13;
hence K . n = H₂(n) by A4; :: thesis: verum

end;

A6: for n being Nat holds
( F . n is_simple_func_in S & dom (F . n) = dom f ) by A1, A3;
A7: for n being Nat holds F . n is nonnegative by A1, A3;
A8: 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

proof

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

end;

A9: for x being Element of X st x in dom f holds
( F # x is convergent & lim (F # x) = f . x )

proof

let x be Element of X; :: thesis: ( x in dom f implies ( F # x is convergent & lim (F # x) = f . x ) )
assume x in dom f ; :: thesis: ( F # x is convergent & lim (F # x) = f . x )

now

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

end;

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

end;

for n being Nat holds K . n = integral' M,f

proof

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

end;

then ( K is convergent & lim K = integral' M,f ) by Th66;
hence integral+ M,f = integral' M,f by A1, A2, A5, A6, A7, A8, A9, Def15; :: thesis: verum