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 Nat holds
( f . n is E -measurable & 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; :: thesis:
defpred S₁[ Element of NAT , set ] means $2 = E /\ (less_dom (|.((f . $1) - g).|,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 E -measurable by A2, A3, A4, Th26;
A9: for n being Element of NAT holds
( |.((f . n) - g).| is E -measurable & 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 E -measurable by A3;
then (f . n) - g is E -measurable by A4, A8, A6, A10, MESFUNC2:11;
hence ( |.((f . n) - g).| is E -measurable & 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 E -measurable by A9;
then E /\ (less_dom (|.((f . n) - g).|,e)) in S by MESFUNC1:def 16;
hence ex Z being Element of S st S₁[n,Z] ; :: thesis:

end;

consider K being sequence of S such that
A13: for n being Element of NAT holds S₁[n,K . n] from FUNCT_2:sch 3(A12);
defpred S₂[ Nat, set ] means $2 = { x where x is Element of X : for k being Nat 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 Nat st n <= k holds
x in K . k } ; :: thesis:
thus ( { x where x is Element of X : for k being Nat st n <= k holds
x in K . k } is Element of bool X & { x where x is Element of X : for k being Nat st n <= k holds
x in K . k } is Element of S & S₂[n, { x where x is Element of X : for k being Nat st n <= k holds
x in K . k } ] ) by Th1; :: thesis:

end;

consider EN being sequence of S such that
A15: for n being Element of NAT holds S₂[n,EN . n] from FUNCT_2:sch 3(A14);
A16: for n being Nat holds S₂[n,EN . n]

proof

let n be Nat; :: thesis:
n in NAT by ORDINAL1:def 12;
hence S₂[n,EN . n] by A15; :: thesis:

end;

A17: 0. <= M . E by MEASURE1:def 2;
then reconsider ME = M . E as Element of REAL by A1, XXREAL_0:14;
defpred S₃[ Element of NAT , set ] means $2 = M . (EN . $1);
A18: for n being Nat 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 Element of REAL by A1, A17, XXREAL_0:14;
let n be Nat; :: thesis:
reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
thus A19: EN . n c= E :: thesis:

proof

let z be object ; :: 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 Nat st n9 <= k holds
x in K . k } by A16;
then ex x being Element of X st
( z = x & ( for k being Nat st n <= k holds
x in K . k ) ) ;
then z in K . n ;
then z in E /\ (less_dom (|.((f . n9) - g).|,e)) by A13;
hence z in E by XBOOLE_0:def 4; :: thesis:

end;

hence A20: M . (EN . n) <= M . E by MEASURE1:31; :: thesis:
A21: -infty < M . (EN . n) by MEASURE1:def 2;
then reconsider r2 = M . (EN . n) as Element of REAL by A1, A20, XXREAL_0:14;
thus M . (EN . n) is Element of REAL by A1, A20, A21, XXREAL_0:14; :: thesis:
thus M . (E \ (EN . n)) = (M . E) - (M . (EN . n)) by A1, A19, A20, 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 A19, MEASURE1:32, XXREAL_0:4; :: thesis:

end;

A22: now :: thesis:

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

end;

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

proof

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

now :: thesis:

end;

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

end;

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

proof

let n, m be Nat; :: thesis:
assume A37: n <= m ; :: thesis:
thus EN . n c= EN . m :: thesis:

proof

let z be object ; :: 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 Nat st n <= k holds
x in K . k } by A16;
then A38: ex x being Element of X st
( z = x & ( for k being Nat st n <= k holds
x in K . k ) ) ;
then for k being Nat st m <= k holds
z in K . k by A37, XXREAL_0:2;
then z in { y where y is Element of X : for k being Nat st m <= k holds
y in K . k } by A38;
hence z in EN . m by A16; :: thesis:

end;

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

end;

set seq3 = NAT --> ME;
A39: for n being Nat holds (NAT --> ME) . n = ME by ORDINAL1:def 12, FUNCOP_1:7;
then A40: NAT --> ME is constant by VALUED_0:def 18;

A41: now :: thesis:

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

end;

dom seq1 = NAT by FUNCT_2:def 1;
then A43: M * EN = seq1 by A35, A41, FUNCT_1:2;

now :: thesis:

let y be set ; :: thesis:
assume y in rng EN ; :: thesis:
then consider x being object such that
A44: x in NAT and
A45: y = EN . x by FUNCT_2:11;
reconsider x9 = x as Nat by A44;
y = EN . x9 by A45;
hence y c= E by A18; :: thesis:

end;

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

proof

reconsider r1 = M . E as Element of REAL by A1, A17, XXREAL_0:14;
A48: for n being Nat holds EN . n c= EN . (n + 1)

proof

let n be Nat; :: thesis:
n <= n + 1 by NAT_1:12;
hence EN . n c= EN . (n + 1) by A36; :: thesis:

end;

A49: now :: thesis:

let n be Nat; :: thesis:
A50: n in NAT by ORDINAL1:def 12;
M . (EN . n) <= M . E by A18;
then A51: seq1 . n <= r1 by A23, A50;
r1 + 0 < r1 + 1 by XREAL_1:8;
hence seq1 . n < r1 + 1 by A51, XXREAL_0:2; :: thesis:

end;

then A52: seq1 is bounded_above by SEQ_2:def 3;
consider r being Real such that
A53: for n being Nat holds seq1 . n < r by A49;
r is UpperBound of rng seq1

proof

let d be ExtReal; :: according to XXREAL_2:def 1 :: thesis:
assume d in rng seq1 ; :: thesis:
then ex x being object st
( x in NAT & d = seq1 . x ) by FUNCT_2:11;
hence d <= r by A53; :: thesis:

end;

then rng seq1 is bounded_above ;
then A54: sup (rng (M * EN)) = upper_bound (rng seq1) by A43, RINFSUP2:1;

now :: thesis:

let n, m be Nat; :: thesis:
assume A55: n <= m ; :: thesis:
A56: n in NAT by ORDINAL1:def 12;
A57: m in NAT by ORDINAL1:def 12;
A58: seq1 . m = M . (EN . m) by A23, A57;
seq1 . n = M . (EN . n) by A23, A56;
hence seq1 . n <= seq1 . m by A36, A55, A58; :: thesis:

end;

then A59: seq1 is non-decreasing by SEQM_3:6;
hence seq1 is convergent by A52; :: thesis:
lim seq1 = upper_bound seq1 by A59, A52, RINFSUP1:24;
hence lim seq1 = M . E by A46, A54, A48, MEASURE2:23; :: thesis:

end;

A60: now :: thesis:

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

end;

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

now :: thesis:

let n be Nat; :: thesis:
A62: n in NAT by ORDINAL1:def 12;
seq2 . n = M . (E \ (EN . n)) by A61, A62;
then A63: seq2 . n = (M . E) - (M . (EN . n)) by A18;
M . (EN . n) = seq1 . n by A23, A62;
then seq2 . n = ME - (seq1 . n) by A63, SUPINF_2:3;
then seq2 . n = ((NAT --> ME) . n) - (seq1 . n) by A39;
hence seq2 . n = ((NAT --> ME) . n) + ((- seq1) . n) by SEQ_1:10; :: thesis:

end;

then A64: seq2 = (NAT --> ME) - seq1 by SEQ_1:7;
then A65: seq2 is convergent by A47, A40;
A66: (NAT --> ME) . 0 = ME by A39;
lim seq2 = (lim (NAT --> ME)) - (lim seq1) by A47, A64, A40, SEQ_2:12;
then lim seq2 = ME - ME by A47, A40, A66, SEQ_4:25;
then consider N being Nat such that
A67: for m being Nat st N <= m holds
|.((seq2 . m) - 0).| < r by A24, A65, SEQ_2:def 7;
reconsider H = E \ (EN . N) as Element of S ;
A68: E \ H = E /\ (EN . N) by XBOOLE_1:48;
EN . N c= E by A18;
then A69: E \ H = EN . N by A68, XBOOLE_1:28;
A70: for k being Nat 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 Nat; :: thesis:
reconsider k9 = k as Element of NAT by ORDINAL1:def 12;
assume A71: 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 Nat st N <= k holds
y in K . k } by A16, A69;
then ex y being Element of X st
( x = y & ( for k being Nat st N <= k holds
y in K . k ) ) ;
then x in K . k by A71;
then A72: x in E /\ (less_dom (|.((f . k9) - g).|,e)) by A13;
then A73: x in E by XBOOLE_0:def 4;
x in less_dom (|.((f . k) - g).|,e) by A72, XBOOLE_0:def 4;
then A74: |.((f . k) - g).| . x < e by MESFUNC1:def 11;
A75: dom ((f . k9) - g) = E by A9;
dom |.((f . k9) - g).| = E by A9;
then |.(((f . k) - g) . x).| < e by A73, A74, MESFUNC1:def 10;
hence |.(((f . k) . x) - (g . x)).| < e by A73, A75, MESFUNC1:def 4; :: thesis:

end;

take H ; :: thesis:
take N ; :: thesis:
A76: N in NAT by ORDINAL1:def 12;
M . (E \ (EN . N)) = seq2 . N by A61, A76;
then A77: 0 <= seq2 . N by MEASURE1:def 2;
|.((seq2 . N) - 0).| < r by A67;
then seq2 . N < r by A77, ABSVALUE:def 1;
hence ( H c= E & M . H < r & ( for k being Nat st N < k holds
for x being Element of X st x in E \ H holds
|.(((f . k) . x) - (g . x)).| < e ) ) by A61, A70, XBOOLE_1:36, A76; :: thesis: