let X be non empty set ; for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for F being with_the_same_dom Functional_Sequence of X,ExtREAL
for P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) & ( for x being Element of X st x in E holds
F # x is convergent ) holds
lim F is_integrable_on M
let S be SigmaField of X; for M being sigma_Measure of S
for E being Element of S
for F being with_the_same_dom Functional_Sequence of X,ExtREAL
for P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) & ( for x being Element of X st x in E holds
F # x is convergent ) holds
lim F is_integrable_on M
let M be sigma_Measure of S; for E being Element of S
for F being with_the_same_dom Functional_Sequence of X,ExtREAL
for P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) & ( for x being Element of X st x in E holds
F # x is convergent ) holds
lim F is_integrable_on M
let E be Element of S; for F being with_the_same_dom Functional_Sequence of X,ExtREAL
for P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) & ( for x being Element of X st x in E holds
F # x is convergent ) holds
lim F is_integrable_on M
let F be with_the_same_dom Functional_Sequence of X,ExtREAL; for P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) & ( for x being Element of X st x in E holds
F # x is convergent ) holds
lim F is_integrable_on M
let P be PartFunc of X,ExtREAL; ( E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) & ( for x being Element of X st x in E holds
F # x is convergent ) implies lim F is_integrable_on M )
assume that
A1:
E = dom (F . 0)
and
A2:
E = dom P
and
A3:
for n being Nat holds F . n is E -measurable
and
A4:
P is_integrable_on M
and
A5:
for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x
and
A6:
for x being Element of X st x in E holds
F # x is convergent
; lim F is_integrable_on M
A7:
E = dom (lim_sup F)
by A1, MESFUNC8:def 8;
A8:
for x being Element of X
for k being Nat st x in E holds
( - (P . x) <= (F # x) . k & (F # x) . k <= P . x )
A18:
lim_sup F is E -measurable
by A1, A3, MESFUNC8:23;
E = dom (lim F)
by A1, MESFUNC8:def 9;
then
lim F = lim_sup F
by A7, A16, PARTFUN1:5;
hence
lim F is_integrable_on M
by A2, A4, A7, A18, A11, MESFUNC5:102; verum