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 f be PartFunc of X,ExtREAL ; :: thesis:
assume that
A1: M . E < +infty and
A2: E = dom (F . 0 ) and
A3: for n being Nat holds F . n is_integrable_on M and
A4: F is_uniformly_convergent_to f ; :: thesis:
consider N being Nat such that
A5: for n being Nat
for x being set st n >= N & x in dom (F . 0 ) holds
|.(((F . n) . x) - (f . x)).| < 1 / 2 by A4, Def2;
reconsider N1 = N as Element of NAT by ORDINAL1:def 13;
consider h being PartFunc of X,ExtREAL such that
A6: h is_simple_func_in S and
A7: dom h = E and
A8: for x being set st x in E holds
h . x = 1. by MESFUNC5:47;
A9: max- h is_measurable_on E by A6, A7, MESFUNC2:28, MESFUNC2:37;
for x being set st x in E holds
h . x >= 0. by A8;
then A10: h is nonnegative by A7, SUPINF_2:71;
then A11: Integral M,h = integral' M,h by A6, MESFUNC5:95;
set AFN = |.(F . N).|;
A12: dom (F . N) = dom |.(F . N).| by MESFUNC1:def 10;

now

let x be set ; :: thesis:
assume x in dom |.(F . N).| ; :: thesis:
then |.(F . N).| . x = |.((F . N) . x).| by MESFUNC1:def 10;
hence 0 <= |.(F . N).| . x by EXTREAL2:51; :: thesis:

end;

then A13: |.(F . N).| is nonnegative by SUPINF_2:71;
then A14: dom (|.(F . N).| + h) = (dom |.(F . N).|) /\ (dom h) by A10, MESFUNC5:28;
A15: for x being set st x in dom (F . 0 ) holds
|.(((F . N) . x) - (f . x)).| < 1 / 2 by A5;

A16: now

let x be set ; :: thesis:
let n be Nat; :: thesis:
assume that
A17: n >= N and
A18: x in dom (F . 0 ) ; :: thesis:
A19: |.(((F . n) . x) - (f . x)).| < 1 / 2 by A5, A17, A18;
A20: |.(((F . N) . x) - (f . x)).| < 1 / 2 by A5, A18;

A21: now

A22: |.(((F . n) . x) - (f . x)).| < 1. by A19, XXREAL_0:2;
then A23: ((F . n) . x) - (f . x) < 1. by EXTREAL2:58;
A24: |.(((F . N) . x) - (f . x)).| < 1. by A20, XXREAL_0:2;
then A25: - 1. < ((F . N) . x) - (f . x) by EXTREAL2:58;
A26: ((F . N) . x) - (f . x) < 1. by A24, EXTREAL2:58;
assume A27: ( f . x = +infty or f . x = -infty ) ; :: thesis:
- 1. < ((F . n) . x) - (f . x) by A22, EXTREAL2:58;
then ( ( (F . n) . x = +infty & (F . N) . x = +infty ) or ( (F . n) . x = -infty & (F . N) . x = -infty ) ) by A27, A25, A23, A26, XXREAL_3:64, XXREAL_3:65;
hence |.((F . n) . x).| <= |.((F . N) . x).| + 1. by EXTREAL2:67, XXREAL_3:63; :: thesis:

end;

dom (|.(F . N).| + h) = (dom |.(F . N).|) /\ (dom h) by A10, A13, MESFUNC5:28;
then dom (|.(F . N).| + h) = E /\ E by A2, A7, A12, MESFUNC8:def 2;
then (|.(F . N).| . x) + (h . x) = (|.(F . N).| + h) . x by A2, A18, MESFUNC1:def 3;
then A28: (|.(F . N).| . x) + 1. = (|.(F . N).| + h) . x by A2, A8, A18;
dom (F . n) = E by A2, MESFUNC8:def 2;
then A29: x in dom |.(F . n).| by A2, A18, MESFUNC1:def 10;

A30: now

A34: now

assume ( (F . N) . x = +infty or (F . N) . x = -infty ) ; :: thesis:
then ( ((F . N) . x) - (f . x) = +infty or ((F . N) . x) - (f . x) = -infty ) by A33, XXREAL_3:13, XXREAL_3:14;
then 1. < |.(((F . N) . x) - (f . x)).| by EXTREAL2:67, XXREAL_0:9;
hence contradiction by A15, A18, XXREAL_0:2; :: thesis:

