let X be non empty set ; :: thesis: for S being SigmaField of X
for E being Element of S
for F being Functional_Sequence of X,ExtREAL st E = dom (F . 0) & F is with_the_same_dom & ( for n being Nat holds
( F . n is nonnegative & 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 nonnegative ) & ( 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 E being Element of S
for F being Functional_Sequence of X,ExtREAL st E = dom (F . 0) & F is with_the_same_dom & ( for n being Nat holds
( F . n is nonnegative & 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 nonnegative ) & ( 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: for F being Functional_Sequence of X,ExtREAL st E = dom (F . 0) & F is with_the_same_dom & ( for n being Nat holds
( F . n is nonnegative & 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 nonnegative ) & ( 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: ( E = dom (F . 0) & F is with_the_same_dom & ( for n being Nat holds
( F . n is nonnegative & 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 nonnegative ) & ( 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 nonnegative & 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 nonnegative ) & ( 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₁[ 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 nonnegative ) & ( 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 nonnegative ) & ( 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

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 nonnegative ) & ( 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;
A6: F . n is nonnegative by A3;
E = dom (F . n) by A1, A2;
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 nonnegative ) & ( 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 A5, A6, MESFUNC5:64; :: thesis: verum

end;

A7: for n being Element of NAT ex G being Element of Funcs (NAT,(PFuncs (X,ExtREAL))) st S₁[n,G]

proof

let n be Element of NAT ; :: thesis: ex G being Element of Funcs (NAT,(PFuncs (X,ExtREAL))) st S₁[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 nonnegative 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₁[n,G]
thus S₁[n,G] by A8, A9, A10, A11; :: thesis: verum

end;

consider FF being sequence of (Funcs (NAT,(PFuncs (X,ExtREAL)))) such that
A12: for n being Element of NAT holds S₁[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 nonnegative ) & ( 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 nonnegative ) & ( 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 nonnegative ) & ( 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 nonnegative ) & ( 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 nonnegative ) & ( 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;