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:
assume A6: 0 < r ; :: thesis:
assume A7: 0 < e ; :: thesis:
for x being Element of X st x in E holds
( f # x is convergent & g . x = lim (f # x) )

proof

let x be Element of X; :: thesis:
assume A8: 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, A8; :: thesis:

end;

then A9: g is_measurable_on E by A2, A3, A4, Th26;
A10: g is real-valued by A4, A5, Th27;
A11: 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:
( dom (f . n) = E & f . n is_measurable_on E & f . n is real-valued ) by A2, A3, Def2;
then A12: (f . n) - g is_measurable_on E by A4, A9, A10, MESFUNC2:13;
dom ((f . n) - g) = (dom (f . n)) /\ (dom g) by A10, MESFUNC2:2;
then dom ((f . n) - g) = E /\ E by A2, A4, Def2;
hence ( |.((f . n) - g).| is_measurable_on E & dom ((f . n) - g) = E & dom |.((f . n) - g).| = E ) by A12, MESFUNC1:def 10, MESFUNC2:29; :: thesis:

end;

defpred S₁[ Element of NAT , set ] means $2 = E /\ (less_dom |.((f . $1) - g).|,(R_EAL e));
A13: 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 A11;
then E /\ (less_dom |.((f . n) - g).|,(R_EAL e)) in S by MESFUNC1:def 17;
hence ex Z being Element of S st S₁[n,Z] ; :: thesis:

end;

consider K being Function of NAT ,S such that
A14: for n being Element of NAT holds S₁[n,K . n] from FUNCT_2:sch 10(A13);
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 } ;
A15: 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 Z = { x where x is Element of X : for k being natural number st n <= k holds
x in K . k } ; :: thesis:
thus ( Z is Element of bool X & Z is Element of S & S₂[n,Z] ) by Th1; :: thesis:

end;

consider EN being Function of NAT ,S such that
A16: for n being Element of NAT holds S₂[n,EN . n] from FUNCT_2:sch 10(A15);
A18: 0. <= M . E by MEASURE1:def 4;
A19: 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

let n be natural number ; :: thesis:
reconsider n' = n as Element of NAT by ORDINAL1:def 13;
thus A20: 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 n' <= k holds
x in K . k } by A16;
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 . n') - g).|,(R_EAL e)) by A14;
hence z in E by XBOOLE_0:def 4; :: thesis:

end;

hence A21: M . (EN . n) <= M . E by MEASURE1:62; :: thesis:
A22: -infty < M . (EN . n) by MEASURE1:def 4;
hence M . (EN . n) is Element of REAL by A1, A21, XXREAL_0:14; :: thesis:
A23: M . (EN . n) < +infty by A1, A21, XXREAL_0:4;
hence M . (E \ (EN . n)) = (M . E) - (M . (EN . n)) by A20, MEASURE1:63; :: thesis:
reconsider r1 = M . E as Real by A1, A18, XXREAL_0:14;
reconsider r2 = M . (EN . n) as Real by A1, A21, A22, XXREAL_0:14;
(M . E) - (M . (EN . n)) = r1 - r2 by SUPINF_2:5;
hence M . (E \ (EN . n)) is Element of REAL by A20, A23, MEASURE1:63; :: thesis:

end;

A24: 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 A25: 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 A16;
then A26: 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 A25, 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 A26;
hence z in EN . m by A16; :: thesis:

end;

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

end;

defpred S₃[ Element of NAT , set ] means $2 = M . (EN . $1);

A27: now

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

end;

consider seq1 being Real_Sequence such that
A28: for n being Element of NAT holds S₃[n,seq1 . n] from FUNCT_2:sch 10(A27);
A29: ( dom (M * EN) = NAT & dom seq1 = NAT ) by FUNCT_2:def 1;

now

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

end;

then A31: M * EN = seq1 by A29, FUNCT_1:9;
A32: union (rng EN) = E

proof

now

let y be set ; :: thesis:
assume y in rng EN ; :: thesis:
then consider x being set such that
A33: ( x in NAT & y = EN . x ) by FUNCT_2:17;
reconsider x' = x as natural number by A33;
y = EN . x' by A33;
hence y c= E by A19; :: thesis:

end;

then A34: union (rng EN) c= E by ZFMISC_1:94;
E c= union (rng EN)