end;

A35: now

assume ( (F . n) . x = +infty or (F . n) . x = -infty ) ; :: thesis:
then ( ((F . n) . x) - (f . x) = +infty or ((F . n) . x) - (f . x) = -infty ) by A33, XXREAL_3:13, XXREAL_3:14;
hence contradiction by A19, EXTREAL2:67, XXREAL_0:9; :: thesis:

end;

then (F . n) . x in REAL by XXREAL_0:14;
then A36: |.((F . n) . x).| - |.((F . N) . x).| <= |.(((F . n) . x) - ((F . N) . x)).| by EXTREAL2:68;
b <= 1 / 2 by A20, MESFUNC5:1;
then a + b < (1 / 2) + (1 / 2) by A19, XREAL_1:10;
then A37: |.(((F . n) . x) - (f . x)).| + |.((f . x) - ((F . N) . x)).| < 1 by SUPINF_2:1;
(- (f . x)) + (f . x) = 0. by XXREAL_3:7;
then ((F . n) . x) - ((F . N) . x) = (((F . n) . x) + ((- (f . x)) + (f . x))) - ((F . N) . x) by XXREAL_3:4;
then ((F . n) . x) - ((F . N) . x) = ((((F . n) . x) + (- (f . x))) + (f . x)) - ((F . N) . x) by A33, A35, XXREAL_3:30;
then ((F . n) . x) - ((F . N) . x) = (((F . n) . x) - (f . x)) + ((f . x) - ((F . N) . x)) by A33, A34, XXREAL_3:31;
then |.(((F . n) . x) - ((F . N) . x)).| <= |.(((F . n) . x) - (f . x)).| + |.((f . x) - ((F . N) . x)).| by EXTREAL2:61;
then |.(((F . n) . x) - ((F . N) . x)).| < 1 by A37, XXREAL_0:2;
then |.((F . n) . x).| - |.((F . N) . x).| <= 1. by A36, XXREAL_0:2;
hence |.((F . n) . x).| <= |.((F . N) . x).| + 1. by XXREAL_3:63; :: thesis:

end;

x in dom |.(F . N).| by A12, A18, MESFUNC8:def 2;
then |.((F . n) . x).| <= (|.(F . N).| . x) + 1. by A30, A21, MESFUNC1:def 10, XXREAL_0:14;
hence |.(F . n).| . x <= (|.(F . N).| + h) . x by A28, A29, MESFUNC1:def 10; :: thesis:

end;

A38: for x being Element of X
for n being Nat st x in E holds
|.((F ^\ N1) . n).| . x <= (|.(F . N).| + h) . x

proof

let x be Element of X; :: thesis:
let n be Nat; :: thesis:
A39: (F ^\ N1) . n = F . (n + N) by NAT_1:def 3;
assume x in E ; :: thesis:
hence |.((F ^\ N1) . n).| . x <= (|.(F . N).| + h) . x by A2, A16, A39, NAT_1:11; :: thesis:

end;

A40: max+ h is_measurable_on E by A6, MESFUNC2:27, MESFUNC2:37;
for x being set st x in dom (max- h) holds
0. <= (max- h) . x by MESFUNC2:15;
then A41: max- h is nonnegative by SUPINF_2:71;
A42: for n being Nat holds F . n is_measurable_on E

proof

let n be Nat; :: thesis:
F . n is_integrable_on M by A3;
then ex A being Element of S st
( A = dom (F . n) & F . n is_measurable_on A ) by MESFUNC5:def 17;
hence F . n is_measurable_on E by A2, MESFUNC8:def 2; :: thesis:

end;

then A43: F . N is_measurable_on E ;
(F ^\ N1) . 0 = F . (0 + N) by NAT_1:def 3;
then A44: dom ((F ^\ N1) . 0 ) = E by A2, MESFUNC8:def 2;

A45: now

