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 and
A2: for n being Nat holds f . n is_measurable_on E and
A3: M . E < +infty and
A4: for n being Nat 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
A5: 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:
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 A4;
consider LN being sequence of S such that
A7: for n being Element of NAT holds S₁[n,LN . n] from FUNCT_2:sch 3(A6);
rng LN is N_Sub_set_fam of X by MEASURE1:23;
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:2;
let e0 be Real; :: thesis:
assume A8: 0 < e0 ; :: thesis:
set e = e0 / 2;
consider G being Element of S such that
A9: G c= E and
A10: M . (E \ G) = 0 and
A11: for x being Element of X st x in E holds
f # x is convergent_to_finite_number and
A12: dom g = E and
A13: for x being Element of X st x in G holds
g . x = lim (f # x) by A5;
MRLN /\ G is Element of S ;
then reconsider L = (meet (rng LN)) /\ G as Element of S ;
set gL = g | L;
A14: L c= G by XBOOLE_1:17;
then M . L <= M . E by A9, MEASURE1:31, XBOOLE_1:1;
then A15: M . L < +infty by A3, XXREAL_0:2;
dom (g | L) = (dom g) /\ L by RELAT_1:61;
then A16: dom (g | L) = L by A9, A12, A14, XBOOLE_1:1, XBOOLE_1:28;
deffunc H₁( Nat) -> Element of bool [:X,ExtREAL:] = (f . $1) | L;
consider fL being Functional_Sequence of X,ExtREAL such that
A17: 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)

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

end;

