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 & E = dom (F . 0 ) ) and
A2: for n being Nat holds F . n is_integrable_on M and
A3: F is_uniformly_convergent_to f ; :: thesis:
A4: for n being Nat holds F . n is_measurable_on E

proof

let n be Nat; :: thesis:
F . n is_integrable_on M by A2;
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 A1, MESFUNC8:def 2; :: thesis:

end;

dom f = dom (F . 0 ) by A3, DefUC;
then A5: dom (lim F) = dom f by MESFUNC8:def 10;

now

let x be Element of X; :: thesis:
assume x in dom f ; :: thesis:
then x in dom (F . 0 ) by A3, DefUC;
then ( x in dom (lim F) & lim (F # x) = f . x ) by A3, UCONV, MESFUNC8:def 10;
hence (lim F) . x = f . x by MESFUNC8:def 10; :: thesis:

end;

then A6: lim F = f by A5, PARTFUN1:34;
consider N being Nat such that
A7: 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 A3, DefUC;
A8: for x being set st x in dom (F . 0 ) holds
|.(((F . N) . x) - (f . x)).| < 1 / 2 by A7;
consider h being PartFunc of X,ExtREAL such that
B1: ( h is_simple_func_in S & dom h = E & ( for x being set st x in E holds
h . x = 1. ) ) by MESFUNC5:47;
for x being set st x in E holds
h . x >= 0. by B1;
then B2: h is nonnegative by B1, SUPINF_2:71;
then ( Integral M,h = integral+ M,h & Integral M,h = integral' M,h ) by B1, MESFUNC5:95;
then B3: integral+ M,h = (R_EAL 1) * (M . (dom h)) by B1, MESFUNC5:110;
B4: dom h = dom |.h.| by MESFUNC1:def 10;

now

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

end;

then B5: h = |.h.| by B4, PARTFUN1:34;
B6: h is_measurable_on E by B1, MESFUNC2:37;
then B7: ( max+ h is_measurable_on E & max- h is_measurable_on E ) by B1, MESFUNC2:27, MESFUNC2:28;
( ( for x being set st x in dom (max+ h) holds
0. <= (max+ h) . x ) & ( for x being set st x in dom (max- h) holds
0. <= (max- h) . x ) ) by MESFUNC2:14, MESFUNC2:15;
then B8: ( max+ h is nonnegative & max- h is nonnegative ) by SUPINF_2:71;
B9: ( dom (max+ h) = dom h & dom (max- h) = dom h ) by MESFUNC2:def 2, MESFUNC2:def 3;
then C1: ( (max+ h) | E = max+ h & (max- h) | E = max- h ) by B1, RELAT_1:97;
dom ((max+ h) + (max- h)) = (dom (max+ h)) /\ (dom (max- h)) by B8, 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 B1, B9, B7, B8, MESFUNC5:84;
then C2: integral+ M,|.h.| = (integral+ M,(max+ h)) + (integral+ M,(max- h)) by C1, MESFUNC2:26;
C3: ( 0 <= integral+ M,(max+ h) & 0 <= integral+ M,(max- h) ) by B1, B9, B7, B8, MESFUNC5:85;
(R_EAL 1) * +infty = +infty by XXREAL_3:def 5;
then integral+ M,|.h.| < +infty by B1, B3, B5, A1, XXREAL_3:83;
then ( integral+ M,(max+ h) <> +infty & integral+ M,(max- h) <> +infty ) by C2, C3, XXREAL_3:def 2;
then ( integral+ M,(max+ h) < +infty & integral+ M,(max- h) < +infty ) by XXREAL_0:4;
then C4: h is_integrable_on M by B1, B6, MESFUNC5:def 17;
set AFN = |.(F . N).|;
( E = dom (F . N) & F . N is_integrable_on M & F . N is_measurable_on E ) by A2, A4, A1, MESFUNC8:def 2;
then |.(F . N).| is_integrable_on M by MESFUNC5:106;
then C5: |.(F . N).| + h is_integrable_on M by C4, MESFUNC5:114;

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 C6: |.(F . N).| is nonnegative by SUPINF_2:71;
then C7: ( dom (|.(F . N).| + h) = (dom |.(F . N).|) /\ (dom h) & |.(F . N).| + h is nonnegative ) by B2, MESFUNC5:28;
C9: dom (F . N) = dom |.(F . N).| by MESFUNC1:def 10;
then C8: E = dom |.(F . N).| by A1, MESFUNC8:def 2;

D1: now

D14: now

assume d: f . x in REAL ; :: thesis:

D17: 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 d, XXREAL_3:13, XXREAL_3:14;
hence contradiction by D13, EXTREAL2:67, XXREAL_0:9; :: thesis:

end;

D18: 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 d, XXREAL_3:13, XXREAL_3:14;
then 1. < |.(((F . N) . x) - (f . x)).| by EXTREAL2:67, XXREAL_0:9;
hence contradiction by D11, A8, XXREAL_0:2; :: thesis:

end;

end;

now

assume D25: ( f . x = +infty or f . x = -infty ) ; :: thesis:
( |.(((F . n) . x) - (f . x)).| < 1. & |.(((F . N) . x) - (f . x)).| < 1. ) by D13, XXREAL_0:2;
then ( - 1. < ((F . n) . x) - (f . x) & - 1. < ((F . N) . x) - (f . x) & ((F . n) . x) - (f . x) < 1. & ((F . N) . x) - (f . x) < 1. ) by EXTREAL2:58;
then ( ( (F . n) . x = +infty & (F . N) . x = +infty ) or ( (F . n) . x = -infty & (F . N) . x = -infty ) ) by D25, XXREAL_3:64, XXREAL_3:65;
hence |.((F . n) . x).| <= |.((F . N) . x).| + 1. by EXTREAL2:67, XXREAL_3:63; :: thesis:

end;

then D26: |.((F . n) . x).| <= (|.(F . N).| . x) + 1. by D12, D14, MESFUNC1:def 10, XXREAL_0:14;
dom (|.(F . N).| + h) = (dom |.(F . N).|) /\ (dom h) by B2, C6, MESFUNC5:28;
then dom (|.(F . N).| + h) = E /\ E by C9, A1, B1, MESFUNC8:def 2;
then (|.(F . N).| . x) + (h . x) = (|.(F . N).| + h) . x by D11, A1, MESFUNC1:def 3;
then D27: (|.(F . N).| . x) + 1. = (|.(F . N).| + h) . x by B1, D11, A1;
dom (F . n) = E by A1, MESFUNC8:def 2;
then x in dom |.(F . n).| by D11, A1, MESFUNC1:def 10;
hence |.(F . n).| . x <= (|.(F . N).| + h) . x by D26, D27, MESFUNC1:def 10; :: thesis:

end;

reconsider N1 = N as Element of NAT by ORDINAL1:def 13;
D3: 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:
assume D31: x in E ; :: thesis:
(F ^\ N1) . n = F . (n + N) by NAT_1:def 3;
hence |.((F ^\ N1) . n).| . x <= (|.(F . N).| + h) . x by D31, A1, D1, NAT_1:11; :: thesis:

end;

D5: 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 A4; :: thesis:

end;

D6: 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:
assume x in E ; :: thesis:
then D61: F # x is convergent by A1, A3, UCONV;

D62: 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;

(F # x) ^\ N1 is convergent by D61, RINFSUP2:21;
hence (F ^\ N1) # x is convergent by D62, FUNCT_2:113; :: thesis:
lim (F # x) = lim ((F # x) ^\ N1) by D61, RINFSUP2:21;
hence lim (F # x) = lim ((F ^\ N1) # x) by D62, FUNCT_2:113; :: thesis:

end;

(F ^\ N1) . 0 = F . (0 + N) by NAT_1:def 3;
then D4: dom ((F ^\ N1) . 0 ) = E by A1, MESFUNC8:def 2;
then dom (lim (F ^\ N1)) = E by MESFUNC8:def 10;
then D7: dom (lim F) = dom (lim (F ^\ N1)) by A1, MESFUNC8:def 10;

D8: now

let x be Element of X; :: thesis:
assume D81: x in dom (lim F) ; :: thesis:
then D82: lim ((F ^\ N1) # x) = (lim (F ^\ N1)) . x by D7, MESFUNC8:def 10;
x in E by D81, A1, MESFUNC8:def 10;
then lim (F # x) = lim ((F ^\ N1) # x) by D6;
hence (lim F) . x = (lim (F ^\ N1)) . x by D81, D82, MESFUNC8:def 10; :: thesis:

end;

consider J being ExtREAL_sequence such that
E1: ( ( for n being Nat holds J . n = Integral M,((F ^\ N1) . n) ) & lim_inf J >= Integral M,(lim_inf (F ^\ N1)) & lim_sup J <= Integral M,(lim_sup (F ^\ N1)) & ( ( 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 D4, D5, B1, C5, C7, C8, D3, Th136x;
E2: |.(lim_inf (F ^\ N1)).| is_integrable_on M by D4, D5, B1, C5, C7, C8, D3, Th136z;
E3: ( dom (lim_inf (F ^\ N1)) = dom ((F ^\ N1) . 0 ) & dom (lim (F ^\ N1)) = dom ((F ^\ N1) . 0 ) ) by MESFUNC8:def 8, MESFUNC8:def 10;

now

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

end;

then E4: lim (F ^\ N1) = lim_inf (F ^\ N1) by E3, PARTFUN1:34;
for x being Element of X st x in E holds
(F ^\ N1) # x is convergent by D6;
then lim (F ^\ N1) is_measurable_on E by D4, D5, MESFUNC8:25;
then E5: lim (F ^\ N1) is_integrable_on M by D4, E3, E4, E2, MESFUNC5:106;
deffunc H₁( Element of NAT ) -> Element of ExtREAL = Integral M,(F . $1);
consider I being Function of NAT ,ExtREAL such that
E6: for n being Element of NAT holds I . n = H₁(n) from FUNCT_2:sch 4();
reconsider I = I as ExtREAL_sequence ;
E7: 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 E6; :: thesis:

end;

now

let n be Element of NAT ; :: thesis:
E8: J . n = Integral M,((F ^\ N1) . n) by E1;
( (F ^\ N1) . n = F . (n + N) & (I ^\ N1) . n = I . (n + N) ) by NAT_1:def 3;
hence J . n = (I ^\ N1) . n by E8, E6; :: thesis:

end;

then J = I ^\ N1 by FUNCT_2:113;
then ( I is convergent & lim I = lim J ) by E1, D6, RINFSUP2:17;
then ( I is convergent & lim I = Integral M,(lim F) ) by D6, E1, D8, D7, 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 E5, E7, A6, D8, D7, PARTFUN1:34; :: thesis: