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_measurable_on E ) ) holds
ex FF being Function of NAT ,(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_measurable_on E ) ) holds
ex FF being Function of NAT ,(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_measurable_on E ) ) holds
ex FF being Function of NAT ,(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_measurable_on E ) ) implies ex FF being Function of NAT ,(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
A3: F is with_the_same_dom and
A2: for n being Nat holds
( F . n is nonnegative & F . n is_measurable_on E ) ; :: thesis: ex FF being Function of NAT ,(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 ) ) )
X1: 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 ) ) )
( E = dom (F . n) & F . n is_measurable_on E & F . n is nonnegative ) by A1, A2, A3, MESFUNC8:def 2;
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 MESFUNC5:70; :: thesis: verum

end;

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 ) ) );
X2: 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
X21: ( ( 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 X1;
reconsider G = G as Element of Funcs NAT ,(PFuncs X,ExtREAL ) by FUNCT_2:11;
take G ; :: thesis: S₁[n,G]
thus S₁[n,G] by X21; :: thesis: verum

end;

consider FF being Function of NAT ,(Funcs NAT ,(PFuncs X,ExtREAL )) such that
XX: for n being Element of NAT holds S₁[n,FF . n] from FUNCT_2:sch 3(X2);
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 13;
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 XX;
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;