then reconsider fL = fL as with_the_same_dom Functional_Sequence of X,ExtREAL by Def2;
A19: L c= E by A9, A14;
A20: 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:
A21: dom (fL # x) = NAT by FUNCT_2:def 1;
A22: dom (f # x) = NAT by FUNCT_2:def 1;
assume A23: x in L ; :: thesis:
A24: for y being object st y in NAT holds
(fL # x) . y = (f # x) . y

proof

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

end;

then A26: fL # x = f # x by FUNCT_2:12;
f # x is convergent_to_finite_number by A11, A19, A23;
hence fL # x is convergent_to_finite_number by A21, A22, A24, FUNCT_1:2; :: thesis:
L c= G by XBOOLE_1:17;
then g . x = lim (f # x) by A13, A23;
hence (g | L) . x = lim (fL # x) by A23, A26, FUNCT_1:49; :: 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 );
A27: for n being Nat holds
( dom (fL . n) = L & fL . n is_measurable_on L & fL . n is real-valued )

proof

let n be Nat; :: thesis:
reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
A28: fL . n = (f . n) | L by A17;
then A29: dom (fL . n) = (dom (f . n)) /\ L by RELAT_1:61;
then dom (fL . n9) = E /\ L by A1, Def2;
hence A30: dom (fL . n) = L by A9, A14, XBOOLE_1:1, XBOOLE_1:28; :: thesis:
f . n is_measurable_on L by A2, A19, MESFUNC1:30;
hence fL . n is_measurable_on L by A28, A29, A30, MESFUNC5:42; :: 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:
dom LN = NAT by FUNCT_2:def 1;
then A31: LN . n9 in rng LN by FUNCT_1:3;
assume A32: x in dom (fL . n) ; :: thesis:
then x in meet (rng LN) by A30, XBOOLE_0:def 4;
then x in LN . n by A31, SETFAM_1:def 1;
then |.((f . n9) . x).| < +infty by A7;
hence |.((fL . n) . x).| < +infty by A28, A32, FUNCT_1:47; :: thesis:

end;

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

end;

then A33: dom (fL . 0) = L ;
A34: for p being Nat ex Hp being Element of S ex Np being Nat st
( Hp c= L & M . Hp < ((e0 / 2) (#) ((1 / 2) GeoSeq)) . p & ( for k being Nat 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 Nat; :: thesis:
reconsider p9 = p as Element of NAT by ORDINAL1:def 12;
A35: ((e0 / 2) (#) ((1 / 2) GeoSeq)) . p = (e0 / 2) * (((1 / 2) GeoSeq) . p9) by SEQ_1:9;
0 < (jj / 2) |^ p by PREPOWER:6;
then A36: 0 < ((1 / 2) GeoSeq) . p9 by PREPOWER:def 1;
0 < (jj / 2) |^ p by PREPOWER:6;
then A37: 0 < ((1 / 2) GeoSeq) . p9 by PREPOWER:def 1;
0 < e0 / 2 by A8;
then 0 < ((e0 / 2) (#) ((1 / 2) GeoSeq)) . p by A36, A35, XREAL_1:129;
hence ex Hp being Element of S ex Np being Nat st
( Hp c= L & M . Hp < ((e0 / 2) (#) ((1 / 2) GeoSeq)) . p & ( for k being Nat 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 A15, A27, A33, A16, A20, A37, Th28; :: thesis:

end;

A38: 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 n9 = n as Nat ;
consider Z being Element of S, Np being Nat such that
A39: Z c= L and
A40: M . Z < ((e0 / 2) (#) ((1 / 2) GeoSeq)) . n9 and
A41: for k being 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) . n9 by A34;
reconsider Np9 = Np as Element of NAT by ORDINAL1:def 12;
for k being Element of NAT st Np9 < k holds
for x being Element of X st x in L \ Z holds
|.(((fL . k) . x) - ((g | L) . x)).| < ((1 / 2) GeoSeq) . n9 by A41;
hence ex Z being Element of S st S₂[n,Z] by A39, A40; :: thesis:

end;

consider HP being sequence of S such that
A42: for p being Element of NAT holds S₂[p,HP . p] from FUNCT_2:sch 3(A38);
defpred S₃[ Element of NAT , set ] means $2 = M . (HP . $1);
A43: for n being Element of NAT ex y being Element of REAL st S₃[n,y]

proof

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

end;

consider me being Real_Sequence such that
A45: for p being Element of NAT holds S₃[p,me . p] from FUNCT_2:sch 3(A43);
A46: 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 A45;
hence me . p <= ((e0 / 2) (#) ((1 / 2) GeoSeq)) . p by A42; :: thesis:

end;

A47: for p being Nat holds
( 0 <= me . p & me . p <= ((e0 / 2) (#) ((1 / 2) GeoSeq)) . p )

proof

let p be Nat; :: thesis:
A48: p in NAT by ORDINAL1:def 12;
0. <= M . (HP . p) by MEASURE1:def 2;
hence ( 0 <= me . p & me . p <= ((e0 / 2) (#) ((1 / 2) GeoSeq)) . p ) by A45, A46, A48; :: thesis:

end;

then for p being Nat holds
( 0 <= me . p & me . p <= ((e0 / 2) (#) ((1 / 2) GeoSeq)) . p ) ;
then A49: me is nonnegative ;
deffunc H₂( Element of NAT ) -> M12(X,S) = E \ (LN . $1);
consider ELN being sequence of S such that
A50: 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:23;
then reconsider RELN = rng ELN as N_Measure_fam of S by MEASURE2:def 1;
A51: E /\ (union (rng HP)) c= union (rng HP) by XBOOLE_1:17;
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 object such that
A52: n in NAT and
A53: A = ELN . n by FUNCT_2:11;
reconsider n = n as Element of NAT by A52;
M . (ELN . n) = M . (E \ (LN . n)) by A50
.= 0 by A7 ;
hence A is measure_zero of M by A53, MEASURE1:def 7; :: thesis:

end;

then union RELN is measure_zero of M by MEASURE2:14;
then A54: M . (union RELN) = 0. by MEASURE1:def 7;

now :: thesis:

let x be object ; :: thesis:
assume A55: x in E \ (meet (rng LN)) ; :: thesis:
then A56: x in E by XBOOLE_0:def 5;
not x in meet (rng LN) by A55, XBOOLE_0:def 5;
then consider Y being set such that
A57: Y in rng LN and
A58: not x in Y by SETFAM_1:def 1;
consider m being object such that
A59: m in dom LN and
A60: Y = LN . m by A57, FUNCT_1:def 3;
reconsider m = m as Element of NAT by A59;
dom ELN = NAT by FUNCT_2:def 1;
then A61: ELN . m in rng ELN by FUNCT_1:3;
ELN . m = E \ (LN . m) by A50;
then x in ELN . m by A56, A58, A60, XBOOLE_0:def 5;
hence x in union RELN by A61, TARSKI:def 4; :: thesis:

end;

then A62: E \ (meet (rng LN)) c= union RELN ;

now :: thesis:

let x be object ; :: thesis:
assume x in union RELN ; :: thesis:
then consider Y being set such that
A63: x in Y and
A64: Y in RELN by TARSKI:def 4;
consider m being object such that
A65: m in dom ELN and
A66: ELN . m = Y by A64, FUNCT_1:def 3;
reconsider m = m as Element of NAT by A65;
dom LN = NAT by FUNCT_2:def 1;
then A67: LN . m in rng LN by FUNCT_1:3;
A68: Y = E \ (LN . m) by A50, A66;
then not x in LN . m by A63, XBOOLE_0:def 5;
then A69: not x in meet (rng LN) by A67, SETFAM_1:def 1;
x in E by A63, A68, XBOOLE_0:def 5;
hence x in E \ (meet (rng LN)) by A69, XBOOLE_0:def 5; :: thesis:

end;

then union RELN c= E \ (meet (rng LN)) ;
then A70: union RELN = E \ (meet (rng LN)) by A62, XBOOLE_0:def 10;
rng HP is N_Sub_set_fam of X by MEASURE1:23;
then A71: rng HP is N_Measure_fam of S by MEASURE2:def 1;
reconsider MRHP = union (rng HP) as Element of S by MEASURE1:24;
L \ MRHP is Element of S ;
then consider F being Element of S such that
A72: F = L \ (union (rng HP)) ;
E \ L = (E \ (meet (rng LN))) \/ (E \ G) by XBOOLE_1:54;
then M . (E \ L) <= (M . (union RELN)) + (M . (E \ G)) by A70, MEASURE1:33;
then M . (E \ L) <= 0. by A10, A54;
then A73: M . (E \ L) = 0 by MEASURE1:def 2;
reconsider MRHP = union (rng HP) as Element of S by MEASURE1:24;
A74: M . ((E \ L) \/ MRHP) <= (M . (E \ L)) + (M . MRHP) by MEASURE1:33;
E \ F = (E \ L) \/ (E /\ (union (rng HP))) by A72, XBOOLE_1:52;
then M . (E \ F) <= M . ((E \ L) \/ MRHP) by A51, MEASURE1:31, XBOOLE_1:9;
then M . (E \ F) <= (M . (E \ L)) + (M . MRHP) by A74, XXREAL_0:2;
then A75: M . (E \ F) <= M . MRHP by A73, XXREAL_3:4;
dom me = NAT by FUNCT_2:def 1;
then A76: dom me = dom (M * HP) by FUNCT_2:def 1;
A77: for x being object st x in dom me holds
me . x = (M * HP) . x

proof

let x be object ; :: thesis:
assume A78: x in dom me ; :: thesis:
then (M * HP) . x = M . (HP . x) by A76, FUNCT_1:12;
hence me . x = (M * HP) . x by A45, A78; :: thesis:

end;

A79: |.(1 / 2).| = 1 / 2 by ABSVALUE:def 1;
then A80: (1 / 2) GeoSeq is summable by SERIES_1:24;
then A81: (e0 / 2) (#) ((1 / 2) GeoSeq) is summable by SERIES_1:10;
then me is summable by A47, SERIES_1:20;
then Sum me = SUM (M * HP) by A49, A76, A77, FUNCT_1:2, PROB_4:12;
then A82: M . (union (rng HP)) <= Sum me by A71, MEASURE2:11;
A83: for q being Real st 0 < q holds
ex p being Element of NAT st ((1 / 2) GeoSeq) . p < q

proof

let q be Real; :: thesis:
assume A84: 0 < q ; :: thesis:
A85: lim ((1 / 2) GeoSeq) = 0 by A80, SERIES_1:4;
(1 / 2) GeoSeq is convergent by A80, SERIES_1:4;
then consider p being Nat such that
A86: for n being Nat st p <= n holds
|.((((1 / 2) GeoSeq) . n) - 0).| < q by A84, A85, SEQ_2:def 7;
take p ; :: thesis:
0 < (jj / 2) |^ p by PREPOWER:6;
then A87: 0 <= ((1 / 2) GeoSeq) . p by PREPOWER:def 1;
A88: p in NAT by ORDINAL1:def 12;
|.((((1 / 2) GeoSeq) . p) - 0).| < q by A86;
hence ( p is Element of NAT & ((1 / 2) GeoSeq) . p < q ) by A87, ABSVALUE:def 1, A88; :: thesis:

end;

A89: 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 A90: 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:3;
then L \ (union (rng HP)) c= L \ (HP . p) by XBOOLE_1:34, ZFMISC_1:74;
hence x in L \ (HP . p) by A72, A90; :: thesis:

end;

A91: for q being Real st 0 < q holds
ex N being Nat st
for n being Nat 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; :: thesis:
assume 0 < q ; :: thesis:
then consider p being Element of NAT such that
A92: ((1 / 2) GeoSeq) . p < q by A83;
consider Np being Element of NAT such that
A93: 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 A42;
take Np ; :: thesis:

hereby :: thesis:

let n be Nat; :: thesis:
reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
assume A94: Np < n ; :: thesis:

hereby :: thesis:

end;

Sum ((1 / 2) GeoSeq) = 1 / (1 - (1 / 2)) by A79, SERIES_1:24;
then A99: Sum ((e0 / 2) (#) ((1 / 2) GeoSeq)) = (e0 / 2) * 2 by A80, SERIES_1:10;
Sum me <= Sum ((e0 / 2) (#) ((1 / 2) GeoSeq)) by A81, A47, SERIES_1:20;
then M . MRHP <= 2 * (e0 / 2) by A82, A99, XXREAL_0:2;
then A100: M . (E \ F) <= e0 by A75, XXREAL_0:2;
F c= L by A72, XBOOLE_1:36;
hence ex F being Element of S st
( F c= E & M . (E \ F) <= e0 & ( for p being Real st 0 < p holds
ex N being Nat st
for n being Nat st N < n holds
for x being Element of X st x in F holds
|.(((f . n) . x) - (g . x)).| < p ) ) by A19, A100, A91, XBOOLE_1:1; :: thesis: