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:
reconsider e = 1 / 2 as Real ;
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)).| < e by A4;
reconsider N1 = N as Nat ;
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 object st x in E holds
h . x = 1. by MESFUNC5:41;
A9: max- h is E -measurable by A6, A7, MESFUNC2:26, MESFUNC2:34;
for x being object st x in E holds
h . x >= 0. by A8;
then A10: h is nonnegative by A7, SUPINF_2:52;
then A11: Integral (M,h) = integral' (M,h) by A6, MESFUNC5:89;
set AFN = |.(F . N).|;
A12: dom (F . N) = dom |.(F . N).| by MESFUNC1:def 10;

now :: thesis:

let x be object ; :: 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 EXTREAL1:14; :: thesis:

end;

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

A16: now :: thesis:

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)).| < jj / 2 by A5, A17, A18;
A20: |.(((F . N) . x) - (f . x)).| < jj / 2 by A5, A18;

A21: now :: thesis:

A22: |.(((F . n) . x) - (f . x)).| < 1 by A19, XXREAL_0:2;
then A23: ((F . n) . x) - (f . x) < 1. by EXTREAL1:21;
A24: |.(((F . N) . x) - (f . x)).| < 1 by A20, XXREAL_0:2;
then A25: - 1. < ((F . N) . x) - (f . x) by EXTREAL1:21;
A26: ((F . N) . x) - (f . x) < 1. by A24, EXTREAL1:21;
assume A27: ( f . x = +infty or f . x = -infty ) ; :: thesis:
- 1. < ((F . n) . x) - (f . x) by A22, EXTREAL1:21;
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:53, XXREAL_3:54;
hence |.((F . n) . x).| <= |.((F . N) . x).| + 1. by EXTREAL1:30, XXREAL_3:52; :: thesis:

end;

dom (|.(F . N).| + h) = (dom |.(F . N).|) /\ (dom h) by A10, A13, MESFUNC5:22;
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 :: thesis:

A35: now :: thesis:

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 A34, XXREAL_3:13, XXREAL_3:14;
then jj < |.(((F . N) . x) - (f . x)).| by EXTREAL1:30, XXREAL_0:9;
hence contradiction by A15, A18, XXREAL_0:2; :: thesis:

end;

A36: now :: thesis:

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 A34, XXREAL_3:13, XXREAL_3:14;
hence contradiction by A19, EXTREAL1:30, XXREAL_0:9, A32; :: thesis:

end;

