let X be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 )

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; :: thesis: verum

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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 )

proof

let x be Element of X; :: thesis: for k being Nat st x in E holds

( - (P . x) <= (F # x) . k & (F # x) . k <= P . x )

let k be Nat; :: thesis: ( x in E implies ( - (P . x) <= (F # x) . k & (F # x) . k <= P . x ) )

assume A9: x in E ; :: thesis: ( - (P . x) <= (F # x) . k & (F # x) . k <= P . x )

then x in dom (F . k) by A1, MESFUNC8:def 2;

then A10: x in dom |.(F . k).| by MESFUNC1:def 10;

|.(F . k).| . x <= P . x by A5, A9;

then |.((F . k) . x).| <= P . x by A10, MESFUNC1:def 10;

then ( - (P . x) <= (F . k) . x & (F . k) . x <= P . x ) by EXTREAL1:23;

hence ( - (P . x) <= (F # x) . k & (F # x) . k <= P . x ) by MESFUNC5:def 13; :: thesis: verum

end;( - (P . x) <= (F # x) . k & (F # x) . k <= P . x )

let k be Nat; :: thesis: ( x in E implies ( - (P . x) <= (F # x) . k & (F # x) . k <= P . x ) )

assume A9: x in E ; :: thesis: ( - (P . x) <= (F # x) . k & (F # x) . k <= P . x )

then x in dom (F . k) by A1, MESFUNC8:def 2;

then A10: x in dom |.(F . k).| by MESFUNC1:def 10;

|.(F . k).| . x <= P . x by A5, A9;

then |.((F . k) . x).| <= P . x by A10, MESFUNC1:def 10;

then ( - (P . x) <= (F . k) . x & (F . k) . x <= P . x ) by EXTREAL1:23;

hence ( - (P . x) <= (F # x) . k & (F # x) . k <= P . x ) by MESFUNC5:def 13; :: thesis: verum

A11: now :: thesis: for x being Element of X st x in dom (lim_sup F) holds

|.((lim_sup F) . x).| <= P . x

|.((lim_sup F) . x).| <= P . x

let x be Element of X; :: thesis: ( x in dom (lim_sup F) implies |.((lim_sup F) . x).| <= P . x )

assume A12: x in dom (lim_sup F) ; :: thesis: |.((lim_sup F) . x).| <= P . x

for k being Nat holds (superior_realsequence (F # x)) . k >= - (P . x)

then A14: (lim_sup F) . x >= - (P . x) by A12, MESFUNC8:def 8;

then P . x >= sup (rng (F # x)) by XXREAL_2:def 3;

then P . x >= sup ((F # x) ^\ 0) by NAT_1:47;

then A15: P . x >= (superior_realsequence (F # x)) . 0 by RINFSUP2:27;

(superior_realsequence (F # x)) . 0 >= inf (superior_realsequence (F # x)) by RINFSUP2:23;

then P . x >= lim_sup (F # x) by A15, XXREAL_0:2;

then P . x >= (lim_sup F) . x by A12, MESFUNC8:def 8;

hence |.((lim_sup F) . x).| <= P . x by A14, EXTREAL1:23; :: thesis: verum

end;assume A12: x in dom (lim_sup F) ; :: thesis: |.((lim_sup F) . x).| <= P . x

for k being Nat holds (superior_realsequence (F # x)) . k >= - (P . x)

proof

then
lim_sup (F # x) >= - (P . x)
by MESFUN10:4;
let k be Nat; :: thesis: (superior_realsequence (F # x)) . k >= - (P . x)

A13: (superior_realsequence (F # x)) . k >= (F # x) . k by RINFSUP2:8;

(F # x) . k >= - (P . x) by A7, A8, A12;

hence (superior_realsequence (F # x)) . k >= - (P . x) by A13, XXREAL_0:2; :: thesis: verum

end;A13: (superior_realsequence (F # x)) . k >= (F # x) . k by RINFSUP2:8;

(F # x) . k >= - (P . x) by A7, A8, A12;

hence (superior_realsequence (F # x)) . k >= - (P . x) by A13, XXREAL_0:2; :: thesis: verum

then A14: (lim_sup F) . x >= - (P . x) by A12, MESFUNC8:def 8;

now :: thesis: for y being ExtReal st y in rng (F # x) holds

P . x >= y

then
P . x is UpperBound of rng (F # x)
by XXREAL_2:def 1;P . x >= y

let y be ExtReal; :: thesis: ( y in rng (F # x) implies P . x >= y )

assume y in rng (F # x) ; :: thesis: P . x >= y

then ex k being object st

( k in dom (F # x) & y = (F # x) . k ) by FUNCT_1:def 3;

hence P . x >= y by A7, A8, A12; :: thesis: verum

end;assume y in rng (F # x) ; :: thesis: P . x >= y

then ex k being object st

( k in dom (F # x) & y = (F # x) . k ) by FUNCT_1:def 3;

hence P . x >= y by A7, A8, A12; :: thesis: verum

then P . x >= sup (rng (F # x)) by XXREAL_2:def 3;

then P . x >= sup ((F # x) ^\ 0) by NAT_1:47;

then A15: P . x >= (superior_realsequence (F # x)) . 0 by RINFSUP2:27;

(superior_realsequence (F # x)) . 0 >= inf (superior_realsequence (F # x)) by RINFSUP2:23;

then P . x >= lim_sup (F # x) by A15, XXREAL_0:2;

then P . x >= (lim_sup F) . x by A12, MESFUNC8:def 8;

hence |.((lim_sup F) . x).| <= P . x by A14, EXTREAL1:23; :: thesis: verum

A16: now :: thesis: for x being Element of X st x in dom (lim F) holds

(lim F) . x = (lim_sup F) . x

A18:
lim_sup F is E -measurable
by A1, A3, MESFUNC8:23;(lim F) . x = (lim_sup F) . x

let x be Element of X; :: thesis: ( x in dom (lim F) implies (lim F) . x = (lim_sup F) . x )

assume A17: x in dom (lim F) ; :: thesis: (lim F) . x = (lim_sup F) . x

then x in E by A1, MESFUNC8:def 9;

then F # x is convergent by A6;

hence (lim F) . x = (lim_sup F) . x by A17, MESFUNC8:14; :: thesis: verum

end;assume A17: x in dom (lim F) ; :: thesis: (lim F) . x = (lim_sup F) . x

then x in E by A1, MESFUNC8:def 9;

then F # x is convergent by A6;

hence (lim F) . x = (lim_sup F) . x by A17, MESFUNC8:14; :: thesis: verum

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; :: thesis: verum