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_measurable_on E ) ; :: thesis:
deffunc H₁( Element of NAT ) -> Element of K21(K22(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 Element of NAT ; :: thesis:
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:113;
set H = inferior_realsequence F;
reconsider G = G as with_the_same_dom Functional_Sequence of X,ExtREAL by A4, FUNCT_2:113;
A6: ( dom ((inferior_realsequence F) . 0 ) = dom (F . 0 ) & dom ((inferior_realsequence F) . 0 ) = dom (G . 0 ) ) by A4, MESFUNC8:def 5;
for x being set st x in dom (G . 0 ) holds
0 <= (G . 0 ) . x

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

P12: now

let n be Nat; :: thesis:
F . n is nonnegative by A2;
then 0 <= (F . n) . x by SUPINF_2:70;
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 P11, A6, inferiorf1a;
then (G . 0 ) . x = inf ((F # x) ^\ 0 ) by A3;
hence 0 <= (G . 0 ) . x by P12, Th63a; :: thesis:

end;

then P1: G . 0 is nonnegative by SUPINF_2:71;
P2: for n being Nat holds G . n is_measurable_on E by A1, A2, A5, MESFUNC8:20;
P3: 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 13;
assume P31: ( n <= m & x in E ) ; :: thesis:
then (inferior_realsequence F) # x = inferior_realsequence (F # x) by A1, MESFUNC8:7;
then ((inferior_realsequence F) # x) . n1 <= ((inferior_realsequence F) # x) . m1 by P31, 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;

then PP: 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 ;

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

end;

then consider J being ExtREAL_sequence such that
P4: ( ( for n being Nat holds J . n = Integral M,(G . n) ) & J is convergent & Integral M,(lim G) = lim J ) by A1, A6, P1, P2, PP, MESFUNC9:52;
deffunc H₂( Element of NAT ) -> Element of ExtREAL = Integral M,(F . $1);
consider I being Function of NAT ,ExtREAL such that
P5: for n being Element of NAT holds I . n = H₂(n) from FUNCT_2:sch 4();
reconsider I = I as ExtREAL_sequence ;
take I ; :: thesis:
P6: for n being Nat holds I . n = Integral M,(F . n)

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

end;

P7: ( dom (lim G) = E & dom (sup G) = E ) by A1, A6, MESFUNC8:def 4, MESFUNC8:def 10;

let x be Element of X; :: thesis:
assume P81: x in dom (lim G) ; :: thesis:
then for n, m being Element of NAT st m <= n holds
(G # x) . m <= (G # x) . n by P7, P3;
then G # x is non-decreasing by RINFSUP2:7;
then P82: lim (G # x) = sup (G # x) by RINFSUP2:37;
(sup G) . x = sup (G # x) by P81, P7, MESFUNC8:def 4;
hence (lim G) . x = (sup G) . x by P82, P81, MESFUNC8:def 10; :: thesis:

end;

then P8: lim G = sup G by P7, PARTFUN1:34;
for n being Nat holds J . n <= I . n

let n be Nat; :: thesis:
Q1: ( dom (F . n) = E & dom (G . n) = E ) by A1, A6, MESFUNC8:def 2;
Q2: ( F . n is_measurable_on E & G . n is_measurable_on E ) by A1, A2, A5, MESFUNC8:20;
Q3: F . n is nonnegative by A2;

q4: now

let x be set ; :: thesis:
assume Q41: x in dom (G . n) ; :: thesis:
0 <= (G . 0 ) . x by P1, SUPINF_2:70;
hence 0 <= (G . n) . x by Q41, Q1, P3; :: thesis:

end;

then Q4: G . n is nonnegative by SUPINF_2:71;
Q0: n is Element of NAT by ORDINAL1:def 13;
then Q5: I . n = Integral M,(F . n) by P5;

let x be Element of X; :: thesis:
assume P01: x in dom (G . n) ; :: thesis:
(inferior_realsequence (F # x)) . n <= (F # x) . n by Q0, RINFSUP2:8;
then ((inferior_realsequence F) . n) . x <= (F # x) . n by P01, A5, 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, Q0; :: thesis:

end;

then integral+ M,(G . n) <= integral+ M,(F . n) by Q1, Q2, Q3, Q4, MESFUNC5:91;
then Integral M,(G . n) <= integral+ M,(F . n) by Q1, Q2, q4, MESFUNC5:94, SUPINF_2:71;
then Integral M,(G . n) <= Integral M,(F . n) by Q1, Q2, Q3, MESFUNC5:94;
hence J . n <= I . n by Q5, P4; :: thesis:

end;

then lim_inf J <= lim_inf I by limseq1;
then lim J <= lim_inf I by P4, RINFSUP2:41;
hence ( ( for n being Nat holds I . n = Integral M,(F . n) ) & Integral M,(lim_inf F) <= lim_inf I ) by P6, P4, P8, A5, MESFUNC8:11; :: thesis: