:: MESFUNC8 semantic presentation begin theorem Th1: :: MESFUNC8:1 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for F being Function of NAT,S for n being Nat holds { x where x is Element of X : for k being Nat st n <= k holds x in F . k } is Element of S proof let X be non empty set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for F being Function of NAT,S for n being Nat holds { x where x is Element of X : for k being Nat st n <= k holds x in F . k } is Element of S let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for F being Function of NAT,S for n being Nat holds { x where x is Element of X : for k being Nat st n <= k holds x in F . k } is Element of S let M be sigma_Measure of S; ::_thesis: for F being Function of NAT,S for n being Nat holds { x where x is Element of X : for k being Nat st n <= k holds x in F . k } is Element of S let F be Function of NAT,S; ::_thesis: for n being Nat holds { x where x is Element of X : for k being Nat st n <= k holds x in F . k } is Element of S let n be Nat; ::_thesis: { x where x is Element of X : for k being Nat st n <= k holds x in F . k } is Element of S set G = { x where x is Element of X : for k being Nat st n <= k holds x in F . k } ; deffunc H1( Element of NAT ) -> Element of S = F . (n + \$1); consider E being Function of NAT,S such that A1: for k being Element of NAT holds E . k = H1(k) from FUNCT_2:sch_4(); now__::_thesis:_for_z_being_set_st_z_in__{__x_where_x_is_Element_of_X_:_for_k_being_Nat_st_n_<=_k_holds_ x_in_F_._k__}__holds_ z_in_meet_(rng_E) let z be set ; ::_thesis: ( z in { x where x is Element of X : for k being Nat st n <= k holds x in F . k } implies z in meet (rng E) ) assume z in { x where x is Element of X : for k being Nat st n <= k holds x in F . k } ; ::_thesis: z in meet (rng E) then A2: ex x being Element of X st ( z = x & ( for k being Nat st n <= k holds x in F . k ) ) ; for Y being set st Y in rng E holds z in Y proof let Y be set ; ::_thesis: ( Y in rng E implies z in Y ) assume Y in rng E ; ::_thesis: z in Y then consider l being set such that A3: l in NAT and A4: Y = E . l by FUNCT_2:11; reconsider l = l as Element of NAT by A3; z in F . (n + l) by A2, NAT_1:12; hence z in Y by A1, A4; ::_thesis: verum end; hence z in meet (rng E) by SETFAM_1:def_1; ::_thesis: verum end; then A5: { x where x is Element of X : for k being Nat st n <= k holds x in F . k } c= meet (rng E) by TARSKI:def_3; rng E is N_Sub_set_fam of X by MEASURE1:23; then rng E is N_Measure_fam of S by MEASURE2:def_1; then A6: meet (rng E) is Element of S by MEASURE2:2; now__::_thesis:_for_z_being_set_st_z_in_meet_(rng_E)_holds_ z_in__{__x_where_x_is_Element_of_X_:_for_k_being_Nat_st_n_<=_k_holds_ x_in_F_._k__}_ let z be set ; ::_thesis: ( z in meet (rng E) implies z in { x where x is Element of X : for k being Nat st n <= k holds x in F . k } ) assume A7: z in meet (rng E) ; ::_thesis: z in { x where x is Element of X : for k being Nat st n <= k holds x in F . k } now__::_thesis:_for_k_being_Nat_st_n_<=_k_holds_ z_in_F_._k let k be Nat; ::_thesis: ( n <= k implies z in F . k ) assume n <= k ; ::_thesis: z in F . k then reconsider l = k - n as Element of NAT by NAT_1:21; E . l in rng E by FUNCT_2:4; then z in E . l by A7, SETFAM_1:def_1; then z in F . (n + l) by A1; hence z in F . k ; ::_thesis: verum end; hence z in { x where x is Element of X : for k being Nat st n <= k holds x in F . k } by A6, A7; ::_thesis: verum end; then meet (rng E) c= { x where x is Element of X : for k being Nat st n <= k holds x in F . k } by TARSKI:def_3; hence { x where x is Element of X : for k being Nat st n <= k holds x in F . k } is Element of S by A6, A5, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th2: :: MESFUNC8:2 for X being non empty set for F being SetSequence of X for n being Element of NAT holds ( (superior_setsequence F) . n = union (rng (F ^\ n)) & (inferior_setsequence F) . n = meet (rng (F ^\ n)) ) proof let X be non empty set ; ::_thesis: for F being SetSequence of X for n being Element of NAT holds ( (superior_setsequence F) . n = union (rng (F ^\ n)) & (inferior_setsequence F) . n = meet (rng (F ^\ n)) ) let F be SetSequence of X; ::_thesis: for n being Element of NAT holds ( (superior_setsequence F) . n = union (rng (F ^\ n)) & (inferior_setsequence F) . n = meet (rng (F ^\ n)) ) let n be Element of NAT ; ::_thesis: ( (superior_setsequence F) . n = union (rng (F ^\ n)) & (inferior_setsequence F) . n = meet (rng (F ^\ n)) ) { (F . k) where k is Element of NAT : n <= k } = rng (F ^\ n) by SETLIM_1:6; hence (superior_setsequence F) . n = union (rng (F ^\ n)) by SETLIM_1:def_3; ::_thesis: (inferior_setsequence F) . n = meet (rng (F ^\ n)) (inferior_setsequence F) . n = meet { (F . k) where k is Element of NAT : n <= k } by SETLIM_1:def_2; hence (inferior_setsequence F) . n = meet (rng (F ^\ n)) by SETLIM_1:6; ::_thesis: verum end; theorem Th3: :: MESFUNC8:3 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for F being SetSequence of S ex G being Function of NAT,S st ( G = inferior_setsequence F & M . (lim_inf F) = sup (rng (M * G)) ) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for F being SetSequence of S ex G being Function of NAT,S st ( G = inferior_setsequence F & M . (lim_inf F) = sup (rng (M * G)) ) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for F being SetSequence of S ex G being Function of NAT,S st ( G = inferior_setsequence F & M . (lim_inf F) = sup (rng (M * G)) ) let M be sigma_Measure of S; ::_thesis: for F being SetSequence of S ex G being Function of NAT,S st ( G = inferior_setsequence F & M . (lim_inf F) = sup (rng (M * G)) ) let F be SetSequence of S; ::_thesis: ex G being Function of NAT,S st ( G = inferior_setsequence F & M . (lim_inf F) = sup (rng (M * G)) ) rng (inferior_setsequence F) c= S ; then reconsider G = inferior_setsequence F as Function of NAT,S by FUNCT_2:6; now__::_thesis:_for_n_being_Element_of_NAT_holds_G_._n_c=_G_._(n_+_1) let n be Element of NAT ; ::_thesis: G . n c= G . (n + 1) n <= n + 1 by NAT_1:12; hence G . n c= G . (n + 1) by PROB_1:def_5; ::_thesis: verum end; then M . (union (rng G)) = sup (rng (M * G)) by MEASURE2:23; hence ex G being Function of NAT,S st ( G = inferior_setsequence F & M . (lim_inf F) = sup (rng (M * G)) ) ; ::_thesis: verum end; theorem Th4: :: MESFUNC8:4 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for F being SetSequence of S st M . (Union F) < +infty holds ex G being Function of NAT,S st ( G = superior_setsequence F & M . (lim_sup F) = inf (rng (M * G)) ) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for F being SetSequence of S st M . (Union F) < +infty holds ex G being Function of NAT,S st ( G = superior_setsequence F & M . (lim_sup F) = inf (rng (M * G)) ) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for F being SetSequence of S st M . (Union F) < +infty holds ex G being Function of NAT,S st ( G = superior_setsequence F & M . (lim_sup F) = inf (rng (M * G)) ) let M be sigma_Measure of S; ::_thesis: for F being SetSequence of S st M . (Union F) < +infty holds ex G being Function of NAT,S st ( G = superior_setsequence F & M . (lim_sup F) = inf (rng (M * G)) ) let F be SetSequence of S; ::_thesis: ( M . (Union F) < +infty implies ex G being Function of NAT,S st ( G = superior_setsequence F & M . (lim_sup F) = inf (rng (M * G)) ) ) rng (superior_setsequence F) c= S ; then reconsider G = superior_setsequence F as Function of NAT,S by FUNCT_2:6; reconsider F1 = F, G1 = G as SetSequence of X ; A1: for n being Element of NAT holds G . (n + 1) c= G . n proof let n be Element of NAT ; ::_thesis: G . (n + 1) c= G . n n <= n + 1 by NAT_1:12; hence G . (n + 1) c= G . n by PROB_1:def_4; ::_thesis: verum end; G . 0 = union { (F . k) where k is Element of NAT : 0 <= k } by SETLIM_1:def_3; then A2: G . 0 = union (rng F) by SETLIM_1:5; consider f being SetSequence of X such that A3: lim_sup F1 = meet f and A4: for n being Element of NAT holds f . n = Union (F1 ^\ n) by KURATO_0:def_2; now__::_thesis:_for_n_being_Element_of_NAT_holds_f_._n_=_G1_._n let n be Element of NAT ; ::_thesis: f . n = G1 . n f . n = Union (F1 ^\ n) by A4; hence f . n = G1 . n by Th2; ::_thesis: verum end; then A5: f = G1 by FUNCT_2:63; assume M . (Union F) < +infty ; ::_thesis: ex G being Function of NAT,S st ( G = superior_setsequence F & M . (lim_sup F) = inf (rng (M * G)) ) then M . (meet (rng G)) = inf (rng (M * G)) by A1, A2, MEASURE3:12; hence ex G being Function of NAT,S st ( G = superior_setsequence F & M . (lim_sup F) = inf (rng (M * G)) ) by A3, A5; ::_thesis: verum end; theorem :: MESFUNC8:5 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for F being SetSequence of S st F is convergent holds ex G being Function of NAT,S st ( G = inferior_setsequence F & M . (lim F) = sup (rng (M * G)) ) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for F being SetSequence of S st F is convergent holds ex G being Function of NAT,S st ( G = inferior_setsequence F & M . (lim F) = sup (rng (M * G)) ) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for F being SetSequence of S st F is convergent holds ex G being Function of NAT,S st ( G = inferior_setsequence F & M . (lim F) = sup (rng (M * G)) ) let M be sigma_Measure of S; ::_thesis: for F being SetSequence of S st F is convergent holds ex G being Function of NAT,S st ( G = inferior_setsequence F & M . (lim F) = sup (rng (M * G)) ) let F be SetSequence of S; ::_thesis: ( F is convergent implies ex G being Function of NAT,S st ( G = inferior_setsequence F & M . (lim F) = sup (rng (M * G)) ) ) assume F is convergent ; ::_thesis: ex G being Function of NAT,S st ( G = inferior_setsequence F & M . (lim F) = sup (rng (M * G)) ) then lim_inf F = lim F by KURATO_0:def_5; hence ex G being Function of NAT,S st ( G = inferior_setsequence F & M . (lim F) = sup (rng (M * G)) ) by Th3; ::_thesis: verum end; theorem :: MESFUNC8:6 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for F being SetSequence of S st F is convergent & M . (Union F) < +infty holds ex G being Function of NAT,S st ( G = superior_setsequence F & M . (lim F) = inf (rng (M * G)) ) by Th4; definition let X, Y be set ; let F be Functional_Sequence of X,Y; attrF is with_the_same_dom means :Def1: :: MESFUNC8:def 1 rng F is with_common_domain ; end; :: deftheorem Def1 defines with_the_same_dom MESFUNC8:def_1_:_ for X, Y being set for F being Functional_Sequence of X,Y holds ( F is with_the_same_dom iff rng F is with_common_domain ); definition let X, Y be set ; let F be Functional_Sequence of X,Y; redefine attr F is with_the_same_dom means :Def2: :: MESFUNC8:def 2 for n, m being Nat holds dom (F . n) = dom (F . m); correctness compatibility ( F is with_the_same_dom iff for n, m being Nat holds dom (F . n) = dom (F . m) ); proof A1: ( ( for n, m being Nat holds dom (F . n) = dom (F . m) ) implies F is with_the_same_dom ) proof assume A2: for n, m being Nat holds dom (F . n) = dom (F . m) ; ::_thesis: F is with_the_same_dom now__::_thesis:_for_f,_g_being_Function_st_f_in_rng_F_&_g_in_rng_F_holds_ dom_f_=_dom_g let f, g be Function; ::_thesis: ( f in rng F & g in rng F implies dom f = dom g ) assume that A3: f in rng F and A4: g in rng F ; ::_thesis: dom f = dom g consider m being set such that A5: m in dom F and A6: g = F . m by A4, FUNCT_1:def_3; consider n being set such that A7: n in dom F and A8: f = F . n by A3, FUNCT_1:def_3; reconsider n = n, m = m as Nat by A7, A5; dom (F . n) = dom (F . m) by A2; hence dom f = dom g by A8, A6; ::_thesis: verum end; then rng F is with_common_domain by CARD_3:def_10; hence F is with_the_same_dom by Def1; ::_thesis: verum end; ( F is with_the_same_dom implies for n, m being Nat holds dom (F . n) = dom (F . m) ) proof assume F is with_the_same_dom ; ::_thesis: for n, m being Nat holds dom (F . n) = dom (F . m) then A9: rng F is with_common_domain by Def1; hereby ::_thesis: verum let n, m be Nat; ::_thesis: dom (F . n) = dom (F . m) A10: dom F = NAT by FUNCT_2:def_1; then m in dom F by ORDINAL1:def_12; then A11: F . m in rng F by FUNCT_1:3; n in dom F by A10, ORDINAL1:def_12; then F . n in rng F by FUNCT_1:3; hence dom (F . n) = dom (F . m) by A9, A11, CARD_3:def_10; ::_thesis: verum end; end; hence ( F is with_the_same_dom iff for n, m being Nat holds dom (F . n) = dom (F . m) ) by A1; ::_thesis: verum end; end; :: deftheorem Def2 defines with_the_same_dom MESFUNC8:def_2_:_ for X, Y being set for F being Functional_Sequence of X,Y holds ( F is with_the_same_dom iff for n, m being Nat holds dom (F . n) = dom (F . m) ); registration let X, Y be set ; cluster non empty Relation-like NAT -defined PFuncs (X,Y) -valued Function-like total V30( NAT , PFuncs (X,Y)) with_the_same_dom for Element of bool [:NAT,(PFuncs (X,Y)):]; existence ex b1 being Functional_Sequence of X,Y st b1 is with_the_same_dom proof deffunc H1( Nat) -> Element of bool [:X,Y:] = <:{},X,Y:>; consider F being Functional_Sequence of X,Y such that A1: for n being Nat holds F . n = H1(n) from SEQFUNC:sch_1(); take F ; ::_thesis: F is with_the_same_dom hereby :: according to MESFUNC8:def_2 ::_thesis: verum let n, m be Nat; ::_thesis: dom (F . n) = dom (F . m) F . n = <:{},X,Y:> by A1; hence dom (F . n) = dom (F . m) by A1; ::_thesis: verum end; end; end; definition let X be non empty set ; let f be Functional_Sequence of X,ExtREAL; func inf f -> PartFunc of X,ExtREAL means :Def3: :: MESFUNC8:def 3 ( dom it = dom (f . 0) & ( for x being Element of X st x in dom it holds it . x = inf (f # x) ) ); existence ex b1 being PartFunc of X,ExtREAL st ( dom b1 = dom (f . 0) & ( for x being Element of X st x in dom b1 holds b1 . x = inf (f # x) ) ) proof defpred S1[ set ] means \$1 in dom (f . 0); deffunc H1( Element of X) -> Element of ExtREAL = inf (f # \$1); consider g being PartFunc of X,ExtREAL such that A1: ( ( for x being Element of X holds ( x in dom g iff S1[x] ) ) & ( for x being Element of X st x in dom g holds g /. x = H1(x) ) ) from PARTFUN2:sch_2(); take g ; ::_thesis: ( dom g = dom (f . 0) & ( for x being Element of X st x in dom g holds g . x = inf (f # x) ) ) A2: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_g_holds_ g_._x_=_inf_(f_#_x) let x be Element of X; ::_thesis: ( x in dom g implies g . x = inf (f # x) ) assume A3: x in dom g ; ::_thesis: g . x = inf (f # x) then g /. x = inf (f # x) by A1; hence g . x = inf (f # x) by A3, PARTFUN1:def_6; ::_thesis: verum end; for x being set holds ( x in dom g iff x in dom (f . 0) ) by A1; hence ( dom g = dom (f . 0) & ( for x being Element of X st x in dom g holds g . x = inf (f # x) ) ) by A2, TARSKI:1; ::_thesis: verum end; uniqueness for b1, b2 being PartFunc of X,ExtREAL st dom b1 = dom (f . 0) & ( for x being Element of X st x in dom b1 holds b1 . x = inf (f # x) ) & dom b2 = dom (f . 0) & ( for x being Element of X st x in dom b2 holds b2 . x = inf (f # x) ) holds b1 = b2 proof let g, h be PartFunc of X,ExtREAL; ::_thesis: ( dom g = dom (f . 0) & ( for x being Element of X st x in dom g holds g . x = inf (f # x) ) & dom h = dom (f . 0) & ( for x being Element of X st x in dom h holds h . x = inf (f # x) ) implies g = h ) assume that A4: dom g = dom (f . 0) and A5: for x being Element of X st x in dom g holds g . x = inf (f # x) ; ::_thesis: ( not dom h = dom (f . 0) or ex x being Element of X st ( x in dom h & not h . x = inf (f # x) ) or g = h ) assume that A6: dom h = dom (f . 0) and A7: for x being Element of X st x in dom h holds h . x = inf (f # x) ; ::_thesis: g = h now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_g_holds_ g_/._x_=_h_/._x let x be Element of X; ::_thesis: ( x in dom g implies g /. x = h /. x ) assume A8: x in dom g ; ::_thesis: g /. x = h /. x then g /. x = g . x by PARTFUN1:def_6; then g /. x = inf (f # x) by A5, A8; then g /. x = h . x by A4, A6, A7, A8; hence g /. x = h /. x by A4, A6, A8, PARTFUN1:def_6; ::_thesis: verum end; hence g = h by A4, A6, PARTFUN2:1; ::_thesis: verum end; end; :: deftheorem Def3 defines inf MESFUNC8:def_3_:_ for X being non empty set for f being Functional_Sequence of X,ExtREAL for b3 being PartFunc of X,ExtREAL holds ( b3 = inf f iff ( dom b3 = dom (f . 0) & ( for x being Element of X st x in dom b3 holds b3 . x = inf (f # x) ) ) ); definition let X be non empty set ; let f be Functional_Sequence of X,ExtREAL; func sup f -> PartFunc of X,ExtREAL means :Def4: :: MESFUNC8:def 4 ( dom it = dom (f . 0) & ( for x being Element of X st x in dom it holds it . x = sup (f # x) ) ); existence ex b1 being PartFunc of X,ExtREAL st ( dom b1 = dom (f . 0) & ( for x being Element of X st x in dom b1 holds b1 . x = sup (f # x) ) ) proof defpred S1[ set ] means \$1 in dom (f . 0); deffunc H1( Element of X) -> Element of ExtREAL = sup (f # \$1); consider g being PartFunc of X,ExtREAL such that A1: ( ( for x being Element of X holds ( x in dom g iff S1[x] ) ) & ( for x being Element of X st x in dom g holds g /. x = H1(x) ) ) from PARTFUN2:sch_2(); take g ; ::_thesis: ( dom g = dom (f . 0) & ( for x being Element of X st x in dom g holds g . x = sup (f # x) ) ) A2: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_g_holds_ g_._x_=_sup_(f_#_x) let x be Element of X; ::_thesis: ( x in dom g implies g . x = sup (f # x) ) assume A3: x in dom g ; ::_thesis: g . x = sup (f # x) then g /. x = sup (f # x) by A1; hence g . x = sup (f # x) by A3, PARTFUN1:def_6; ::_thesis: verum end; for x being set holds ( x in dom g iff x in dom (f . 0) ) by A1; hence ( dom g = dom (f . 0) & ( for x being Element of X st x in dom g holds g . x = sup (f # x) ) ) by A2, TARSKI:1; ::_thesis: verum end; uniqueness for b1, b2 being PartFunc of X,ExtREAL st dom b1 = dom (f . 0) & ( for x being Element of X st x in dom b1 holds b1 . x = sup (f # x) ) & dom b2 = dom (f . 0) & ( for x being Element of X st x in dom b2 holds b2 . x = sup (f # x) ) holds b1 = b2 proof let g, h be PartFunc of X,ExtREAL; ::_thesis: ( dom g = dom (f . 0) & ( for x being Element of X st x in dom g holds g . x = sup (f # x) ) & dom h = dom (f . 0) & ( for x being Element of X st x in dom h holds h . x = sup (f # x) ) implies g = h ) assume that A4: dom g = dom (f . 0) and A5: for x being Element of X st x in dom g holds g . x = sup (f # x) ; ::_thesis: ( not dom h = dom (f . 0) or ex x being Element of X st ( x in dom h & not h . x = sup (f # x) ) or g = h ) assume that A6: dom h = dom (f . 0) and A7: for x being Element of X st x in dom h holds h . x = sup (f # x) ; ::_thesis: g = h now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_g_holds_ g_/._x_=_h_/._x let x be Element of X; ::_thesis: ( x in dom g implies g /. x = h /. x ) assume A8: x in dom g ; ::_thesis: g /. x = h /. x then g /. x = g . x by PARTFUN1:def_6; then g /. x = sup (f # x) by A5, A8; then g /. x = h . x by A4, A6, A7, A8; hence g /. x = h /. x by A4, A6, A8, PARTFUN1:def_6; ::_thesis: verum end; hence g = h by A4, A6, PARTFUN2:1; ::_thesis: verum end; end; :: deftheorem Def4 defines sup MESFUNC8:def_4_:_ for X being non empty set for f being Functional_Sequence of X,ExtREAL for b3 being PartFunc of X,ExtREAL holds ( b3 = sup f iff ( dom b3 = dom (f . 0) & ( for x being Element of X st x in dom b3 holds b3 . x = sup (f # x) ) ) ); definition let X be non empty set ; let f be Functional_Sequence of X,ExtREAL; func inferior_realsequence f -> with_the_same_dom Functional_Sequence of X,ExtREAL means :Def5: :: MESFUNC8:def 5 for n being Nat holds ( dom (it . n) = dom (f . 0) & ( for x being Element of X st x in dom (it . n) holds (it . n) . x = (inferior_realsequence (f # x)) . n ) ); existence ex b1 being with_the_same_dom Functional_Sequence of X,ExtREAL st for n being Nat holds ( dom (b1 . n) = dom (f . 0) & ( for x being Element of X st x in dom (b1 . n) holds (b1 . n) . x = (inferior_realsequence (f # x)) . n ) ) proof defpred S1[ Element of NAT , Function] means ( dom \$2 = dom (f . 0) & ( for x being Element of X st x in dom \$2 holds \$2 . x = (inferior_realsequence (f # x)) . \$1 ) ); A1: for n being Element of NAT ex y being Element of PFuncs (X,ExtREAL) st S1[n,y] proof defpred S2[ set ] means \$1 in dom (f . 0); let n be Element of NAT ; ::_thesis: ex y being Element of PFuncs (X,ExtREAL) st S1[n,y] deffunc H1( Element of X) -> Element of ExtREAL = (inferior_realsequence (f # \$1)) . n; consider g being PartFunc of X,ExtREAL such that A2: ( ( for x being Element of X holds ( x in dom g iff S2[x] ) ) & ( for x being Element of X st x in dom g holds g /. x = H1(x) ) ) from PARTFUN2:sch_2(); take g ; ::_thesis: ( g is Element of PFuncs (X,ExtREAL) & S1[n,g] ) A3: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_g_holds_ g_._x_=_(inferior_realsequence_(f_#_x))_._n let x be Element of X; ::_thesis: ( x in dom g implies g . x = (inferior_realsequence (f # x)) . n ) assume A4: x in dom g ; ::_thesis: g . x = (inferior_realsequence (f # x)) . n then g /. x = (inferior_realsequence (f # x)) . n by A2; hence g . x = (inferior_realsequence (f # x)) . n by A4, PARTFUN1:def_6; ::_thesis: verum end; for x being set holds ( x in dom g iff x in dom (f . 0) ) by A2; hence ( g is Element of PFuncs (X,ExtREAL) & S1[n,g] ) by A3, PARTFUN1:45, TARSKI:1; ::_thesis: verum end; consider g being Function of NAT,(PFuncs (X,ExtREAL)) such that A5: for n being Element of NAT holds S1[n,g . n] from FUNCT_2:sch_3(A1); A6: for n being Nat holds ( dom (g . n) = dom (f . 0) & ( for x being Element of X st x in dom (g . n) holds (g . n) . x = (inferior_realsequence (f # x)) . n ) ) proof let n be Nat; ::_thesis: ( dom (g . n) = dom (f . 0) & ( for x being Element of X st x in dom (g . n) holds (g . n) . x = (inferior_realsequence (f # x)) . n ) ) reconsider n9 = n as Element of NAT by ORDINAL1:def_12; dom (g . n9) = dom (f . 0) by A5; hence ( dom (g . n) = dom (f . 0) & ( for x being Element of X st x in dom (g . n) holds (g . n) . x = (inferior_realsequence (f # x)) . n ) ) by A5; ::_thesis: verum end; reconsider g = g as Functional_Sequence of X,ExtREAL ; now__::_thesis:_for_k,_l_being_Nat_holds_dom_(g_._k)_=_dom_(g_._l) let k, l be Nat; ::_thesis: dom (g . k) = dom (g . l) reconsider k9 = k, l9 = l as Element of NAT by ORDINAL1:def_12; dom (g . k9) = dom (f . 0) by A5; then dom (g . k) = dom (g . l9) by A5; hence dom (g . k) = dom (g . l) ; ::_thesis: verum end; then reconsider g = g as with_the_same_dom Functional_Sequence of X,ExtREAL by Def2; take g ; ::_thesis: for n being Nat holds ( dom (g . n) = dom (f . 0) & ( for x being Element of X st x in dom (g . n) holds (g . n) . x = (inferior_realsequence (f # x)) . n ) ) thus for n being Nat holds ( dom (g . n) = dom (f . 0) & ( for x being Element of X st x in dom (g . n) holds (g . n) . x = (inferior_realsequence (f # x)) . n ) ) by A6; ::_thesis: verum end; uniqueness for b1, b2 being with_the_same_dom Functional_Sequence of X,ExtREAL st ( for n being Nat holds ( dom (b1 . n) = dom (f . 0) & ( for x being Element of X st x in dom (b1 . n) holds (b1 . n) . x = (inferior_realsequence (f # x)) . n ) ) ) & ( for n being Nat holds ( dom (b2 . n) = dom (f . 0) & ( for x being Element of X st x in dom (b2 . n) holds (b2 . n) . x = (inferior_realsequence (f # x)) . n ) ) ) holds b1 = b2 proof let g, h be with_the_same_dom Functional_Sequence of X,ExtREAL; ::_thesis: ( ( for n being Nat holds ( dom (g . n) = dom (f . 0) & ( for x being Element of X st x in dom (g . n) holds (g . n) . x = (inferior_realsequence (f # x)) . n ) ) ) & ( for n being Nat holds ( dom (h . n) = dom (f . 0) & ( for x being Element of X st x in dom (h . n) holds (h . n) . x = (inferior_realsequence (f # x)) . n ) ) ) implies g = h ) assume A7: for n being Nat holds ( dom (g . n) = dom (f . 0) & ( for x being Element of X st x in dom (g . n) holds (g . n) . x = (inferior_realsequence (f # x)) . n ) ) ; ::_thesis: ( ex n being Nat st ( dom (h . n) = dom (f . 0) implies ex x being Element of X st ( x in dom (h . n) & not (h . n) . x = (inferior_realsequence (f # x)) . n ) ) or g = h ) assume A8: for n being Nat holds ( dom (h . n) = dom (f . 0) & ( for x being Element of X st x in dom (h . n) holds (h . n) . x = (inferior_realsequence (f # x)) . n ) ) ; ::_thesis: g = h now__::_thesis:_for_n_being_Element_of_NAT_holds_g_._n_=_h_._n let n be Element of NAT ; ::_thesis: g . n = h . n A9: dom (g . n) = dom (f . 0) by A7 .= dom (h . n) by A8 ; now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(g_._n)_holds_ (g_._n)_/._x_=_(h_._n)_/._x let x be Element of X; ::_thesis: ( x in dom (g . n) implies (g . n) /. x = (h . n) /. x ) assume A10: x in dom (g . n) ; ::_thesis: (g . n) /. x = (h . n) /. x then (g . n) /. x = (g . n) . x by PARTFUN1:def_6; then (g . n) /. x = (inferior_realsequence (f # x)) . n by A7, A10; then (g . n) /. x = (h . n) . x by A8, A9, A10; hence (g . n) /. x = (h . n) /. x by A9, A10, PARTFUN1:def_6; ::_thesis: verum end; hence g . n = h . n by A9, PARTFUN2:1; ::_thesis: verum end; hence g = h by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def5 defines inferior_realsequence MESFUNC8:def_5_:_ for X being non empty set for f being Functional_Sequence of X,ExtREAL for b3 being with_the_same_dom Functional_Sequence of X,ExtREAL holds ( b3 = inferior_realsequence f iff for n being Nat holds ( dom (b3 . n) = dom (f . 0) & ( for x being Element of X st x in dom (b3 . n) holds (b3 . n) . x = (inferior_realsequence (f # x)) . n ) ) ); definition let X be non empty set ; let f be Functional_Sequence of X,ExtREAL; func superior_realsequence f -> with_the_same_dom Functional_Sequence of X,ExtREAL means :Def6: :: MESFUNC8:def 6 for n being Nat holds ( dom (it . n) = dom (f . 0) & ( for x being Element of X st x in dom (it . n) holds (it . n) . x = (superior_realsequence (f # x)) . n ) ); existence ex b1 being with_the_same_dom Functional_Sequence of X,ExtREAL st for n being Nat holds ( dom (b1 . n) = dom (f . 0) & ( for x being Element of X st x in dom (b1 . n) holds (b1 . n) . x = (superior_realsequence (f # x)) . n ) ) proof defpred S1[ Element of NAT , Function] means ( dom \$2 = dom (f . 0) & ( for x being Element of X st x in dom \$2 holds \$2 . x = (superior_realsequence (f # x)) . \$1 ) ); A1: for n being Element of NAT ex y being Element of PFuncs (X,ExtREAL) st S1[n,y] proof defpred S2[ set ] means \$1 in dom (f . 0); let n be Element of NAT ; ::_thesis: ex y being Element of PFuncs (X,ExtREAL) st S1[n,y] deffunc H1( Element of X) -> Element of ExtREAL = (superior_realsequence (f # \$1)) . n; consider g being PartFunc of X,ExtREAL such that A2: ( ( for x being Element of X holds ( x in dom g iff S2[x] ) ) & ( for x being Element of X st x in dom g holds g /. x = H1(x) ) ) from PARTFUN2:sch_2(); take g ; ::_thesis: ( g is Element of PFuncs (X,ExtREAL) & S1[n,g] ) A3: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_g_holds_ g_._x_=_(superior_realsequence_(f_#_x))_._n let x be Element of X; ::_thesis: ( x in dom g implies g . x = (superior_realsequence (f # x)) . n ) assume A4: x in dom g ; ::_thesis: g . x = (superior_realsequence (f # x)) . n then g /. x = (superior_realsequence (f # x)) . n by A2; hence g . x = (superior_realsequence (f # x)) . n by A4, PARTFUN1:def_6; ::_thesis: verum end; for x being set holds ( x in dom g iff x in dom (f . 0) ) by A2; hence ( g is Element of PFuncs (X,ExtREAL) & S1[n,g] ) by A3, PARTFUN1:45, TARSKI:1; ::_thesis: verum end; consider g being Function of NAT,(PFuncs (X,ExtREAL)) such that A5: for n being Element of NAT holds S1[n,g . n] from FUNCT_2:sch_3(A1); A6: for n being Nat holds ( dom (g . n) = dom (f . 0) & ( for x being Element of X st x in dom (g . n) holds (g . n) . x = (superior_realsequence (f # x)) . n ) ) proof let n be Nat; ::_thesis: ( dom (g . n) = dom (f . 0) & ( for x being Element of X st x in dom (g . n) holds (g . n) . x = (superior_realsequence (f # x)) . n ) ) reconsider n9 = n as Element of NAT by ORDINAL1:def_12; dom (g . n9) = dom (f . 0) by A5; hence ( dom (g . n) = dom (f . 0) & ( for x being Element of X st x in dom (g . n) holds (g . n) . x = (superior_realsequence (f # x)) . n ) ) by A5; ::_thesis: verum end; reconsider g = g as Functional_Sequence of X,ExtREAL ; now__::_thesis:_for_k,_l_being_Nat_holds_dom_(g_._k)_=_dom_(g_._l) let k, l be Nat; ::_thesis: dom (g . k) = dom (g . l) reconsider k9 = k, l9 = l as Element of NAT by ORDINAL1:def_12; dom (g . k9) = dom (f . 0) by A5; then dom (g . k) = dom (g . l9) by A5; hence dom (g . k) = dom (g . l) ; ::_thesis: verum end; then reconsider g = g as with_the_same_dom Functional_Sequence of X,ExtREAL by Def2; take g ; ::_thesis: for n being Nat holds ( dom (g . n) = dom (f . 0) & ( for x being Element of X st x in dom (g . n) holds (g . n) . x = (superior_realsequence (f # x)) . n ) ) thus for n being Nat holds ( dom (g . n) = dom (f . 0) & ( for x being Element of X st x in dom (g . n) holds (g . n) . x = (superior_realsequence (f # x)) . n ) ) by A6; ::_thesis: verum end; uniqueness for b1, b2 being with_the_same_dom Functional_Sequence of X,ExtREAL st ( for n being Nat holds ( dom (b1 . n) = dom (f . 0) & ( for x being Element of X st x in dom (b1 . n) holds (b1 . n) . x = (superior_realsequence (f # x)) . n ) ) ) & ( for n being Nat holds ( dom (b2 . n) = dom (f . 0) & ( for x being Element of X st x in dom (b2 . n) holds (b2 . n) . x = (superior_realsequence (f # x)) . n ) ) ) holds b1 = b2 proof let g, h be with_the_same_dom Functional_Sequence of X,ExtREAL; ::_thesis: ( ( for n being Nat holds ( dom (g . n) = dom (f . 0) & ( for x being Element of X st x in dom (g . n) holds (g . n) . x = (superior_realsequence (f # x)) . n ) ) ) & ( for n being Nat holds ( dom (h . n) = dom (f . 0) & ( for x being Element of X st x in dom (h . n) holds (h . n) . x = (superior_realsequence (f # x)) . n ) ) ) implies g = h ) assume A7: for n being Nat holds ( dom (g . n) = dom (f . 0) & ( for x being Element of X st x in dom (g . n) holds (g . n) . x = (superior_realsequence (f # x)) . n ) ) ; ::_thesis: ( ex n being Nat st ( dom (h . n) = dom (f . 0) implies ex x being Element of X st ( x in dom (h . n) & not (h . n) . x = (superior_realsequence (f # x)) . n ) ) or g = h ) assume A8: for n being Nat holds ( dom (h . n) = dom (f . 0) & ( for x being Element of X st x in dom (h . n) holds (h . n) . x = (superior_realsequence (f # x)) . n ) ) ; ::_thesis: g = h now__::_thesis:_for_n_being_Element_of_NAT_holds_g_._n_=_h_._n let n be Element of NAT ; ::_thesis: g . n = h . n A9: dom (g . n) = dom (f . 0) by A7 .= dom (h . n) by A8 ; now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(g_._n)_holds_ (g_._n)_/._x_=_(h_._n)_/._x let x be Element of X; ::_thesis: ( x in dom (g . n) implies (g . n) /. x = (h . n) /. x ) assume A10: x in dom (g . n) ; ::_thesis: (g . n) /. x = (h . n) /. x then (g . n) /. x = (g . n) . x by PARTFUN1:def_6; then (g . n) /. x = (superior_realsequence (f # x)) . n by A7, A10; then (g . n) /. x = (h . n) . x by A8, A9, A10; hence (g . n) /. x = (h . n) /. x by A9, A10, PARTFUN1:def_6; ::_thesis: verum end; hence g . n = h . n by A9, PARTFUN2:1; ::_thesis: verum end; hence g = h by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def6 defines superior_realsequence MESFUNC8:def_6_:_ for X being non empty set for f being Functional_Sequence of X,ExtREAL for b3 being with_the_same_dom Functional_Sequence of X,ExtREAL holds ( b3 = superior_realsequence f iff for n being Nat holds ( dom (b3 . n) = dom (f . 0) & ( for x being Element of X st x in dom (b3 . n) holds (b3 . n) . x = (superior_realsequence (f # x)) . n ) ) ); theorem Th7: :: MESFUNC8:7 for X being non empty set for f being Functional_Sequence of X,ExtREAL for x being Element of X st x in dom (f . 0) holds (inferior_realsequence f) # x = inferior_realsequence (f # x) proof let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,ExtREAL for x being Element of X st x in dom (f . 0) holds (inferior_realsequence f) # x = inferior_realsequence (f # x) let f be Functional_Sequence of X,ExtREAL; ::_thesis: for x being Element of X st x in dom (f . 0) holds (inferior_realsequence f) # x = inferior_realsequence (f # x) set F = inferior_realsequence f; hereby ::_thesis: verum let x be Element of X; ::_thesis: ( x in dom (f . 0) implies (inferior_realsequence f) # x = inferior_realsequence (f # x) ) assume A1: x in dom (f . 0) ; ::_thesis: (inferior_realsequence f) # x = inferior_realsequence (f # x) now__::_thesis:_for_n_being_Element_of_NAT_holds_((inferior_realsequence_f)_#_x)_._n_=_(inferior_realsequence_(f_#_x))_._n let n be Element of NAT ; ::_thesis: ((inferior_realsequence f) # x) . n = (inferior_realsequence (f # x)) . n A2: ((inferior_realsequence f) # x) . n = ((inferior_realsequence f) . n) . x by MESFUNC5:def_13; dom ((inferior_realsequence f) . n) = dom (f . 0) by Def5; hence ((inferior_realsequence f) # x) . n = (inferior_realsequence (f # x)) . n by A1, A2, Def5; ::_thesis: verum end; hence (inferior_realsequence f) # x = inferior_realsequence (f # x) by FUNCT_2:63; ::_thesis: verum end; end; registration let X, Y be set ; let f be with_the_same_dom Functional_Sequence of X,Y; let n be Element of NAT ; clusterf ^\ n -> with_the_same_dom for Functional_Sequence of X,Y; coherence for b1 being Functional_Sequence of X,Y st b1 = f ^\ n holds b1 is with_the_same_dom proof for k, l being Nat holds dom ((f ^\ n) . k) = dom ((f ^\ n) . l) proof reconsider g = f as Function of NAT,(PFuncs (X,Y)) ; let k, l be Nat; ::_thesis: dom ((f ^\ n) . k) = dom ((f ^\ n) . l) reconsider k9 = k, l9 = l as Element of NAT by ORDINAL1:def_12; dom ((f ^\ n) . k) = dom (g . (n + k9)) by NAT_1:def_3; then dom ((f ^\ n) . k) = dom (g . (n + l9)) by Def2; hence dom ((f ^\ n) . k) = dom ((f ^\ n) . l) by NAT_1:def_3; ::_thesis: verum end; hence for b1 being Functional_Sequence of X,Y st b1 = f ^\ n holds b1 is with_the_same_dom by Def2; ::_thesis: verum end; end; theorem Th8: :: MESFUNC8:8 for X being non empty set for f being with_the_same_dom Functional_Sequence of X,ExtREAL for n being Element of NAT holds (inferior_realsequence f) . n = inf (f ^\ n) proof let X be non empty set ; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,ExtREAL for n being Element of NAT holds (inferior_realsequence f) . n = inf (f ^\ n) let f be with_the_same_dom Functional_Sequence of X,ExtREAL; ::_thesis: for n being Element of NAT holds (inferior_realsequence f) . n = inf (f ^\ n) let n be Element of NAT ; ::_thesis: (inferior_realsequence f) . n = inf (f ^\ n) reconsider g = f as Function of NAT,(PFuncs (X,ExtREAL)) ; dom (inf (f ^\ n)) = dom ((f ^\ n) . 0) by Def3; then dom (inf (f ^\ n)) = dom (g . (n + 0)) by NAT_1:def_3; then A1: dom (inf (f ^\ n)) = dom (f . 0) by Def2; A2: dom ((inferior_realsequence f) . n) = dom (f . 0) by Def5; now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(inf_(f_^\_n))_holds_ (inf_(f_^\_n))_._x_=_((inferior_realsequence_f)_._n)_._x let x be Element of X; ::_thesis: ( x in dom (inf (f ^\ n)) implies (inf (f ^\ n)) . x = ((inferior_realsequence f) . n) . x ) assume A3: x in dom (inf (f ^\ n)) ; ::_thesis: (inf (f ^\ n)) . x = ((inferior_realsequence f) . n) . x now__::_thesis:_for_k_being_Element_of_NAT_holds_((f_^\_n)_#_x)_._k_=_((f_#_x)_^\_n)_._k let k be Element of NAT ; ::_thesis: ((f ^\ n) # x) . k = ((f # x) ^\ n) . k ((f ^\ n) # x) . k = ((f ^\ n) . k) . x by MESFUNC5:def_13; then ((f ^\ n) # x) . k = (g . (n + k)) . x by NAT_1:def_3; then ((f ^\ n) # x) . k = (f # x) . (n + k) by MESFUNC5:def_13; hence ((f ^\ n) # x) . k = ((f # x) ^\ n) . k by NAT_1:def_3; ::_thesis: verum end; then (f ^\ n) # x = (f # x) ^\ n by FUNCT_2:63; then A4: (inf (f ^\ n)) . x = inf ((f # x) ^\ n) by A3, Def3; ((inferior_realsequence f) . n) . x = (inferior_realsequence (f # x)) . n by A2, A1, A3, Def5; hence (inf (f ^\ n)) . x = ((inferior_realsequence f) . n) . x by A4, RINFSUP2:27; ::_thesis: verum end; hence (inferior_realsequence f) . n = inf (f ^\ n) by A2, A1, PARTFUN1:5; ::_thesis: verum end; theorem Th9: :: MESFUNC8:9 for X being non empty set for f being with_the_same_dom Functional_Sequence of X,ExtREAL for n being Element of NAT holds (superior_realsequence f) . n = sup (f ^\ n) proof let X be non empty set ; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,ExtREAL for n being Element of NAT holds (superior_realsequence f) . n = sup (f ^\ n) let f be with_the_same_dom Functional_Sequence of X,ExtREAL; ::_thesis: for n being Element of NAT holds (superior_realsequence f) . n = sup (f ^\ n) let n be Element of NAT ; ::_thesis: (superior_realsequence f) . n = sup (f ^\ n) reconsider g = f as Function of NAT,(PFuncs (X,ExtREAL)) ; dom (sup (f ^\ n)) = dom ((f ^\ n) . 0) by Def4; then dom (sup (f ^\ n)) = dom (g . (n + 0)) by NAT_1:def_3; then A1: dom (sup (f ^\ n)) = dom (f . 0) by Def2; A2: dom ((superior_realsequence f) . n) = dom (f . 0) by Def6; now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(sup_(f_^\_n))_holds_ (sup_(f_^\_n))_._x_=_((superior_realsequence_f)_._n)_._x let x be Element of X; ::_thesis: ( x in dom (sup (f ^\ n)) implies (sup (f ^\ n)) . x = ((superior_realsequence f) . n) . x ) assume A3: x in dom (sup (f ^\ n)) ; ::_thesis: (sup (f ^\ n)) . x = ((superior_realsequence f) . n) . x now__::_thesis:_for_k_being_Element_of_NAT_holds_((f_^\_n)_#_x)_._k_=_((f_#_x)_^\_n)_._k let k be Element of NAT ; ::_thesis: ((f ^\ n) # x) . k = ((f # x) ^\ n) . k ((f ^\ n) # x) . k = ((f ^\ n) . k) . x by MESFUNC5:def_13; then ((f ^\ n) # x) . k = (g . (n + k)) . x by NAT_1:def_3; then ((f ^\ n) # x) . k = (f # x) . (n + k) by MESFUNC5:def_13; hence ((f ^\ n) # x) . k = ((f # x) ^\ n) . k by NAT_1:def_3; ::_thesis: verum end; then (f ^\ n) # x = (f # x) ^\ n by FUNCT_2:63; then A4: (sup (f ^\ n)) . x = sup ((f # x) ^\ n) by A3, Def4; ((superior_realsequence f) . n) . x = (superior_realsequence (f # x)) . n by A2, A1, A3, Def6; hence (sup (f ^\ n)) . x = ((superior_realsequence f) . n) . x by A4, RINFSUP2:27; ::_thesis: verum end; hence (superior_realsequence f) . n = sup (f ^\ n) by A2, A1, PARTFUN1:5; ::_thesis: verum end; theorem Th10: :: MESFUNC8:10 for X being non empty set for f being Functional_Sequence of X,ExtREAL for x being Element of X st x in dom (f . 0) holds (superior_realsequence f) # x = superior_realsequence (f # x) proof let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,ExtREAL for x being Element of X st x in dom (f . 0) holds (superior_realsequence f) # x = superior_realsequence (f # x) let f be Functional_Sequence of X,ExtREAL; ::_thesis: for x being Element of X st x in dom (f . 0) holds (superior_realsequence f) # x = superior_realsequence (f # x) let x be Element of X; ::_thesis: ( x in dom (f . 0) implies (superior_realsequence f) # x = superior_realsequence (f # x) ) set F = superior_realsequence f; assume A1: x in dom (f . 0) ; ::_thesis: (superior_realsequence f) # x = superior_realsequence (f # x) now__::_thesis:_for_n_being_Element_of_NAT_holds_((superior_realsequence_f)_#_x)_._n_=_(superior_realsequence_(f_#_x))_._n let n be Element of NAT ; ::_thesis: ((superior_realsequence f) # x) . n = (superior_realsequence (f # x)) . n A2: ((superior_realsequence f) # x) . n = ((superior_realsequence f) . n) . x by MESFUNC5:def_13; dom ((superior_realsequence f) . n) = dom (f . 0) by Def6; hence ((superior_realsequence f) # x) . n = (superior_realsequence (f # x)) . n by A1, A2, Def6; ::_thesis: verum end; hence (superior_realsequence f) # x = superior_realsequence (f # x) by FUNCT_2:63; ::_thesis: verum end; definition let X be non empty set ; let f be Functional_Sequence of X,ExtREAL; func lim_inf f -> PartFunc of X,ExtREAL means :Def7: :: MESFUNC8:def 7 ( dom it = dom (f . 0) & ( for x being Element of X st x in dom it holds it . x = lim_inf (f # x) ) ); existence ex b1 being PartFunc of X,ExtREAL st ( dom b1 = dom (f . 0) & ( for x being Element of X st x in dom b1 holds b1 . x = lim_inf (f # x) ) ) proof defpred S1[ set ] means \$1 in dom (f . 0); deffunc H1( Element of X) -> Element of ExtREAL = lim_inf (f # \$1); consider g being PartFunc of X,ExtREAL such that A1: ( ( for x being Element of X holds ( x in dom g iff S1[x] ) ) & ( for x being Element of X st x in dom g holds g /. x = H1(x) ) ) from PARTFUN2:sch_2(); take g ; ::_thesis: ( dom g = dom (f . 0) & ( for x being Element of X st x in dom g holds g . x = lim_inf (f # x) ) ) A2: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_g_holds_ g_._x_=_lim_inf_(f_#_x) let x be Element of X; ::_thesis: ( x in dom g implies g . x = lim_inf (f # x) ) assume A3: x in dom g ; ::_thesis: g . x = lim_inf (f # x) then g /. x = lim_inf (f # x) by A1; hence g . x = lim_inf (f # x) by A3, PARTFUN1:def_6; ::_thesis: verum end; for x being set holds ( x in dom g iff x in dom (f . 0) ) by A1; hence ( dom g = dom (f . 0) & ( for x being Element of X st x in dom g holds g . x = lim_inf (f # x) ) ) by A2, TARSKI:1; ::_thesis: verum end; uniqueness for b1, b2 being PartFunc of X,ExtREAL st dom b1 = dom (f . 0) & ( for x being Element of X st x in dom b1 holds b1 . x = lim_inf (f # x) ) & dom b2 = dom (f . 0) & ( for x being Element of X st x in dom b2 holds b2 . x = lim_inf (f # x) ) holds b1 = b2 proof let g, h be PartFunc of X,ExtREAL; ::_thesis: ( dom g = dom (f . 0) & ( for x being Element of X st x in dom g holds g . x = lim_inf (f # x) ) & dom h = dom (f . 0) & ( for x being Element of X st x in dom h holds h . x = lim_inf (f # x) ) implies g = h ) assume that A4: dom g = dom (f . 0) and A5: for x being Element of X st x in dom g holds g . x = lim_inf (f # x) and A6: dom h = dom (f . 0) and A7: for x being Element of X st x in dom h holds h . x = lim_inf (f # x) ; ::_thesis: g = h now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_g_holds_ g_/._x_=_h_/._x let x be Element of X; ::_thesis: ( x in dom g implies g /. x = h /. x ) assume A8: x in dom g ; ::_thesis: g /. x = h /. x then g /. x = g . x by PARTFUN1:def_6; then g /. x = lim_inf (f # x) by A5, A8; then g /. x = h . x by A4, A6, A7, A8; hence g /. x = h /. x by A4, A6, A8, PARTFUN1:def_6; ::_thesis: verum end; hence g = h by A4, A6, PARTFUN2:1; ::_thesis: verum end; end; :: deftheorem Def7 defines lim_inf MESFUNC8:def_7_:_ for X being non empty set for f being Functional_Sequence of X,ExtREAL for b3 being PartFunc of X,ExtREAL holds ( b3 = lim_inf f iff ( dom b3 = dom (f . 0) & ( for x being Element of X st x in dom b3 holds b3 . x = lim_inf (f # x) ) ) ); definition let X be non empty set ; let f be Functional_Sequence of X,ExtREAL; func lim_sup f -> PartFunc of X,ExtREAL means :Def8: :: MESFUNC8:def 8 ( dom it = dom (f . 0) & ( for x being Element of X st x in dom it holds it . x = lim_sup (f # x) ) ); existence ex b1 being PartFunc of X,ExtREAL st ( dom b1 = dom (f . 0) & ( for x being Element of X st x in dom b1 holds b1 . x = lim_sup (f # x) ) ) proof defpred S1[ set ] means \$1 in dom (f . 0); deffunc H1( Element of X) -> Element of ExtREAL = lim_sup (f # \$1); consider g being PartFunc of X,ExtREAL such that A1: ( ( for x being Element of X holds ( x in dom g iff S1[x] ) ) & ( for x being Element of X st x in dom g holds g /. x = H1(x) ) ) from PARTFUN2:sch_2(); take g ; ::_thesis: ( dom g = dom (f . 0) & ( for x being Element of X st x in dom g holds g . x = lim_sup (f # x) ) ) A2: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_g_holds_ g_._x_=_lim_sup_(f_#_x) let x be Element of X; ::_thesis: ( x in dom g implies g . x = lim_sup (f # x) ) assume A3: x in dom g ; ::_thesis: g . x = lim_sup (f # x) then g /. x = lim_sup (f # x) by A1; hence g . x = lim_sup (f # x) by A3, PARTFUN1:def_6; ::_thesis: verum end; for x being set holds ( x in dom g iff x in dom (f . 0) ) by A1; hence ( dom g = dom (f . 0) & ( for x being Element of X st x in dom g holds g . x = lim_sup (f # x) ) ) by A2, TARSKI:1; ::_thesis: verum end; uniqueness for b1, b2 being PartFunc of X,ExtREAL st dom b1 = dom (f . 0) & ( for x being Element of X st x in dom b1 holds b1 . x = lim_sup (f # x) ) & dom b2 = dom (f . 0) & ( for x being Element of X st x in dom b2 holds b2 . x = lim_sup (f # x) ) holds b1 = b2 proof let g, h be PartFunc of X,ExtREAL; ::_thesis: ( dom g = dom (f . 0) & ( for x being Element of X st x in dom g holds g . x = lim_sup (f # x) ) & dom h = dom (f . 0) & ( for x being Element of X st x in dom h holds h . x = lim_sup (f # x) ) implies g = h ) assume that A4: dom g = dom (f . 0) and A5: for x being Element of X st x in dom g holds g . x = lim_sup (f # x) ; ::_thesis: ( not dom h = dom (f . 0) or ex x being Element of X st ( x in dom h & not h . x = lim_sup (f # x) ) or g = h ) assume that A6: dom h = dom (f . 0) and A7: for x being Element of X st x in dom h holds h . x = lim_sup (f # x) ; ::_thesis: g = h now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_g_holds_ g_/._x_=_h_/._x let x be Element of X; ::_thesis: ( x in dom g implies g /. x = h /. x ) assume A8: x in dom g ; ::_thesis: g /. x = h /. x then g /. x = g . x by PARTFUN1:def_6; then g /. x = lim_sup (f # x) by A5, A8; then g /. x = h . x by A4, A6, A7, A8; hence g /. x = h /. x by A4, A6, A8, PARTFUN1:def_6; ::_thesis: verum end; hence g = h by A4, A6, PARTFUN2:1; ::_thesis: verum end; end; :: deftheorem Def8 defines lim_sup MESFUNC8:def_8_:_ for X being non empty set for f being Functional_Sequence of X,ExtREAL for b3 being PartFunc of X,ExtREAL holds ( b3 = lim_sup f iff ( dom b3 = dom (f . 0) & ( for x being Element of X st x in dom b3 holds b3 . x = lim_sup (f # x) ) ) ); theorem Th11: :: MESFUNC8:11 for X being non empty set for f being Functional_Sequence of X,ExtREAL holds ( ( for x being Element of X st x in dom (lim_inf f) holds ( (lim_inf f) . x = sup (inferior_realsequence (f # x)) & (lim_inf f) . x = sup ((inferior_realsequence f) # x) & (lim_inf f) . x = (sup (inferior_realsequence f)) . x ) ) & lim_inf f = sup (inferior_realsequence f) ) proof let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,ExtREAL holds ( ( for x being Element of X st x in dom (lim_inf f) holds ( (lim_inf f) . x = sup (inferior_realsequence (f # x)) & (lim_inf f) . x = sup ((inferior_realsequence f) # x) & (lim_inf f) . x = (sup (inferior_realsequence f)) . x ) ) & lim_inf f = sup (inferior_realsequence f) ) let f be Functional_Sequence of X,ExtREAL; ::_thesis: ( ( for x being Element of X st x in dom (lim_inf f) holds ( (lim_inf f) . x = sup (inferior_realsequence (f # x)) & (lim_inf f) . x = sup ((inferior_realsequence f) # x) & (lim_inf f) . x = (sup (inferior_realsequence f)) . x ) ) & lim_inf f = sup (inferior_realsequence f) ) dom (sup (inferior_realsequence f)) = dom ((inferior_realsequence f) . 0) by Def4; then dom (sup (inferior_realsequence f)) = dom (f . 0) by Def5; then A1: dom (sup (inferior_realsequence f)) = dom (lim_inf f) by Def7; A2: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(lim_inf_f)_holds_ (_(lim_inf_f)_._x_=_sup_(inferior_realsequence_(f_#_x))_&_(lim_inf_f)_._x_=_sup_((inferior_realsequence_f)_#_x)_&_(lim_inf_f)_._x_=_(sup_(inferior_realsequence_f))_._x_) let x be Element of X; ::_thesis: ( x in dom (lim_inf f) implies ( (lim_inf f) . x = sup (inferior_realsequence (f # x)) & (lim_inf f) . x = sup ((inferior_realsequence f) # x) & (lim_inf f) . x = (sup (inferior_realsequence f)) . x ) ) assume A3: x in dom (lim_inf f) ; ::_thesis: ( (lim_inf f) . x = sup (inferior_realsequence (f # x)) & (lim_inf f) . x = sup ((inferior_realsequence f) # x) & (lim_inf f) . x = (sup (inferior_realsequence f)) . x ) then A4: (lim_inf f) . x = lim_inf (f # x) by Def7; hence (lim_inf f) . x = sup (inferior_realsequence (f # x)) ; ::_thesis: ( (lim_inf f) . x = sup ((inferior_realsequence f) # x) & (lim_inf f) . x = (sup (inferior_realsequence f)) . x ) dom (lim_inf f) = dom (f . 0) by Def7; hence (lim_inf f) . x = sup ((inferior_realsequence f) # x) by A3, A4, Th7; ::_thesis: (lim_inf f) . x = (sup (inferior_realsequence f)) . x hence (lim_inf f) . x = (sup (inferior_realsequence f)) . x by A1, A3, Def4; ::_thesis: verum end; then for x being Element of X st x in dom (lim_inf f) holds (lim_inf f) . x = (sup (inferior_realsequence f)) . x ; hence ( ( for x being Element of X st x in dom (lim_inf f) holds ( (lim_inf f) . x = sup (inferior_realsequence (f # x)) & (lim_inf f) . x = sup ((inferior_realsequence f) # x) & (lim_inf f) . x = (sup (inferior_realsequence f)) . x ) ) & lim_inf f = sup (inferior_realsequence f) ) by A1, A2, PARTFUN1:5; ::_thesis: verum end; theorem Th12: :: MESFUNC8:12 for X being non empty set for f being Functional_Sequence of X,ExtREAL holds ( ( for x being Element of X st x in dom (lim_sup f) holds ( (lim_sup f) . x = inf (superior_realsequence (f # x)) & (lim_sup f) . x = inf ((superior_realsequence f) # x) & (lim_sup f) . x = (inf (superior_realsequence f)) . x ) ) & lim_sup f = inf (superior_realsequence f) ) proof let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,ExtREAL holds ( ( for x being Element of X st x in dom (lim_sup f) holds ( (lim_sup f) . x = inf (superior_realsequence (f # x)) & (lim_sup f) . x = inf ((superior_realsequence f) # x) & (lim_sup f) . x = (inf (superior_realsequence f)) . x ) ) & lim_sup f = inf (superior_realsequence f) ) let f be Functional_Sequence of X,ExtREAL; ::_thesis: ( ( for x being Element of X st x in dom (lim_sup f) holds ( (lim_sup f) . x = inf (superior_realsequence (f # x)) & (lim_sup f) . x = inf ((superior_realsequence f) # x) & (lim_sup f) . x = (inf (superior_realsequence f)) . x ) ) & lim_sup f = inf (superior_realsequence f) ) A1: dom (inf (superior_realsequence f)) = dom ((superior_realsequence f) . 0) by Def3 .= dom (f . 0) by Def6 .= dom (lim_sup f) by Def8 ; A2: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(lim_sup_f)_holds_ (_(lim_sup_f)_._x_=_inf_(superior_realsequence_(f_#_x))_&_(lim_sup_f)_._x_=_inf_((superior_realsequence_f)_#_x)_&_(lim_sup_f)_._x_=_(inf_(superior_realsequence_f))_._x_) let x be Element of X; ::_thesis: ( x in dom (lim_sup f) implies ( (lim_sup f) . x = inf (superior_realsequence (f # x)) & (lim_sup f) . x = inf ((superior_realsequence f) # x) & (lim_sup f) . x = (inf (superior_realsequence f)) . x ) ) assume A3: x in dom (lim_sup f) ; ::_thesis: ( (lim_sup f) . x = inf (superior_realsequence (f # x)) & (lim_sup f) . x = inf ((superior_realsequence f) # x) & (lim_sup f) . x = (inf (superior_realsequence f)) . x ) then A4: (lim_sup f) . x = lim_sup (f # x) by Def8; hence (lim_sup f) . x = inf (superior_realsequence (f # x)) ; ::_thesis: ( (lim_sup f) . x = inf ((superior_realsequence f) # x) & (lim_sup f) . x = (inf (superior_realsequence f)) . x ) dom (lim_sup f) = dom (f . 0) by Def8; hence (lim_sup f) . x = inf ((superior_realsequence f) # x) by A3, A4, Th10; ::_thesis: (lim_sup f) . x = (inf (superior_realsequence f)) . x hence (lim_sup f) . x = (inf (superior_realsequence f)) . x by A1, A3, Def3; ::_thesis: verum end; then for x being Element of X st x in dom (lim_sup f) holds (lim_sup f) . x = (inf (superior_realsequence f)) . x ; hence ( ( for x being Element of X st x in dom (lim_sup f) holds ( (lim_sup f) . x = inf (superior_realsequence (f # x)) & (lim_sup f) . x = inf ((superior_realsequence f) # x) & (lim_sup f) . x = (inf (superior_realsequence f)) . x ) ) & lim_sup f = inf (superior_realsequence f) ) by A1, A2, PARTFUN1:5; ::_thesis: verum end; theorem :: MESFUNC8:13 for X being non empty set for f being Functional_Sequence of X,ExtREAL for x being Element of X st x in dom (f . 0) holds ( f # x is convergent iff (lim_sup f) . x = (lim_inf f) . x ) proof let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,ExtREAL for x being Element of X st x in dom (f . 0) holds ( f # x is convergent iff (lim_sup f) . x = (lim_inf f) . x ) let f be Functional_Sequence of X,ExtREAL; ::_thesis: for x being Element of X st x in dom (f . 0) holds ( f # x is convergent iff (lim_sup f) . x = (lim_inf f) . x ) let x be Element of X; ::_thesis: ( x in dom (f . 0) implies ( f # x is convergent iff (lim_sup f) . x = (lim_inf f) . x ) ) assume A1: x in dom (f . 0) ; ::_thesis: ( f # x is convergent iff (lim_sup f) . x = (lim_inf f) . x ) then x in dom (lim_inf f) by Def7; then A2: (lim_inf f) . x = lim_inf (f # x) by Def7; x in dom (lim_sup f) by A1, Def8; then (lim_sup f) . x = lim_sup (f # x) by Def8; hence ( f # x is convergent iff (lim_sup f) . x = (lim_inf f) . x ) by A2, RINFSUP2:40; ::_thesis: verum end; definition let X be non empty set ; let f be Functional_Sequence of X,ExtREAL; func lim f -> PartFunc of X,ExtREAL means :Def9: :: MESFUNC8:def 9 ( dom it = dom (f . 0) & ( for x being Element of X st x in dom it holds it . x = lim (f # x) ) ); existence ex b1 being PartFunc of X,ExtREAL st ( dom b1 = dom (f . 0) & ( for x being Element of X st x in dom b1 holds b1 . x = lim (f # x) ) ) proof defpred S1[ set ] means \$1 in dom (f . 0); deffunc H1( Element of X) -> Element of ExtREAL = lim (f # \$1); consider g being PartFunc of X,ExtREAL such that A1: ( ( for x being Element of X holds ( x in dom g iff S1[x] ) ) & ( for x being Element of X st x in dom g holds g /. x = H1(x) ) ) from PARTFUN2:sch_2(); take g ; ::_thesis: ( dom g = dom (f . 0) & ( for x being Element of X st x in dom g holds g . x = lim (f # x) ) ) A2: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_g_holds_ g_._x_=_lim_(f_#_x) let x be Element of X; ::_thesis: ( x in dom g implies g . x = lim (f # x) ) assume A3: x in dom g ; ::_thesis: g . x = lim (f # x) then g /. x = lim (f # x) by A1; hence g . x = lim (f # x) by A3, PARTFUN1:def_6; ::_thesis: verum end; for x being set holds ( x in dom g iff x in dom (f . 0) ) by A1; hence ( dom g = dom (f . 0) & ( for x being Element of X st x in dom g holds g . x = lim (f # x) ) ) by A2, TARSKI:1; ::_thesis: verum end; uniqueness for b1, b2 being PartFunc of X,ExtREAL st dom b1 = dom (f . 0) & ( for x being Element of X st x in dom b1 holds b1 . x = lim (f # x) ) & dom b2 = dom (f . 0) & ( for x being Element of X st x in dom b2 holds b2 . x = lim (f # x) ) holds b1 = b2 proof let g, h be PartFunc of X,ExtREAL; ::_thesis: ( dom g = dom (f . 0) & ( for x being Element of X st x in dom g holds g . x = lim (f # x) ) & dom h = dom (f . 0) & ( for x being Element of X st x in dom h holds h . x = lim (f # x) ) implies g = h ) assume that A4: dom g = dom (f . 0) and A5: for x being Element of X st x in dom g holds g . x = lim (f # x) ; ::_thesis: ( not dom h = dom (f . 0) or ex x being Element of X st ( x in dom h & not h . x = lim (f # x) ) or g = h ) assume that A6: dom h = dom (f . 0) and A7: for x being Element of X st x in dom h holds h . x = lim (f # x) ; ::_thesis: g = h now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_g_holds_ g_/._x_=_h_/._x let x be Element of X; ::_thesis: ( x in dom g implies g /. x = h /. x ) assume A8: x in dom g ; ::_thesis: g /. x = h /. x then g /. x = g . x by PARTFUN1:def_6; then g /. x = lim (f # x) by A5, A8; then g /. x = h . x by A4, A6, A7, A8; hence g /. x = h /. x by A4, A6, A8, PARTFUN1:def_6; ::_thesis: verum end; hence g = h by A4, A6, PARTFUN2:1; ::_thesis: verum end; end; :: deftheorem Def9 defines lim MESFUNC8:def_9_:_ for X being non empty set for f being Functional_Sequence of X,ExtREAL for b3 being PartFunc of X,ExtREAL holds ( b3 = lim f iff ( dom b3 = dom (f . 0) & ( for x being Element of X st x in dom b3 holds b3 . x = lim (f # x) ) ) ); theorem Th14: :: MESFUNC8:14 for X being non empty set for f being Functional_Sequence of X,ExtREAL for x being Element of X st x in dom (lim f) & f # x is convergent holds ( (lim f) . x = (lim_sup f) . x & (lim f) . x = (lim_inf f) . x ) proof let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,ExtREAL for x being Element of X st x in dom (lim f) & f # x is convergent holds ( (lim f) . x = (lim_sup f) . x & (lim f) . x = (lim_inf f) . x ) let f be Functional_Sequence of X,ExtREAL; ::_thesis: for x being Element of X st x in dom (lim f) & f # x is convergent holds ( (lim f) . x = (lim_sup f) . x & (lim f) . x = (lim_inf f) . x ) let x be Element of X; ::_thesis: ( x in dom (lim f) & f # x is convergent implies ( (lim f) . x = (lim_sup f) . x & (lim f) . x = (lim_inf f) . x ) ) assume that A1: x in dom (lim f) and A2: f # x is convergent ; ::_thesis: ( (lim f) . x = (lim_sup f) . x & (lim f) . x = (lim_inf f) . x ) A3: lim (f # x) = lim_inf (f # x) by A2, RINFSUP2:41; A4: x in dom (f . 0) by A1, Def9; then x in dom (lim_sup f) by Def8; then A5: (lim_sup f) . x = lim_sup (f # x) by Def8; x in dom (lim_inf f) by A4, Def7; then A6: (lim_inf f) . x = lim_inf (f # x) by Def7; lim (f # x) = lim_sup (f # x) by A2, RINFSUP2:41; hence ( (lim f) . x = (lim_sup f) . x & (lim f) . x = (lim_inf f) . x ) by A1, A5, A6, A3, Def9; ::_thesis: verum end; theorem Th15: :: MESFUNC8:15 for X being non empty set for S being SigmaField of X for f being with_the_same_dom Functional_Sequence of X,ExtREAL for F being SetSequence of S for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) ) holds union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r))) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being with_the_same_dom Functional_Sequence of X,ExtREAL for F being SetSequence of S for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) ) holds union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r))) let S be SigmaField of X; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,ExtREAL for F being SetSequence of S for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) ) holds union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r))) let f be with_the_same_dom Functional_Sequence of X,ExtREAL; ::_thesis: for F being SetSequence of S for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) ) holds union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r))) let F be SetSequence of S; ::_thesis: for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) ) holds union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r))) let r be real number ; ::_thesis: ( ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) ) implies union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r))) ) set E = dom (f . 0); assume A1: for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) ; ::_thesis: union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r))) now__::_thesis:_for_x_being_set_st_x_in_(dom_(f_._0))_/\_(great_dom_((sup_f),(R_EAL_r)))_holds_ x_in_union_(rng_F) let x be set ; ::_thesis: ( x in (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r))) implies x in union (rng F) ) assume A2: x in (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r))) ; ::_thesis: x in union (rng F) then reconsider z = x as Element of X ; A3: x in dom (f . 0) by A2, XBOOLE_0:def_4; x in great_dom ((sup f),(R_EAL r)) by A2, XBOOLE_0:def_4; then A4: R_EAL r < (sup f) . z by MESFUNC1:def_13; ex n being Element of NAT st R_EAL r < (f . n) . z proof assume A5: for n being Element of NAT holds (f . n) . z <= R_EAL r ; ::_thesis: contradiction for x being ext-real number st x in rng (f # z) holds x <= R_EAL r proof let x be ext-real number ; ::_thesis: ( x in rng (f # z) implies x <= R_EAL r ) assume x in rng (f # z) ; ::_thesis: x <= R_EAL r then consider m being set such that A6: m in NAT and A7: x = (f # z) . m by FUNCT_2:11; reconsider m = m as Element of NAT by A6; x = (f . m) . z by A7, MESFUNC5:def_13; hence x <= R_EAL r by A5; ::_thesis: verum end; then R_EAL r is UpperBound of rng (f # z) by XXREAL_2:def_1; then A8: sup (f # z) <= R_EAL r by XXREAL_2:def_3; x in dom (sup f) by A3, Def4; hence contradiction by A4, A8, Def4; ::_thesis: verum end; then consider n being Element of NAT such that A9: R_EAL r < (f . n) . z ; x in dom (f . n) by A3, Def2; then A10: x in great_dom ((f . n),(R_EAL r)) by A9, MESFUNC1:def_13; A11: F . n in rng F by FUNCT_2:4; A12: F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) by A1; x in dom (f . 0) by A2, XBOOLE_0:def_4; then x in F . n by A10, A12, XBOOLE_0:def_4; hence x in union (rng F) by A11, TARSKI:def_4; ::_thesis: verum end; then A13: (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r))) c= union (rng F) by TARSKI:def_3; now__::_thesis:_for_x_being_set_st_x_in_union_(rng_F)_holds_ x_in_(dom_(f_._0))_/\_(great_dom_((sup_f),(R_EAL_r))) let x be set ; ::_thesis: ( x in union (rng F) implies x in (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r))) ) assume x in union (rng F) ; ::_thesis: x in (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r))) then consider y being set such that A14: x in y and A15: y in rng F by TARSKI:def_4; reconsider z = x as Element of X by A14, A15; consider n being set such that A16: n in dom F and A17: y = F . n by A15, FUNCT_1:def_3; reconsider n = n as Element of NAT by A16; A18: F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) by A1; then x in great_dom ((f . n),r) by A14, A17, XBOOLE_0:def_4; then A19: r < (f . n) . z by MESFUNC1:def_13; A20: (f . n) . z = (f # z) . n by MESFUNC5:def_13; A21: x in dom (f . 0) by A14, A17, A18, XBOOLE_0:def_4; then A22: x in dom (sup f) by Def4; then (sup f) . z = sup (f # z) by Def4; then (f . n) . z <= (sup f) . z by A20, RINFSUP2:23; then R_EAL r < (sup f) . z by A19, XXREAL_0:2; then x in great_dom ((sup f),(R_EAL r)) by A22, MESFUNC1:def_13; hence x in (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r))) by A21, XBOOLE_0:def_4; ::_thesis: verum end; then union (rng F) c= (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r))) by TARSKI:def_3; hence union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r))) by A13, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th16: :: MESFUNC8:16 for X being non empty set for S being SigmaField of X for f being with_the_same_dom Functional_Sequence of X,ExtREAL for F being SetSequence of S for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),(R_EAL r))) ) holds meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),(R_EAL r))) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being with_the_same_dom Functional_Sequence of X,ExtREAL for F being SetSequence of S for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),(R_EAL r))) ) holds meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),(R_EAL r))) let S be SigmaField of X; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,ExtREAL for F being SetSequence of S for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),(R_EAL r))) ) holds meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),(R_EAL r))) let f be with_the_same_dom Functional_Sequence of X,ExtREAL; ::_thesis: for F being SetSequence of S for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),(R_EAL r))) ) holds meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),(R_EAL r))) let F be SetSequence of S; ::_thesis: for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),(R_EAL r))) ) holds meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),(R_EAL r))) let r be real number ; ::_thesis: ( ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),(R_EAL r))) ) implies meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),(R_EAL r))) ) set E = dom (f . 0); assume A1: for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),(R_EAL r))) ; ::_thesis: meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),(R_EAL r))) now__::_thesis:_for_x_being_set_st_x_in_meet_(rng_F)_holds_ x_in_(dom_(f_._0))_/\_(great_eq_dom_((inf_f),(R_EAL_r))) let x be set ; ::_thesis: ( x in meet (rng F) implies x in (dom (f . 0)) /\ (great_eq_dom ((inf f),(R_EAL r))) ) assume A2: x in meet (rng F) ; ::_thesis: x in (dom (f . 0)) /\ (great_eq_dom ((inf f),(R_EAL r))) then reconsider z = x as Element of X ; A3: F . 0 = (dom (f . 0)) /\ (great_eq_dom ((f . 0),(R_EAL r))) by A1; F . 0 in rng F by FUNCT_2:4; then x in F . 0 by A2, SETFAM_1:def_1; then A4: x in dom (f . 0) by A3, XBOOLE_0:def_4; then A5: x in dom (inf f) by Def3; A6: now__::_thesis:_for_n_being_Element_of_NAT_holds_R_EAL_r_<=_(f_#_z)_._n let n be Element of NAT ; ::_thesis: R_EAL r <= (f # z) . n F . n in rng F by FUNCT_2:4; then A7: z in F . n by A2, SETFAM_1:def_1; F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),(R_EAL r))) by A1; then x in great_eq_dom ((f . n),(R_EAL r)) by A7, XBOOLE_0:def_4; then R_EAL r <= (f . n) . z by MESFUNC1:def_14; hence R_EAL r <= (f # z) . n by MESFUNC5:def_13; ::_thesis: verum end; now__::_thesis:_for_s_being_ext-real_number_st_s_in_rng_(f_#_z)_holds_ R_EAL_r_<=_s let s be ext-real number ; ::_thesis: ( s in rng (f # z) implies R_EAL r <= s ) assume s in rng (f # z) ; ::_thesis: R_EAL r <= s then ex k being set st ( k in NAT & s = (f # z) . k ) by FUNCT_2:11; hence R_EAL r <= s by A6; ::_thesis: verum end; then R_EAL r is LowerBound of rng (f # z) by XXREAL_2:def_2; then R_EAL r <= inf (f # z) by XXREAL_2:def_4; then R_EAL r <= (inf f) . x by A5, Def3; then x in great_eq_dom ((inf f),(R_EAL r)) by A5, MESFUNC1:def_14; hence x in (dom (f . 0)) /\ (great_eq_dom ((inf f),(R_EAL r))) by A4, XBOOLE_0:def_4; ::_thesis: verum end; then A8: meet (rng F) c= (dom (f . 0)) /\ (great_eq_dom ((inf f),(R_EAL r))) by TARSKI:def_3; now__::_thesis:_for_x_being_set_st_x_in_(dom_(f_._0))_/\_(great_eq_dom_((inf_f),(R_EAL_r)))_holds_ x_in_meet_(rng_F) let x be set ; ::_thesis: ( x in (dom (f . 0)) /\ (great_eq_dom ((inf f),(R_EAL r))) implies x in meet (rng F) ) assume A9: x in (dom (f . 0)) /\ (great_eq_dom ((inf f),(R_EAL r))) ; ::_thesis: x in meet (rng F) then reconsider z = x as Element of X ; A10: x in dom (f . 0) by A9, XBOOLE_0:def_4; x in great_eq_dom ((inf f),(R_EAL r)) by A9, XBOOLE_0:def_4; then A11: R_EAL r <= (inf f) . z by MESFUNC1:def_14; now__::_thesis:_for_y_being_set_st_y_in_rng_F_holds_ x_in_y let y be set ; ::_thesis: ( y in rng F implies x in y ) assume y in rng F ; ::_thesis: x in y then consider n being set such that A12: n in NAT and A13: y = F . n by FUNCT_2:11; reconsider n = n as Element of NAT by A12; A14: x in dom (f . n) by A10, Def2; x in dom (inf f) by A10, Def3; then A15: (inf f) . z = inf (f # z) by Def3; A16: x in dom (f . 0) by A9, XBOOLE_0:def_4; (f . n) . z = (f # z) . n by MESFUNC5:def_13; then inf (f # z) <= (f . n) . z by RINFSUP2:23; then R_EAL r <= (f . n) . z by A11, A15, XXREAL_0:2; then A17: x in great_eq_dom ((f . n),(R_EAL r)) by A14, MESFUNC1:def_14; F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),(R_EAL r))) by A1; hence x in y by A13, A16, A17, XBOOLE_0:def_4; ::_thesis: verum end; hence x in meet (rng F) by SETFAM_1:def_1; ::_thesis: verum end; then (dom (f . 0)) /\ (great_eq_dom ((inf f),(R_EAL r))) c= meet (rng F) by TARSKI:def_3; hence meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),(R_EAL r))) by A8, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th17: :: MESFUNC8:17 for X being non empty set for S being SigmaField of X for f being with_the_same_dom Functional_Sequence of X,ExtREAL for F being SetSequence of S for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) ) holds for n being Nat holds (superior_setsequence F) . n = (dom (f . 0)) /\ (great_dom (((superior_realsequence f) . n),(R_EAL r))) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being with_the_same_dom Functional_Sequence of X,ExtREAL for F being SetSequence of S for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) ) holds for n being Nat holds (superior_setsequence F) . n = (dom (f . 0)) /\ (great_dom (((superior_realsequence f) . n),(R_EAL r))) let S be SigmaField of X; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,ExtREAL for F being SetSequence of S for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) ) holds for n being Nat holds (superior_setsequence F) . n = (dom (f . 0)) /\ (great_dom (((superior_realsequence f) . n),(R_EAL r))) let f be with_the_same_dom Functional_Sequence of X,ExtREAL; ::_thesis: for F being SetSequence of S for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) ) holds for n being Nat holds (superior_setsequence F) . n = (dom (f . 0)) /\ (great_dom (((superior_realsequence f) . n),(R_EAL r))) let F be SetSequence of S; ::_thesis: for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) ) holds for n being Nat holds (superior_setsequence F) . n = (dom (f . 0)) /\ (great_dom (((superior_realsequence f) . n),(R_EAL r))) let r be real number ; ::_thesis: ( ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) ) implies for n being Nat holds (superior_setsequence F) . n = (dom (f . 0)) /\ (great_dom (((superior_realsequence f) . n),(R_EAL r))) ) set E = dom (f . 0); assume A1: for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) ; ::_thesis: for n being Nat holds (superior_setsequence F) . n = (dom (f . 0)) /\ (great_dom (((superior_realsequence f) . n),(R_EAL r))) let n be Nat; ::_thesis: (superior_setsequence F) . n = (dom (f . 0)) /\ (great_dom (((superior_realsequence f) . n),(R_EAL r))) reconsider n9 = n as Element of NAT by ORDINAL1:def_12; set f1 = f ^\ n9; set F1 = F ^\ n9; A2: now__::_thesis:_for_k_being_Nat_holds_(F_^\_n9)_._k_=_(dom_(f_._0))_/\_(great_dom_(((f_^\_n9)_._k),(R_EAL_r))) let k be Nat; ::_thesis: (F ^\ n9) . k = (dom (f . 0)) /\ (great_dom (((f ^\ n9) . k),(R_EAL r))) reconsider k9 = k as Element of NAT by ORDINAL1:def_12; (F ^\ n9) . k = F . (n + k9) by NAT_1:def_3; then (F ^\ n9) . k = (dom (f . 0)) /\ (great_dom ((f . (n + k9)),(R_EAL r))) by A1; hence (F ^\ n9) . k = (dom (f . 0)) /\ (great_dom (((f ^\ n9) . k),(R_EAL r))) by NAT_1:def_3; ::_thesis: verum end; A3: union (rng (F ^\ n9)) = (superior_setsequence F) . n by Th2; consider g being Function of NAT,(PFuncs (X,ExtREAL)) such that A6: f = g and f ^\ n9 = g ^\ n9 ; (f ^\ n9) . 0 = g . (n + 0) by A6, NAT_1:def_3; then dom ((f ^\ n9) . 0) = dom (f . 0) by A6, Def2; then union (rng (F ^\ n9)) = (dom (f . 0)) /\ (great_dom ((sup (f ^\ n9)),(R_EAL r))) by A2, Th15; hence (superior_setsequence F) . n = (dom (f . 0)) /\ (great_dom (((superior_realsequence f) . n),(R_EAL r))) by A3, Th9; ::_thesis: verum end; theorem Th18: :: MESFUNC8:18 for X being non empty set for S being SigmaField of X for f being with_the_same_dom Functional_Sequence of X,ExtREAL for F being SetSequence of S for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),(R_EAL r))) ) holds for n being Nat holds (inferior_setsequence F) . n = (dom (f . 0)) /\ (great_eq_dom (((inferior_realsequence f) . n),(R_EAL r))) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being with_the_same_dom Functional_Sequence of X,ExtREAL for F being SetSequence of S for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),(R_EAL r))) ) holds for n being Nat holds (inferior_setsequence F) . n = (dom (f . 0)) /\ (great_eq_dom (((inferior_realsequence f) . n),(R_EAL r))) let S be SigmaField of X; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,ExtREAL for F being SetSequence of S for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),(R_EAL r))) ) holds for n being Nat holds (inferior_setsequence F) . n = (dom (f . 0)) /\ (great_eq_dom (((inferior_realsequence f) . n),(R_EAL r))) let f be with_the_same_dom Functional_Sequence of X,ExtREAL; ::_thesis: for F being SetSequence of S for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),(R_EAL r))) ) holds for n being Nat holds (inferior_setsequence F) . n = (dom (f . 0)) /\ (great_eq_dom (((inferior_realsequence f) . n),(R_EAL r))) let F be SetSequence of S; ::_thesis: for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),(R_EAL r))) ) holds for n being Nat holds (inferior_setsequence F) . n = (dom (f . 0)) /\ (great_eq_dom (((inferior_realsequence f) . n),(R_EAL r))) let r be real number ; ::_thesis: ( ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),(R_EAL r))) ) implies for n being Nat holds (inferior_setsequence F) . n = (dom (f . 0)) /\ (great_eq_dom (((inferior_realsequence f) . n),(R_EAL r))) ) set E = dom (f . 0); assume A1: for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),(R_EAL r))) ; ::_thesis: for n being Nat holds (inferior_setsequence F) . n = (dom (f . 0)) /\ (great_eq_dom (((inferior_realsequence f) . n),(R_EAL r))) let n be Nat; ::_thesis: (inferior_setsequence F) . n = (dom (f . 0)) /\ (great_eq_dom (((inferior_realsequence f) . n),(R_EAL r))) reconsider n9 = n as Element of NAT by ORDINAL1:def_12; set f1 = f ^\ n9; set F1 = F ^\ n9; A2: now__::_thesis:_for_k_being_Nat_holds_(F_^\_n9)_._k_=_(dom_(f_._0))_/\_(great_eq_dom_(((f_^\_n9)_._k),(R_EAL_r))) let k be Nat; ::_thesis: (F ^\ n9) . k = (dom (f . 0)) /\ (great_eq_dom (((f ^\ n9) . k),(R_EAL r))) reconsider k9 = k as Element of NAT by ORDINAL1:def_12; (F ^\ n9) . k = F . (n + k9) by NAT_1:def_3; then (F ^\ n9) . k = (dom (f . 0)) /\ (great_eq_dom ((f . (n + k9)),(R_EAL r))) by A1; hence (F ^\ n9) . k = (dom (f . 0)) /\ (great_eq_dom (((f ^\ n9) . k),(R_EAL r))) by NAT_1:def_3; ::_thesis: verum end; A3: meet (rng (F ^\ n9)) = (inferior_setsequence F) . n by Th2; consider g being Function of NAT,(PFuncs (X,ExtREAL)) such that A6: f = g and f ^\ n9 = g ^\ n9 ; (f ^\ n9) . 0 = g . (n + 0) by A6, NAT_1:def_3; then dom ((f ^\ n9) . 0) = dom (f . 0) by A6, Def2; then meet (rng (F ^\ n9)) = (dom (f . 0)) /\ (great_eq_dom ((inf (f ^\ n9)),(R_EAL r))) by A2, Th16; hence (inferior_setsequence F) . n = (dom (f . 0)) /\ (great_eq_dom (((inferior_realsequence f) . n),(R_EAL r))) by A3, Th8; ::_thesis: verum end; theorem Th19: :: MESFUNC8:19 for X being non empty set for S being SigmaField of X for f being with_the_same_dom Functional_Sequence of X,ExtREAL for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds for n being Nat holds (superior_realsequence f) . n is_measurable_on E proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being with_the_same_dom Functional_Sequence of X,ExtREAL for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds for n being Nat holds (superior_realsequence f) . n is_measurable_on E let S be SigmaField of X; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,ExtREAL for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds for n being Nat holds (superior_realsequence f) . n is_measurable_on E let f be with_the_same_dom Functional_Sequence of X,ExtREAL; ::_thesis: for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds for n being Nat holds (superior_realsequence f) . n is_measurable_on E let E be Element of S; ::_thesis: ( dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) implies for n being Nat holds (superior_realsequence f) . n is_measurable_on E ) assume that A1: dom (f . 0) = E and A2: for n being Nat holds f . n is_measurable_on E ; ::_thesis: for n being Nat holds (superior_realsequence f) . n is_measurable_on E let n be Nat; ::_thesis: (superior_realsequence f) . n is_measurable_on E reconsider n9 = n as Element of NAT by ORDINAL1:def_12; A3: now__::_thesis:_for_r_being_real_number_holds_E_/\_(great_dom_(((superior_realsequence_f)_._n),(R_EAL_r)))_in_S let r be real number ; ::_thesis: E /\ (great_dom (((superior_realsequence f) . n),(R_EAL r))) in S deffunc H1( Element of NAT ) -> Element of bool X = E /\ (great_dom ((f . \$1),(R_EAL r))); consider F being Function of NAT,(bool X) such that A4: for x being Element of NAT holds F . x = H1(x) from FUNCT_2:sch_4(); now__::_thesis:_for_i_being_Nat_holds_F_._i_in_S let i be Nat; ::_thesis: F . i in S A5: f . i is_measurable_on E by A2; i in NAT by ORDINAL1:def_12; then A6: F . i = E /\ (great_dom ((f . i),(R_EAL r))) by A4; dom (f . i) = E by A1, Def2; hence F . i in S by A6, A5, MESFUNC1:29; ::_thesis: verum end; then A7: rng F c= S by NAT_1:52; A8: for x being Nat holds F . x = E /\ (great_dom ((f . x),(R_EAL r))) proof let x be Nat; ::_thesis: F . x = E /\ (great_dom ((f . x),(R_EAL r))) reconsider x9 = x as Element of NAT by ORDINAL1:def_12; F . x9 = E /\ (great_dom ((f . x9),(R_EAL r))) by A4; hence F . x = E /\ (great_dom ((f . x),(R_EAL r))) ; ::_thesis: verum end; reconsider F = F as SetSequence of S by A7, RELAT_1:def_19; (superior_setsequence F) . n9 in rng (superior_setsequence F) by NAT_1:51; then (superior_setsequence F) . n9 in S ; hence E /\ (great_dom (((superior_realsequence f) . n),(R_EAL r))) in S by A1, A8, Th17; ::_thesis: verum end; dom ((superior_realsequence f) . n9) = E by A1, Def6; hence (superior_realsequence f) . n is_measurable_on E by A3, MESFUNC1:29; ::_thesis: verum end; theorem Th20: :: MESFUNC8:20 for X being non empty set for S being SigmaField of X for f being with_the_same_dom Functional_Sequence of X,ExtREAL for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds for n being Nat holds (inferior_realsequence f) . n is_measurable_on E proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being with_the_same_dom Functional_Sequence of X,ExtREAL for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds for n being Nat holds (inferior_realsequence f) . n is_measurable_on E let S be SigmaField of X; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,ExtREAL for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds for n being Nat holds (inferior_realsequence f) . n is_measurable_on E let f be with_the_same_dom Functional_Sequence of X,ExtREAL; ::_thesis: for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds for n being Nat holds (inferior_realsequence f) . n is_measurable_on E let E be Element of S; ::_thesis: ( dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) implies for n being Nat holds (inferior_realsequence f) . n is_measurable_on E ) assume that A1: dom (f . 0) = E and A2: for n being Nat holds f . n is_measurable_on E ; ::_thesis: for n being Nat holds (inferior_realsequence f) . n is_measurable_on E let n be Nat; ::_thesis: (inferior_realsequence f) . n is_measurable_on E reconsider n9 = n as Element of NAT by ORDINAL1:def_12; A3: now__::_thesis:_for_r_being_real_number_holds_E_/\_(great_eq_dom_(((inferior_realsequence_f)_._n),(R_EAL_r)))_in_S let r be real number ; ::_thesis: E /\ (great_eq_dom (((inferior_realsequence f) . n),(R_EAL r))) in S deffunc H1( Element of NAT ) -> Element of bool X = E /\ (great_eq_dom ((f . \$1),(R_EAL r))); consider F being Function of NAT,(bool X) such that A4: for x being Element of NAT holds F . x = H1(x) from FUNCT_2:sch_4(); now__::_thesis:_for_i_being_Nat_holds_F_._i_in_S let i be Nat; ::_thesis: F . i in S A5: f . i is_measurable_on E by A2; i in NAT by ORDINAL1:def_12; then A6: F . i = E /\ (great_eq_dom ((f . i),(R_EAL r))) by A4; dom (f . i) = E by A1, Def2; hence F . i in S by A6, A5, MESFUNC1:27; ::_thesis: verum end; then A7: rng F c= S by NAT_1:52; A8: for x being Nat holds F . x = E /\ (great_eq_dom ((f . x),(R_EAL r))) proof let x be Nat; ::_thesis: F . x = E /\ (great_eq_dom ((f . x),(R_EAL r))) reconsider x9 = x as Element of NAT by ORDINAL1:def_12; F . x9 = E /\ (great_eq_dom ((f . x9),(R_EAL r))) by A4; hence F . x = E /\ (great_eq_dom ((f . x),(R_EAL r))) ; ::_thesis: verum end; reconsider F = F as SetSequence of S by A7, RELAT_1:def_19; (inferior_setsequence F) . n9 in rng (inferior_setsequence F) by NAT_1:51; then (inferior_setsequence F) . n9 in S ; hence E /\ (great_eq_dom (((inferior_realsequence f) . n),(R_EAL r))) in S by A1, A8, Th18; ::_thesis: verum end; dom ((inferior_realsequence f) . n9) = E by A1, Def5; hence (inferior_realsequence f) . n is_measurable_on E by A3, MESFUNC1:27; ::_thesis: verum end; theorem Th21: :: MESFUNC8:21 for X being non empty set for S being SigmaField of X for f being Functional_Sequence of X,ExtREAL for F being SetSequence of S for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom (((superior_realsequence f) . n),(R_EAL r))) ) holds meet F = (dom (f . 0)) /\ (great_eq_dom ((lim_sup f),(R_EAL r))) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being Functional_Sequence of X,ExtREAL for F being SetSequence of S for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom (((superior_realsequence f) . n),(R_EAL r))) ) holds meet F = (dom (f . 0)) /\ (great_eq_dom ((lim_sup f),(R_EAL r))) let S be SigmaField of X; ::_thesis: for f being Functional_Sequence of X,ExtREAL for F being SetSequence of S for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom (((superior_realsequence f) . n),(R_EAL r))) ) holds meet F = (dom (f . 0)) /\ (great_eq_dom ((lim_sup f),(R_EAL r))) let f be Functional_Sequence of X,ExtREAL; ::_thesis: for F being SetSequence of S for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom (((superior_realsequence f) . n),(R_EAL r))) ) holds meet F = (dom (f . 0)) /\ (great_eq_dom ((lim_sup f),(R_EAL r))) let F be SetSequence of S; ::_thesis: for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom (((superior_realsequence f) . n),(R_EAL r))) ) holds meet F = (dom (f . 0)) /\ (great_eq_dom ((lim_sup f),(R_EAL r))) let r be real number ; ::_thesis: ( ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom (((superior_realsequence f) . n),(R_EAL r))) ) implies meet F = (dom (f . 0)) /\ (great_eq_dom ((lim_sup f),(R_EAL r))) ) set E = dom (f . 0); set g = superior_realsequence f; assume A1: for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom (((superior_realsequence f) . n),(R_EAL r))) ; ::_thesis: meet F = (dom (f . 0)) /\ (great_eq_dom ((lim_sup f),(R_EAL r))) dom ((superior_realsequence f) . 0) = dom (f . 0) by Def6; then meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf (superior_realsequence f)),(R_EAL r))) by A1, Th16; hence meet F = (dom (f . 0)) /\ (great_eq_dom ((lim_sup f),(R_EAL r))) by Th12; ::_thesis: verum end; theorem Th22: :: MESFUNC8:22 for X being non empty set for S being SigmaField of X for f being Functional_Sequence of X,ExtREAL for F being SetSequence of S for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom (((inferior_realsequence f) . n),(R_EAL r))) ) holds union (rng F) = (dom (f . 0)) /\ (great_dom ((lim_inf f),(R_EAL r))) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being Functional_Sequence of X,ExtREAL for F being SetSequence of S for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom (((inferior_realsequence f) . n),(R_EAL r))) ) holds union (rng F) = (dom (f . 0)) /\ (great_dom ((lim_inf f),(R_EAL r))) let S be SigmaField of X; ::_thesis: for f being Functional_Sequence of X,ExtREAL for F being SetSequence of S for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom (((inferior_realsequence f) . n),(R_EAL r))) ) holds union (rng F) = (dom (f . 0)) /\ (great_dom ((lim_inf f),(R_EAL r))) let f be Functional_Sequence of X,ExtREAL; ::_thesis: for F being SetSequence of S for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom (((inferior_realsequence f) . n),(R_EAL r))) ) holds union (rng F) = (dom (f . 0)) /\ (great_dom ((lim_inf f),(R_EAL r))) let F be SetSequence of S; ::_thesis: for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom (((inferior_realsequence f) . n),(R_EAL r))) ) holds union (rng F) = (dom (f . 0)) /\ (great_dom ((lim_inf f),(R_EAL r))) let r be real number ; ::_thesis: ( ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom (((inferior_realsequence f) . n),(R_EAL r))) ) implies union (rng F) = (dom (f . 0)) /\ (great_dom ((lim_inf f),(R_EAL r))) ) set E = dom (f . 0); set g = inferior_realsequence f; assume A1: for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom (((inferior_realsequence f) . n),(R_EAL r))) ; ::_thesis: union (rng F) = (dom (f . 0)) /\ (great_dom ((lim_inf f),(R_EAL r))) dom ((inferior_realsequence f) . 0) = dom (f . 0) by Def5; then union (rng F) = (dom (f . 0)) /\ (great_dom ((sup (inferior_realsequence f)),(R_EAL r))) by A1, Th15; hence union (rng F) = (dom (f . 0)) /\ (great_dom ((lim_inf f),(R_EAL r))) by Th11; ::_thesis: verum end; theorem Th23: :: MESFUNC8:23 for X being non empty set for S being SigmaField of X for f being with_the_same_dom Functional_Sequence of X,ExtREAL for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds lim_sup f is_measurable_on E proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being with_the_same_dom Functional_Sequence of X,ExtREAL for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds lim_sup f is_measurable_on E let S be SigmaField of X; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,ExtREAL for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds lim_sup f is_measurable_on E let f be with_the_same_dom Functional_Sequence of X,ExtREAL; ::_thesis: for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds lim_sup f is_measurable_on E let E be Element of S; ::_thesis: ( dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) implies lim_sup f is_measurable_on E ) assume that A1: dom (f . 0) = E and A2: for n being Nat holds f . n is_measurable_on E ; ::_thesis: lim_sup f is_measurable_on E A3: now__::_thesis:_for_r_being_real_number_holds_E_/\_(great_eq_dom_((lim_sup_f),(R_EAL_r)))_in_S let r be real number ; ::_thesis: E /\ (great_eq_dom ((lim_sup f),(R_EAL r))) in S deffunc H1( Element of NAT ) -> Element of bool X = E /\ (great_eq_dom (((superior_realsequence f) . \$1),(R_EAL r))); consider F being Function of NAT,(bool X) such that A4: for x being Element of NAT holds F . x = H1(x) from FUNCT_2:sch_4(); now__::_thesis:_for_i_being_Nat_holds_F_._i_in_S let i be Nat; ::_thesis: F . i in S A5: dom ((superior_realsequence f) . i) = dom (f . 0) by Def6; i in NAT by ORDINAL1:def_12; then A6: F . i = E /\ (great_eq_dom (((superior_realsequence f) . i),(R_EAL r))) by A4; (superior_realsequence f) . i is_measurable_on E by A1, A2, Th19; hence F . i in S by A1, A6, A5, MESFUNC1:27; ::_thesis: verum end; then A7: rng F c= S by NAT_1:52; A8: for x being Nat holds F . x = E /\ (great_eq_dom (((superior_realsequence f) . x),(R_EAL r))) proof let x be Nat; ::_thesis: F . x = E /\ (great_eq_dom (((superior_realsequence f) . x),(R_EAL r))) reconsider x9 = x as Element of NAT by ORDINAL1:def_12; F . x9 = E /\ (great_eq_dom (((superior_realsequence f) . x9),(R_EAL r))) by A4; hence F . x = E /\ (great_eq_dom (((superior_realsequence f) . x),(R_EAL r))) ; ::_thesis: verum end; reconsider F = F as SetSequence of S by A7, RELAT_1:def_19; rng F c= S ; then F is Function of NAT,S by FUNCT_2:6; then A9: rng F is N_Sub_set_fam of X by MEASURE1:23; A10: rng F is N_Measure_fam of S by A9, MEASURE2:def_1; meet F = E /\ (great_eq_dom ((lim_sup f),(R_EAL r))) by A1, A8, Th21; hence E /\ (great_eq_dom ((lim_sup f),(R_EAL r))) in S by A10, MEASURE2:2; ::_thesis: verum end; dom (lim_sup f) = dom (f . 0) by Def8; hence lim_sup f is_measurable_on E by A1, A3, MESFUNC1:27; ::_thesis: verum end; theorem :: MESFUNC8:24 for X being non empty set for S being SigmaField of X for f being with_the_same_dom Functional_Sequence of X,ExtREAL for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds lim_inf f is_measurable_on E proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being with_the_same_dom Functional_Sequence of X,ExtREAL for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds lim_inf f is_measurable_on E let S be SigmaField of X; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,ExtREAL for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds lim_inf f is_measurable_on E let f be with_the_same_dom Functional_Sequence of X,ExtREAL; ::_thesis: for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds lim_inf f is_measurable_on E let E be Element of S; ::_thesis: ( dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) implies lim_inf f is_measurable_on E ) assume that A1: dom (f . 0) = E and A2: for n being Nat holds f . n is_measurable_on E ; ::_thesis: lim_inf f is_measurable_on E A3: now__::_thesis:_for_r_being_real_number_holds_E_/\_(great_dom_((lim_inf_f),(R_EAL_r)))_in_S let r be real number ; ::_thesis: E /\ (great_dom ((lim_inf f),(R_EAL r))) in S deffunc H1( Element of NAT ) -> Element of bool X = E /\ (great_dom (((inferior_realsequence f) . \$1),(R_EAL r))); consider F being Function of NAT,(bool X) such that A4: for x being Element of NAT holds F . x = H1(x) from FUNCT_2:sch_4(); now__::_thesis:_for_i_being_Nat_holds_F_._i_in_S let i be Nat; ::_thesis: F . i in S i in NAT by ORDINAL1:def_12; then A5: F . i = E /\ (great_dom (((inferior_realsequence f) . i),(R_EAL r))) by A4; A6: dom ((inferior_realsequence f) . i) = E by A1, Def5; (inferior_realsequence f) . i is_measurable_on E by A1, A2, Th20; hence F . i in S by A5, A6, MESFUNC1:29; ::_thesis: verum end; then A7: rng F c= S by NAT_1:52; A8: for x being Nat holds F . x = E /\ (great_dom (((inferior_realsequence f) . x),(R_EAL r))) proof let x be Nat; ::_thesis: F . x = E /\ (great_dom (((inferior_realsequence f) . x),(R_EAL r))) reconsider x9 = x as Element of NAT by ORDINAL1:def_12; F . x9 = E /\ (great_dom (((inferior_realsequence f) . x9),(R_EAL r))) by A4; hence F . x = E /\ (great_dom (((inferior_realsequence f) . x),(R_EAL r))) ; ::_thesis: verum end; reconsider F = F as SetSequence of S by A7, RELAT_1:def_19; rng F c= S ; then F is Function of NAT,S by FUNCT_2:6; then A9: rng F is N_Sub_set_fam of X by MEASURE1:23; A10: rng F is N_Measure_fam of S by A9, MEASURE2:def_1; union (rng F) = E /\ (great_dom ((lim_inf f),(R_EAL r))) by A1, A8, Th22; hence E /\ (great_dom ((lim_inf f),(R_EAL r))) in S by A10, MEASURE2:2; ::_thesis: verum end; dom (lim_inf f) = E by A1, Def7; hence lim_inf f is_measurable_on E by A3, MESFUNC1:29; ::_thesis: verum end; theorem Th25: :: MESFUNC8:25 for X being non empty set for S being SigmaField of X for f being with_the_same_dom Functional_Sequence of X,ExtREAL for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & ( for x being Element of X st x in E holds f # x is convergent ) holds lim f is_measurable_on E proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being with_the_same_dom Functional_Sequence of X,ExtREAL for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & ( for x being Element of X st x in E holds f # x is convergent ) holds lim f is_measurable_on E let S be SigmaField of X; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,ExtREAL for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & ( for x being Element of X st x in E holds f # x is convergent ) holds lim f is_measurable_on E let f be with_the_same_dom Functional_Sequence of X,ExtREAL; ::_thesis: for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & ( for x being Element of X st x in E holds f # x is convergent ) holds lim f is_measurable_on E let E be Element of S; ::_thesis: ( dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & ( for x being Element of X st x in E holds f # x is convergent ) implies lim f is_measurable_on E ) assume A1: dom (f . 0) = E ; ::_thesis: ( ex n being Nat st not f . n is_measurable_on E or ex x being Element of X st ( x in E & not f # x is convergent ) or lim f is_measurable_on E ) then A2: dom (lim_sup f) = E by Def8; assume that A3: for n being Nat holds f . n is_measurable_on E and A4: for x being Element of X st x in E holds f # x is convergent ; ::_thesis: lim f is_measurable_on E A5: dom (lim f) = E by A1, Def9; A6: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(lim_f)_holds_ (lim_f)_._x_=_(lim_sup_f)_._x let x be Element of X; ::_thesis: ( x in dom (lim f) implies (lim f) . x = (lim_sup f) . x ) assume A7: x in dom (lim f) ; ::_thesis: (lim f) . x = (lim_sup f) . x then f # x is convergent by A5, A4; hence (lim f) . x = (lim_sup f) . x by A7, Th14; ::_thesis: verum end; lim_sup f is_measurable_on E by A1, A3, Th23; hence lim f is_measurable_on E by A5, A2, A6, PARTFUN1:5; ::_thesis: verum end; theorem Th26: :: MESFUNC8:26 for X being non empty set for S being SigmaField of X for f being with_the_same_dom Functional_Sequence of X,ExtREAL for g being PartFunc of X,ExtREAL for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & dom g = E & ( for x being Element of X st x in E holds ( f # x is convergent & g . x = lim (f # x) ) ) holds g is_measurable_on E proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being with_the_same_dom Functional_Sequence of X,ExtREAL for g being PartFunc of X,ExtREAL for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & dom g = E & ( for x being Element of X st x in E holds ( f # x is convergent & g . x = lim (f # x) ) ) holds g is_measurable_on E let S be SigmaField of X; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,ExtREAL for g being PartFunc of X,ExtREAL for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & dom g = E & ( for x being Element of X st x in E holds ( f # x is convergent & g . x = lim (f # x) ) ) holds g is_measurable_on E let f be with_the_same_dom Functional_Sequence of X,ExtREAL; ::_thesis: for g being PartFunc of X,ExtREAL for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & dom g = E & ( for x being Element of X st x in E holds ( f # x is convergent & g . x = lim (f # x) ) ) holds g is_measurable_on E let g be PartFunc of X,ExtREAL; ::_thesis: for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & dom g = E & ( for x being Element of X st x in E holds ( f # x is convergent & g . x = lim (f # x) ) ) holds g is_measurable_on E let E be Element of S; ::_thesis: ( dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & dom g = E & ( for x being Element of X st x in E holds ( f # x is convergent & g . x = lim (f # x) ) ) implies g is_measurable_on E ) assume that A1: dom (f . 0) = E and A2: for n being Nat holds f . n is_measurable_on E and A3: dom g = E and A4: for x being Element of X st x in E holds ( f # x is convergent & g . x = lim (f # x) ) ; ::_thesis: g is_measurable_on E A5: dom (lim f) = E by A1, Def9; now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(lim_f)_holds_ g_._x_=_(lim_f)_._x let x be Element of X; ::_thesis: ( x in dom (lim f) implies g . x = (lim f) . x ) assume A6: x in dom (lim f) ; ::_thesis: g . x = (lim f) . x then g . x = lim (f # x) by A4, A5; hence g . x = (lim f) . x by A6, Def9; ::_thesis: verum end; then A7: g = lim f by A3, A5, PARTFUN1:5; for x being Element of X st x in E holds f # x is convergent by A4; hence g is_measurable_on E by A1, A2, A7, Th25; ::_thesis: verum end; theorem Th27: :: MESFUNC8:27 for X being non empty set for f being Functional_Sequence of X,ExtREAL for g being PartFunc of X,ExtREAL st ( for x being Element of X st x in dom g holds ( f # x is convergent_to_finite_number & g . x = lim (f # x) ) ) holds g is real-valued proof let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,ExtREAL for g being PartFunc of X,ExtREAL st ( for x being Element of X st x in dom g holds ( f # x is convergent_to_finite_number & g . x = lim (f # x) ) ) holds g is real-valued let f be Functional_Sequence of X,ExtREAL; ::_thesis: for g being PartFunc of X,ExtREAL st ( for x being Element of X st x in dom g holds ( f # x is convergent_to_finite_number & g . x = lim (f # x) ) ) holds g is real-valued let g be PartFunc of X,ExtREAL; ::_thesis: ( ( for x being Element of X st x in dom g holds ( f # x is convergent_to_finite_number & g . x = lim (f # x) ) ) implies g is real-valued ) assume A1: for x being Element of X st x in dom g holds ( f # x is convergent_to_finite_number & g . x = lim (f # x) ) ; ::_thesis: g is real-valued now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_g_holds_ |.(g_._x).|_<_+infty let x be Element of X; ::_thesis: ( x in dom g implies |.(g . x).| < +infty ) assume A2: x in dom g ; ::_thesis: |.(g . x).| < +infty then A3: ( not lim (f # x) = +infty or not f # x is convergent_to_+infty ) by A1, MESFUNC5:50; f # x is convergent_to_finite_number by A1, A2; then A4: f # x is convergent by MESFUNC5:def_11; ( not lim (f # x) = -infty or not f # x is convergent_to_-infty ) by A1, A2, MESFUNC5:51; then consider g0 being real number such that A5: lim (f # x) = g0 and 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 and f # x is convergent_to_finite_number by A4, A3, MESFUNC5:def_12; g0 is Real by XREAL_0:def_1; then |.(g . x).| = abs g0 by A1, A2, A5, EXTREAL2:1; hence |.(g . x).| < +infty by XXREAL_0:9; ::_thesis: verum end; hence g is real-valued by MESFUNC2:def_1; ::_thesis: verum end; begin theorem Th28: :: MESFUNC8:28 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for f being with_the_same_dom Functional_Sequence of X,ExtREAL for g being PartFunc of X,ExtREAL for E being Element of S st M . E < +infty & dom (f . 0) = E & ( for n being Nat holds ( f . n is_measurable_on E & f . n is real-valued ) ) & dom g = E & ( for x being Element of X st x in E holds ( f # x is convergent_to_finite_number & g . x = lim (f # x) ) ) holds for r, e being real number st 0 < r & 0 < e holds ex H being Element of S ex N being Nat st ( 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 ) ) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for f being with_the_same_dom Functional_Sequence of X,ExtREAL for g being PartFunc of X,ExtREAL for E being Element of S st M . E < +infty & dom (f . 0) = E & ( for n being Nat holds ( f . n is_measurable_on E & f . n is real-valued ) ) & dom g = E & ( for x being Element of X st x in E holds ( f # x is convergent_to_finite_number & g . x = lim (f # x) ) ) holds for r, e being real number st 0 < r & 0 < e holds ex H being Element of S ex N being Nat st ( 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 ) ) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f being with_the_same_dom Functional_Sequence of X,ExtREAL for g being PartFunc of X,ExtREAL for E being Element of S st M . E < +infty & dom (f . 0) = E & ( for n being Nat holds ( f . n is_measurable_on E & f . n is real-valued ) ) & dom g = E & ( for x being Element of X st x in E holds ( f # x is convergent_to_finite_number & g . x = lim (f # x) ) ) holds for r, e being real number st 0 < r & 0 < e holds ex H being Element of S ex N being Nat st ( 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 ) ) let M be sigma_Measure of S; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,ExtREAL for g being PartFunc of X,ExtREAL for E being Element of S st M . E < +infty & dom (f . 0) = E & ( for n being Nat holds ( f . n is_measurable_on E & f . n is real-valued ) ) & dom g = E & ( for x being Element of X st x in E holds ( f # x is convergent_to_finite_number & g . x = lim (f # x) ) ) holds for r, e being real number st 0 < r & 0 < e holds ex H being Element of S ex N being Nat st ( 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 ) ) let f be with_the_same_dom Functional_Sequence of X,ExtREAL; ::_thesis: for g being PartFunc of X,ExtREAL for E being Element of S st M . E < +infty & dom (f . 0) = E & ( for n being Nat holds ( f . n is_measurable_on E & f . n is real-valued ) ) & dom g = E & ( for x being Element of X st x in E holds ( f # x is convergent_to_finite_number & g . x = lim (f # x) ) ) holds for r, e being real number st 0 < r & 0 < e holds ex H being Element of S ex N being Nat st ( 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 ) ) let g be PartFunc of X,ExtREAL; ::_thesis: for E being Element of S st M . E < +infty & dom (f . 0) = E & ( for n being Nat holds ( f . n is_measurable_on E & f . n is real-valued ) ) & dom g = E & ( for x being Element of X st x in E holds ( f # x is convergent_to_finite_number & g . x = lim (f # x) ) ) holds for r, e being real number st 0 < r & 0 < e holds ex H being Element of S ex N being Nat st ( 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 ) ) let E be Element of S; ::_thesis: ( M . E < +infty & dom (f . 0) = E & ( for n being Nat holds ( f . n is_measurable_on E & f . n is real-valued ) ) & dom g = E & ( for x being Element of X st x in E holds ( f # x is convergent_to_finite_number & g . x = lim (f # x) ) ) implies for r, e being real number st 0 < r & 0 < e holds ex H being Element of S ex N being Nat st ( 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 ) ) ) assume that A1: M . E < +infty and A2: dom (f . 0) = E and A3: for n being Nat 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: for r, e being real number st 0 < r & 0 < e holds ex H being Element of S ex N being Nat st ( 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 ) ) let r, e be real number ; ::_thesis: ( 0 < r & 0 < e implies ex H being Element of S ex N being Nat st ( 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 ) ) ) defpred S1[ Element of NAT , set ] means \$2 = E /\ (less_dom (|.((f . \$1) - g).|,(R_EAL 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) ) proof let x be Element of X; ::_thesis: ( x in E implies ( f # x is convergent & g . x = lim (f # x) ) ) assume A7: x in E ; ::_thesis: ( f # x is convergent & g . x = lim (f # x) ) then f # x is convergent_to_finite_number by A5; hence f # x is convergent by MESFUNC5:def_11; ::_thesis: g . x = lim (f # x) thus g . x = lim (f # x) by A5, A7; ::_thesis: verum end; then A8: g is_measurable_on E by A2, A3, A4, Th26; A9: 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: ( |.((f . n) - g).| is_measurable_on E & dom ((f . n) - g) = E & dom |.((f . n) - g).| = E ) 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_measurable_on E by A3; then (f . n) - g is_measurable_on E by A4, A8, A6, A10, MESFUNC2:11; hence ( |.((f . n) - g).| is_measurable_on E & dom ((f . n) - g) = E & dom |.((f . n) - g).| = E ) by A11, MESFUNC1:def_10, MESFUNC2:27; ::_thesis: verum end; A12: for n being Element of NAT ex Z being Element of S st S1[n,Z] proof let n be Element of NAT ; ::_thesis: ex Z being Element of S st S1[n,Z] |.((f . n) - g).| is_measurable_on E by A9; then E /\ (less_dom (|.((f . n) - g).|,(R_EAL e))) in S by MESFUNC1:def_16; hence ex Z being Element of S st S1[n,Z] ; ::_thesis: verum end; consider K being Function of NAT,S such that A13: for n being Element of NAT holds S1[n,K . n] from FUNCT_2:sch_3(A12); defpred S2[ Element of 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 S2[n,Z] proof let n be Element of NAT ; ::_thesis: ex Z being Element of S st S2[n,Z] take { x where x is Element of X : for k being Nat st n <= k holds x in K . k } ; ::_thesis: ( { 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 & S2[n, { x where x is Element of X : for k being Nat st n <= k holds x in K . k } ] ) 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 & S2[n, { x where x is Element of X : for k being Nat st n <= k holds x in K . k } ] ) by Th1; ::_thesis: verum end; consider EN being Function of NAT,S such that A15: for n being Element of NAT holds S2[n,EN . n] from FUNCT_2:sch_3(A14); A16: 0. <= M . E by MEASURE1:def_2; then reconsider ME = M . E as Real by A1, XXREAL_0:14; defpred S3[ Element of NAT , set ] means \$2 = M . (EN . \$1); A17: 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 Real by A1, A16, XXREAL_0:14; let n be Nat; ::_thesis: ( 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 ) reconsider n9 = n as Element of NAT by ORDINAL1:def_12; thus A18: EN . n c= E ::_thesis: ( 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 z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in EN . n or z in E ) assume z in EN . n ; ::_thesis: z in E then z in { x where x is Element of X : for k being Nat st n9 <= k holds x in K . k } by A15; 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).|,(R_EAL e))) by A13; hence z in E by XBOOLE_0:def_4; ::_thesis: verum end; hence A19: M . (EN . n) <= M . E by MEASURE1:31; ::_thesis: ( M . (EN . n) is Element of REAL & M . (E \ (EN . n)) = (M . E) - (M . (EN . n)) & M . (E \ (EN . n)) is Element of REAL ) A20: -infty < M . (EN . n) by MEASURE1:def_2; then reconsider r2 = M . (EN . n) as Real by A1, A19, XXREAL_0:14; thus M . (EN . n) is Element of REAL by A1, A19, A20, XXREAL_0:14; ::_thesis: ( M . (E \ (EN . n)) = (M . E) - (M . (EN . n)) & M . (E \ (EN . n)) is Element of REAL ) thus M . (E \ (EN . n)) = (M . E) - (M . (EN . n)) by A1, A18, A19, MEASURE1:32, XXREAL_0:4; ::_thesis: M . (E \ (EN . n)) is Element of REAL (M . E) - (M . (EN . n)) = r1 - r2 by SUPINF_2:3; hence M . (E \ (EN . n)) is Element of REAL by A18, MEASURE1:32, XXREAL_0:4; ::_thesis: verum end; A21: now__::_thesis:_for_n_being_Element_of_NAT_ex_y_being_Element_of_REAL_st_S3[n,y] let n be Element of NAT ; ::_thesis: ex y being Element of REAL st S3[n,y] M . (EN . n) is Element of REAL by A17; hence ex y being Element of REAL st S3[n,y] ; ::_thesis: verum end; consider seq1 being Real_Sequence such that A22: for n being Element of NAT holds S3[n,seq1 . n] from FUNCT_2:sch_3(A21); assume A23: 0 < r ; ::_thesis: ( not 0 < e or ex H being Element of S ex N being Nat st ( 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 ) ) ) assume A24: 0 < e ; ::_thesis: ex H being Element of S ex N being Nat st ( 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 ) ) A25: E c= union (rng EN) proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in E or z in union (rng EN) ) assume A26: z in E ; ::_thesis: z in union (rng EN) then reconsider x = z as Element of X ; A27: ( not lim (f # x) = +infty or not f # x is convergent_to_+infty ) by A5, A26, MESFUNC5:50; f # x is convergent_to_finite_number by A5, A26; then A28: f # x is convergent by MESFUNC5:def_11; ( not lim (f # x) = -infty or not f # x is convergent_to_-infty ) by A5, A26, MESFUNC5:51; 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 A28, A27, MESFUNC5:def_12; then consider n being Nat such that A29: for m being Nat st n <= m holds |.(((f # x) . m) - (lim (f # x))).| < e by A24; reconsider n0 = n as Element of NAT by ORDINAL1:def_12; A30: g . x = lim (f # x) by A5, A26; now__::_thesis:_for_k_being_Nat_st_n0_<=_k_holds_ x_in_K_._k let k be Nat; ::_thesis: ( n0 <= k implies x in K . k ) reconsider k9 = k as Element of NAT by ORDINAL1:def_12; A31: dom |.((f . k9) - g).| = E by A9; assume n0 <= k ; ::_thesis: x in K . k then |.(((f # x) . k) - (lim (f # x))).| < e by A29; then A32: |.(((f . k) . x) - (g . x)).| < e by A30, MESFUNC5:def_13; dom ((f . k9) - g) = E by A9; then |.(((f . k) - g) . x).| < e by A26, A32, MESFUNC1:def_4; then |.((f . k) - g).| . x < e by A26, A31, MESFUNC1:def_10; then x in less_dom (|.((f . k) - g).|,(R_EAL e)) by A26, A31, MESFUNC1:def_11; then x in E /\ (less_dom (|.((f . k) - g).|,(R_EAL e))) by A26, XBOOLE_0:def_4; then x in K . k9 by A13; hence x in K . k ; ::_thesis: verum end; then x in { y where y is Element of X : for k being Nat st n0 <= k holds y in K . k } ; then A33: x in EN . n0 by A15; EN . n0 in rng EN by FUNCT_2:4; hence z in union (rng EN) by A33, TARSKI:def_4; ::_thesis: verum end; defpred S4[ Element of NAT , set ] means \$2 = M . (E \ (EN . \$1)); A34: dom (M * EN) = NAT by FUNCT_2:def_1; A35: 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: ( n <= m implies ( EN . n c= EN . m & M . (EN . n) <= M . (EN . m) ) ) assume A36: n <= m ; ::_thesis: ( EN . n c= EN . m & M . (EN . n) <= M . (EN . m) ) thus EN . n c= EN . m ::_thesis: M . (EN . n) <= M . (EN . m) proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in EN . n or z in EN . m ) assume z in EN . n ; ::_thesis: z in EN . m then z in { x where x is Element of X : for k being Nat st n <= k holds x in K . k } by A15; then A37: 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 A36, 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 A37; hence z in EN . m by A15; ::_thesis: verum end; hence M . (EN . n) <= M . (EN . m) by MEASURE1:31; ::_thesis: verum end; set seq3 = NAT --> ME; A38: for n being Nat holds (NAT --> ME) . n = ME proof let n be Nat; ::_thesis: (NAT --> ME) . n = ME n in NAT by ORDINAL1:def_12; hence (NAT --> ME) . n = ME by FUNCOP_1:7; ::_thesis: verum end; then A39: NAT --> ME is constant by VALUED_0:def_18; A40: now__::_thesis:_for_x_being_set_st_x_in_dom_(M_*_EN)_holds_ (M_*_EN)_._x_=_seq1_._x let x be set ; ::_thesis: ( x in dom (M * EN) implies (M * EN) . x = seq1 . x ) assume A41: x in dom (M * EN) ; ::_thesis: (M * EN) . x = seq1 . x then reconsider n = x as Element of NAT ; (M * EN) . x = M . (EN . n) by A41, FUNCT_1:12; hence (M * EN) . x = seq1 . x by A22; ::_thesis: verum end; dom seq1 = NAT by FUNCT_2:def_1; then A42: M * EN = seq1 by A34, A40, FUNCT_1:2; now__::_thesis:_for_y_being_set_st_y_in_rng_EN_holds_ y_c=_E let y be set ; ::_thesis: ( y in rng EN implies y c= E ) assume y in rng EN ; ::_thesis: y c= E then consider x being set such that A43: x in NAT and A44: y = EN . x by FUNCT_2:11; reconsider x9 = x as Nat by A43; y = EN . x9 by A44; hence y c= E by A17; ::_thesis: verum end; then union (rng EN) c= E by ZFMISC_1:76; then A45: union (rng EN) = E by A25, XBOOLE_0:def_10; A46: ( seq1 is convergent & lim seq1 = M . E ) proof reconsider r1 = M . E as Real by A1, A16, XXREAL_0:14; A47: for n being Element of NAT holds EN . n c= EN . (n + 1) proof let n be Element of NAT ; ::_thesis: EN . n c= EN . (n + 1) n <= n + 1 by NAT_1:12; hence EN . n c= EN . (n + 1) by A35; ::_thesis: verum end; A48: now__::_thesis:_for_n_being_Element_of_NAT_holds_seq1_._n_<_r1_+_1 let n be Element of NAT ; ::_thesis: seq1 . n < r1 + 1 M . (EN . n) <= M . E by A17; then A49: seq1 . n <= r1 by A22; r1 + 0 < r1 + 1 by XREAL_1:8; hence seq1 . n < r1 + 1 by A49, XXREAL_0:2; ::_thesis: verum end; then A50: seq1 is bounded_above by SEQ_2:def_3; consider r being real number such that A51: for n being Element of NAT holds seq1 . n < r by A48; r is UpperBound of rng seq1 proof let d be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not d in rng seq1 or d <= r ) assume d in rng seq1 ; ::_thesis: d <= r then ex x being set st ( x in NAT & d = seq1 . x ) by FUNCT_2:11; hence d <= r by A51; ::_thesis: verum end; then rng seq1 is bounded_above by XXREAL_2:def_10; then A52: sup (rng (M * EN)) = upper_bound (rng seq1) by A42, RINFSUP2:1; now__::_thesis:_for_n,_m_being_Element_of_NAT_st_n_<=_m_holds_ seq1_._n_<=_seq1_._m let n, m be Element of NAT ; ::_thesis: ( n <= m implies seq1 . n <= seq1 . m ) assume A53: n <= m ; ::_thesis: seq1 . n <= seq1 . m A54: seq1 . m = M . (EN . m) by A22; seq1 . n = M . (EN . n) by A22; hence seq1 . n <= seq1 . m by A35, A53, A54; ::_thesis: verum end; then A55: seq1 is V53() by SEQM_3:6; hence seq1 is convergent by A50; ::_thesis: lim seq1 = M . E lim seq1 = upper_bound seq1 by A55, A50, RINFSUP1:24; hence lim seq1 = M . E by A45, A52, A47, MEASURE2:23; ::_thesis: verum end; A56: now__::_thesis:_for_n_being_Element_of_NAT_ex_y_being_Element_of_REAL_st_S4[n,y] let n be Element of NAT ; ::_thesis: ex y being Element of REAL st S4[n,y] M . (E \ (EN . n)) is Element of REAL by A17; hence ex y being Element of REAL st S4[n,y] ; ::_thesis: verum end; consider seq2 being Real_Sequence such that A57: for n being Element of NAT holds S4[n,seq2 . n] from FUNCT_2:sch_3(A56); now__::_thesis:_for_n_being_Element_of_NAT_holds_seq2_._n_=_((NAT_-->_ME)_._n)_+_((-_seq1)_._n) let n be Element of NAT ; ::_thesis: seq2 . n = ((NAT --> ME) . n) + ((- seq1) . n) seq2 . n = M . (E \ (EN . n)) by A57; then A58: seq2 . n = (M . E) - (M . (EN . n)) by A17; M . (EN . n) = seq1 . n by A22; then seq2 . n = ME - (seq1 . n) by A58, SUPINF_2:3; then seq2 . n = ((NAT --> ME) . n) - (seq1 . n) by A38; hence seq2 . n = ((NAT --> ME) . n) + ((- seq1) . n) by SEQ_1:10; ::_thesis: verum end; then A59: seq2 = (NAT --> ME) - seq1 by SEQ_1:7; then A60: seq2 is convergent by A46, A39, SEQ_2:11; A61: (NAT --> ME) . 0 = ME by A38; lim seq2 = (lim (NAT --> ME)) - (lim seq1) by A46, A59, A39, SEQ_2:12; then lim seq2 = ME - ME by A46, A39, A61, SEQ_4:25; then consider N being Element of NAT such that A62: for m being Element of NAT st N <= m holds abs ((seq2 . m) - 0) < r by A23, A60, SEQ_2:def_7; reconsider H = E \ (EN . N) as Element of S ; A63: E \ H = E /\ (EN . N) by XBOOLE_1:48; EN . N c= E by A17; then A64: E \ H = EN . N by A63, XBOOLE_1:28; A65: 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: ( N < k implies for x being Element of X st x in E \ H holds |.(((f . k) . x) - (g . x)).| < e ) reconsider k9 = k as Element of NAT by ORDINAL1:def_12; assume A66: N < k ; ::_thesis: for x being Element of X st x in E \ H holds |.(((f . k) . x) - (g . x)).| < e let x be Element of X; ::_thesis: ( x in E \ H implies |.(((f . k) . x) - (g . x)).| < e ) assume x in E \ H ; ::_thesis: |.(((f . k) . x) - (g . x)).| < e then x in { y where y is Element of X : for k being Nat st N <= k holds y in K . k } by A15, A64; 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 A66; then A67: x in E /\ (less_dom (|.((f . k9) - g).|,(R_EAL e))) by A13; then A68: x in E by XBOOLE_0:def_4; x in less_dom (|.((f . k) - g).|,(R_EAL e)) by A67, XBOOLE_0:def_4; then A69: |.((f . k) - g).| . x < R_EAL e by MESFUNC1:def_11; A70: dom ((f . k9) - g) = E by A9; dom |.((f . k9) - g).| = E by A9; then |.(((f . k) - g) . x).| < e by A68, A69, MESFUNC1:def_10; hence |.(((f . k) . x) - (g . x)).| < e by A68, A70, MESFUNC1:def_4; ::_thesis: verum end; take H ; ::_thesis: ex N being Nat st ( 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 ) ) take N ; ::_thesis: ( 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 ) ) M . (E \ (EN . N)) = seq2 . N by A57; then A71: 0 <= seq2 . N by MEASURE1:def_2; abs ((seq2 . N) - 0) < r by A62; then seq2 . N < r by A71, 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 A57, A65, XBOOLE_1:36; ::_thesis: verum end; theorem :: MESFUNC8:29 for X, Y being non empty set for E being set for F, G being Function of X,Y st ( for x being 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 ; ::_thesis: for E being set for F, G being Function of X,Y st ( for x being Element of X holds G . x = E \ (F . x) ) holds union (rng G) = E \ (meet (rng F)) let E be set ; ::_thesis: for F, G being Function of X,Y st ( for x being Element of X holds G . x = E \ (F . x) ) holds union (rng G) = E \ (meet (rng F)) let F, G be Function of X,Y; ::_thesis: ( ( for x being Element of X holds G . x = E \ (F . x) ) implies union (rng G) = E \ (meet (rng F)) ) assume A1: for x being Element of X holds G . x = E \ (F . x) ; ::_thesis: union (rng G) = E \ (meet (rng F)) A2: dom G = X by FUNCT_2:def_1; now__::_thesis:_for_Z_being_set_st_Z_in_DIFFERENCE_({E},(rng_F))_holds_ Z_in_rng_G let Z be set ; ::_thesis: ( Z in DIFFERENCE ({E},(rng F)) implies Z in rng G ) assume Z in DIFFERENCE ({E},(rng F)) ; ::_thesis: Z in rng G then consider X1, Y being 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 being set such that A6: x in dom F and A7: Y = F . x by A4, FUNCT_1:def_3; reconsider x = 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; ::_thesis: verum end; then A8: DIFFERENCE ({E},(rng F)) c= rng G by TARSKI:def_3; A9: dom F = X by FUNCT_2:def_1; now__::_thesis:_for_Z_being_set_st_Z_in_rng_G_holds_ Z_in_DIFFERENCE_({E},(rng_F)) let Z be set ; ::_thesis: ( Z in rng G implies Z in DIFFERENCE ({E},(rng F)) ) A10: E in {E} by TARSKI:def_1; assume Z in rng G ; ::_thesis: Z in DIFFERENCE ({E},(rng F)) then consider x being set such that A11: x in dom G and A12: Z = G . x by FUNCT_1:def_3; reconsider x = 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; ::_thesis: verum end; then rng G c= DIFFERENCE ({E},(rng F)) by TARSKI:def_3; then DIFFERENCE ({E},(rng F)) = rng G by A8, XBOOLE_0:def_10; hence union (rng G) = E \ (meet (rng F)) by SETFAM_1:27; ::_thesis: verum end; theorem :: MESFUNC8:30 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for f being with_the_same_dom Functional_Sequence of X,ExtREAL for g being PartFunc of X,ExtREAL for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & M . E < +infty & ( 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 ) ) ) & 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) ) ) holds for e being real number st 0 < e holds ex F being Element of S st ( F c= E & M . (E \ F) <= e & ( for p being real number 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 ) ) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for f being with_the_same_dom Functional_Sequence of X,ExtREAL for g being PartFunc of X,ExtREAL for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & M . E < +infty & ( 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 ) ) ) & 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) ) ) holds for e being real number st 0 < e holds ex F being Element of S st ( F c= E & M . (E \ F) <= e & ( for p being real number 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 ) ) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f being with_the_same_dom Functional_Sequence of X,ExtREAL for g being PartFunc of X,ExtREAL for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & M . E < +infty & ( 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 ) ) ) & 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) ) ) holds for e being real number st 0 < e holds ex F being Element of S st ( F c= E & M . (E \ F) <= e & ( for p being real number 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 ) ) let M be sigma_Measure of S; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,ExtREAL for g being PartFunc of X,ExtREAL for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & M . E < +infty & ( 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 ) ) ) & 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) ) ) holds for e being real number st 0 < e holds ex F being Element of S st ( F c= E & M . (E \ F) <= e & ( for p being real number 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 ) ) let f be with_the_same_dom Functional_Sequence of X,ExtREAL; ::_thesis: for g being PartFunc of X,ExtREAL for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & M . E < +infty & ( 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 ) ) ) & 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) ) ) holds for e being real number st 0 < e holds ex F being Element of S st ( F c= E & M . (E \ F) <= e & ( for p being real number 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 ) ) let g be PartFunc of X,ExtREAL; ::_thesis: for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & M . E < +infty & ( 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 ) ) ) & 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) ) ) holds for e being real number st 0 < e holds ex F being Element of S st ( F c= E & M . (E \ F) <= e & ( for p being real number 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 ) ) let E be Element of S; ::_thesis: ( dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & M . E < +infty & ( 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 ) ) ) & 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) ) ) implies for e being real number st 0 < e holds ex F being Element of S st ( F c= E & M . (E \ F) <= e & ( for p being real number 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 ) ) ) 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: for e being real number st 0 < e holds ex F being Element of S st ( F c= E & M . (E \ F) <= e & ( for p being real number 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 ) ) defpred S1[ 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 S1[n,Z] by A4; consider LN being Function of NAT,S such that A7: for n being Element of NAT holds S1[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 number ; ::_thesis: ( 0 < e0 implies 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 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 ) ) ) assume A8: 0 < e0 ; ::_thesis: 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 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 ) ) 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 H1( 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 = H1(n) from SEQFUNC:sch_1(); for n, m being Nat holds dom (fL . n) = dom (fL . m) proof let n, m be Nat; ::_thesis: dom (fL . n) = dom (fL . m) 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: verum end; then reconsider fL = fL as with_the_same_dom Functional_Sequence of X,ExtREAL by Def2; A19: L c= E by A9, A14, XBOOLE_1:1; 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: ( x in L implies ( fL # x is convergent_to_finite_number & (g | L) . x = lim (fL # 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 ; ::_thesis: ( fL # x is convergent_to_finite_number & (g | L) . x = lim (fL # x) ) A24: for y being set st y in NAT holds (fL # x) . y = (f # x) . y proof let y be set ; ::_thesis: ( y in NAT implies (fL # x) . y = (f # x) . y ) assume y in NAT ; ::_thesis: (fL # x) . y = (f # x) . y 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: verum 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: (g | L) . x = lim (fL # x) 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: verum end; defpred S2[ 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: ( dom (fL . n) = L & fL . n is_measurable_on L & fL . n is real-valued ) 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: ( fL . n is_measurable_on L & fL . n is real-valued ) 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: fL . n is real-valued 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: ( x in dom (fL . n) implies |.((fL . n) . x).| < +infty ) 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: |.((fL . n) . x).| < +infty 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: verum end; hence fL . n is real-valued by MESFUNC2:def_1; ::_thesis: verum 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: 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 ) ) 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 < (1 / 2) |^ p by PREPOWER:6; then A36: 0 < ((1 / 2) GeoSeq) . p9 by PREPOWER:def_1; 0 < (1 / 2) |^ p by PREPOWER:6; then A37: 0 < ((1 / 2) GeoSeq) . p9 by PREPOWER:def_1; 0 < e0 / 2 by A8, XREAL_1:139; 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: verum end; A38: for n being Element of NAT ex Z being Element of S st S2[n,Z] proof let n be Element of NAT ; ::_thesis: ex Z being Element of S st S2[n,Z] 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 S2[n,Z] by A39, A40; ::_thesis: verum end; consider HP being Function of NAT,S such that A42: for p being Element of NAT holds S2[p,HP . p] from FUNCT_2:sch_3(A38); defpred S3[ Element of NAT , set ] means \$2 = M . (HP . \$1); A43: for n being Element of NAT ex y being Element of REAL st S3[n,y] proof let n be Element of NAT ; ::_thesis: ex y being Element of REAL st S3[n,y] A44: -infty < M . (HP . n) by MEASURE1:def_2; M . (HP . n) < ((e0 / 2) (#) ((1 / 2) GeoSeq)) . n by A42; then M . (HP . n) is Real by A44, XXREAL_0:48; hence ex y being Element of REAL st S3[n,y] ; ::_thesis: verum end; consider me being Real_Sequence such that A45: for p being Element of NAT holds S3[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 <= ((e0 / 2) (#) ((1 / 2) GeoSeq)) . p me . p = M . (HP . p) by A45; hence me . p <= ((e0 / 2) (#) ((1 / 2) GeoSeq)) . p by A42; ::_thesis: verum end; A47: 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 <= me . p & me . p <= ((e0 / 2) (#) ((1 / 2) GeoSeq)) . p ) 0. <= M . (HP . p) by MEASURE1:def_2; hence ( 0 <= me . p & me . p <= ((e0 / 2) (#) ((1 / 2) GeoSeq)) . p ) by A45, A46; ::_thesis: verum end; then A48: me is nonnegative by RINFSUP1:def_3; deffunc H2( Element of NAT ) -> M11(X,S) = E \ (LN . \$1); consider ELN being Function of NAT,S such that A49: for n being Element of NAT holds ELN . n = H2(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; A50: 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: ( A in RELN implies A is measure_zero of M ) assume A in RELN ; ::_thesis: A is measure_zero of M then consider n being set such that A51: n in NAT and A52: A = ELN . n by FUNCT_2:11; reconsider n = n as Element of NAT by A51; M . (ELN . n) = M . (E \ (LN . n)) by A49 .= 0 by A7 ; hence A is measure_zero of M by A52, MEASURE1:def_7; ::_thesis: verum end; then union RELN is measure_zero of M by MEASURE2:14; then A53: M . (union RELN) = 0. by MEASURE1:def_7; now__::_thesis:_for_x_being_set_st_x_in_E_\_(meet_(rng_LN))_holds_ x_in_union_RELN let x be set ; ::_thesis: ( x in E \ (meet (rng LN)) implies x in union RELN ) assume A54: x in E \ (meet (rng LN)) ; ::_thesis: x in union RELN then A55: x in E by XBOOLE_0:def_5; not x in meet (rng LN) by A54, XBOOLE_0:def_5; then consider Y being set such that A56: Y in rng LN and A57: not x in Y by SETFAM_1:def_1; consider m being set such that A58: m in dom LN and A59: Y = LN . m by A56, FUNCT_1:def_3; reconsider m = m as Element of NAT by A58; dom ELN = NAT by FUNCT_2:def_1; then A60: ELN . m in rng ELN by FUNCT_1:3; ELN . m = E \ (LN . m) by A49; then x in ELN . m by A55, A57, A59, XBOOLE_0:def_5; hence x in union RELN by A60, TARSKI:def_4; ::_thesis: verum end; then A61: E \ (meet (rng LN)) c= union RELN by TARSKI:def_3; now__::_thesis:_for_x_being_set_st_x_in_union_RELN_holds_ x_in_E_\_(meet_(rng_LN)) let x be set ; ::_thesis: ( x in union RELN implies x in E \ (meet (rng LN)) ) assume x in union RELN ; ::_thesis: x in E \ (meet (rng LN)) then consider Y being set such that A62: x in Y and A63: Y in RELN by TARSKI:def_4; consider m being set such that A64: m in dom ELN and A65: ELN . m = Y by A63, FUNCT_1:def_3; reconsider m = m as Element of NAT by A64; dom LN = NAT by FUNCT_2:def_1; then A66: LN . m in rng LN by FUNCT_1:3; A67: Y = E \ (LN . m) by A49, A65; then not x in LN . m by A62, XBOOLE_0:def_5; then A68: not x in meet (rng LN) by A66, SETFAM_1:def_1; x in E by A62, A67, XBOOLE_0:def_5; hence x in E \ (meet (rng LN)) by A68, XBOOLE_0:def_5; ::_thesis: verum end; then union RELN c= E \ (meet (rng LN)) by TARSKI:def_3; then A69: union RELN = E \ (meet (rng LN)) by A61, XBOOLE_0:def_10; rng HP is N_Sub_set_fam of X by MEASURE1:23; then A70: 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 A71: 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 A69, MEASURE1:33; then M . (E \ L) <= 0. by A10, A53; then A72: M . (E \ L) = 0 by MEASURE1:def_2; reconsider MRHP = union (rng HP) as Element of S by MEASURE1:24; A73: M . ((E \ L) \/ MRHP) <= (M . (E \ L)) + (M . MRHP) by MEASURE1:33; E \ F = (E \ L) \/ (E /\ (union (rng HP))) by A71, XBOOLE_1:52; then M . (E \ F) <= M . ((E \ L) \/ MRHP) by A50, MEASURE1:31, XBOOLE_1:9; then M . (E \ F) <= (M . (E \ L)) + (M . MRHP) by A73, XXREAL_0:2; then A74: M . (E \ F) <= M . MRHP by A72, XXREAL_3:4; dom me = NAT by FUNCT_2:def_1; then A75: dom me = dom (M * HP) by FUNCT_2:def_1; A76: for x being set st x in dom me holds me . x = (M * HP) . x proof let x be set ; ::_thesis: ( x in dom me implies me . x = (M * HP) . x ) assume A77: x in dom me ; ::_thesis: me . x = (M * HP) . x then (M * HP) . x = M . (HP . x) by A75, FUNCT_1:12; hence me . x = (M * HP) . x by A45, A77; ::_thesis: verum end; A78: abs (1 / 2) = 1 / 2 by ABSVALUE:def_1; then A79: (1 / 2) GeoSeq is summable by SERIES_1:24; then A80: (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 A48, A75, A76, FUNCT_1:2, PROB_4:12; then A81: M . (union (rng HP)) <= Sum me by A70, MEASURE2:11; A82: 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: ( 0 < q implies ex p being Element of NAT st ((1 / 2) GeoSeq) . p < q ) assume A83: 0 < q ; ::_thesis: ex p being Element of NAT st ((1 / 2) GeoSeq) . p < q A84: lim ((1 / 2) GeoSeq) = 0 by A79, SERIES_1:4; (1 / 2) GeoSeq is convergent by A79, SERIES_1:4; then consider p being Element of NAT such that A85: for n being Element of NAT st p <= n holds abs ((((1 / 2) GeoSeq) . n) - 0) < q by A83, A84, SEQ_2:def_7; take p ; ::_thesis: ((1 / 2) GeoSeq) . p < q 0 < (1 / 2) |^ p by PREPOWER:6; then A86: 0 <= ((1 / 2) GeoSeq) . p by PREPOWER:def_1; abs ((((1 / 2) GeoSeq) . p) - 0) < q by A85; hence ((1 / 2) GeoSeq) . p < q by A86, ABSVALUE:def_1; ::_thesis: verum end; A87: 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: ( x in F implies for p being Element of NAT holds x in L \ (HP . p) ) assume A88: x in F ; ::_thesis: for p being Element of NAT holds x in L \ (HP . p) let p be Element of NAT ; ::_thesis: x in L \ (HP . p) 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 A71, A88; ::_thesis: verum end; A89: for q being real number 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 number ; ::_thesis: ( 0 < q implies 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 ) assume 0 < q ; ::_thesis: 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 then consider p being Element of NAT such that A90: ((1 / 2) GeoSeq) . p < q by A82; consider Np being Element of NAT such that A91: 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: for n being Nat st Np < n holds for x being Element of X st x in F holds |.(((f . n) . x) - (g . x)).| < q hereby ::_thesis: verum let n be Nat; ::_thesis: ( Np < n implies for x being Element of X st x in F holds |.(((f . n) . x) - (g . x)).| < q ) reconsider n9 = n as Element of NAT by ORDINAL1:def_12; assume A92: Np < n ; ::_thesis: for x being Element of X st x in F holds |.(((f . n) . x) - (g . x)).| < q hereby ::_thesis: verum let x be Element of X; ::_thesis: ( x in F implies |.(((f . n) . x) - (g . x)).| < q ) A93: fL . n = (f . n) | L by A17; assume A94: x in F ; ::_thesis: |.(((f . n) . x) - (g . x)).| < q then |.(((fL . n9) . x) - ((g | L) . x)).| < ((1 / 2) GeoSeq) . p by A87, A91, A92; then A95: |.(((fL . n) . x) - ((g | L) . x)).| < q by A90, XXREAL_0:2; A96: F c= L by A71, XBOOLE_1:36; then (g | L) . x = g . x by A94, FUNCT_1:49; hence |.(((f . n) . x) - (g . x)).| < q by A94, A95, A93, A96, FUNCT_1:49; ::_thesis: verum end; end; end; Sum ((1 / 2) GeoSeq) = 1 / (1 - (1 / 2)) by A78, SERIES_1:24; then A97: Sum ((e0 / 2) (#) ((1 / 2) GeoSeq)) = (e0 / 2) * 2 by A79, SERIES_1:10; Sum me <= Sum ((e0 / 2) (#) ((1 / 2) GeoSeq)) by A80, A47, SERIES_1:20; then M . MRHP <= 2 * (e0 / 2) by A81, A97, XXREAL_0:2; then A98: M . (E \ F) <= e0 by A74, XXREAL_0:2; F c= L by A71, XBOOLE_1:36; 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 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, A98, A89, XBOOLE_1:1; ::_thesis: verum end;