let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let f be with_the_same_dom Functional_Sequence of X,ExtREAL; :: thesis:
let g be PartFunc of X,ExtREAL; :: thesis:
let E be Element of S; :: thesis:
assume that
A1: M . E < +infty and
A2: dom (f . 0) = E and
A3: for n being natural number holds
( f . n is_measurable_on E & f . n is real-valued ) and
A4: dom g = E and
A5: for x being Element of X st x in E holds
( f # x is convergent_to_finite_number & g . x = lim (f # x) ) ; :: thesis:
let r, e be real number ; :: thesis:
defpred S₁[ Element of NAT , set ] means $2 = E /\ (less_dom (|.((f . $1) - g).|,(R_EAL e)));
A6: g is real-valued by A4, A5, Th27;
for x being Element of X st x in E holds
( f # x is convergent & g . x = lim (f # x) )

let x be Element of X; :: thesis:
assume A7: x in E ; :: thesis:
then f # x is convergent_to_finite_number by A5;
hence f # x is convergent by MESFUNC5:def 11; :: thesis:
thus g . x = lim (f # x) by A5, A7; :: thesis:

end;

then A8: g is_measurable_on E by A2, A3, A4, Th26;
A9: for n being Element of NAT holds
( |.((f . n) - g).| is_measurable_on E & dom ((f . n) - g) = E & dom |.((f . n) - g).| = E )

proof

let n be Element of NAT ; :: thesis:
A10: f . n is real-valued by A3;
dom ((f . n) - g) = (dom (f . n)) /\ (dom g) by A6, MESFUNC2:2;
then A11: dom ((f . n) - g) = E /\ E by A2, A4, Def2;
f . n is_measurable_on E by A3;
then (f . n) - g is_measurable_on E by A4, A8, A6, A10, MESFUNC2:11;
hence ( |.((f . n) - g).| is_measurable_on E & dom ((f . n) - g) = E & dom |.((f . n) - g).| = E ) by A11, MESFUNC1:def 10, MESFUNC2:27; :: thesis:

end;

A12: for n being Element of NAT ex Z being Element of S st S₁[n,Z]

proof

let n be Element of NAT ; :: thesis:
|.((f . n) - g).| is_measurable_on E by A9;
then E /\ (less_dom (|.((f . n) - g).|,(R_EAL e))) in S by MESFUNC1:def 16;
hence ex Z being Element of S st S₁[n,Z] ; :: thesis:

end;

consider K being Function of NAT,S such that
A13: for n being Element of NAT holds S₁[n,K . n] from FUNCT_2:sch 10(A12);
defpred S₂[ Element of NAT , set ] means $2 = { x where x is Element of X : for k being natural number st $1 <= k holds
x in K . k } ;
A14: for n being Element of NAT ex Z being Element of S st S₂[n,Z]

proof

let n be Element of NAT ; :: thesis:
take { x where x is Element of X : for k being natural number st n <= k holds
x in K . k } ; :: thesis:
thus ( { x where x is Element of X : for k being natural number st n <= k holds
x in K . k } is Element of bool X & { x where x is Element of X : for k being natural number st n <= k holds
x in K . k } is Element of S & S₂[n, { x where x is Element of X : for k being natural number st n <= k holds
x in K . k } ] ) by Th1; :: thesis:

end;

consider EN being Function of NAT,S such that
A15: for n being Element of NAT holds S₂[n,EN . n] from FUNCT_2:sch 10(A14);
A16: 0. <= M . E by MEASURE1:def 2;
then reconsider ME = M . E as Real by A1, XXREAL_0:14;
defpred S₃[ Element of NAT , set ] means $2 = M . (EN . $1);
A17: for n being natural number holds
( EN . n c= E & M . (EN . n) <= M . E & M . (EN . n) is Element of REAL & M . (E \ (EN . n)) = (M . E) - (M . (EN . n)) & M . (E \ (EN . n)) is Element of REAL )

proof

reconsider r1 = M . E as Real by A1, A16, XXREAL_0:14;
let n be natural number ; :: thesis:
reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
thus A18: EN . n c= E :: thesis:

proof

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume z in EN . n ; :: thesis:
then z in { x where x is Element of X : for k being natural number st n9 <= k holds
x in K . k } by A15;
then ex x being Element of X st
( z = x & ( for k being natural number st n <= k holds
x in K . k ) ) ;
then z in K . n ;
then z in E /\ (less_dom (|.((f . n9) - g).|,(R_EAL e))) by A13;
hence z in E by XBOOLE_0:def 4; :: thesis:

end;

hence A19: M . (EN . n) <= M . E by MEASURE1:31; :: thesis:
A20: -infty < M . (EN . n) by MEASURE1:def 2;
then reconsider r2 = M . (EN . n) as Real by A1, A19, XXREAL_0:14;
thus M . (EN . n) is Element of REAL by A1, A19, A20, XXREAL_0:14; :: thesis:
thus M . (E \ (EN . n)) = (M . E) - (M . (EN . n)) by A1, A18, A19, MEASURE1:32, XXREAL_0:4; :: thesis:
(M . E) - (M . (EN . n)) = r1 - r2 by SUPINF_2:3;
hence M . (E \ (EN . n)) is Element of REAL by A18, MEASURE1:32, XXREAL_0:4; :: thesis:

end;

A21: now

let n be Element of NAT ; :: thesis:
M . (EN . n) is Element of REAL by A17;
hence ex y being Element of REAL st S₃[n,y] ; :: thesis:

end;

consider seq1 being Real_Sequence such that
A22: for n being Element of NAT holds S₃[n,seq1 . n] from FUNCT_2:sch 10(A21);
assume A23: 0 < r ; :: thesis:
assume A24: 0 < e ; :: thesis:
A25: E c= union (rng EN)

proof

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume A26: z in E ; :: thesis:
then reconsider x = z as Element of X ;
A27: ( not lim (f # x) = +infty or not f # x is convergent_to_+infty ) by A5, A26, MESFUNC5:50;
f # x is convergent_to_finite_number by A5, A26;
then A28: f # x is convergent by MESFUNC5:def 11;
( not lim (f # x) = -infty or not f # x is convergent_to_-infty ) by A5, A26, MESFUNC5:51;
then ex g being real number st
( lim (f # x) = g & ( for p being real number st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((f # x) . m) - (lim (f # x))).| < p ) & f # x is convergent_to_finite_number ) by A28, A27, MESFUNC5:def 12;
then consider n being Nat such that
A29: for m being Nat st n <= m holds
|.(((f # x) . m) - (lim (f # x))).| < e by A24;
reconsider n0 = n as Element of NAT by ORDINAL1:def 12;
A30: g . x = lim (f # x) by A5, A26;

now

let k be natural number ; :: thesis:
reconsider k9 = k as Element of NAT by ORDINAL1:def 12;
A31: dom |.((f . k9) - g).| = E by A9;
assume n0 <= k ; :: thesis:
then |.(((f # x) . k) - (lim (f # x))).| < e by A29;
then A32: |.(((f . k) . x) - (g . x)).| < e by A30, MESFUNC5:def 13;
dom ((f . k9) - g) = E by A9;
then |.(((f . k) - g) . x).| < e by A26, A32, MESFUNC1:def 4;
then |.((f . k) - g).| . x < e by A26, A31, MESFUNC1:def 10;
then x in less_dom (|.((f . k) - g).|,(R_EAL e)) by A26, A31, MESFUNC1:def 11;
then x in E /\ (less_dom (|.((f . k) - g).|,(R_EAL e))) by A26, XBOOLE_0:def 4;
then x in K . k9 by A13;
hence x in K . k ; :: thesis:

end;

then x in { y where y is Element of X : for k being natural number st n0 <= k holds
y in K . k } ;
then A33: x in EN . n0 by A15;
EN . n0 in rng EN by FUNCT_2:4;
hence z in union (rng EN) by A33, TARSKI:def 4; :: thesis:

end;

defpred S₄[ Element of NAT , set ] means $2 = M . (E \ (EN . $1));
A34: dom (M * EN) = NAT by FUNCT_2:def 1;
A35: for n, m being Element of NAT st n <= m holds
( EN . n c= EN . m & M . (EN . n) <= M . (EN . m) )

proof

let n, m be Element of NAT ; :: thesis:
assume A36: n <= m ; :: thesis:
thus EN . n c= EN . m :: thesis:

proof

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume z in EN . n ; :: thesis:
then z in { x where x is Element of X : for k being natural number st n <= k holds
x in K . k } by A15;
then A37: ex x being Element of X st
( z = x & ( for k being natural number st n <= k holds
x in K . k ) ) ;
then for k being natural number st m <= k holds
z in K . k by A36, XXREAL_0:2;
then z in { y where y is Element of X : for k being natural number st m <= k holds
y in K . k } by A37;
hence z in EN . m by A15; :: thesis:

end;

hence M . (EN . n) <= M . (EN . m) by MEASURE1:31; :: thesis:

end;

set seq3 = NAT --> ME;
A38: for n being Nat holds (NAT --> ME) . n = ME

proof

let n be Nat; :: thesis:
n in NAT by ORDINAL1:def 12;
hence (NAT --> ME) . n = ME by FUNCOP_1:7; :: thesis:

end;

then A39: NAT --> ME is constant by VALUED_0:def 18;

A40: now

let x be set ; :: thesis:
assume A41: x in dom (M * EN) ; :: thesis:
then reconsider n = x as Element of NAT ;
(M * EN) . x = M . (EN . n) by A41, FUNCT_1:12;
hence (M * EN) . x = seq1 . x by A22; :: thesis:

end;

dom seq1 = NAT by FUNCT_2:def 1;
then A42: M * EN = seq1 by A34, A40, FUNCT_1:2;

now

let y be set ; :: thesis:
assume y in rng EN ; :: thesis:
then consider x being set such that
A43: x in NAT and
A44: y = EN . x by FUNCT_2:11;
reconsider x9 = x as natural number by A43;
y = EN . x9 by A44;
hence y c= E by A17; :: thesis:

end;

then union (rng EN) c= E by ZFMISC_1:76;
then A45: union (rng EN) = E by A25, XBOOLE_0:def 10;
A46: ( seq1 is convergent & lim seq1 = M . E )

proof

reconsider r1 = M . E as Real by A1, A16, XXREAL_0:14;
A47: for n being Element of NAT holds EN . n c= EN . (n + 1)

proof

let n be Element of NAT ; :: thesis:
n <= n + 1 by NAT_1:12;
hence EN . n c= EN . (n + 1) by A35; :: thesis:

end;

A48: now

let n be Element of NAT ; :: thesis:
M . (EN . n) <= M . E by A17;
then A49: seq1 . n <= r1 by A22;
r1 + 0 < r1 + 1 by XREAL_1:8;
hence seq1 . n < r1 + 1 by A49, XXREAL_0:2; :: thesis:

end;

then A50: seq1 is bounded_above by SEQ_2:def 3;
consider r being real number such that
A51: for n being Element of NAT holds seq1 . n < r by A48;
r is UpperBound of rng seq1

proof

let d be ext-real number ; :: according to XXREAL_2:def 1 :: thesis:
assume d in rng seq1 ; :: thesis:
then ex x being set st
( x in NAT & d = seq1 . x ) by FUNCT_2:11;
hence d <= r by A51; :: thesis:

end;

then rng seq1 is bounded_above by XXREAL_2:def 10;
then A52: sup (rng (M * EN)) = upper_bound (rng seq1) by A42, RINFSUP2:1;

now

let n, m be Element of NAT ; :: thesis:
assume A53: n <= m ; :: thesis:
A54: seq1 . m = M . (EN . m) by A22;
seq1 . n = M . (EN . n) by A22;
hence seq1 . n <= seq1 . m by A35, A53, A54; :: thesis:

end;

then A55: seq1 is non-decreasing by SEQM_3:6;
hence seq1 is convergent by A50; :: thesis:
lim seq1 = upper_bound seq1 by A55, A50, RINFSUP1:24;
hence lim seq1 = M . E by A45, A52, A47, MEASURE2:23; :: thesis:

end;

A56: now

let n be Element of NAT ; :: thesis:
M . (E \ (EN . n)) is Element of REAL by A17;
hence ex y being Element of REAL st S₄[n,y] ; :: thesis:

end;

consider seq2 being Real_Sequence such that
A57: for n being Element of NAT holds S₄[n,seq2 . n] from FUNCT_2:sch 10(A56);

now

let n be Element of NAT ; :: thesis:
seq2 . n = M . (E \ (EN . n)) by A57;
then A58: seq2 . n = (M . E) - (M . (EN . n)) by A17;
M . (EN . n) = seq1 . n by A22;
then seq2 . n = ME - (seq1 . n) by A58, SUPINF_2:3;
then seq2 . n = ((NAT --> ME) . n) - (seq1 . n) by A38;
hence seq2 . n = ((NAT --> ME) . n) + ((- seq1) . n) by SEQ_1:10; :: thesis:

end;

then A59: seq2 = (NAT --> ME) - seq1 by SEQ_1:7;
then A60: seq2 is convergent by A46, A39, SEQ_2:11;
A61: (NAT --> ME) . 0 = ME by A38;
lim seq2 = (lim (NAT --> ME)) - (lim seq1) by A46, A59, A39, SEQ_2:12;
then lim seq2 = ME - ME by A46, A39, A61, SEQ_4:25;
then consider N being Element of NAT such that
A62: for m being Element of NAT st N <= m holds
abs ((seq2 . m) - 0) < r by A23, A60, SEQ_2:def 7;
reconsider H = E \ (EN . N) as Element of S ;
A63: E \ H = E /\ (EN . N) by XBOOLE_1:48;
EN . N c= E by A17;
then A64: E \ H = EN . N by A63, XBOOLE_1:28;
A65: for k being natural number st N < k holds
for x being Element of X st x in E \ H holds
|.(((f . k) . x) - (g . x)).| < e

proof

let k be natural number ; :: thesis:
reconsider k9 = k as Element of NAT by ORDINAL1:def 12;
assume A66: N < k ; :: thesis:
let x be Element of X; :: thesis:
assume x in E \ H ; :: thesis:
then x in { y where y is Element of X : for k being natural number st N <= k holds
y in K . k } by A15, A64;
then ex y being Element of X st
( x = y & ( for k being natural number st N <= k holds
y in K . k ) ) ;
then x in K . k by A66;
then A67: x in E /\ (less_dom (|.((f . k9) - g).|,(R_EAL e))) by A13;
then A68: x in E by XBOOLE_0:def 4;
x in less_dom (|.((f . k) - g).|,(R_EAL e)) by A67, XBOOLE_0:def 4;
then A69: |.((f . k) - g).| . x < R_EAL e by MESFUNC1:def 11;
A70: dom ((f . k9) - g) = E by A9;
dom |.((f . k9) - g).| = E by A9;
then |.(((f . k) - g) . x).| < e by A68, A69, MESFUNC1:def 10;
hence |.(((f . k) . x) - (g . x)).| < e by A68, A70, MESFUNC1:def 4; :: thesis:

end;

take H ; :: thesis:
take N ; :: thesis:
M . (E \ (EN . N)) = seq2 . N by A57;
then A71: 0 <= seq2 . N by MEASURE1:def 2;
abs ((seq2 . N) - 0) < r by A62;
then seq2 . N < r by A71, ABSVALUE:def 1;
hence ( H c= E & M . H < r & ( for k being natural number st N < k holds
for x being Element of X st x in E \ H holds
|.(((f . k) . x) - (g . x)).| < e ) ) by A57, A65, XBOOLE_1:36; :: thesis: