ME; A39: for n be Nat holds seq3.n=ME by ORDINAL1:def 12,FUNCOP_1:7; then A40: seq3 is constant by VALUED_0:def 18; A41: now let x be object; assume A42: x in dom (M*EN); 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; end; dom seq1 = NAT by FUNCT_2:def 1; then A43: M*EN=seq1 by A35,A41,FUNCT_1:2; now let y be set; assume y in rng EN; then consider x be 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; 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; n <=n+1 by NAT_1:12; hence thesis by A36; end; A49: now let n be Nat; 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 qua Nat) < r1+1 by XREAL_1:8; hence seq1.n < r1+1 by A51,XXREAL_0:2; end; then A52: seq1 is bounded_above by SEQ_2:def 3; consider r be Real such that A53: for n be Nat holds seq1.n < r by A49; r is UpperBound of rng seq1 proof let d be ExtReal; assume d in rng seq1; then ex x be object st x in NAT & d=seq1.x by FUNCT_2:11; hence d <= r by A53; end; then rng seq1 is bounded_above; then A54: sup rng(M*EN) = upper_bound rng seq1 by A43,RINFSUP2:1; now let n,m be Nat; assume A55: n<=m; 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; end; then A59: seq1 is non-decreasing by SEQM_3:6; hence seq1 is convergent by A52; lim seq1 = upper_bound seq1 by A59,A52,RINFSUP1:24; hence thesis by A46,A54,A48,MEASURE2:23; end; A60: now let n be Element of NAT; M.(E \ EN.n) is Element of REAL by A18; hence ex y be Element of REAL st U[n,y]; end; consider seq2 be Real_Sequence such that A61: for n be Element of NAT holds U[n,seq2.n] from FUNCT_2:sch 3(A60 ); now let n be Nat; 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 = seq3.n - seq1.n by A39; hence seq2.n = seq3.n +(- seq1).n by SEQ_1:10; end; then A64: seq2 = seq3 - seq1 by SEQ_1:7; then A65: seq2 is convergent by A47,A40; A66: seq3.0 = ME by A39; lim seq2 = lim seq3 -lim seq1 by A47,A64,A40,SEQ_2:12; then lim seq2 =ME - ME by A47,A40,A66,SEQ_4:25; then consider N be Nat such that A67: for m be Nat st N<=m holds |.seq2.m-0 qua Complex .|< 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 be Nat st N < k holds for x be Element of X st x in E \H holds |. (f.k).x - g.x .| < e proof let k be Nat; reconsider k9=k as Element of NAT by ORDINAL1:def 12; assume A71: N < k; let x be Element of X; assume x in E\H; then x in {y where y is Element of X : for k st N <= k holds y in K.k} by A16,A69; then ex y be Element of X st x=y & for k 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 thesis by A73,A75,MESFUNC1:def 4; end; take H,N; 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 qua Complex .|< r by A67; then seq2.N < r by A77,ABSVALUE:def 1; hence thesis by A61,A70,XBOOLE_1:36,A76; end; theorem for X,Y be non empty set, E be set, F,G be Function of X,Y st for x be Element of X holds G.x = E \ F.x holds union rng G = E \ meet rng F proof let X,Y be non empty set ,E be set ,F,G be Function of X,Y; assume A1: for x be Element of X holds G.x = E \ F.x; A2: dom G = X by FUNCT_2:def 1; now let Z be object; assume Z in DIFFERENCE({E},rng F); then consider X1,Y be set such that A3: X1 in {E} and A4: Y in rng F and A5: Z = X1 \ Y by SETFAM_1:def 6; consider x be object such that A6: x in dom F and A7: Y = F.x by A4,FUNCT_1:def 3; reconsider x as Element of X by A6; X1 = E by A3,TARSKI:def 1; then Z = G.x by A1,A5,A7; hence Z in rng G by A2,FUNCT_1:3; end; then A8: DIFFERENCE({E},rng F) c= rng G; A9: dom F = X by FUNCT_2:def 1; now let Z be object; A10: E in {E} by TARSKI:def 1; assume Z in rng G; then consider x be object such that A11: x in dom G and A12: Z = G.x by FUNCT_1:def 3; reconsider x as Element of X by A11; A13: F.x in rng F by A9,FUNCT_1:3; Z = E \ F.x by A1,A12; hence Z in DIFFERENCE({E},rng F) by A13,A10,SETFAM_1:def 6; end; then rng G c= DIFFERENCE({E},rng F); then DIFFERENCE({E},rng F) = rng G by A8,XBOOLE_0:def 10; hence thesis by SETFAM_1:27; end; reconsider jj=1 as Real; ::$N Egorov's theorem theorem for M be sigma_Measure of S, f be with_the_same_dom Functional_Sequence of X,ExtREAL, g be PartFunc of X,ExtREAL, E be Element of S st (dom (f.0) = E & for n be Nat holds f.n is_measurable_on E) & M.E < +infty & (for n be Nat holds ex L be Element of S st L c= E & M.(E \L) = 0 & for x be Element of X st x in L holds |. (f.n).x .| < +infty) & ex G be Element of S st G c= E & M.(E\G) = 0 & (for x be Element of X st x in E holds f#x is convergent_to_finite_number) & dom g = E & (for x be Element of X st x in G holds g.x = lim (f#x)) holds for e be Real st 0 < e ex F be Element of S st F c= E & M.(E\F) <= e & for p be Real st 0 < p ex N be Nat st for n be Nat st N < n holds for x be Element of X st x in F holds |. (f.n).x - g.x .| < p proof let M be sigma_Measure of S, f be with_the_same_dom Functional_Sequence of X ,ExtREAL, g be PartFunc of X,ExtREAL, E be Element of S such that A1: dom(f.0) = E and A2: for n be Nat holds f.n is_measurable_on E and A3: M.E < +infty and A4: for n be Nat holds ex L be Element of S st L c= E & M.(E\ L) = 0 & for x be Element of X st x in L holds |. (f.n).x .| < +infty and A5: ex G be Element of S st G c= E & M.(E\G) = 0 & (for x be Element of X st x in E holds (f#x) is convergent_to_finite_number) & dom g = E & for x be Element of X st x in G holds g.x = lim (f#x); defpred P[Element of NAT,set] means $2 c= E & M.(E\$2) = 0 & for x be Element of X st x in ($2) holds |. (f.$1).x .| < +infty; A6: for n be Element of NAT ex Z be Element of S st P[n,Z] by A4; consider LN be sequence of S such that A7: for n be Element of NAT holds P[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; assume A8: 0 < e0; set e=e0/2; consider G be Element of S such that A9: G c= E and A10: M.(E\G) = 0 and A11: for x be Element of X st x in E holds f#x is convergent_to_finite_number and A12: dom g = E and A13: for x be 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 gL = dom g /\ L by RELAT_1:61; then A16: dom gL = L by A9,A12,A14,XBOOLE_1:1,28; deffunc FNL(Nat) = (f.$1)|L; consider fL be Functional_Sequence of X,ExtREAL such that A17: for n be Nat holds fL.n=FNL(n) from SEQFUNC:sch 1; for n,m be Nat holds dom (fL.n) = dom (fL.m) proof let n,m be Nat; 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 thesis by A18,Def2; end; then reconsider fL as with_the_same_dom Functional_Sequence of X,ExtREAL by Def2; A19: L c= E by A9,A14; A20: for x be Element of X st x in L holds fL#x is convergent_to_finite_number & gL.x = lim (fL#x) proof let x be Element of X; 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; A24: for y be object st y in NAT holds (fL#x).y = (f#x).y proof let y be object; assume y in NAT; 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 thesis by A25,MESFUNC5:def 13; 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; L c= G by XBOOLE_1:17; then g.x = lim (f#x) by A13,A23; hence thesis by A23,A26,FUNCT_1:49; end; defpred R[Element of NAT,set] means $2 c= L & M.($2) < (e(#)(1/2)GeoSeq).$1 & ex Np be Element of NAT st for k be Element of NAT st Np < k holds for x be Element of X st x in L\$2 holds |. (fL.k).x - gL.x .| < ((1/2)GeoSeq).$1; A27: for n be Nat holds dom (fL.n) = L & fL.n is_measurable_on L & fL.n is real-valued proof let n be Nat; 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,28; f.n is_measurable_on L by A2,A19,MESFUNC1:30; hence fL.n is_measurable_on L by A28,A29,A30,MESFUNC5:42; for x be Element of X st x in dom (fL.n) holds |. (fL.n).x .| < +infty proof let x be Element of X; 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); 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 thesis by A28,A32,FUNCT_1:47; end; hence thesis by MESFUNC2:def 1; end; then A33: dom (fL.0) = L; A34: for p be Nat ex Hp be Element of S, Np be Nat st Hp c= L & M.(Hp) < (e(#) (1/2) GeoSeq).p & for k be Nat st Np < k holds for x be Element of X st x in L\Hp holds |. (fL.k).x - gL.x .| < ((1/2) GeoSeq).p proof let p be Nat; reconsider p9=p as Element of NAT by ORDINAL1:def 12; A35: (e(#)(1/2) GeoSeq).p = e*((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 < e by A8; then 0 < (e(#)(1/2) GeoSeq).p by A36,A35,XREAL_1:129; hence thesis by A15,A27,A33,A16,A20,A37,Th28; end; A38: for n be Element of NAT ex Z be Element of S st R[n,Z] proof let n be Element of NAT; reconsider n9=n as Nat; consider Z be Element of S, Np be Nat such that A39: Z c= L and A40: M.Z < (e(#)(1/2)GeoSeq).n9 and A41: for k be Nat st Np < k holds for x be Element of X st x in L\Z holds |. (fL.k).x - gL.x .| < ((1/2)GeoSeq).n9 by A34; reconsider Np9=Np as Element of NAT by ORDINAL1:def 12; for k be Element of NAT st Np9 < k holds for x be Element of X st x in L\Z holds |. (fL.k).x - gL.x .| < ((1/2)GeoSeq).n9 by A41; hence thesis by A39,A40; end; consider HP be sequence of S such that A42: for p be Element of NAT holds R[p,HP.p] from FUNCT_2:sch 3(A38); defpred U[Element of NAT,set] means $2= M.(HP.$1); A43: for n be Element of NAT ex y be Element of REAL st U[n,y] proof let n be Element of NAT; A44: -infty < M.(HP.n) by MEASURE1:def 2; M.(HP.n) < (e(#)(1/2)GeoSeq).n by A42; then M.(HP.n) in REAL by A44,XXREAL_0:48; hence thesis; end; consider me be Real_Sequence such that A45: for p be Element of NAT holds U[p,me.p] from FUNCT_2:sch 3(A43); A46: for p be Element of NAT holds me.p <= (e(#)(1/2) GeoSeq).p proof let p be Element of NAT; me.p = M.(HP.p) by A45; hence thesis by A42; end; A47: for p be Nat holds 0 <=me.p & me.p <= (e(#)(1/2)GeoSeq).p proof let p be Nat; A48: p in NAT by ORDINAL1:def 12; 0. <= M.(HP.p) by MEASURE1:def 2; hence thesis by A45,A46,A48; end; then for p be Nat holds 0 <=me.p & me.p <= (e(#)(1/2)GeoSeq).p; then A49: me is nonnegative; deffunc ELN(Element of NAT) = E \ (LN.$1); consider ELN be sequence of S such that A50: for n be Element of NAT holds ELN.n=ELN(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 being set; assume A in RELN; then consider n be object such that A52: n in NAT and A53: A=ELN.n by FUNCT_2:11; reconsider n as Element of NAT by A52; M.(ELN.n) = M.(E \(LN.n)) by A50 .=0 by A7; hence thesis by A53,MEASURE1:def 7; end; then union RELN is measure_zero of M by MEASURE2:14; then A54: M.(union RELN) = 0. by MEASURE1:def 7; now let x be object; assume A55: x in E \ (meet rng LN); 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 be set such that A57: Y in rng LN and A58: not x in Y by SETFAM_1:def 1; consider m be object such that A59: m in dom LN and A60: Y = LN.m by A57,FUNCT_1:def 3; reconsider 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; end; then A62: E \ (meet rng LN) c= union RELN; now let x be object; assume x in union RELN; then consider Y be set such that A63: x in Y and A64: Y in RELN by TARSKI:def 4; consider m be object such that A65: m in dom ELN and A66: ELN.m = Y by A64,FUNCT_1:def 3; reconsider 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; 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 be 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 be object st x in dom me holds me.x = (M*HP).x proof let x be object; assume A78: x in dom me; then (M*HP).x= M.(HP.x) by A76,FUNCT_1:12; hence thesis by A45,A78; end; A79: |.1/2 qua Complex.| = 1/2 by ABSVALUE:def 1; then A80: (1/2)GeoSeq is summable by SERIES_1:24; then A81: e(#)(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 be Real st 0 < q ex p be Element of NAT st ((1/2) GeoSeq) .p < q proof let q be Real; assume A84: 0 < q; A85: lim (1/2)GeoSeq = 0 by A80,SERIES_1:4; (1/2) GeoSeq is convergent by A80,SERIES_1:4; then consider p be Nat such that A86: for n be Nat st p <=n holds |.((1/2) GeoSeq).n - 0 qua Complex .| < q by A84,A85,SEQ_2:def 7; take p; 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 qua Complex .| < q by A86; hence thesis by A87,ABSVALUE:def 1,A88; end; A89: for x be Element of X st x in F holds for p be Element of NAT holds x in L \ HP.p proof let x be Element of X; assume A90: x in F; let p be Element of NAT; 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 thesis by A72,A90; end; A91: for q be Real st 0 < q ex N be Nat st for n be Nat st N < n holds for x be Element of X st x in F holds |. (f.n).x - g.x .| < q proof let q be Real; assume 0 < q; then consider p be Element of NAT such that A92: ((1/2) GeoSeq).p < q by A83; consider Np be Element of NAT such that A93: for k be Element of NAT st Np < k holds for x be Element of X st x in L\HP.p holds |. (fL.k).x - gL.x .| < ((1/2)GeoSeq).p by A42; take Np; hereby let n be Nat; reconsider n9 =n as Element of NAT by ORDINAL1:def 12; assume A94: Np < n; hereby let x be Element of X; A95: fL.n= (f.n)|L by A17; assume A96: x in F; then |. (fL.n9).x - gL.x .| < ((1/2)GeoSeq).p by A89,A93,A94; then A97: |. (fL.n).x - gL.x .| < q by A92,XXREAL_0:2; A98: F c= L by A72,XBOOLE_1:36; then gL.x = g.x by A96,FUNCT_1:49; hence |. (f.n).x - g.x .| < q by A96,A97,A95,A98,FUNCT_1:49; end; end; end; Sum((1/2)GeoSeq) = 1/(1-(1/2)) by A79,SERIES_1:24; then A99: Sum(e(#)(1/2)GeoSeq) = e* 2 by A80,SERIES_1:10; Sum me <= Sum(e(#)(1/2)GeoSeq) by A81,A47,SERIES_1:20; then M.MRHP <= 2*e 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 thesis by A19,A100,A91,XBOOLE_1:1; end;