proof

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume A35: z in E ; :: thesis:
then reconsider x = z as Element of X ;
A36: ( f # x is convergent_to_finite_number & g . x = lim (f # x) ) by A5, A35;
then A37: f # x is convergent by MESFUNC5:def 11;
( ( not lim (f # x) = -infty or not f # x is convergent_to_-infty ) & ( not lim (f # x) = +infty or not f # x is convergent_to_+infty ) ) by A36, MESFUNC5:56, MESFUNC5:57;
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 A37, MESFUNC5:def 12;
then consider n being Nat such that
A38: for m being Nat st n <= m holds
|.(((f # x) . m) - (lim (f # x))).| < e by A7;
reconsider n0 = n as Element of NAT by ORDINAL1:def 13;

now

let k be natural number ; :: thesis:
reconsider k' = k as Element of NAT by ORDINAL1:def 13;
assume A39: n0 <= k ; :: thesis:
A40: dom ((f . k') - g) = E by A11;
A41: dom |.((f . k') - g).| = E by A11;
|.(((f # x) . k) - (lim (f # x))).| < e by A38, A39;
then |.(((f . k) . x) - (g . x)).| < e by A36, MESFUNC5:def 13;
then |.(((f . k) - g) . x).| < e by A35, A40, MESFUNC1:def 4;
then |.((f . k) - g).| . x < e by A35, A41, MESFUNC1:def 10;
then x in less_dom |.((f . k) - g).|,(R_EAL e) by A35, A41, MESFUNC1:def 12;
then x in E /\ (less_dom |.((f . k) - g).|,(R_EAL e)) by A35, XBOOLE_0:def 4;
then x in K . k' by A14;
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 A42: x in EN . n0 by A16;
EN . n0 in rng EN by FUNCT_2:6;
hence z in union (rng EN) by A42, TARSKI:def 4; :: thesis:

end;

hence union (rng EN) = E by A34, XBOOLE_0:def 10; :: thesis:

end;

A43: ( seq1 is convergent & lim seq1 = M . E )

proof

now

let n, m be Element of NAT ; :: thesis:
assume A44: n <= m ; :: thesis:
( seq1 . n = M . (EN . n) & seq1 . m = M . (EN . m) ) by A28;
hence seq1 . n <= seq1 . m by A24, A44; :: thesis:

end;

then A45: seq1 is non-decreasing by SEQM_3:12;
reconsider r1 = M . E as Real by A1, A18, XXREAL_0:14;

A46: now

let n be Element of NAT ; :: thesis:
M . (EN . n) <= M . E by A19;
then A47: seq1 . n <= r1 by A28;
r1 + 0 < r1 + 1 by XREAL_1:10;
hence seq1 . n < r1 + 1 by A47, XXREAL_0:2; :: thesis:

end;

then A48: seq1 is bounded_above by SEQ_2:def 3;
hence seq1 is convergent by A45; :: thesis:
consider r being real number such that
A49: for n being Element of NAT holds seq1 . n < r by A46;

now

let d be real number ; :: thesis:
assume d in rng seq1 ; :: thesis:
then ex x being set st
( x in NAT & d = seq1 . x ) by FUNCT_2:17;
hence d <= r by A49; :: thesis:

end;

then rng seq1 is bounded_above by SEQ_4:def 1;
then A50: sup (rng (M * EN)) = sup (rng seq1) by A31, RINFSUP2:1;
A51: 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 A24; :: thesis:

end;

lim seq1 = sup seq1 by A45, A48, RINFSUP1:24;
hence lim seq1 = M . E by A32, A50, A51, MEASURE2:27; :: thesis:

end;

defpred S₄[ Element of NAT , set ] means $2 = M . (E \ (EN . $1));

A52: now

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

end;

consider seq2 being Real_Sequence such that
A53: for n being Element of NAT holds S₄[n,seq2 . n] from FUNCT_2:sch 10(A52);
reconsider ME = M . E as Real by A1, A18, XXREAL_0:14;
set seq3 = NAT --> ME;
B54: for n being Nat holds (NAT --> ME) . n = ME

proof

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

end;

now

let n be Element of NAT ; :: thesis:
A55: M . (EN . n) = seq1 . n by A28;
seq2 . n = M . (E \ (EN . n)) by A53;
then seq2 . n = (M . E) - (M . (EN . n)) by A19;
then seq2 . n = ME - (seq1 . n) by A55, SUPINF_2:5;
then seq2 . n = ((NAT --> ME) . n) - (seq1 . n) by B54;
hence seq2 . n = ((NAT --> ME) . n) + ((- seq1) . n) by SEQ_1:14; :: thesis:

end;

then A56: seq2 = (NAT --> ME) - seq1 by SEQ_1:11;
A57: NAT --> ME is constant by B54, VALUED_0:def 18;
then A58: NAT --> ME is convergent ;
A59: (NAT --> ME) . 0 = ME by B54;
A60: seq2 is convergent by A43, A56, A58, SEQ_2:25;
lim seq2 = (lim (NAT --> ME)) - (lim seq1) by A43, A56, A58, SEQ_2:26;
then lim seq2 = ME - ME by A43, A57, A59, SEQ_4:40;
then consider N being Element of NAT such that
A61: for m being Element of NAT st N <= m holds
abs ((seq2 . m) - 0 ) < r by A6, A60, SEQ_2:def 7;
A62: abs ((seq2 . N) - 0 ) < r by A61;
M . (E \ (EN . N)) = seq2 . N by A53;
then 0 <= seq2 . N by MEASURE1:def 4;
then A63: seq2 . N < r by A62, ABSVALUE:def 1;
reconsider H = E \ (EN . N) as Element of S ;
take H ; :: thesis:
take N ; :: thesis:
( E \ H = E /\ (EN . N) & EN . N c= E ) by A19, XBOOLE_1:48;
then A64: E \ H = EN . N by XBOOLE_1:28;
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 k' = k as Element of NAT by ORDINAL1:def 13;
assume A65: 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 A16, 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 A65;
then x in E /\ (less_dom |.((f . k') - g).|,(R_EAL e)) by A14;
then A66: ( x in E & x in less_dom |.((f . k) - g).|,(R_EAL e) ) by XBOOLE_0:def 4;
then A67: |.((f . k) - g).| . x < R_EAL e by MESFUNC1:def 12;
A68: dom ((f . k') - g) = E by A11;
dom |.((f . k') - g).| = E by A11;
then |.(((f . k) - g) . x).| < e by A66, A67, MESFUNC1:def 10;
hence |.(((f . k) . x) - (g . x)).| < e by A66, A68, MESFUNC1:def 4; :: thesis:

end;

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 A53, A63, XBOOLE_1:36; :: thesis: