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: ( dom (f . 0 ) = E & ( for n being natural number holds f . n is_measurable_on E ) ) and
A2: M . E < +infty and
A3: for n being natural number ex L being Element of S st
( L c= E & M . (E \ L) = 0 & ( for x being Element of X st x in L holds
|.((f . n) . x).| < +infty ) ) and
A4: ex G being Element of S st
( G c= E & M . (E \ G) = 0 & ( for x being Element of X st x in E holds
f # x is convergent_to_finite_number ) & dom g = E & ( for x being Element of X st x in G holds
g . x = lim (f # x) ) ) ; :: thesis:
let e0 be real number ; :: thesis:
assume A5: 0 < e0 ; :: thesis:
set e = e0 / 2;
defpred S₁[ Element of NAT , set ] means ( $2 c= E & M . (E \ $2) = 0 & ( for x being Element of X st x in $2 holds
|.((f . $1) . x).| < +infty ) );
A6: for n being Element of NAT ex Z being Element of S st S₁[n,Z] by A3;
consider LN being Function of NAT ,S such that
A7: for n being Element of NAT holds S₁[n,LN . n] from FUNCT_2:sch 10(A6);
consider G being Element of S such that
A8: ( G c= E & M . (E \ G) = 0 & ( for x being Element of X st x in E holds
f # x is convergent_to_finite_number ) & dom g = E & ( for x being Element of X st x in G holds
g . x = lim (f # x) ) ) by A4;
rng LN is N_Sub_set_fam of X by MEASURE1:52;
then rng LN is N_Measure_fam of S by MEASURE2:def 1;
then reconsider MRLN = meet (rng LN) as Element of S by MEASURE2:3;
MRLN /\ G is Element of S ;
then reconsider L = (meet (rng LN)) /\ G as Element of S ;
A9: E \ L = (E \ (meet (rng LN))) \/ (E \ G) by XBOOLE_1:54;
deffunc H₁( Element of NAT ) -> Element of S = E \ (LN . $1);
consider ELN being Function of NAT ,S such that
A10: for n being Element of NAT holds ELN . n = H₁(n) from FUNCT_2:sch 4();
rng ELN is N_Sub_set_fam of X by MEASURE1:52;
then reconsider RELN = rng ELN as N_Measure_fam of S by MEASURE2:def 1;
for A being set st A in RELN holds
A is measure_zero of M

proof

let A be set ; :: thesis:
assume A in RELN ; :: thesis:
then consider n being set such that
A11: ( n in NAT & A = ELN . n ) by FUNCT_2:17;
reconsider n = n as Element of NAT by A11;
M . (ELN . n) = M . (E \ (LN . n)) by A10
.= 0 by A7 ;
hence A is measure_zero of M by A11, MEASURE1:def 13; :: thesis:

end;

then union RELN is measure_zero of M by MEASURE2:16;
then A12: M . (union RELN) = 0. by MEASURE1:def 13;

now

let x be set ; :: thesis:
assume x in union RELN ; :: thesis:
then consider Y being set such that
A13: ( x in Y & Y in RELN ) by TARSKI:def 4;
consider m being set such that
A14: ( m in dom ELN & ELN . m = Y ) by A13, FUNCT_1:def 5;
reconsider m = m as Element of NAT by A14;
Y = E \ (LN . m) by A10, A14;
then A15: ( x in E & not x in LN . m ) by A13, XBOOLE_0:def 5;
dom LN = NAT by FUNCT_2:def 1;
then LN . m in rng LN by FUNCT_1:12;
then not x in meet (rng LN) by A15, SETFAM_1:def 1;
hence x in E \ (meet (rng LN)) by A15, XBOOLE_0:def 5; :: thesis:

end;

then A16: union RELN c= E \ (meet (rng LN)) by TARSKI:def 3;

now

let x be set ; :: thesis:
assume x in E \ (meet (rng LN)) ; :: thesis:
then A17: ( x in E & not x in meet (rng LN) ) by XBOOLE_0:def 5;
then consider Y being set such that
A18: ( Y in rng LN & not x in Y ) by SETFAM_1:def 1;
consider m being set such that
A19: ( m in dom LN & Y = LN . m ) by A18, FUNCT_1:def 5;
reconsider m = m as Element of NAT by A19;
ELN . m = E \ (LN . m) by A10;
then A20: x in ELN . m by A17, A18, A19, XBOOLE_0:def 5;
dom ELN = NAT by FUNCT_2:def 1;
then ELN . m in rng ELN by FUNCT_1:12;
hence x in union RELN by A20, TARSKI:def 4; :: thesis:

end;

then E \ (meet (rng LN)) c= union RELN by TARSKI:def 3;
then union RELN = E \ (meet (rng LN)) by A16, XBOOLE_0:def 10;
then M . (E \ L) <= (M . (union RELN)) + (M . (E \ G)) by A9, MEASURE1:64;
then A21: M . (E \ L) <= 0. by A8, A12;
A22: M . (E \ L) = 0 by A21, MEASURE1:def 4;
deffunc H₂( Nat) -> Element of bool [:X,ExtREAL :] = (f . $1) | L;
consider fL being Functional_Sequence of X,ExtREAL such that
A23: for n being Nat holds fL . n = H₂(n) from SEQFUNC:sch 1();
for n, m being Nat holds dom (fL . n) = dom (fL . m)

proof

let n, m be Nat; :: thesis:
( fL . n = (f . n) | L & fL . m = (f . m) | L ) by A23;
then ( dom (fL . n) = (dom (f . n)) /\ L & dom (fL . m) = (dom (f . m)) /\ L ) by RELAT_1:90;
hence dom (fL . n) = dom (fL . m) by Def2; :: thesis:

end;

then reconsider fL = fL as with_the_same_dom Functional_Sequence of X,ExtREAL by Def2;
set gL = g | L;
L c= G by XBOOLE_1:17;
then A24: L c= E by A8, XBOOLE_1:1;
then M . L <= M . E by MEASURE1:62;
then A25: M . L < +infty by A2, XXREAL_0:2;
for n being natural number holds
( dom (fL . n) = L & fL . n is_measurable_on L & fL . n is real-valued )

proof

let n be natural number ; :: thesis:
reconsider n' = n as Element of NAT by ORDINAL1:def 13;
A26: fL . n = (f . n) | L by A23;
then A27: dom (fL . n) = (dom (f . n)) /\ L by RELAT_1:90;
then dom (fL . n') = E /\ L by A1, Def2;
hence A28: dom (fL . n) = L by A24, XBOOLE_1:28; :: thesis:
f . n is_measurable_on L by A1, A24, MESFUNC1:34;
hence fL . n is_measurable_on L by A26, A27, A28, MESFUNC5:48; :: thesis:
for x being Element of X st x in dom (fL . n) holds
|.((fL . n) . x).| < +infty

proof

let x be Element of X; :: thesis:
assume A29: x in dom (fL . n) ; :: thesis:
then A30: x in meet (rng LN) by A28, XBOOLE_0:def 4;
dom LN = NAT by FUNCT_2:def 1;
then LN . n' in rng LN by FUNCT_1:12;
then x in LN . n by A30, SETFAM_1:def 1;
then |.((f . n') . x).| < +infty by A7;
hence |.((fL . n) . x).| < +infty by A26, A29, FUNCT_1:70; :: thesis:

end;

hence fL . n is real-valued by MESFUNC2:def 1; :: thesis:

end;

then A31: ( dom (fL . 0 ) = L & ( for n being natural number holds
( fL . n is_measurable_on L & fL . n is real-valued ) ) ) ;
dom (g | L) = (dom g) /\ L by RELAT_1:90;
then A32: dom (g | L) = L by A8, A24, XBOOLE_1:28;
A33: for x being Element of X st x in L holds
( fL # x is convergent_to_finite_number & (g | L) . x = lim (fL # x) )

proof

let x be Element of X; :: thesis:
assume A34: x in L ; :: thesis:
then A35: f # x is convergent_to_finite_number by A8, A24;
A36: ( dom (fL # x) = NAT & dom (f # x) = NAT ) by FUNCT_2:def 1;
A37: for y being set st y in NAT holds
(fL # x) . y = (f # x) . y

proof

let y be set ; :: thesis:
assume y in NAT ; :: thesis:
then reconsider n = y as Element of NAT ;
((f . n) | L) . x = (f . n) . x by A34, FUNCT_1:72;
then A38: (fL . n) . x = (f . n) . x by A23;
(f . n) . x = (f # x) . n by MESFUNC5:def 13;
hence (fL # x) . y = (f # x) . y by A38, MESFUNC5:def 13; :: thesis:

end;

hence fL # x is convergent_to_finite_number by A35, A36, FUNCT_1:9; :: thesis:
L c= G by XBOOLE_1:17;
then A39: g . x = lim (f # x) by A8, A34;
fL # x = f # x by A37, FUNCT_2:18;
hence (g | L) . x = lim (fL # x) by A34, A39, FUNCT_1:72; :: thesis:

end;

A40: for p being natural number ex Hp being Element of S ex Np being natural number st
( Hp c= L & M . Hp < ((e0 / 2) (#) ((1 / 2) GeoSeq )) . p & ( for k being natural number st Np < k holds
for x being Element of X st x in L \ Hp holds
|.(((fL . k) . x) - ((g | L) . x)).| < ((1 / 2) GeoSeq ) . p ) )

proof

let p be natural number ; :: thesis:
reconsider p' = p as Element of NAT by ORDINAL1:def 13;
0 < (1 / 2) |^ p by PREPOWER:13;
then A41: 0 < ((1 / 2) GeoSeq ) . p' by PREPOWER:def 1;
A42: 0 < e0 / 2 by A5, XREAL_1:141;
((e0 / 2) (#) ((1 / 2) GeoSeq )) . p = (e0 / 2) * (((1 / 2) GeoSeq ) . p') by SEQ_1:13;
then A43: 0 < ((e0 / 2) (#) ((1 / 2) GeoSeq )) . p by A41, A42, XREAL_1:131;
0 < (1 / 2) |^ p by PREPOWER:13;
then 0 < ((1 / 2) GeoSeq ) . p' by PREPOWER:def 1;
hence ex Hp being Element of S ex Np being natural number st
( Hp c= L & M . Hp < ((e0 / 2) (#) ((1 / 2) GeoSeq )) . p & ( for k being natural number st Np < k holds
for x being Element of X st x in L \ Hp holds
|.(((fL . k) . x) - ((g | L) . x)).| < ((1 / 2) GeoSeq ) . p ) ) by A25, A31, A32, A33, A43, Th28; :: thesis:

end;

defpred S₂[ Element of NAT , set ] means ( $2 c= L & M . $2 < ((e0 / 2) (#) ((1 / 2) GeoSeq )) . $1 & ex Np being Element of NAT st
for k being Element of NAT st Np < k holds
for x being Element of X st x in L \ $2 holds
|.(((fL . k) . x) - ((g | L) . x)).| < ((1 / 2) GeoSeq ) . $1 );
A44: for n being Element of NAT ex Z being Element of S st S₂[n,Z]

proof

let n be Element of NAT ; :: thesis:
reconsider n' = n as natural number ;
consider Z being Element of S, Np being natural number such that
A45: ( Z c= L & M . Z < ((e0 / 2) (#) ((1 / 2) GeoSeq )) . n' & ( for k being natural number st Np < k holds
for x being Element of X st x in L \ Z holds
|.(((fL . k) . x) - ((g | L) . x)).| < ((1 / 2) GeoSeq ) . n' ) ) by A40;
reconsider Np' = Np as Element of NAT by ORDINAL1:def 13;
( Z c= L & M . Z < ((e0 / 2) (#) ((1 / 2) GeoSeq )) . n & ( for k being Element of NAT st Np' < k holds
for x being Element of X st x in L \ Z holds
|.(((fL . k) . x) - ((g | L) . x)).| < ((1 / 2) GeoSeq ) . n' ) ) by A45;
hence ex Z being Element of S st S₂[n,Z] ; :: thesis:

end;

consider HP being Function of NAT ,S such that
A46: for p being Element of NAT holds S₂[p,HP . p] from FUNCT_2:sch 10(A44);
reconsider MRHP = union (rng HP) as Element of S by MEASURE1:53;
L \ MRHP is Element of S ;
then consider F being Element of S such that
A47: F = L \ (union (rng HP)) ;
A48: F c= L by A47, XBOOLE_1:36;
defpred S₃[ Element of NAT , set ] means $2 = M . (HP . $1);
A49: for n being Element of NAT ex y being Element of REAL st S₃[n,y]

proof

let n be Element of NAT ; :: thesis:
M . (HP . n) < ((e0 / 2) (#) ((1 / 2) GeoSeq )) . n by A46;
then A50: M . (HP . n) < +infty by XXREAL_0:2, XXREAL_0:9;
-infty < M . (HP . n) by MEASURE1:def 4;
then M . (HP . n) is Real by A50, XXREAL_0:48;
hence ex y being Element of REAL st S₃[n,y] ; :: thesis:

end;

consider me being Real_Sequence such that
A51: for p being Element of NAT holds S₃[p,me . p] from FUNCT_2:sch 10(A49);
A52: for p being Element of NAT holds me . p <= ((e0 / 2) (#) ((1 / 2) GeoSeq )) . p

proof

let p be Element of NAT ; :: thesis:
me . p = M . (HP . p) by A51;
hence me . p <= ((e0 / 2) (#) ((1 / 2) GeoSeq )) . p by A46; :: thesis:

end;

abs (1 / 2) = 1 / 2 by ABSVALUE:def 1;
then A53: ( (1 / 2) GeoSeq is summable & Sum ((1 / 2) GeoSeq ) = 1 / (1 - (1 / 2)) ) by SERIES_1:28;
then A54: (e0 / 2) (#) ((1 / 2) GeoSeq ) is summable by SERIES_1:13;
for p being Element of NAT holds
( 0 <= me . p & me . p <= ((e0 / 2) (#) ((1 / 2) GeoSeq )) . p )

proof

let p be Element of NAT ; :: thesis:
0. <= M . (HP . p) by MEASURE1:def 4;
hence ( 0 <= me . p & me . p <= ((e0 / 2) (#) ((1 / 2) GeoSeq )) . p ) by A51, A52; :: thesis:

end;

then A55: ( me is summable & Sum me <= Sum ((e0 / 2) (#) ((1 / 2) GeoSeq )) & me is nonnegative ) by A54, RINFSUP1:def 3, SERIES_1:24;
dom me = NAT by FUNCT_2:def 1;
then A56: dom me = dom (M * HP) by FUNCT_2:def 1;
for x being set st x in dom me holds
me . x = (M * HP) . x

proof

let x be set ; :: thesis:
assume A57: x in dom me ; :: thesis:
then (M * HP) . x = M . (HP . x) by A56, FUNCT_1:22;
hence me . x = (M * HP) . x by A51, A57; :: thesis:

end;

then me = M * HP by A56, FUNCT_1:9;
then A58: Sum me = SUM (M * HP) by A55, PROB_4:13;
rng HP is N_Sub_set_fam of X by MEASURE1:52;
then rng HP is N_Measure_fam of S by MEASURE2:def 1;
then A59: M . (union (rng HP)) <= Sum me by A58, MEASURE2:13;
A60: Sum ((e0 / 2) (#) ((1 / 2) GeoSeq )) = (e0 / 2) * 2 by A53, SERIES_1:13;
A61: for x being Element of X st x in F holds
for p being Element of NAT holds x in L \ (HP . p)

proof

let x be Element of X; :: thesis:
assume A62: x in F ; :: thesis:
let p be Element of NAT ; :: thesis:
dom HP = NAT by FUNCT_2:def 1;
then HP . p in rng HP by FUNCT_1:12;
then L \ (union (rng HP)) c= L \ (HP . p) by XBOOLE_1:34, ZFMISC_1:92;
hence x in L \ (HP . p) by A47, A62; :: thesis:

end;

A63: for q being real number st 0 < q holds
ex p being Element of NAT st ((1 / 2) GeoSeq ) . p < q

proof

let q be real number ; :: thesis:
assume A64: 0 < q ; :: thesis:
( (1 / 2) GeoSeq is convergent & lim ((1 / 2) GeoSeq ) = 0 ) by A53, SERIES_1:7;
then consider p being Element of NAT such that
A65: for n being Element of NAT st p <= n holds
abs ((((1 / 2) GeoSeq ) . n) - 0 ) < q by A64, SEQ_2:def 7;
take p ; :: thesis:
A66: abs ((((1 / 2) GeoSeq ) . p) - 0 ) < q by A65;
0 < (1 / 2) |^ p by PREPOWER:13;
then 0 <= ((1 / 2) GeoSeq ) . p by PREPOWER:def 1;
hence ((1 / 2) GeoSeq ) . p < q by A66, ABSVALUE:def 1; :: thesis:

end;

reconsider MRHP = union (rng HP) as Element of S by MEASURE1:53;
A67: F c= E by A24, A48, XBOOLE_1:1;
A68: E \ F = (E \ L) \/ (E /\ (union (rng HP))) by A47, XBOOLE_1:52;
E /\ (union (rng HP)) c= union (rng HP) by XBOOLE_1:17;
then A69: M . (E \ F) <= M . ((E \ L) \/ MRHP) by A68, MEASURE1:62, XBOOLE_1:9;
M . ((E \ L) \/ MRHP) <= (M . (E \ L)) + (M . MRHP) by MEASURE1:64;
then M . (E \ F) <= (M . (E \ L)) + (M . MRHP) by A69, XXREAL_0:2;
then A70: M . (E \ F) <= M . MRHP by A22, XXREAL_3:4;
M . MRHP <= 2 * (e0 / 2) by A55, A59, A60, XXREAL_0:2;
then A71: M . (E \ F) <= e0 by A70, XXREAL_0:2;
for q being real number st 0 < q holds
ex N being natural number st
for n being natural number st N < n holds
for x being Element of X st x in F holds
|.(((f . n) . x) - (g . x)).| < q

proof

let q be real number ; :: thesis:
assume 0 < q ; :: thesis:
then consider p being Element of NAT such that
A72: ((1 / 2) GeoSeq ) . p < q by A63;
consider Np being Element of NAT such that
A73: for k being Element of NAT st Np < k holds
for x being Element of X st x in L \ (HP . p) holds
|.(((fL . k) . x) - ((g | L) . x)).| < ((1 / 2) GeoSeq ) . p by A46;
take Np ; :: thesis:

hereby :: thesis:

let n be natural number ; :: thesis:
reconsider n' = n as Element of NAT by ORDINAL1:def 13;
assume A74: Np < n ; :: thesis:

hereby :: thesis:

let x be Element of X; :: thesis:
assume A75: x in F ; :: thesis:
then |.(((fL . n') . x) - ((g | L) . x)).| < ((1 / 2) GeoSeq ) . p by A61, A73, A74;
then A76: |.(((fL . n) . x) - ((g | L) . x)).| < q by A72, XXREAL_0:2;
A77: fL . n = (f . n) | L by A23;
A78: F c= L by A47, XBOOLE_1:36;
then (g | L) . x = g . x by A75, FUNCT_1:72;
hence |.(((f . n) . x) - (g . x)).| < q by A75, A76, A77, A78, FUNCT_1:72; :: thesis:

end;

hence ex F being Element of S st
( F c= E & M . (E \ F) <= e0 & ( for p being real number st 0 < p holds
ex N being natural number st
for n being natural number st N < n holds
for x being Element of X st x in F holds
|.(((f . n) . x) - (g . x)).| < p ) ) by A67, A71; :: thesis: