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:
assume that
A1: E = dom (F . 0) and
A2: for n being Nat holds
( F . n is nonnegative & F . n is E -measurable ) ; :: thesis:
set H = inferior_realsequence F;
deffunc H₁( Element of NAT ) -> Element of K16(K17(X,ExtREAL)) = inf (F ^\ $1);
consider G being Function such that
A3: ( dom G = NAT & ( for n being Element of NAT holds G . n = H₁(n) ) ) from FUNCT_1:sch 4();

let n be Nat; :: thesis:
n in NAT by ORDINAL1:def 12;
then G . n = inf (F ^\ n) by A3;
hence G . n is PartFunc of X,ExtREAL ; :: thesis:

end;

then reconsider G = G as Functional_Sequence of X,ExtREAL by A3, SEQFUNC:1;
A4: for n being Element of NAT holds G . n = (inferior_realsequence F) . n

let n be Element of NAT ; :: thesis:
(inferior_realsequence F) . n = inf (F ^\ n) by MESFUNC8:8;
hence G . n = (inferior_realsequence F) . n by A3; :: thesis:

end;

then A5: G = inferior_realsequence F by FUNCT_2:63;
reconsider G = G as with_the_same_dom Functional_Sequence of X,ExtREAL by A4, FUNCT_2:63;
A6: dom ((inferior_realsequence F) . 0) = dom (G . 0) by A4;
A7: for n, m being Nat
for x being Element of X st n <= m & x in E holds
( (G . n) . x <= (G . m) . x & (G # x) . n <= (G # x) . m )

let n, m be Nat; :: thesis:
let x be Element of X; :: thesis:
reconsider n1 = n, m1 = m as Element of NAT by ORDINAL1:def 12;
assume that
A8: n <= m and
A9: x in E ; :: thesis:
(inferior_realsequence F) # x = inferior_realsequence (F # x) by A1, A9, MESFUNC8:7;
then ((inferior_realsequence F) # x) . n1 <= ((inferior_realsequence F) # x) . m1 by A8, RINFSUP2:7;
then ((inferior_realsequence F) . n) . x <= ((inferior_realsequence F) # x) . m by MESFUNC5:def 13;
hence (G . n) . x <= (G . m) . x by A5, MESFUNC5:def 13; :: thesis:
then (G # x) . n <= (G . m) . x by MESFUNC5:def 13;
hence (G # x) . n <= (G # x) . m by MESFUNC5:def 13; :: thesis:

end;

A10: now :: thesis:

let x be Element of X; :: thesis:
assume x in E ; :: thesis:
then for n, m being Nat st m <= n holds
(G # x) . m <= (G # x) . n by A7;
then G # x is non-decreasing by RINFSUP2:7;
hence G # x is convergent by RINFSUP2:37; :: thesis:

end;

deffunc H₂( Element of NAT ) -> Element of ExtREAL = Integral (M,(F . $1));
consider I being sequence of ExtREAL such that
A11: for n being Element of NAT holds I . n = H₂(n) from FUNCT_2:sch 4();
A12: for n being Nat holds G . n is E -measurable by A1, A2, A5, MESFUNC8:20;
A13: dom ((inferior_realsequence F) . 0) = dom (F . 0) by MESFUNC8:def 5;
then A14: dom (lim G) = E by A1, A6, MESFUNC8:def 9;
for x being object st x in dom (G . 0) holds
0 <= (G . 0) . x

let x be object ; :: thesis:
assume A15: x in dom (G . 0) ; :: thesis:
then reconsider x = x as Element of X ;

A16: now :: thesis:

let n be Nat; :: thesis:
F . n is nonnegative by A2;
then 0 <= (F . n) . x by SUPINF_2:51;
then 0 <= (F # x) . (0 + n) by MESFUNC5:def 13;
hence 0. <= ((F # x) ^\ 0) . n by NAT_1:def 3; :: thesis:

end;

(F ^\ 0) . 0 = F . (0 + 0) by NAT_1:def 3;
then dom (inf (F ^\ 0)) = dom (F . 0) by MESFUNC8:def 3;
then (inf (F ^\ 0)) . x = inf ((F # x) ^\ 0) by A13, A6, A15, Th6;
then (G . 0) . x = inf ((F # x) ^\ 0) by A3;
hence 0 <= (G . 0) . x by A16, Th4; :: thesis:

end;

then A17: G . 0 is nonnegative by SUPINF_2:52;
for n, m being Nat st n <= m holds
for x being Element of X st x in E holds
(G . n) . x <= (G . m) . x by A7;
then consider J being ExtREAL_sequence such that
A18: for n being Nat holds J . n = Integral (M,(G . n)) and
A19: J is convergent and
A20: Integral (M,(lim G)) = lim J by A1, A13, A6, A17, A12, A10, MESFUNC9:52;
reconsider I = I as ExtREAL_sequence ;
for n being Nat holds J . n <= I . n

let n be Nat; :: thesis:
A21: dom (F . n) = E by A1, MESFUNC8:def 2;
A22: F . n is nonnegative by A2;
A23: n is Element of NAT by ORDINAL1:def 12;

A24: now :: thesis:

let x be Element of X; :: thesis:
assume A25: x in dom (G . n) ; :: thesis:
(inferior_realsequence (F # x)) . n <= (F # x) . n by RINFSUP2:8;
then ((inferior_realsequence F) . n) . x <= (F # x) . n by A5, A25, MESFUNC8:def 5;
then ((inferior_realsequence F) . n) . x <= (F . n) . x by MESFUNC5:def 13;
hence (G . n) . x <= (F . n) . x by A4, A23; :: thesis:

end;

A26: F . n is E -measurable by A2;
A27: G . n is E -measurable by A1, A2, A5, MESFUNC8:20;
A28: dom (G . n) = E by A1, A13, A6, MESFUNC8:def 2;

A29: now :: thesis:

let x be object ; :: thesis:
assume A30: x in dom (G . n) ; :: thesis:
0 <= (G . 0) . x by A17, SUPINF_2:51;
hence 0 <= (G . n) . x by A7, A28, A30; :: thesis:

end;

then G . n is nonnegative by SUPINF_2:52;
then integral+ (M,(G . n)) <= integral+ (M,(F . n)) by A21, A28, A26, A27, A22, A24, MESFUNC5:85;
then Integral (M,(G . n)) <= integral+ (M,(F . n)) by A28, A27, A29, MESFUNC5:88, SUPINF_2:52;
then A31: Integral (M,(G . n)) <= Integral (M,(F . n)) by A21, A26, A22, MESFUNC5:88;
I . n = Integral (M,(F . n)) by A11, A23;
hence J . n <= I . n by A18, A31; :: thesis:

end;

then lim_inf J <= lim_inf I by Th3;
then A32: lim J <= lim_inf I by A19, RINFSUP2:41;
A33: dom (sup G) = E by A1, A13, A6, MESFUNC8:def 4;

let x be Element of X; :: thesis:
assume A34: x in dom (lim G) ; :: thesis:
then for n, m being Nat st m <= n holds
(G # x) . m <= (G # x) . n by A7, A14;
then G # x is non-decreasing by RINFSUP2:7;
then A35: lim (G # x) = sup (G # x) by RINFSUP2:37;
(sup G) . x = sup (G # x) by A14, A33, A34, MESFUNC8:def 4;
hence (lim G) . x = (sup G) . x by A34, A35, MESFUNC8:def 9; :: thesis:

end;

then A36: lim G = sup G by A14, A33, PARTFUN1:5;
take I ; :: thesis:
for n being Nat holds I . n = Integral (M,(F . n))

let n be Nat; :: thesis:
n is Element of NAT by ORDINAL1:def 12;
hence I . n = Integral (M,(F . n)) by A11; :: thesis:

end;

hence ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & Integral (M,(lim_inf F)) <= lim_inf I ) by A5, A20, A36, A32, MESFUNC8:11; :: thesis: