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) )
proof
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) )
A10: now :: thesis: for n, m being Nat st n <= m holds
(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;
A13: g . x = (F # x) . 0 by Def13;
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;
dom g = dom f by A3;
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