let X be non empty set ; :: thesis:
let F be with_the_same_dom Functional_Sequence of X,ExtREAL ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let E be Element of S; :: thesis:
let P be PartFunc of X,ExtREAL ; :: thesis:
assume that
A1: ( E = dom (F . 0 ) & E = dom P ) and
A2: for n being Nat holds F . n is_measurable_on E and
A3: ( P is_integrable_on M & P is nonnegative ) and
A4: for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ; :: thesis:

hereby :: thesis:

let n be Nat; :: thesis:
B1: ( E = dom (F . n) & F . n is_measurable_on E ) by A1, A2, MESFUNC8:def 2;

let x be Element of X; :: thesis:
assume B2: x in dom (F . n) ; :: thesis:
then B3: x in dom |.(F . n).| by MESFUNC1:def 10;
|.(F . n).| . x <= P . x by B1, B2, A4;
hence |.((F . n) . x).| <= P . x by B3, MESFUNC1:def 10; :: thesis:

end;

then F . n is_integrable_on M by B1, A1, A3, MESFUNC5:108;
hence |.(F . n).| is_integrable_on M by B1, MESFUNC5:106; :: thesis:

end;

C0: ( E = dom (lim_inf F) & E = dom (lim_sup F) ) by A1, MESFUNC8:def 8, MESFUNC8:def 9;
C1: ( lim_inf F is_measurable_on E & lim_sup F is_measurable_on E ) by A1, A2, MESFUNC8:23, MESFUNC8:24;
C2: 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 )

let x be Element of X; :: thesis:
let k be Nat; :: thesis:
assume C3: x in E ; :: thesis:
then x in dom (F . k) by A1, MESFUNC8:def 2;
then C4: x in dom |.(F . k).| by MESFUNC1:def 10;
|.(F . k).| . x <= P . x by A4, C3;
then |.((F . k) . x).| <= P . x by C4, MESFUNC1:def 10;
then ( - (P . x) <= (F . k) . x & (F . k) . x <= P . x ) by EXTREAL2:60;
hence ( - (P . x) <= (F # x) . k & (F # x) . k <= P . x ) by MESFUNC5:def 13; :: thesis:

end;

now

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

let k be Nat; :: thesis:
reconsider k1 = k as Element of NAT by ORDINAL1:def 13;
D4: (inferior_realsequence (F # x)) . k1 <= (F # x) . k1 by RINFSUP2:8;
(F # x) . k <= P . x by C2, D3;
hence (inferior_realsequence (F # x)) . k <= P . x by D4, XXREAL_0:2; :: thesis:

end;

then lim_inf (F # x) <= P . x by Th63b;
then D5: (lim_inf F) . x <= P . x by D2, MESFUNC8:def 8;

let y be ext-real number ; :: thesis:
assume y in rng (F # x) ; :: thesis:
then consider k being set such that
D6: ( k in dom (F # x) & y = (F # x) . k ) by FUNCT_1:def 5;
thus - (P . x) <= y by D6, C2, D3; :: thesis:

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:48;
then D7: - (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 D7, XXREAL_0:2;
then - (P . x) <= (lim_inf F) . x by D2, MESFUNC8:def 8;
hence |.((lim_inf F) . x).| <= P . x by D5, EXTREAL2:60; :: thesis:

end;

then lim_inf F is_integrable_on M by C0, C1, A1, A3, MESFUNC5:108;
hence |.(lim_inf F).| is_integrable_on M by C0, C1, MESFUNC5:106; :: thesis:

let x be Element of X; :: thesis:
assume D12: x in dom (lim_sup F) ; :: thesis:
for k being Nat holds (superior_realsequence (F # x)) . k >= - (P . x)

let k be Nat; :: thesis:
reconsider k1 = k as Element of NAT by ORDINAL1:def 13;
D14: (superior_realsequence (F # x)) . k1 >= (F # x) . k1 by RINFSUP2:8;
(F # x) . k >= - (P . x) by C2, D12, C0;
hence (superior_realsequence (F # x)) . k >= - (P . x) by D14, XXREAL_0:2; :: thesis:

end;

then lim_sup (F # x) >= - (P . x) by Th63a;
then D15: (lim_sup F) . x >= - (P . x) by D12, MESFUNC8:def 9;

let y be ext-real number ; :: thesis:
assume y in rng (F # x) ; :: thesis:
then consider k being set such that
D16: ( k in dom (F # x) & y = (F # x) . k ) by FUNCT_1:def 5;
thus P . x >= y by D16, C2, D12, C0; :: thesis:

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:48;
then D17: 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 D17, XXREAL_0:2;
then P . x >= (lim_sup F) . x by D12, MESFUNC8:def 9;
hence |.((lim_sup F) . x).| <= P . x by D15, EXTREAL2:60; :: thesis:

end;

then lim_sup F is_integrable_on M by C0, C1, A1, A3, MESFUNC5:108;
hence |.(lim_sup F).| is_integrable_on M by C0, C1, MESFUNC5:106; :: thesis: