let X be non empty set ; :: thesis: for F being with_the_same_dom Functional_Sequence of X,ExtREAL
for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
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 ) holds
( ( for n being Nat holds |.(F . n).| is_integrable_on M ) & |.(lim_inf F).| is_integrable_on M & |.(lim_sup F).| is_integrable_on M )
let F be with_the_same_dom Functional_Sequence of X,ExtREAL; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
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 ) holds
( ( for n being Nat holds |.(F . n).| is_integrable_on M ) & |.(lim_inf F).| is_integrable_on M & |.(lim_sup 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 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 ) holds
( ( for n being Nat holds |.(F . n).| is_integrable_on M ) & |.(lim_inf F).| is_integrable_on M & |.(lim_sup F).| is_integrable_on M )
let M be sigma_Measure of S; :: thesis: for E being Element of S
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 ) holds
( ( for n being Nat holds |.(F . n).| is_integrable_on M ) & |.(lim_inf F).| is_integrable_on M & |.(lim_sup F).| is_integrable_on M )
let E be Element of S; :: 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 ) holds
( ( for n being Nat holds |.(F . n).| is_integrable_on M ) & |.(lim_inf F).| is_integrable_on M & |.(lim_sup 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 ) implies ( ( for n being Nat holds |.(F . n).| is_integrable_on M ) & |.(lim_inf F).| is_integrable_on M & |.(lim_sup 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 ; :: thesis: ( ( for n being Nat holds |.(F . n).| is_integrable_on M ) & |.(lim_inf F).| is_integrable_on M & |.(lim_sup F).| is_integrable_on M )
A6: lim_inf F is E -measurable by A1, A3, MESFUNC8:24;

hereby :: thesis: ( |.(lim_inf F).| is_integrable_on M & |.(lim_sup F).| is_integrable_on M )

let n be Nat; :: thesis: |.(F . n).| is_integrable_on M
A7: F . n is E -measurable by A3;
A8: E = dom (F . n) by A1, MESFUNC8:def 2;

now :: thesis: for x being Element of X st x in dom (F . n) holds
|.((F . n) . x).| <= P . x

let x be Element of X; :: thesis: ( x in dom (F . n) implies |.((F . n) . x).| <= P . x )
assume A9: x in dom (F . n) ; :: thesis: |.((F . n) . x).| <= P . x
then A10: x in dom |.(F . n).| by MESFUNC1:def 10;
|.(F . n).| . x <= P . x by A5, A8, A9;
hence |.((F . n) . x).| <= P . x by A10, MESFUNC1:def 10; :: thesis: verum

end;

then F . n is_integrable_on M by A2, A4, A8, A7, MESFUNC5:102;
hence |.(F . n).| is_integrable_on M by MESFUNC5:100; :: thesis: verum

end;

A11: E = dom (lim_inf F) by A1, MESFUNC8:def 7;
A12: lim_sup F is E -measurable by A1, A3, MESFUNC8:23;
A13: 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 A14: 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 A15: x in dom |.(F . k).| by MESFUNC1:def 10;
|.(F . k).| . x <= P . x by A5, A14;
then A16: |.((F . k) . x).| <= P . x by A15, MESFUNC1:def 10;
then A17: (F . k) . x <= P . x by EXTREAL1:23;
- (P . x) <= (F . k) . x by A16, EXTREAL1:23;
hence ( - (P . x) <= (F # x) . k & (F # x) . k <= P . x ) by A17, MESFUNC5:def 13; :: thesis: verum

end;

now :: thesis: for x being Element of X st x in dom (lim_inf F) holds
|.((lim_inf F) . x).| <= P . x

let x be Element of X; :: thesis: ( x in dom (lim_inf F) implies |.((lim_inf F) . x).| <= P . x )
assume A18: x in dom (lim_inf F) ; :: thesis: |.((lim_inf F) . x).| <= P . x
then A19: x in E by A1, MESFUNC8:def 7;
for k being Nat holds (inferior_realsequence (F # x)) . k <= P . x

proof

let k be Nat; :: thesis: (inferior_realsequence (F # x)) . k <= P . x
reconsider k1 = k as Nat ;
A20: (inferior_realsequence (F # x)) . k1 <= (F # x) . k1 by RINFSUP2:8;
(F # x) . k <= P . x by A13, A19;
hence (inferior_realsequence (F # x)) . k <= P . x by A20, XXREAL_0:2; :: thesis: verum

end;

then lim_inf (F # x) <= P . x by Th5;
then A21: (lim_inf F) . x <= P . x by A18, MESFUNC8:def 7;

now :: thesis: for y being ExtReal st y in rng (F # x) holds
- (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 A13, A19; :: thesis: verum

end;

then - (P . x) is LowerBound of rng (F # x) by XXREAL_2:def 2;
then - (P . x) <= inf (F # x) by XXREAL_2:def 4;
then - (P . x) <= inf ((F # x) ^\ 0) by NAT_1:47;
then A22: - (P . x) <= (inferior_realsequence (F # x)) . 0 by RINFSUP2:27;
(inferior_realsequence (F # x)) . 0 <= sup (inferior_realsequence (F # x)) by RINFSUP2:23;
then - (P . x) <= lim_inf (F # x) by A22, XXREAL_0:2;
then - (P . x) <= (lim_inf F) . x by A18, MESFUNC8:def 7;
hence |.((lim_inf F) . x).| <= P . x by A21, EXTREAL1:23; :: thesis: verum

end;

then lim_inf F is_integrable_on M by A2, A4, A11, A6, MESFUNC5:102;
hence |.(lim_inf F).| is_integrable_on M by MESFUNC5:100; :: thesis: |.(lim_sup F).| is_integrable_on M
A23: E = dom (lim_sup F) by A1, MESFUNC8:def 8;

now :: thesis: for x being Element of X st x in dom (lim_sup F) holds
|.((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 A24: 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

let k be Nat; :: thesis: (superior_realsequence (F # x)) . k >= - (P . x)
reconsider k1 = k as Nat ;
A25: (superior_realsequence (F # x)) . k1 >= (F # x) . k1 by RINFSUP2:8;
(F # x) . k >= - (P . x) by A23, A13, A24;
hence (superior_realsequence (F # x)) . k >= - (P . x) by A25, XXREAL_0:2; :: thesis: verum

end;

then lim_sup (F # x) >= - (P . x) by Th4;
then A26: (lim_sup F) . x >= - (P . x) by A24, MESFUNC8:def 8;

now :: thesis: for y being ExtReal st y in rng (F # x) holds
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 A23, A13, A24; :: thesis: verum

end;

then P . x is UpperBound of rng (F # x) by XXREAL_2:def 1;
then P . x >= sup (rng (F # x)) by XXREAL_2:def 3;
then P . x >= sup ((F # x) ^\ 0) by NAT_1:47;
then A27: 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 A27, XXREAL_0:2;
then P . x >= (lim_sup F) . x by A24, MESFUNC8:def 8;
hence |.((lim_sup F) . x).| <= P . x by A26, EXTREAL1:23; :: thesis: verum

end;

then lim_sup F is_integrable_on M by A2, A4, A23, A12, MESFUNC5:102;
hence |.(lim_sup F).| is_integrable_on M by MESFUNC5:100; :: thesis: verum