let X be non empty set ; :: thesis: for S being SigmaField of X
for f being PartFunc of X,ExtREAL st ex A being Element of S st
( A = dom f & f is A -measurable ) & f is nonpositive holds
ex F being Functional_Sequence of X,ExtREAL 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 nonpositive ) & ( 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 ) ) )
let S be SigmaField of X; :: thesis: for f being PartFunc of X,ExtREAL st ex A being Element of S st
( A = dom f & f is A -measurable ) & f is nonpositive holds
ex F being Functional_Sequence of X,ExtREAL 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 nonpositive ) & ( 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 ) ) )
let f be PartFunc of X,ExtREAL; :: thesis: ( ex A being Element of S st
( A = dom f & f is A -measurable ) & f is nonpositive implies ex F being Functional_Sequence of X,ExtREAL 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 nonpositive ) & ( 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 ) ) ) )
assume that
A1: ex A being Element of S st
( A = dom f & f is A -measurable ) and
A2: f is nonpositive ; :: thesis: ex F being Functional_Sequence of X,ExtREAL 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 nonpositive ) & ( 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 ) ) )
set g = - f;
consider A being Element of S such that
A3: ( A = dom f & f is A -measurable ) by A1;
A4: A = dom (- f) by A3, MESFUNC1:def 7;
then consider G being Functional_Sequence of X,ExtREAL such that
A6: ( ( for n being Nat holds
( G . n is_simple_func_in S & dom (G . n) = dom (- f) ) ) & ( for n being Nat holds G . n is nonnegative ) & ( for n, m being Nat st n <= m holds
for x being Element of X st x in dom (- f) holds
(G . n) . x <= (G . m) . x ) & ( for x being Element of X st x in dom (- f) holds
( G # x is convergent & lim (G # x) = (- f) . x ) ) ) by A2, A3, MEASUR11:63, MESFUNC5:64;
take F = - G; :: thesis: ( ( 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 nonpositive ) & ( 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 ) ) )
thus A8: for n being Nat holds
( F . n is_simple_func_in S & dom (F . n) = dom f ) :: thesis: ( ( for n being Nat holds F . n is nonpositive ) & ( 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 ) ) )

proof

let n be Nat; :: thesis: ( F . n is_simple_func_in S & dom (F . n) = dom f )
A9: dom (G . n) = dom (- f) by A6;
A10: F . n = - (G . n) by Th37;
hence F . n is_simple_func_in S by A6, Th30; :: thesis: dom (F . n) = dom f
thus dom (F . n) = dom f by A3, A4, A9, A10, MESFUNC1:def 7; :: thesis: verum

end;

thus for n being Nat holds F . n is nonpositive :: thesis: ( ( 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 ) ) )

proof

let n be Nat; :: thesis: F . n is nonpositive
A12: G . n is nonnegative by A6;
F . n = - (G . n) by Th37;
hence F . n is nonpositive by A12; :: thesis: verum

end;

thus 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 :: thesis: for x being Element of X st x in dom f holds
( F # x is convergent & lim (F # x) = f . 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 A14: 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 A15: x in dom f ; :: thesis: (F . n) . x >= (F . m) . x
( dom (F . n) = dom f & F . n = - (G . n) & dom (F . m) = dom f & F . m = - (G . m) ) by A8, Th37;
then ( (F . n) . x = - ((G . n) . x) & (F . m) . x = - ((G . m) . x) ) by A15, MESFUNC1:def 7;
hence (F . n) . x >= (F . m) . x by A15, A3, A4, A6, A14, XXREAL_3:38; :: thesis: verum

end;

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

proof

let x be Element of X; :: thesis: ( x in dom f implies ( F # x is convergent & lim (F # x) = f . x ) )
assume A17: x in dom f ; :: thesis: ( F # x is convergent & lim (F # x) = f . x )
then A18: ( G # x is convergent & lim (G # x) = (- f) . x ) by A3, A4, A6;
hence F # x is convergent by Th39; :: thesis: lim (F # x) = f . x
lim (F # x) = - ((- f) . x) by A18, Th39;
then lim (F # x) = - (- (f . x)) by A3, A4, A17, MESFUNC1:def 7;
hence lim (F # x) = f . x ; :: thesis: verum

end;