consider F being Functional_Sequence of X,ExtREAL such that

A3: for n being Nat holds

( F . n is_simple_func_in S & dom (F . n) = dom f ) and

A4: for n being Nat holds F . n is nonnegative and

A5: 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 and

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

( F # x is convergent & lim (F # x) = f . x ) by A1, A2, Th64;

reconsider g = F . 0 as PartFunc of X,ExtREAL ;

A7: g is_simple_func_in S by A3;

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

( F # x is convergent & g . x <= lim (F # x) )

then ex G being ExtREAL_sequence st

( ( for n being Nat holds G . n = integral' (M,(F . n)) ) & G is convergent & sup (rng G) = lim G & integral' (M,g) <= lim G ) by A3, A4, A5, A8, A7, Th75;

then consider G being ExtREAL_sequence such that

A14: for n being Nat holds G . n = integral' (M,(F . n)) and

A15: G is convergent and

integral' (M,g) <= lim G ;

take lim G ; :: thesis: ex F being Functional_Sequence of X,ExtREAL ex K being ExtREAL_sequence st

( ( for n being Nat holds

( F . n is_simple_func_in S & dom (F . n) = dom f ) ) & ( for n being Nat holds F . n is nonnegative ) & ( 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 ) & ( for x being Element of X st x in dom f holds

( F # x is convergent & lim (F # x) = f . x ) ) & ( for n being Nat holds K . n = integral' (M,(F . n)) ) & K is convergent & lim G = lim K )

thus ex F being Functional_Sequence of X,ExtREAL ex K being ExtREAL_sequence st

( ( for n being Nat holds

( F . n is_simple_func_in S & dom (F . n) = dom f ) ) & ( for n being Nat holds F . n is nonnegative ) & ( 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 ) & ( for x being Element of X st x in dom f holds

( F # x is convergent & lim (F # x) = f . x ) ) & ( for n being Nat holds K . n = integral' (M,(F . n)) ) & K is convergent & lim G = lim K ) by A3, A4, A5, A6, A14, A15; :: thesis: verum

A3: for n being Nat holds

( F . n is_simple_func_in S & dom (F . n) = dom f ) and

A4: for n being Nat holds F . n is nonnegative and

A5: 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 and

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

( F # x is convergent & lim (F # x) = f . x ) by A1, A2, Th64;

reconsider g = F . 0 as PartFunc of X,ExtREAL ;

A7: g is_simple_func_in S by A3;

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

( F # x is convergent & g . x <= lim (F # x) )

proof

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

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

lim (F # x) = sup (rng (F # x)) by A10, Th54;

hence ( F # x is convergent & g . x <= lim (F # x) ) by A10, A13, Th54, Th56; :: thesis: verum

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

A10: now :: thesis: for n, m being Nat st n <= m holds

(F # x) . n <= (F # x) . m

A13:
g . x = (F # x) . 0
by Def13;(F # x) . n <= (F # x) . m

let n, m be Nat; :: thesis: ( n <= m implies (F # x) . n <= (F # x) . m )

assume A11: n <= m ; :: thesis: (F # x) . n <= (F # x) . m

A12: (F # x) . m = (F . m) . x by Def13;

(F # x) . n = (F . n) . x by Def13;

hence (F # x) . n <= (F # x) . m by A5, A9, A11, A12; :: thesis: verum

end;assume A11: n <= m ; :: thesis: (F # x) . n <= (F # x) . m

A12: (F # x) . m = (F . m) . x by Def13;

(F # x) . n = (F . n) . x by Def13;

hence (F # x) . n <= (F # x) . m by A5, A9, A11, A12; :: thesis: verum

lim (F # x) = sup (rng (F # x)) by A10, Th54;

hence ( F # x is convergent & g . x <= lim (F # x) ) by A10, A13, Th54, Th56; :: thesis: verum

then ex G being ExtREAL_sequence st

( ( for n being Nat holds G . n = integral' (M,(F . n)) ) & G is convergent & sup (rng G) = lim G & integral' (M,g) <= lim G ) by A3, A4, A5, A8, A7, Th75;

then consider G being ExtREAL_sequence such that

A14: for n being Nat holds G . n = integral' (M,(F . n)) and

A15: G is convergent and

integral' (M,g) <= lim G ;

take lim G ; :: thesis: ex F being Functional_Sequence of X,ExtREAL ex K being ExtREAL_sequence st

( ( for n being Nat holds

( F . n is_simple_func_in S & dom (F . n) = dom f ) ) & ( for n being Nat holds F . n is nonnegative ) & ( 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 ) & ( for x being Element of X st x in dom f holds

( F # x is convergent & lim (F # x) = f . x ) ) & ( for n being Nat holds K . n = integral' (M,(F . n)) ) & K is convergent & lim G = lim K )

thus ex F being Functional_Sequence of X,ExtREAL ex K being ExtREAL_sequence st

( ( for n being Nat holds

( F . n is_simple_func_in S & dom (F . n) = dom f ) ) & ( for n being Nat holds F . n is nonnegative ) & ( 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 ) & ( for x being Element of X st x in dom f holds

( F # x is convergent & lim (F # x) = f . x ) ) & ( for n being Nat holds K . n = integral' (M,(F . n)) ) & K is convergent & lim G = lim K ) by A3, A4, A5, A6, A14, A15; :: thesis: verum