let X be non empty set ; :: thesis: for S being SigmaField of X

for M being sigma_Measure of S

for F being Functional_Sequence of X,ExtREAL

for E being Element of S st E = dom (F . 0) & F is with_the_same_dom & ( for n being Nat holds

( F . n is nonpositive & F . n is E -measurable ) ) holds

ex FF being sequence of (Funcs (NAT,(PFuncs (X,ExtREAL)))) st

for n being Nat holds

( ( for m being Nat holds

( (FF . n) . m is_simple_func_in S & dom ((FF . n) . m) = dom (F . n) ) ) & ( for m being Nat holds (FF . n) . m is nonpositive ) & ( for j, k being Nat st j <= k holds

for x being Element of X st x in dom (F . n) holds

((FF . n) . j) . x >= ((FF . n) . k) . x ) & ( for x being Element of X st x in dom (F . n) holds

( (FF . n) # x is convergent & lim ((FF . n) # x) = (F . n) . x ) ) )

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for F being Functional_Sequence of X,ExtREAL

for E being Element of S st E = dom (F . 0) & F is with_the_same_dom & ( for n being Nat holds

( F . n is nonpositive & F . n is E -measurable ) ) holds

ex FF being sequence of (Funcs (NAT,(PFuncs (X,ExtREAL)))) st

for n being Nat holds

( ( for m being Nat holds

( (FF . n) . m is_simple_func_in S & dom ((FF . n) . m) = dom (F . n) ) ) & ( for m being Nat holds (FF . n) . m is nonpositive ) & ( for j, k being Nat st j <= k holds

for x being Element of X st x in dom (F . n) holds

((FF . n) . j) . x >= ((FF . n) . k) . x ) & ( for x being Element of X st x in dom (F . n) holds

( (FF . n) # x is convergent & lim ((FF . n) # x) = (F . n) . x ) ) )

let M be sigma_Measure of S; :: thesis: for F being Functional_Sequence of X,ExtREAL

for E being Element of S st E = dom (F . 0) & F is with_the_same_dom & ( for n being Nat holds

( F . n is nonpositive & F . n is E -measurable ) ) holds

ex FF being sequence of (Funcs (NAT,(PFuncs (X,ExtREAL)))) st

for n being Nat holds

( ( for m being Nat holds

( (FF . n) . m is_simple_func_in S & dom ((FF . n) . m) = dom (F . n) ) ) & ( for m being Nat holds (FF . n) . m is nonpositive ) & ( for j, k being Nat st j <= k holds

for x being Element of X st x in dom (F . n) holds

((FF . n) . j) . x >= ((FF . n) . k) . x ) & ( for x being Element of X st x in dom (F . n) holds

( (FF . n) # x is convergent & lim ((FF . n) # x) = (F . n) . x ) ) )

let F be Functional_Sequence of X,ExtREAL; :: thesis: for E being Element of S st E = dom (F . 0) & F is with_the_same_dom & ( for n being Nat holds

( F . n is nonpositive & F . n is E -measurable ) ) holds

ex FF being sequence of (Funcs (NAT,(PFuncs (X,ExtREAL)))) st

for n being Nat holds

( ( for m being Nat holds

( (FF . n) . m is_simple_func_in S & dom ((FF . n) . m) = dom (F . n) ) ) & ( for m being Nat holds (FF . n) . m is nonpositive ) & ( for j, k being Nat st j <= k holds

for x being Element of X st x in dom (F . n) holds

((FF . n) . j) . x >= ((FF . n) . k) . x ) & ( for x being Element of X st x in dom (F . n) holds

( (FF . n) # x is convergent & lim ((FF . n) # x) = (F . n) . x ) ) )

let E be Element of S; :: thesis: ( E = dom (F . 0) & F is with_the_same_dom & ( for n being Nat holds

( F . n is nonpositive & F . n is E -measurable ) ) implies ex FF being sequence of (Funcs (NAT,(PFuncs (X,ExtREAL)))) st

for n being Nat holds

( ( for m being Nat holds

( (FF . n) . m is_simple_func_in S & dom ((FF . n) . m) = dom (F . n) ) ) & ( for m being Nat holds (FF . n) . m is nonpositive ) & ( for j, k being Nat st j <= k holds

for x being Element of X st x in dom (F . n) holds

((FF . n) . j) . x >= ((FF . n) . k) . x ) & ( for x being Element of X st x in dom (F . n) holds

( (FF . n) # x is convergent & lim ((FF . n) # x) = (F . n) . x ) ) ) )

assume that

A1: E = dom (F . 0) and

A2: F is with_the_same_dom and

A3: for n being Nat holds

( F . n is nonpositive & F . n is E -measurable ) ; :: thesis: ex FF being sequence of (Funcs (NAT,(PFuncs (X,ExtREAL)))) st

for n being Nat holds

( ( for m being Nat holds

( (FF . n) . m is_simple_func_in S & dom ((FF . n) . m) = dom (F . n) ) ) & ( for m being Nat holds (FF . n) . m is nonpositive ) & ( for j, k being Nat st j <= k holds

for x being Element of X st x in dom (F . n) holds

((FF . n) . j) . x >= ((FF . n) . k) . x ) & ( for x being Element of X st x in dom (F . n) holds

( (FF . n) # x is convergent & lim ((FF . n) # x) = (F . n) . x ) ) )

defpred S_{1}[ Element of NAT , set ] means for G being Functional_Sequence of X,ExtREAL st $2 = G holds

( ( for m being Nat holds

( G . m is_simple_func_in S & dom (G . m) = dom (F . $1) ) ) & ( for m being Nat holds G . m is nonpositive ) & ( for j, k being Nat st j <= k holds

for x being Element of X st x in dom (F . $1) holds

(G . j) . x >= (G . k) . x ) & ( for x being Element of X st x in dom (F . $1) holds

( G # x is convergent & lim (G # x) = (F . $1) . x ) ) );

A4: for n being Element of NAT ex G being Functional_Sequence of X,ExtREAL st

( ( for m being Nat holds

( G . m is_simple_func_in S & dom (G . m) = dom (F . n) ) ) & ( for m being Nat holds G . m is nonpositive ) & ( for j, k being Nat st j <= k holds

for x being Element of X st x in dom (F . n) holds

(G . j) . x >= (G . k) . x ) & ( for x being Element of X st x in dom (F . n) holds

( G # x is convergent & lim (G # x) = (F . n) . x ) ) )_{1}[n,G]

A12: for n being Element of NAT holds S_{1}[n,FF . n]
from FUNCT_2:sch 3(A7);

take FF ; :: thesis: for n being Nat holds

( ( for m being Nat holds

( (FF . n) . m is_simple_func_in S & dom ((FF . n) . m) = dom (F . n) ) ) & ( for m being Nat holds (FF . n) . m is nonpositive ) & ( for j, k being Nat st j <= k holds

for x being Element of X st x in dom (F . n) holds

((FF . n) . j) . x >= ((FF . n) . k) . x ) & ( for x being Element of X st x in dom (F . n) holds

( (FF . n) # x is convergent & lim ((FF . n) # x) = (F . n) . x ) ) )

thus for n being Nat holds

( ( for m being Nat holds

( (FF . n) . m is_simple_func_in S & dom ((FF . n) . m) = dom (F . n) ) ) & ( for m being Nat holds (FF . n) . m is nonpositive ) & ( for j, k being Nat st j <= k holds

for x being Element of X st x in dom (F . n) holds

((FF . n) . j) . x >= ((FF . n) . k) . x ) & ( for x being Element of X st x in dom (F . n) holds

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

for M being sigma_Measure of S

for F being Functional_Sequence of X,ExtREAL

for E being Element of S st E = dom (F . 0) & F is with_the_same_dom & ( for n being Nat holds

( F . n is nonpositive & F . n is E -measurable ) ) holds

ex FF being sequence of (Funcs (NAT,(PFuncs (X,ExtREAL)))) st

for n being Nat holds

( ( for m being Nat holds

( (FF . n) . m is_simple_func_in S & dom ((FF . n) . m) = dom (F . n) ) ) & ( for m being Nat holds (FF . n) . m is nonpositive ) & ( for j, k being Nat st j <= k holds

for x being Element of X st x in dom (F . n) holds

((FF . n) . j) . x >= ((FF . n) . k) . x ) & ( for x being Element of X st x in dom (F . n) holds

( (FF . n) # x is convergent & lim ((FF . n) # x) = (F . n) . x ) ) )

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for F being Functional_Sequence of X,ExtREAL

for E being Element of S st E = dom (F . 0) & F is with_the_same_dom & ( for n being Nat holds

( F . n is nonpositive & F . n is E -measurable ) ) holds

ex FF being sequence of (Funcs (NAT,(PFuncs (X,ExtREAL)))) st

for n being Nat holds

( ( for m being Nat holds

( (FF . n) . m is_simple_func_in S & dom ((FF . n) . m) = dom (F . n) ) ) & ( for m being Nat holds (FF . n) . m is nonpositive ) & ( for j, k being Nat st j <= k holds

for x being Element of X st x in dom (F . n) holds

((FF . n) . j) . x >= ((FF . n) . k) . x ) & ( for x being Element of X st x in dom (F . n) holds

( (FF . n) # x is convergent & lim ((FF . n) # x) = (F . n) . x ) ) )

let M be sigma_Measure of S; :: thesis: for F being Functional_Sequence of X,ExtREAL

for E being Element of S st E = dom (F . 0) & F is with_the_same_dom & ( for n being Nat holds

( F . n is nonpositive & F . n is E -measurable ) ) holds

ex FF being sequence of (Funcs (NAT,(PFuncs (X,ExtREAL)))) st

for n being Nat holds

( ( for m being Nat holds

( (FF . n) . m is_simple_func_in S & dom ((FF . n) . m) = dom (F . n) ) ) & ( for m being Nat holds (FF . n) . m is nonpositive ) & ( for j, k being Nat st j <= k holds

for x being Element of X st x in dom (F . n) holds

((FF . n) . j) . x >= ((FF . n) . k) . x ) & ( for x being Element of X st x in dom (F . n) holds

( (FF . n) # x is convergent & lim ((FF . n) # x) = (F . n) . x ) ) )

let F be Functional_Sequence of X,ExtREAL; :: thesis: for E being Element of S st E = dom (F . 0) & F is with_the_same_dom & ( for n being Nat holds

( F . n is nonpositive & F . n is E -measurable ) ) holds

ex FF being sequence of (Funcs (NAT,(PFuncs (X,ExtREAL)))) st

for n being Nat holds

( ( for m being Nat holds

( (FF . n) . m is_simple_func_in S & dom ((FF . n) . m) = dom (F . n) ) ) & ( for m being Nat holds (FF . n) . m is nonpositive ) & ( for j, k being Nat st j <= k holds

for x being Element of X st x in dom (F . n) holds

((FF . n) . j) . x >= ((FF . n) . k) . x ) & ( for x being Element of X st x in dom (F . n) holds

( (FF . n) # x is convergent & lim ((FF . n) # x) = (F . n) . x ) ) )

let E be Element of S; :: thesis: ( E = dom (F . 0) & F is with_the_same_dom & ( for n being Nat holds

( F . n is nonpositive & F . n is E -measurable ) ) implies ex FF being sequence of (Funcs (NAT,(PFuncs (X,ExtREAL)))) st

for n being Nat holds

( ( for m being Nat holds

( (FF . n) . m is_simple_func_in S & dom ((FF . n) . m) = dom (F . n) ) ) & ( for m being Nat holds (FF . n) . m is nonpositive ) & ( for j, k being Nat st j <= k holds

for x being Element of X st x in dom (F . n) holds

((FF . n) . j) . x >= ((FF . n) . k) . x ) & ( for x being Element of X st x in dom (F . n) holds

( (FF . n) # x is convergent & lim ((FF . n) # x) = (F . n) . x ) ) ) )

assume that

A1: E = dom (F . 0) and

A2: F is with_the_same_dom and

A3: for n being Nat holds

( F . n is nonpositive & F . n is E -measurable ) ; :: thesis: ex FF being sequence of (Funcs (NAT,(PFuncs (X,ExtREAL)))) st

for n being Nat holds

( ( for m being Nat holds

( (FF . n) . m is_simple_func_in S & dom ((FF . n) . m) = dom (F . n) ) ) & ( for m being Nat holds (FF . n) . m is nonpositive ) & ( for j, k being Nat st j <= k holds

for x being Element of X st x in dom (F . n) holds

((FF . n) . j) . x >= ((FF . n) . k) . x ) & ( for x being Element of X st x in dom (F . n) holds

( (FF . n) # x is convergent & lim ((FF . n) # x) = (F . n) . x ) ) )

defpred S

( ( for m being Nat holds

( G . m is_simple_func_in S & dom (G . m) = dom (F . $1) ) ) & ( for m being Nat holds G . m is nonpositive ) & ( for j, k being Nat st j <= k holds

for x being Element of X st x in dom (F . $1) holds

(G . j) . x >= (G . k) . x ) & ( for x being Element of X st x in dom (F . $1) holds

( G # x is convergent & lim (G # x) = (F . $1) . x ) ) );

A4: for n being Element of NAT ex G being Functional_Sequence of X,ExtREAL st

( ( for m being Nat holds

( G . m is_simple_func_in S & dom (G . m) = dom (F . n) ) ) & ( for m being Nat holds G . m is nonpositive ) & ( for j, k being Nat st j <= k holds

for x being Element of X st x in dom (F . n) holds

(G . j) . x >= (G . k) . x ) & ( for x being Element of X st x in dom (F . n) holds

( G # x is convergent & lim (G # x) = (F . n) . x ) ) )

proof

A7:
for n being Element of NAT ex G being Element of Funcs (NAT,(PFuncs (X,ExtREAL))) st S
let n be Element of NAT ; :: thesis: ex G being Functional_Sequence of X,ExtREAL st

( ( for m being Nat holds

( G . m is_simple_func_in S & dom (G . m) = dom (F . n) ) ) & ( for m being Nat holds G . m is nonpositive ) & ( for j, k being Nat st j <= k holds

for x being Element of X st x in dom (F . n) holds

(G . j) . x >= (G . k) . x ) & ( for x being Element of X st x in dom (F . n) holds

( G # x is convergent & lim (G # x) = (F . n) . x ) ) )

A5: F . n is E -measurable by A3;

F . n is nonpositive by A3;

hence ex G being Functional_Sequence of X,ExtREAL st

( ( for m being Nat holds

( G . m is_simple_func_in S & dom (G . m) = dom (F . n) ) ) & ( for m being Nat holds G . m is nonpositive ) & ( for j, k being Nat st j <= k holds

for x being Element of X st x in dom (F . n) holds

(G . j) . x >= (G . k) . x ) & ( for x being Element of X st x in dom (F . n) holds

( G # x is convergent & lim (G # x) = (F . n) . x ) ) ) by A1, A2, A5, Th56, MESFUNC8:def 2; :: thesis: verum

end;( ( for m being Nat holds

( G . m is_simple_func_in S & dom (G . m) = dom (F . n) ) ) & ( for m being Nat holds G . m is nonpositive ) & ( for j, k being Nat st j <= k holds

for x being Element of X st x in dom (F . n) holds

(G . j) . x >= (G . k) . x ) & ( for x being Element of X st x in dom (F . n) holds

( G # x is convergent & lim (G # x) = (F . n) . x ) ) )

A5: F . n is E -measurable by A3;

F . n is nonpositive by A3;

hence ex G being Functional_Sequence of X,ExtREAL st

( ( for m being Nat holds

( G . m is_simple_func_in S & dom (G . m) = dom (F . n) ) ) & ( for m being Nat holds G . m is nonpositive ) & ( for j, k being Nat st j <= k holds

for x being Element of X st x in dom (F . n) holds

(G . j) . x >= (G . k) . x ) & ( for x being Element of X st x in dom (F . n) holds

( G # x is convergent & lim (G # x) = (F . n) . x ) ) ) by A1, A2, A5, Th56, MESFUNC8:def 2; :: thesis: verum

proof

consider FF being sequence of (Funcs (NAT,(PFuncs (X,ExtREAL)))) such that
let n be Element of NAT ; :: thesis: ex G being Element of Funcs (NAT,(PFuncs (X,ExtREAL))) st S_{1}[n,G]

consider G being Functional_Sequence of X,ExtREAL such that

A8: for m being Nat holds

( G . m is_simple_func_in S & dom (G . m) = dom (F . n) ) and

A9: for m being Nat holds G . m is nonpositive and

A10: for j, k being Nat st j <= k holds

for x being Element of X st x in dom (F . n) holds

(G . j) . x >= (G . k) . x and

A11: for x being Element of X st x in dom (F . n) holds

( G # x is convergent & lim (G # x) = (F . n) . x ) by A4;

reconsider G = G as Element of Funcs (NAT,(PFuncs (X,ExtREAL))) by FUNCT_2:8;

take G ; :: thesis: S_{1}[n,G]

thus S_{1}[n,G]
by A8, A9, A10, A11; :: thesis: verum

end;consider G being Functional_Sequence of X,ExtREAL such that

A8: for m being Nat holds

( G . m is_simple_func_in S & dom (G . m) = dom (F . n) ) and

A9: for m being Nat holds G . m is nonpositive and

A10: for j, k being Nat st j <= k holds

for x being Element of X st x in dom (F . n) holds

(G . j) . x >= (G . k) . x and

A11: for x being Element of X st x in dom (F . n) holds

( G # x is convergent & lim (G # x) = (F . n) . x ) by A4;

reconsider G = G as Element of Funcs (NAT,(PFuncs (X,ExtREAL))) by FUNCT_2:8;

take G ; :: thesis: S

thus S

A12: for n being Element of NAT holds S

take FF ; :: thesis: for n being Nat holds

( ( for m being Nat holds

( (FF . n) . m is_simple_func_in S & dom ((FF . n) . m) = dom (F . n) ) ) & ( for m being Nat holds (FF . n) . m is nonpositive ) & ( for j, k being Nat st j <= k holds

for x being Element of X st x in dom (F . n) holds

((FF . n) . j) . x >= ((FF . n) . k) . x ) & ( for x being Element of X st x in dom (F . n) holds

( (FF . n) # x is convergent & lim ((FF . n) # x) = (F . n) . x ) ) )

thus for n being Nat holds

( ( for m being Nat holds

( (FF . n) . m is_simple_func_in S & dom ((FF . n) . m) = dom (F . n) ) ) & ( for m being Nat holds (FF . n) . m is nonpositive ) & ( for j, k being Nat st j <= k holds

for x being Element of X st x in dom (F . n) holds

((FF . n) . j) . x >= ((FF . n) . k) . x ) & ( for x being Element of X st x in dom (F . n) holds

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

proof

let n be Nat; :: thesis: ( ( for m being Nat holds

( (FF . n) . m is_simple_func_in S & dom ((FF . n) . m) = dom (F . n) ) ) & ( for m being Nat holds (FF . n) . m is nonpositive ) & ( for j, k being Nat st j <= k holds

for x being Element of X st x in dom (F . n) holds

((FF . n) . j) . x >= ((FF . n) . k) . x ) & ( for x being Element of X st x in dom (F . n) holds

( (FF . n) # x is convergent & lim ((FF . n) # x) = (F . n) . x ) ) )

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

for G being Functional_Sequence of X,ExtREAL st FF . n1 = G holds

( ( for m being Nat holds

( G . m is_simple_func_in S & dom (G . m) = dom (F . n1) ) ) & ( for m being Nat holds G . m is nonpositive ) & ( for j, k being Nat st j <= k holds

for x being Element of X st x in dom (F . n1) holds

(G . j) . x >= (G . k) . x ) & ( for x being Element of X st x in dom (F . n1) holds

( G # x is convergent & lim (G # x) = (F . n1) . x ) ) ) by A12;

hence ( ( for m being Nat holds

( (FF . n) . m is_simple_func_in S & dom ((FF . n) . m) = dom (F . n) ) ) & ( for m being Nat holds (FF . n) . m is nonpositive ) & ( for j, k being Nat st j <= k holds

for x being Element of X st x in dom (F . n) holds

((FF . n) . j) . x >= ((FF . n) . k) . x ) & ( for x being Element of X st x in dom (F . n) holds

( (FF . n) # x is convergent & lim ((FF . n) # x) = (F . n) . x ) ) ) ; :: thesis: verum

end;( (FF . n) . m is_simple_func_in S & dom ((FF . n) . m) = dom (F . n) ) ) & ( for m being Nat holds (FF . n) . m is nonpositive ) & ( for j, k being Nat st j <= k holds

for x being Element of X st x in dom (F . n) holds

((FF . n) . j) . x >= ((FF . n) . k) . x ) & ( for x being Element of X st x in dom (F . n) holds

( (FF . n) # x is convergent & lim ((FF . n) # x) = (F . n) . x ) ) )

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

for G being Functional_Sequence of X,ExtREAL st FF . n1 = G holds

( ( for m being Nat holds

( G . m is_simple_func_in S & dom (G . m) = dom (F . n1) ) ) & ( for m being Nat holds G . m is nonpositive ) & ( for j, k being Nat st j <= k holds

for x being Element of X st x in dom (F . n1) holds

(G . j) . x >= (G . k) . x ) & ( for x being Element of X st x in dom (F . n1) holds

( G # x is convergent & lim (G # x) = (F . n1) . x ) ) ) by A12;

hence ( ( for m being Nat holds

( (FF . n) . m is_simple_func_in S & dom ((FF . n) . m) = dom (F . n) ) ) & ( for m being Nat holds (FF . n) . m is nonpositive ) & ( for j, k being Nat st j <= k holds

for x being Element of X st x in dom (F . n) holds

((FF . n) . j) . x >= ((FF . n) . k) . x ) & ( for x being Element of X st x in dom (F . n) holds

( (FF . n) # x is convergent & lim ((FF . n) # x) = (F . n) . x ) ) ) ; :: thesis: verum