then (F . n) . x in REAL by XXREAL_0:14;
then A37: |.((F . n) . x).| - |.((F . N) . x).| <= |.(((F . n) . x) - ((F . N) . x)).| by EXTREAL1:31;
b <= 1 / 2 by A20, MESFUNC5:1;
then a + b < (1 / 2) + (1 / 2) by A19, XREAL_1:8;
then A38: |.(((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 A34, A36, XXREAL_3:29;
then ((F . n) . x) - ((F . N) . x) = (((F . n) . x) - (f . x)) + ((f . x) - ((F . N) . x)) by A34, A35, XXREAL_3:30;
then |.(((F . n) . x) - ((F . N) . x)).| <= |.(((F . n) . x) - (f . x)).| + |.((f . x) - ((F . N) . x)).| by EXTREAL1:24;
then |.(((F . n) . x) - ((F . N) . x)).| < 1 by A38, XXREAL_0:2;
then |.((F . n) . x).| - |.((F . N) . x).| <= 1. by A37, XXREAL_0:2;
hence |.((F . n) . x).| <= |.((F . N) . x).| + 1. by XXREAL_3:52; :: 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;

A39: 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:
A40: (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, A40, NAT_1:11; :: thesis:

end;

A41: max+ h is E -measurable by A6, MESFUNC2:25, MESFUNC2:34;
for x being object st x in dom (max- h) holds
0. <= (max- h) . x by MESFUNC2:13;
then A42: max- h is nonnegative by SUPINF_2:52;
A43: for n being Nat holds F . n is E -measurable

proof

let n be Nat; :: thesis:
F . n is_integrable_on M by A3;
then consider A being Element of S such that
AA: ( A = dom (F . n) & F . n is A -measurable ) ;
for r being Real holds E /\ (less_dom ((F . n),r)) in S

proof

let r be Real; :: thesis:
E = dom (F . n) by A2, MESFUNC8:def 2;
then E = A by AA;
hence E /\ (less_dom ((F . n),r)) in S by AA; :: thesis:

end;

hence F . n is E -measurable ; :: thesis:

end;

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

A46: now :: thesis:

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

end;

dom f = dom (F . 0) by A4;
then dom (lim F) = dom f by MESFUNC8:def 9;
then A49: lim F = f by A46, PARTFUN1:5;
F . N is_integrable_on M by A3;
then A51: |.(F . N).| is_integrable_on M by MESFUNC5:100;
deffunc H₁( Nat) -> Element of ExtREAL = Integral (M,(F . $1));
A52: 1 * +infty = +infty by XXREAL_3:def 5;

A53: now :: thesis:

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

end;

dom h = dom |.h.| by MESFUNC1:def 10;
then A55: h = |.h.| by A53, PARTFUN1:5;
Integral (M,h) = integral+ (M,h) by A6, A10, MESFUNC5:89;
then integral+ (M,h) = jj * (M . (dom h)) by A7, A8, A11, MESFUNC5:104;
then A56: integral+ (M,|.h.|) < +infty by A1, A7, A55, A52, XXREAL_3:72;
A57: for n being Nat holds (F ^\ N1) . n is E -measurable

proof

let n be Nat; :: thesis:
(F ^\ N1) . n = F . (n + N) by NAT_1:def 3;
hence (F ^\ N1) . n is E -measurable by A43; :: thesis:

end;

A58: 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:

A59: now :: thesis:

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 A60: F # x is convergent by A2, A4, Th20;
then (F # x) ^\ N1 is convergent by RINFSUP2:21;
hence (F ^\ N1) # x is convergent by A59, FUNCT_2:63; :: thesis:
lim (F # x) = lim ((F # x) ^\ N1) by A60, RINFSUP2:21;
hence lim (F # x) = lim ((F ^\ N1) # x) by A59, FUNCT_2:63; :: thesis:

end;

then for x being Element of X st x in E holds
(F ^\ N1) # x is convergent ;
then A61: lim (F ^\ N1) is E -measurable by A57, A45, MESFUNC8:25;
dom (lim (F ^\ N1)) = E by A45, MESFUNC8:def 9;
then A62: dom (lim F) = dom (lim (F ^\ N1)) by A2, MESFUNC8:def 9;

A63: now :: thesis:

let x be Element of X; :: thesis:
assume A64: x in dom (lim F) ; :: thesis:
then x in E by A2, MESFUNC8:def 9;
then A65: lim (F # x) = lim ((F ^\ N1) # x) by A58;
lim ((F ^\ N1) # x) = (lim (F ^\ N1)) . x by A62, A64, MESFUNC8:def 9;
hence (lim F) . x = (lim (F ^\ N1)) . x by A64, A65, MESFUNC8:def 9; :: thesis:

end;

A66: dom (max- h) = dom h by MESFUNC2:def 3;
then A67: (max- h) | E = max- h by A7, RELAT_1:68;
A68: dom (max+ h) = dom h by MESFUNC2:def 2;
then A69: (max+ h) | E = max+ h by A7, RELAT_1:68;
for x being object st x in dom (max+ h) holds
0. <= (max+ h) . x by MESFUNC2:12;
then A70: max+ h is nonnegative by SUPINF_2:52;
then dom ((max+ h) + (max- h)) = (dom (max+ h)) /\ (dom (max- h)) by A42, MESFUNC5:22;
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, A41, A9, A70, A42, A68, A66, MESFUNC5:78;
then A71: integral+ (M,|.h.|) = (integral+ (M,(max+ h))) + (integral+ (M,(max- h))) by A69, A67, MESFUNC2:24;
A72: h is E -measurable by A6, MESFUNC2:34;
then 0 <= integral+ (M,(max- h)) by A7, A42, A66, MESFUNC2:26, MESFUNC5:79;
then integral+ (M,(max+ h)) <> +infty by A71, A56, XXREAL_3:def 2;
then A73: integral+ (M,(max+ h)) < +infty by XXREAL_0:4;
0 <= integral+ (M,(max+ h)) by A7, A72, A70, A68, MESFUNC2:25, MESFUNC5:79;
then integral+ (M,(max- h)) <> +infty by A71, A56, XXREAL_3:def 2;
then integral+ (M,(max- h)) < +infty by XXREAL_0:4;
then h is_integrable_on M by A7, A72, A73;
then A74: |.(F . N).| + h is_integrable_on M by A51, MESFUNC5:108;
A75: E = dom |.(F . N).| by A2, A12, MESFUNC8:def 2;
then A76: |.(lim_inf (F ^\ N1)).| is_integrable_on M by A7, A74, A14, A39, A57, A45, Th16;
|.(F . N).| + h is nonnegative by A10, A13, MESFUNC5:22;
then consider J being ExtREAL_sequence such that
A77: 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
A78: ( ( 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, A74, A14, A75, A39, A57, A45, Th17;
consider I being sequence of ExtREAL such that
A79: for n being Element of NAT holds I . n = H₁(n) from FUNCT_2:sch 4();
reconsider I = I as ExtREAL_sequence ;
A80: dom (lim_inf (F ^\ N1)) = dom ((F ^\ N1) . 0) by MESFUNC8:def 7;

A81: now :: thesis:

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

end;

dom (lim (F ^\ N1)) = dom ((F ^\ N1) . 0) by MESFUNC8:def 9;
then lim (F ^\ N1) = lim_inf (F ^\ N1) by A80, A81, PARTFUN1:5;
then A83: lim (F ^\ N1) is_integrable_on M by A45, A76, A80, A61, MESFUNC5:100;
A84: for n being Nat holds I . n = Integral (M,(F . n))

proof

let n be Nat; :: thesis:
n in NAT by ORDINAL1:def 12;
hence I . n = Integral (M,(F . n)) by A79; :: thesis:

end;

now :: thesis:

let n be Element of NAT ; :: thesis:
A85: (F ^\ N1) . n = F . (n + N) by NAT_1:def 3;
A86: (I ^\ N1) . n = I . (n + N) by NAT_1:def 3;
reconsider nn = n + N as Element of NAT by ORDINAL1:def 12;
thus J . n = Integral (M,((F ^\ N1) . n)) by A77
.= I . nn by A79, A85
.= (I ^\ N1) . n by A86 ; :: thesis:

end;

then A87: J = I ^\ N1 by FUNCT_2:63;
then A88: I is convergent by A58, A78, RINFSUP2:17;
lim I = lim J by A58, A78, A87, RINFSUP2:17;
then lim I = Integral (M,(lim F)) by A58, A62, A63, A78, PARTFUN1:5;
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 A49, A62, A63, A83, A84, A88, PARTFUN1:5; :: thesis: