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 that

A1: f is_simple_func_in S and

A2: f is nonnegative ; :: thesis: integral+ (M,f) = integral' (M,f)

deffunc H_{1}( 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_{1}(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_{2}( Nat) -> Element of ExtREAL = integral' (M,(F . $1));

consider K being sequence of ExtREAL such that

A5: for n being Element of NAT holds K . n = H_{2}(n)
from FUNCT_2:sch 4();

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 4;

then reconsider A = dom f as Element of S by MESFUNC2:31;

A9: f is A -measurable by A1, MESFUNC2:34;

A10: for x being Element of X st x in dom f holds

( F # x is convergent & lim (F # x) = f . x )

A12: for n being Nat holds

( F . n is_simple_func_in S & dom (F . n) = dom f ) by A1, A3;

K is convergent by A7, Th60;

hence integral+ (M,f) = integral' (M,f) by A2, A9, A6, A12, A11, A4, A10, A8, Def15; :: thesis: verum

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 that

A1: f is_simple_func_in S and

A2: f is nonnegative ; :: thesis: integral+ (M,f) = integral' (M,f)

deffunc H

consider F being Functional_Sequence of X,ExtREAL such that

A3: for n being Nat holds F . n = H

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

proof

deffunc H
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;(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

consider K being sequence of ExtREAL such that

A5: for n being Element of NAT holds K . n = H

A6: now :: thesis: for n being Nat holds K . n = H_{2}(n)

A7:
for n being Nat holds K . n = integral' (M,f)
let n be Nat; :: thesis: K . n = H_{2}(n)

n in NAT by ORDINAL1:def 12;

hence K . n = H_{2}(n)
by A5; :: thesis: verum

end;n in NAT by ORDINAL1:def 12;

hence K . n = H

proof

then A8:
lim K = integral' (M,f)
by Th60;
let n be Nat; :: thesis: K . n = integral' (M,f)

thus K . n = integral' (M,(F . n)) by A6

.= integral' (M,f) by A3 ; :: thesis: verum

end;thus K . n = integral' (M,(F . n)) by A6

.= integral' (M,f) by A3 ; :: thesis: verum

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 4;

then reconsider A = dom f as Element of S by MESFUNC2:31;

A9: f is A -measurable by A1, MESFUNC2:34;

A10: for x being Element of X st x in dom f holds

( F # x is convergent & lim (F # x) = f . x )

proof

A11:
for n being Nat holds F . n is nonnegative
by A2, A3;
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 )

end;assume x in dom f ; :: thesis: ( F # x is convergent & lim (F # x) = f . x )

now :: thesis: for n being Nat holds (F # x) . n = f . x

hence
( F # x is convergent & lim (F # x) = f . x )
by Th60; :: thesis: verumlet 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;thus (F # x) . n = (F . n) . x by Def13

.= f . x by A3 ; :: thesis: verum

A12: for n being Nat holds

( F . n is_simple_func_in S & dom (F . n) = dom f ) by A1, A3;

K is convergent by A7, Th60;

hence integral+ (M,f) = integral' (M,f) by A2, A9, A6, A12, A11, A4, A10, A8, Def15; :: thesis: verum