let x be Element of X; :: thesis:
assume x in dom f ; :: thesis:
then A46: x in dom (F . 0 ) by A4, Def2;
then A47: x in dom (lim F) by MESFUNC8:def 10;
lim (F # x) = f . x by A4, A46, Th21;
hence (lim F) . x = f . x by A47, MESFUNC8:def 10; :: thesis:

end;

dom f = dom (F . 0 ) by A4, Def2;
then dom (lim F) = dom f by MESFUNC8:def 10;
then A48: lim F = f by A45, PARTFUN1:34;
A49: F . N is_integrable_on M by A3;
E = dom (F . N) by A2, MESFUNC8:def 2;
then A50: |.(F . N).| is_integrable_on M by A49, A43, MESFUNC5:106;
deffunc H₁( Element of NAT ) -> Element of ExtREAL = Integral M,(F . $1);
A51: (R_EAL 1) * +infty = +infty by XXREAL_3:def 5;

A52: now

let x be Element of X; :: thesis:
assume x in dom h ; :: thesis:
then A53: x in dom |.h.| by MESFUNC1:def 10;
0 <= h . x by A10, SUPINF_2:70;
then |.(h . x).| = h . x by EXTREAL1:def 3;
hence |.h.| . x = h . x by A53, MESFUNC1:def 10; :: thesis:

end;

dom h = dom |.h.| by MESFUNC1:def 10;
then A54: h = |.h.| by A52, PARTFUN1:34;
Integral M,h = integral+ M,h by A6, A10, MESFUNC5:95;
then integral+ M,h = (R_EAL 1) * (M . (dom h)) by A7, A8, A11, MESFUNC5:110;
then A55: integral+ M,|.h.| < +infty by A1, A7, A54, A51, XXREAL_3:83;
A56: for n being Nat holds (F ^\ N1) . n is_measurable_on E

proof

let n be Nat; :: thesis:
(F ^\ N1) . n = F . (n + N) by NAT_1:def 3;
hence (F ^\ N1) . n is_measurable_on E by A42; :: thesis:

end;

A57: for x being Element of X st x in E holds
( (F ^\ N1) # x is convergent & lim (F # x) = lim ((F ^\ N1) # x) )

proof

let x be Element of X; :: thesis:

A58: now

let n be Element of NAT ; :: thesis:
((F ^\ N1) # x) . n = ((F ^\ N1) . n) . x by MESFUNC5:def 13;
then ((F ^\ N1) # x) . n = (F . (n + N)) . x by NAT_1:def 3;
then ((F ^\ N1) # x) . n = (F # x) . (n + N) by MESFUNC5:def 13;
hence ((F ^\ N1) # x) . n = ((F # x) ^\ N1) . n by NAT_1:def 3; :: thesis:

end;

assume x in E ; :: thesis:
then A59: F # x is convergent by A2, A4, Th21;
then (F # x) ^\ N1 is convergent by RINFSUP2:21;
hence (F ^\ N1) # x is convergent by A58, FUNCT_2:113; :: thesis:
lim (F # x) = lim ((F # x) ^\ N1) by A59, RINFSUP2:21;
hence lim (F # x) = lim ((F ^\ N1) # x) by A58, FUNCT_2:113; :: thesis:

end;

then for x being Element of X st x in E holds
(F ^\ N1) # x is convergent ;
then A60: lim (F ^\ N1) is_measurable_on E by A56, A44, MESFUNC8:25;
dom (lim (F ^\ N1)) = E by A44, MESFUNC8:def 10;
then A61: dom (lim F) = dom (lim (F ^\ N1)) by A2, MESFUNC8:def 10;

A62: now

let x be Element of X; :: thesis:
assume A63: x in dom (lim F) ; :: thesis:
then x in E by A2, MESFUNC8:def 10;
then A64: lim (F # x) = lim ((F ^\ N1) # x) by A57;
lim ((F ^\ N1) # x) = (lim (F ^\ N1)) . x by A61, A63, MESFUNC8:def 10;
hence (lim F) . x = (lim (F ^\ N1)) . x by A63, A64, MESFUNC8:def 10; :: thesis:

end;

A65: dom (max- h) = dom h by MESFUNC2:def 3;
then A66: (max- h) | E = max- h by A7, RELAT_1:97;
A67: dom (max+ h) = dom h by MESFUNC2:def 2;
then A68: (max+ h) | E = max+ h by A7, RELAT_1:97;
for x being set st x in dom (max+ h) holds
0. <= (max+ h) . x by MESFUNC2:14;
then A69: max+ h is nonnegative by SUPINF_2:71;
then dom ((max+ h) + (max- h)) = (dom (max+ h)) /\ (dom (max- h)) by A41, MESFUNC5:28;
then ex C being Element of S st
( C = E & integral+ M,((max+ h) + (max- h)) = (integral+ M,((max+ h) | C)) + (integral+ M,((max- h) | C)) ) by A7, A40, A9, A69, A41, A67, A65, MESFUNC5:84;
then A70: integral+ M,|.h.| = (integral+ M,(max+ h)) + (integral+ M,(max- h)) by A68, A66, MESFUNC2:26;
A71: h is_measurable_on E by A6, MESFUNC2:37;
then 0 <= integral+ M,(max- h) by A7, A41, A65, MESFUNC2:28, MESFUNC5:85;
then integral+ M,(max+ h) <> +infty by A70, A55, XXREAL_3:def 2;
then A72: integral+ M,(max+ h) < +infty by XXREAL_0:4;
0 <= integral+ M,(max+ h) by A7, A71, A69, A67, MESFUNC2:27, MESFUNC5:85;
then integral+ M,(max- h) <> +infty by A70, A55, XXREAL_3:def 2;
then integral+ M,(max- h) < +infty by XXREAL_0:4;
then h is_integrable_on M by A7, A71, A72, MESFUNC5:def 17;
then A73: |.(F . N).| + h is_integrable_on M by A50, MESFUNC5:114;
A74: E = dom |.(F . N).| by A2, A12, MESFUNC8:def 2;
then A75: |.(lim_inf (F ^\ N1)).| is_integrable_on M by A7, A73, A14, A38, A56, A44, Th17;
|.(F . N).| + h is nonnegative by A10, A13, MESFUNC5:28;
then consider J being ExtREAL_sequence such that
A76: for n being Nat holds J . n = Integral M,((F ^\ N1) . n) and
lim_inf J >= Integral M,(lim_inf (F ^\ N1)) and
lim_sup J <= Integral M,(lim_sup (F ^\ N1)) and
A77: ( ( for x being Element of X st x in E holds
(F ^\ N1) # x is convergent ) implies ( J is convergent & lim J = Integral M,(lim (F ^\ N1)) ) ) by A7, A73, A14, A74, A38, A56, A44, Th18;
consider I being Function of NAT ,ExtREAL such that
A78: for n being Element of NAT holds I . n = H₁(n) from FUNCT_2:sch 4();
reconsider I = I as ExtREAL_sequence ;
A79: dom (lim_inf (F ^\ N1)) = dom ((F ^\ N1) . 0 ) by MESFUNC8:def 8;

A80: now

let x be Element of X; :: thesis:
assume A81: x in dom (lim (F ^\ N1)) ; :: thesis:
then x in E by A44, MESFUNC8:def 10;
then (F ^\ N1) # x is convergent by A57;
hence (lim (F ^\ N1)) . x = (lim_inf (F ^\ N1)) . x by A81, MESFUNC8:14; :: thesis:

end;

dom (lim (F ^\ N1)) = dom ((F ^\ N1) . 0 ) by MESFUNC8:def 10;
then lim (F ^\ N1) = lim_inf (F ^\ N1) by A79, A80, PARTFUN1:34;
then A82: lim (F ^\ N1) is_integrable_on M by A44, A75, A79, A60, MESFUNC5:106;
A83: for n being Nat holds I . n = Integral M,(F . n)

proof

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

end;

now

let n be Element of NAT ; :: thesis:
A84: (F ^\ N1) . n = F . (n + N) by NAT_1:def 3;
A85: (I ^\ N1) . n = I . (n + N) by NAT_1:def 3;
J . n = Integral M,((F ^\ N1) . n) by A76;
hence J . n = (I ^\ N1) . n by A78, A84, A85; :: thesis:

end;

then A86: J = I ^\ N1 by FUNCT_2:113;
then A87: I is convergent by A57, A77, RINFSUP2:17;
lim I = lim J by A57, A77, A86, RINFSUP2:17;
then lim I = Integral M,(lim F) by A57, A61, A62, A77, PARTFUN1:34;
hence ( f is_integrable_on M & ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral M,(F . n) ) & I is convergent & lim I = Integral M,f ) ) by A48, A61, A62, A82, A83, A87, PARTFUN1:34; :: thesis: