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 ) ) )

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 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 )

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

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

thus
for n being Nat holds F . n is nonpositive
:: thesis: ( ( for n, m being Nat st n <= m holds
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;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

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

thus
for n, m being Nat st n <= m holds
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;A12: G . n is nonnegative by A6;

F . n = - (G . n) by Th37;

hence F . n is nonpositive by A12; :: thesis: verum

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

thus
for x being Element of X st x in dom f holds
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;(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

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