let X be non empty set ; 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; 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; 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; 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; ( 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 )
; 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 S1[ 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 ) ) )
A7:
for n being Element of NAT ex G being Element of Funcs (NAT,(PFuncs (X,ExtREAL))) st S1[n,G]
proof
let n be
Element of
NAT ;
ex G being Element of Funcs (NAT,(PFuncs (X,ExtREAL))) st S1[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
;
S1[n,G]
thus
S1[
n,
G]
by A8, A9, A10, A11;
verum
end;
consider FF being sequence of (Funcs (NAT,(PFuncs (X,ExtREAL)))) such that
A12:
for n being Element of NAT holds S1[n,FF . n]
from FUNCT_2:sch 3(A7);
take
FF
; 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 ) ) )
verum