:: MEASURE8 semantic presentation begin theorem Th1: :: MEASURE8:1 for seq being ExtREAL_sequence holds Ser seq = Partial_Sums seq proof let seq be ExtREAL_sequence; ::_thesis: Ser seq = Partial_Sums seq for x being set st x in NAT holds (Ser seq) . x = (Partial_Sums seq) . x proof defpred S1[ Nat] means (Ser seq) . $1 = (Partial_Sums seq) . $1; let x be set ; ::_thesis: ( x in NAT implies (Ser seq) . x = (Partial_Sums seq) . x ) A1: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume S1[k] ; ::_thesis: S1[k + 1] then (Ser seq) . (k + 1) = ((Partial_Sums seq) . k) + (seq . (k + 1)) by SUPINF_2:44; hence S1[k + 1] by MESFUNC9:def_1; ::_thesis: verum end; assume x in NAT ; ::_thesis: (Ser seq) . x = (Partial_Sums seq) . x then reconsider n = x as Element of NAT ; (Ser seq) . 0 = seq . 0 by SUPINF_2:44 .= (Partial_Sums seq) . 0 by MESFUNC9:def_1 ; then A2: S1[ 0 ] ; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A2, A1); then (Ser seq) . x = (Partial_Sums seq) . n ; hence (Ser seq) . x = (Partial_Sums seq) . x ; ::_thesis: verum end; hence Ser seq = Partial_Sums seq by FUNCT_2:12; ::_thesis: verum end; theorem Th2: :: MEASURE8:2 for seq being ExtREAL_sequence st seq is nonnegative holds ( seq is summable & SUM seq = Sum seq ) proof let seq be ExtREAL_sequence; ::_thesis: ( seq is nonnegative implies ( seq is summable & SUM seq = Sum seq ) ) assume seq is nonnegative ; ::_thesis: ( seq is summable & SUM seq = Sum seq ) then A1: Partial_Sums seq is non-decreasing by MESFUNC9:16; then Partial_Sums seq is convergent by RINFSUP2:37; hence seq is summable by MESFUNC9:def_2; ::_thesis: SUM seq = Sum seq lim (Partial_Sums seq) = sup (Partial_Sums seq) by A1, RINFSUP2:37; hence Sum seq = SUM seq by Th1; ::_thesis: verum end; theorem Th3: :: MEASURE8:3 for seq1, seq2, seq being ExtREAL_sequence st seq1 is nonnegative & seq2 is nonnegative & ( for n being Nat holds seq . n = (seq1 . n) + (seq2 . n) ) holds ( seq is nonnegative & SUM seq = (SUM seq1) + (SUM seq2) & Sum seq = (Sum seq1) + (Sum seq2) ) proof let seq1, seq2, seq be ExtREAL_sequence; ::_thesis: ( seq1 is nonnegative & seq2 is nonnegative & ( for n being Nat holds seq . n = (seq1 . n) + (seq2 . n) ) implies ( seq is nonnegative & SUM seq = (SUM seq1) + (SUM seq2) & Sum seq = (Sum seq1) + (Sum seq2) ) ) assume that A1: seq1 is nonnegative and A2: seq2 is nonnegative ; ::_thesis: ( ex n being Nat st not seq . n = (seq1 . n) + (seq2 . n) or ( seq is nonnegative & SUM seq = (SUM seq1) + (SUM seq2) & Sum seq = (Sum seq1) + (Sum seq2) ) ) reconsider Hseq = Ser seq2 as ExtREAL_sequence ; reconsider Gseq = Ser seq1 as ExtREAL_sequence ; reconsider Fseq = Ser seq as ExtREAL_sequence ; assume A3: for n being Nat holds seq . n = (seq1 . n) + (seq2 . n) ; ::_thesis: ( seq is nonnegative & SUM seq = (SUM seq1) + (SUM seq2) & Sum seq = (Sum seq1) + (Sum seq2) ) then A4: for n being Element of NAT holds seq . n = (seq1 . n) + (seq2 . n) ; A5: for k being Nat holds Fseq . k = (Gseq . k) + (Hseq . k) proof let k be Nat; ::_thesis: Fseq . k = (Gseq . k) + (Hseq . k) k in NAT by ORDINAL1:def_12; hence Fseq . k = (Gseq . k) + (Hseq . k) by A1, A2, A4, MEASURE7:3; ::_thesis: verum end; for m, n being ext-real number st m in dom Fseq & n in dom Fseq & m <= n holds Fseq . m <= Fseq . n proof let m, n be ext-real number ; ::_thesis: ( m in dom Fseq & n in dom Fseq & m <= n implies Fseq . m <= Fseq . n ) assume that A6: m in dom Fseq and A7: n in dom Fseq and A8: m <= n ; ::_thesis: Fseq . m <= Fseq . n ( Gseq . m <= Gseq . n & Hseq . m <= Hseq . n ) by A1, A2, A6, A7, A8, MEASURE7:8; then (Gseq . m) + (Hseq . m) <= (Gseq . n) + (Hseq . n) by XXREAL_3:36; then Fseq . m <= (Gseq . n) + (Hseq . n) by A1, A2, A4, A6, MEASURE7:3; hence Fseq . m <= Fseq . n by A1, A2, A4, A7, MEASURE7:3; ::_thesis: verum end; then Fseq is non-decreasing by VALUED_0:def_15; then A9: lim Fseq = sup Fseq by RINFSUP2:37; Partial_Sums seq1 is non-decreasing by A1, MESFUNC9:16; then Gseq is non-decreasing by Th1; then A10: ( Gseq is convergent & lim Gseq = sup Gseq ) by RINFSUP2:37; Partial_Sums seq2 is nonnegative by A2, MESFUNC9:16; then A11: Hseq is nonnegative by Th1; now__::_thesis:_for_n_being_set_st_n_in_dom_seq_holds_ seq_._n_>=_0 let n be set ; ::_thesis: ( n in dom seq implies seq . n >= 0 ) assume n in dom seq ; ::_thesis: seq . n >= 0 then reconsider n9 = n as Element of NAT ; A12: seq2 . n9 >= 0 by A2, SUPINF_2:51; ( seq . n = (seq1 . n9) + (seq2 . n9) & seq1 . n9 >= 0 ) by A1, A3, SUPINF_2:51; hence seq . n >= 0 by A12; ::_thesis: verum end; hence A13: seq is nonnegative by SUPINF_2:52; ::_thesis: ( SUM seq = (SUM seq1) + (SUM seq2) & Sum seq = (Sum seq1) + (Sum seq2) ) Partial_Sums seq2 is non-decreasing by A2, MESFUNC9:16; then Hseq is non-decreasing by Th1; then A14: ( Hseq is convergent & lim Hseq = sup Hseq ) by RINFSUP2:37; Partial_Sums seq1 is nonnegative by A1, MESFUNC9:16; then Gseq is nonnegative by Th1; hence SUM seq = (SUM seq1) + (SUM seq2) by A10, A11, A14, A5, A9, MESFUNC9:11; ::_thesis: Sum seq = (Sum seq1) + (Sum seq2) then Sum seq = (SUM seq1) + (SUM seq2) by A13, Th2; then Sum seq = (Sum seq1) + (SUM seq2) by A1, Th2; hence Sum seq = (Sum seq1) + (Sum seq2) by A2, Th2; ::_thesis: verum end; registration let X be set ; let F be Field_Subset of X; cluster non empty Relation-like NAT -defined F -valued Function-like V27( NAT ) quasi_total disjoint_valued for Element of bool [:NAT,F:]; existence ex b1 being Function of NAT,F st b1 is disjoint_valued proof consider f being Function of NAT,{{}} such that A1: for n being Element of NAT holds f . n = {} by MEASURE1:16; {} in F by PROB_1:4; then {{}} c= F by ZFMISC_1:31; then reconsider f = f as Function of NAT,F by FUNCT_2:7; take f ; ::_thesis: f is disjoint_valued A2: for x being set holds f . x = {} proof let x be set ; ::_thesis: f . x = {} ( x in dom f implies f . x = {} ) by A1; hence f . x = {} by FUNCT_1:def_2; ::_thesis: verum end; thus for x, y being set st x <> y holds f . x misses f . y :: according to PROB_2:def_2 ::_thesis: verum proof let x, y be set ; ::_thesis: ( x <> y implies f . x misses f . y ) f . x = {} by A2; hence ( x <> y implies f . x misses f . y ) by XBOOLE_1:65; ::_thesis: verum end; end; end; definition let X be set ; let F be Field_Subset of X; mode FinSequence of F -> FinSequence of bool X means :Def1: :: MEASURE8:def 1 for k being Nat st k in dom it holds it . k in F; existence ex b1 being FinSequence of bool X st for k being Nat st k in dom b1 holds b1 . k in F proof consider f being FinSequence of bool X such that A1: for k being Nat st k in dom f holds f . k = X by PROB_3:47; take f ; ::_thesis: for k being Nat st k in dom f holds f . k in F hereby ::_thesis: verum let k be Nat; ::_thesis: ( k in dom f implies f . k in F ) assume k in dom f ; ::_thesis: f . k in F then f . k = X by A1; hence f . k in F by PROB_1:5; ::_thesis: verum end; end; end; :: deftheorem Def1 defines FinSequence MEASURE8:def_1_:_ for X being set for F being Field_Subset of X for b3 being FinSequence of bool X holds ( b3 is FinSequence of F iff for k being Nat st k in dom b3 holds b3 . k in F ); registration let X be set ; let F be Field_Subset of X; cluster Relation-like NAT -defined bool X -valued Function-like FinSequence-like disjoint_valued for FinSequence of F; existence ex b1 being FinSequence of F st b1 is disjoint_valued proof {} c= X by XBOOLE_1:2; then reconsider f = <*{}*> as FinSequence of bool X by FINSEQ_1:74; for k being Nat st k in dom f holds f . k in F proof let k be Nat; ::_thesis: ( k in dom f implies f . k in F ) assume k in dom f ; ::_thesis: f . k in F then k in Seg 1 by FINSEQ_1:def_8; then k = 1 by FINSEQ_1:2, TARSKI:def_1; then f . k = {} by FINSEQ_1:def_8; hence f . k in F by PROB_1:4; ::_thesis: verum end; then reconsider f = <*{}*> as FinSequence of F by Def1; take f ; ::_thesis: f is disjoint_valued A1: for n being set holds f . n = {} proof let n be set ; ::_thesis: f . n = {} now__::_thesis:_(_n_in_dom_f_implies_f_._n_=_{}_) assume n in dom f ; ::_thesis: f . n = {} then n in Seg 1 by FINSEQ_1:def_8; then n = 1 by FINSEQ_1:2, TARSKI:def_1; hence f . n = {} by FINSEQ_1:def_8; ::_thesis: verum end; hence f . n = {} by FUNCT_1:def_2; ::_thesis: verum end; thus for x, y being set st x <> y holds f . x misses f . y :: according to PROB_2:def_2 ::_thesis: verum proof let x, y be set ; ::_thesis: ( x <> y implies f . x misses f . y ) f . x = {} by A1; hence ( x <> y implies f . x misses f . y ) by XBOOLE_1:65; ::_thesis: verum end; end; end; definition let X be set ; let F be Field_Subset of X; mode Sep_FinSequence of F is disjoint_valued FinSequence of F; end; definition let X be set ; let F be Field_Subset of X; mode Sep_Sequence of F is disjoint_valued Function of NAT,F; end; definition let X be set ; let F be Field_Subset of X; mode Set_Sequence of F -> SetSequence of X means :Def2: :: MEASURE8:def 2 for n being Nat holds it . n in F; existence ex b1 being SetSequence of X st for n being Nat holds b1 . n in F proof X in bool X by ZFMISC_1:def_1; then reconsider A = NAT --> X as SetSequence of X by FUNCOP_1:45; take A ; ::_thesis: for n being Nat holds A . n in F let n be Nat; ::_thesis: A . n in F n is Element of NAT by ORDINAL1:def_12; then A . n = X by FUNCOP_1:7; hence A . n in F by PROB_1:5; ::_thesis: verum end; end; :: deftheorem Def2 defines Set_Sequence MEASURE8:def_2_:_ for X being set for F being Field_Subset of X for b3 being SetSequence of X holds ( b3 is Set_Sequence of F iff for n being Nat holds b3 . n in F ); definition let X be set ; let A be Subset of X; let F be Field_Subset of X; mode Covering of A,F -> Set_Sequence of F means :Def3: :: MEASURE8:def 3 A c= union (rng it); existence ex b1 being Set_Sequence of F st A c= union (rng b1) proof X in bool X by ZFMISC_1:def_1; then reconsider IT = NAT --> X as SetSequence of X by FUNCOP_1:45; for n being Nat holds IT . n in F proof let n be Nat; ::_thesis: IT . n in F n in NAT by ORDINAL1:def_12; then IT . n = X by FUNCOP_1:7; hence IT . n in F by PROB_1:5; ::_thesis: verum end; then reconsider IT = IT as Set_Sequence of F by Def2; take IT ; ::_thesis: A c= union (rng IT) rng IT = {X} by FUNCOP_1:8; then X c= union (rng IT) by ZFMISC_1:25; hence A c= union (rng IT) by XBOOLE_1:1; ::_thesis: verum end; end; :: deftheorem Def3 defines Covering MEASURE8:def_3_:_ for X being set for A being Subset of X for F being Field_Subset of X for b4 being Set_Sequence of F holds ( b4 is Covering of A,F iff A c= union (rng b4) ); definition let X be set ; let F be Field_Subset of X; let FSets be Set_Sequence of F; let n be Nat; :: original: . redefine funcFSets . n -> Element of F; correctness coherence FSets . n is Element of F; by Def2; end; Lm1: for X being set for F being Field_Subset of X holds NAT --> X is Set_Sequence of F proof let X be set ; ::_thesis: for F being Field_Subset of X holds NAT --> X is Set_Sequence of F let F be Field_Subset of X; ::_thesis: NAT --> X is Set_Sequence of F X in bool X by ZFMISC_1:def_1; then reconsider G0 = NAT --> X as SetSequence of X by FUNCOP_1:45; A1: rng (NAT --> X) = {X} by FUNCOP_1:8; for n being Nat holds G0 . n in F proof let n be Nat; ::_thesis: G0 . n in F n in NAT by ORDINAL1:def_12; then G0 . n in {X} by A1, FUNCT_2:4; then G0 . n = X by TARSKI:def_1; hence G0 . n in F by PROB_1:5; ::_thesis: verum end; hence NAT --> X is Set_Sequence of F by Def2; ::_thesis: verum end; definition let X be set ; let F be Field_Subset of X; let Sets be SetSequence of X; mode Covering of Sets,F -> Function of NAT,(Funcs (NAT,(bool X))) means :Def4: :: MEASURE8:def 4 for n being Nat holds it . n is Covering of Sets . n,F; existence ex b1 being Function of NAT,(Funcs (NAT,(bool X))) st for n being Nat holds b1 . n is Covering of Sets . n,F proof reconsider G0 = NAT --> X as Set_Sequence of F by Lm1; reconsider G = G0 as Element of Funcs (NAT,(bool X)) by FUNCT_2:8; reconsider H = NAT --> G as Function of NAT,(Funcs (NAT,(bool X))) ; take H ; ::_thesis: for n being Nat holds H . n is Covering of Sets . n,F hereby ::_thesis: verum let n be Nat; ::_thesis: H . n is Covering of Sets . n,F rng (NAT --> X) = {X} by FUNCOP_1:8; then X c= union (rng (NAT --> X)) by ZFMISC_1:25; then A1: Sets . n c= union (rng (NAT --> X)) by XBOOLE_1:1; n in NAT by ORDINAL1:def_12; then H . n = NAT --> X by FUNCOP_1:7; hence H . n is Covering of Sets . n,F by A1, Def3; ::_thesis: verum end; end; end; :: deftheorem Def4 defines Covering MEASURE8:def_4_:_ for X being set for F being Field_Subset of X for Sets being SetSequence of X for b4 being Function of NAT,(Funcs (NAT,(bool X))) holds ( b4 is Covering of Sets,F iff for n being Nat holds b4 . n is Covering of Sets . n,F ); definition let X be set ; let F be Field_Subset of X; let M be Measure of F; let FSets be Set_Sequence of F; func vol (M,FSets) -> ExtREAL_sequence means :Def5: :: MEASURE8:def 5 for n being Nat holds it . n = M . (FSets . n); existence ex b1 being ExtREAL_sequence st for n being Nat holds b1 . n = M . (FSets . n) proof deffunc H1( Element of NAT ) -> Element of ExtREAL = M . (FSets . $1); consider IT being Function of NAT,ExtREAL such that A1: for n being Element of NAT holds IT . n = H1(n) from FUNCT_2:sch_4(); take IT ; ::_thesis: for n being Nat holds IT . n = M . (FSets . n) hereby ::_thesis: verum let n be Nat; ::_thesis: IT . n = M . (FSets . n) n in NAT by ORDINAL1:def_12; hence IT . n = M . (FSets . n) by A1; ::_thesis: verum end; end; uniqueness for b1, b2 being ExtREAL_sequence st ( for n being Nat holds b1 . n = M . (FSets . n) ) & ( for n being Nat holds b2 . n = M . (FSets . n) ) holds b1 = b2 proof let V1, V2 be Function of NAT,ExtREAL; ::_thesis: ( ( for n being Nat holds V1 . n = M . (FSets . n) ) & ( for n being Nat holds V2 . n = M . (FSets . n) ) implies V1 = V2 ) assume that A2: for n being Nat holds V1 . n = M . (FSets . n) and A3: for n being Nat holds V2 . n = M . (FSets . n) ; ::_thesis: V1 = V2 now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_ V1_._x_=_V2_._x let x be set ; ::_thesis: ( x in NAT implies V1 . x = V2 . x ) assume x in NAT ; ::_thesis: V1 . x = V2 . x then reconsider n = x as Nat ; thus V1 . x = M . (FSets . n) by A2 .= V2 . x by A3 ; ::_thesis: verum end; hence V1 = V2 by FUNCT_2:12; ::_thesis: verum end; end; :: deftheorem Def5 defines vol MEASURE8:def_5_:_ for X being set for F being Field_Subset of X for M being Measure of F for FSets being Set_Sequence of F for b5 being ExtREAL_sequence holds ( b5 = vol (M,FSets) iff for n being Nat holds b5 . n = M . (FSets . n) ); theorem Th4: :: MEASURE8:4 for X being set for F being Field_Subset of X for M being Measure of F for FSets being Set_Sequence of F holds vol (M,FSets) is nonnegative proof let X be set ; ::_thesis: for F being Field_Subset of X for M being Measure of F for FSets being Set_Sequence of F holds vol (M,FSets) is nonnegative let F be Field_Subset of X; ::_thesis: for M being Measure of F for FSets being Set_Sequence of F holds vol (M,FSets) is nonnegative let M be Measure of F; ::_thesis: for FSets being Set_Sequence of F holds vol (M,FSets) is nonnegative let FSets be Set_Sequence of F; ::_thesis: vol (M,FSets) is nonnegative for n being Element of NAT holds 0 <= (vol (M,FSets)) . n proof let n be Element of NAT ; ::_thesis: 0 <= (vol (M,FSets)) . n ( (vol (M,FSets)) . n = M . (FSets . n) & {} in F ) by Def5, PROB_1:4; then M . {} <= (vol (M,FSets)) . n by MEASURE1:8, XBOOLE_1:2; hence 0 <= (vol (M,FSets)) . n by VALUED_0:def_19; ::_thesis: verum end; hence vol (M,FSets) is nonnegative by SUPINF_2:39; ::_thesis: verum end; definition let X be set ; let F be Field_Subset of X; let Sets be SetSequence of X; let Cvr be Covering of Sets,F; let n be Nat; :: original: . redefine funcCvr . n -> Covering of Sets . n,F; correctness coherence Cvr . n is Covering of Sets . n,F; by Def4; end; definition let X be set ; let F be Field_Subset of X; let Sets be SetSequence of X; let M be Measure of F; let Cvr be Covering of Sets,F; func Volume (M,Cvr) -> ExtREAL_sequence means :Def6: :: MEASURE8:def 6 for n being Nat holds it . n = SUM (vol (M,(Cvr . n))); existence ex b1 being ExtREAL_sequence st for n being Nat holds b1 . n = SUM (vol (M,(Cvr . n))) proof defpred S1[ Element of NAT , Element of ExtREAL ] means $2 = SUM (vol (M,(Cvr . $1))); A1: for n being Element of NAT ex y being Element of ExtREAL st S1[n,y] ; consider G0 being Function of NAT,ExtREAL such that A2: for n being Element of NAT holds S1[n,G0 . n] from FUNCT_2:sch_3(A1); take G0 ; ::_thesis: for n being Nat holds G0 . n = SUM (vol (M,(Cvr . n))) hereby ::_thesis: verum let n be Nat; ::_thesis: G0 . n = SUM (vol (M,(Cvr . n))) n in NAT by ORDINAL1:def_12; hence G0 . n = SUM (vol (M,(Cvr . n))) by A2; ::_thesis: verum end; end; uniqueness for b1, b2 being ExtREAL_sequence st ( for n being Nat holds b1 . n = SUM (vol (M,(Cvr . n))) ) & ( for n being Nat holds b2 . n = SUM (vol (M,(Cvr . n))) ) holds b1 = b2 proof let G1, G2 be Function of NAT,ExtREAL; ::_thesis: ( ( for n being Nat holds G1 . n = SUM (vol (M,(Cvr . n))) ) & ( for n being Nat holds G2 . n = SUM (vol (M,(Cvr . n))) ) implies G1 = G2 ) assume that A3: for n being Nat holds G1 . n = SUM (vol (M,(Cvr . n))) and A4: for n being Nat holds G2 . n = SUM (vol (M,(Cvr . n))) ; ::_thesis: G1 = G2 now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_ G1_._x_=_G2_._x let x be set ; ::_thesis: ( x in NAT implies G1 . x = G2 . x ) assume x in NAT ; ::_thesis: G1 . x = G2 . x then reconsider n = x as Nat ; thus G1 . x = SUM (vol (M,(Cvr . n))) by A3 .= G2 . x by A4 ; ::_thesis: verum end; hence G1 = G2 by FUNCT_2:12; ::_thesis: verum end; end; :: deftheorem Def6 defines Volume MEASURE8:def_6_:_ for X being set for F being Field_Subset of X for Sets being SetSequence of X for M being Measure of F for Cvr being Covering of Sets,F for b6 being ExtREAL_sequence holds ( b6 = Volume (M,Cvr) iff for n being Nat holds b6 . n = SUM (vol (M,(Cvr . n))) ); theorem Th5: :: MEASURE8:5 for X being set for F being Field_Subset of X for M being Measure of F for Sets being SetSequence of X for n being Nat for Cvr being Covering of Sets,F holds 0 <= (Volume (M,Cvr)) . n proof let X be set ; ::_thesis: for F being Field_Subset of X for M being Measure of F for Sets being SetSequence of X for n being Nat for Cvr being Covering of Sets,F holds 0 <= (Volume (M,Cvr)) . n let F be Field_Subset of X; ::_thesis: for M being Measure of F for Sets being SetSequence of X for n being Nat for Cvr being Covering of Sets,F holds 0 <= (Volume (M,Cvr)) . n let M be Measure of F; ::_thesis: for Sets being SetSequence of X for n being Nat for Cvr being Covering of Sets,F holds 0 <= (Volume (M,Cvr)) . n let Sets be SetSequence of X; ::_thesis: for n being Nat for Cvr being Covering of Sets,F holds 0 <= (Volume (M,Cvr)) . n let n be Nat; ::_thesis: for Cvr being Covering of Sets,F holds 0 <= (Volume (M,Cvr)) . n let Cvr be Covering of Sets,F; ::_thesis: 0 <= (Volume (M,Cvr)) . n for k being Element of NAT holds 0 <= (vol (M,(Cvr . n))) . k proof let k be Element of NAT ; ::_thesis: 0 <= (vol (M,(Cvr . n))) . k 0 <= M . ((Cvr . n) . k) by SUPINF_2:51; hence 0 <= (vol (M,(Cvr . n))) . k by Def5; ::_thesis: verum end; then A1: vol (M,(Cvr . n)) is nonnegative by SUPINF_2:39; (Volume (M,Cvr)) . n = SUM (vol (M,(Cvr . n))) by Def6; hence 0 <= (Volume (M,Cvr)) . n by A1, MEASURE6:2; ::_thesis: verum end; definition let X be set ; let F be Field_Subset of X; let M be Measure of F; let A be Subset of X; func Svc (M,A) -> Subset of ExtREAL means :Def7: :: MEASURE8:def 7 for x being R_eal holds ( x in it iff ex CA being Covering of A,F st x = SUM (vol (M,CA)) ); existence ex b1 being Subset of ExtREAL st for x being R_eal holds ( x in b1 iff ex CA being Covering of A,F st x = SUM (vol (M,CA)) ) proof defpred S1[ set ] means ex CA being Covering of A,F st $1 = SUM (vol (M,CA)); consider D being set such that A1: for x being set holds ( x in D iff ( x in ExtREAL & S1[x] ) ) from XBOOLE_0:sch_1(); for z being set st z in D holds z in ExtREAL by A1; then reconsider D = D as Subset of ExtREAL by TARSKI:def_3; take D ; ::_thesis: for x being R_eal holds ( x in D iff ex CA being Covering of A,F st x = SUM (vol (M,CA)) ) thus for x being R_eal holds ( x in D iff ex CA being Covering of A,F st x = SUM (vol (M,CA)) ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Subset of ExtREAL st ( for x being R_eal holds ( x in b1 iff ex CA being Covering of A,F st x = SUM (vol (M,CA)) ) ) & ( for x being R_eal holds ( x in b2 iff ex CA being Covering of A,F st x = SUM (vol (M,CA)) ) ) holds b1 = b2 proof defpred S1[ set ] means ex CA being Covering of A,F st $1 = SUM (vol (M,CA)); let D1, D2 be Subset of ExtREAL; ::_thesis: ( ( for x being R_eal holds ( x in D1 iff ex CA being Covering of A,F st x = SUM (vol (M,CA)) ) ) & ( for x being R_eal holds ( x in D2 iff ex CA being Covering of A,F st x = SUM (vol (M,CA)) ) ) implies D1 = D2 ) assume that A2: for x being R_eal holds ( x in D1 iff S1[x] ) and A3: for x being R_eal holds ( x in D2 iff S1[x] ) ; ::_thesis: D1 = D2 thus D1 = D2 from SUBSET_1:sch_2(A2, A3); ::_thesis: verum end; end; :: deftheorem Def7 defines Svc MEASURE8:def_7_:_ for X being set for F being Field_Subset of X for M being Measure of F for A being Subset of X for b5 being Subset of ExtREAL holds ( b5 = Svc (M,A) iff for x being R_eal holds ( x in b5 iff ex CA being Covering of A,F st x = SUM (vol (M,CA)) ) ); registration let X be set ; let A be Subset of X; let F be Field_Subset of X; let M be Measure of F; cluster Svc (M,A) -> non empty ; coherence not Svc (M,A) is empty proof ( X c= X & {} c= X ) by XBOOLE_1:2; then consider CA being Function of NAT,(bool X) such that A1: rng CA = {X,{}} and CA . 0 = X and for n being Element of NAT st 0 < n holds CA . n = {} by MEASURE1:19; for n being Nat holds CA . n in F proof let n be Nat; ::_thesis: CA . n in F n in NAT by ORDINAL1:def_12; then A2: CA . n in rng CA by FUNCT_2:4; ( X in F & {} in F ) by PROB_1:4, PROB_1:5; then rng CA c= F by A1, ZFMISC_1:32; hence CA . n in F by A2; ::_thesis: verum end; then ( union {X,{}} = X \/ {} & CA is Set_Sequence of F ) by Def2, ZFMISC_1:75; then reconsider CA = CA as Covering of A,F by A1, Def3; defpred S1[ set ] means ex G being Covering of A,F st X = SUM (vol (M,G)); consider D being set such that A3: for x being set holds ( x in D iff ( x in ExtREAL & S1[x] ) ) from XBOOLE_0:sch_1(); SUM (vol (M,CA)) in D by A3; hence not Svc (M,A) is empty by Def7; ::_thesis: verum end; end; definition let X be set ; let F be Field_Subset of X; let M be Measure of F; func C_Meas M -> Function of (bool X),ExtREAL means :Def8: :: MEASURE8:def 8 for A being Subset of X holds it . A = inf (Svc (M,A)); existence ex b1 being Function of (bool X),ExtREAL st for A being Subset of X holds b1 . A = inf (Svc (M,A)) proof deffunc H1( Element of bool X) -> Element of ExtREAL = inf (Svc (M,$1)); thus ex G being Function of (bool X),ExtREAL st for A being Subset of X holds G . A = H1(A) from FUNCT_2:sch_4(); ::_thesis: verum end; uniqueness for b1, b2 being Function of (bool X),ExtREAL st ( for A being Subset of X holds b1 . A = inf (Svc (M,A)) ) & ( for A being Subset of X holds b2 . A = inf (Svc (M,A)) ) holds b1 = b2 proof deffunc H1( Subset of X) -> Element of ExtREAL = inf (Svc (M,$1)); thus for F1, F2 being Function of (bool X),ExtREAL st ( for A being Subset of X holds F1 . A = H1(A) ) & ( for A being Subset of X holds F2 . A = H1(A) ) holds F1 = F2 from BINOP_2:sch_1(); ::_thesis: verum end; end; :: deftheorem Def8 defines C_Meas MEASURE8:def_8_:_ for X being set for F being Field_Subset of X for M being Measure of F for b4 being Function of (bool X),ExtREAL holds ( b4 = C_Meas M iff for A being Subset of X holds b4 . A = inf (Svc (M,A)) ); definition func InvPairFunc -> Function of NAT,[:NAT,NAT:] equals :: MEASURE8:def 9 PairFunc " ; correctness coherence PairFunc " is Function of NAT,[:NAT,NAT:]; by FUNCTOR1:2, NAGATA_2:2; end; :: deftheorem defines InvPairFunc MEASURE8:def_9_:_ InvPairFunc = PairFunc " ; definition let X be set ; let F be Field_Subset of X; let Sets be SetSequence of X; let Cvr be Covering of Sets,F; func On Cvr -> Covering of union (rng Sets),F means :Def10: :: MEASURE8:def 10 for n being Nat holds it . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n); existence ex b1 being Covering of union (rng Sets),F st for n being Nat holds b1 . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) proof defpred S1[ Element of NAT , Subset of X] means $2 = (Cvr . ((pr1 InvPairFunc) . $1)) . ((pr2 InvPairFunc) . $1); A1: for n being Element of NAT ex y being Subset of X st S1[n,y] ; consider Seq0 being Function of NAT,(bool X) such that A2: for n being Element of NAT holds S1[n,Seq0 . n] from FUNCT_2:sch_3(A1); reconsider Seq0 = Seq0 as SetSequence of X ; for n being Nat holds Seq0 . n in F proof let n be Nat; ::_thesis: Seq0 . n in F n in NAT by ORDINAL1:def_12; then Seq0 . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) by A2; hence Seq0 . n in F ; ::_thesis: verum end; then reconsider Seq0 = Seq0 as Set_Sequence of F by Def2; union (rng Sets) c= union (rng Seq0) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (rng Sets) or x in union (rng Seq0) ) assume x in union (rng Sets) ; ::_thesis: x in union (rng Seq0) then consider A being set such that A3: x in A and A4: A in rng Sets by TARSKI:def_4; consider n1 being Element of NAT such that A5: A = Sets . n1 by A4, FUNCT_2:113; Sets . n1 c= union (rng (Cvr . n1)) by Def3; then consider AA being set such that A6: x in AA and A7: AA in rng (Cvr . n1) by A3, A5, TARSKI:def_4; consider n2 being Element of NAT such that A8: AA = (Cvr . n1) . n2 by A7, FUNCT_2:113; dom PairFunc = rng InvPairFunc by FUNCT_1:33, NAGATA_2:2; then rng InvPairFunc = [:NAT,NAT:] by FUNCT_2:def_1; then [n1,n2] in rng InvPairFunc by ZFMISC_1:def_2; then consider n being Element of NAT such that A9: [n1,n2] = InvPairFunc . n by FUNCT_2:113; [((pr1 InvPairFunc) . n),((pr2 InvPairFunc) . n)] = [n1,n2] by A9, FUNCT_2:119; then ( (pr1 InvPairFunc) . n = n1 & (pr2 InvPairFunc) . n = n2 ) by XTUPLE_0:1; then A10: x in Seq0 . n by A2, A6, A8; Seq0 . n in rng Seq0 by FUNCT_2:4; hence x in union (rng Seq0) by A10, TARSKI:def_4; ::_thesis: verum end; then reconsider Seq0 = Seq0 as Covering of union (rng Sets),F by Def3; take Seq0 ; ::_thesis: for n being Nat holds Seq0 . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) hereby ::_thesis: verum let n be Nat; ::_thesis: Seq0 . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) n in NAT by ORDINAL1:def_12; hence Seq0 . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) by A2; ::_thesis: verum end; end; uniqueness for b1, b2 being Covering of union (rng Sets),F st ( for n being Nat holds b1 . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) ) & ( for n being Nat holds b2 . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) ) holds b1 = b2 proof let Seq1, Seq2 be Covering of union (rng Sets),F; ::_thesis: ( ( for n being Nat holds Seq1 . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) ) & ( for n being Nat holds Seq2 . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) ) implies Seq1 = Seq2 ) assume that A11: for n being Nat holds Seq1 . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) and A12: for n being Nat holds Seq2 . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) ; ::_thesis: Seq1 = Seq2 for n being set st n in NAT holds Seq1 . n = Seq2 . n proof let n be set ; ::_thesis: ( n in NAT implies Seq1 . n = Seq2 . n ) assume n in NAT ; ::_thesis: Seq1 . n = Seq2 . n then reconsider n = n as Element of NAT ; Seq1 . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) by A11; hence Seq1 . n = Seq2 . n by A12; ::_thesis: verum end; hence Seq1 = Seq2 by FUNCT_2:12; ::_thesis: verum end; end; :: deftheorem Def10 defines On MEASURE8:def_10_:_ for X being set for F being Field_Subset of X for Sets being SetSequence of X for Cvr being Covering of Sets,F for b5 being Covering of union (rng Sets),F holds ( b5 = On Cvr iff for n being Nat holds b5 . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) ); theorem Th6: :: MEASURE8:6 for X being set for F being Field_Subset of X for M being Measure of F for k being Element of NAT ex m being Nat st for Sets being SetSequence of X for Cvr being Covering of Sets,F holds (Partial_Sums (vol (M,(On Cvr)))) . k <= (Partial_Sums (Volume (M,Cvr))) . m proof let X be set ; ::_thesis: for F being Field_Subset of X for M being Measure of F for k being Element of NAT ex m being Nat st for Sets being SetSequence of X for Cvr being Covering of Sets,F holds (Partial_Sums (vol (M,(On Cvr)))) . k <= (Partial_Sums (Volume (M,Cvr))) . m let F be Field_Subset of X; ::_thesis: for M being Measure of F for k being Element of NAT ex m being Nat st for Sets being SetSequence of X for Cvr being Covering of Sets,F holds (Partial_Sums (vol (M,(On Cvr)))) . k <= (Partial_Sums (Volume (M,Cvr))) . m let M be Measure of F; ::_thesis: for k being Element of NAT ex m being Nat st for Sets being SetSequence of X for Cvr being Covering of Sets,F holds (Partial_Sums (vol (M,(On Cvr)))) . k <= (Partial_Sums (Volume (M,Cvr))) . m defpred S1[ Element of NAT ] means ex m being Nat st for Sets being SetSequence of X for Cvr being Covering of Sets,F holds (Partial_Sums (vol (M,(On Cvr)))) . $1 <= (Partial_Sums (Volume (M,Cvr))) . m; {} c= X by XBOOLE_1:2; then reconsider D = NAT --> {} as Function of NAT,(bool X) by FUNCOP_1:45; reconsider y = D as Element of Funcs (NAT,(bool X)) by FUNCT_2:8; A1: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) set a = (pr1 InvPairFunc) . (k + 1); set b = (pr2 InvPairFunc) . (k + 1); set N0 = { s where s is Element of NAT : (pr1 InvPairFunc) . (k + 1) = (pr1 InvPairFunc) . s } ; A2: { s where s is Element of NAT : (pr1 InvPairFunc) . (k + 1) = (pr1 InvPairFunc) . s } c= NAT proof let s1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not s1 in { s where s is Element of NAT : (pr1 InvPairFunc) . (k + 1) = (pr1 InvPairFunc) . s } or s1 in NAT ) assume s1 in { s where s is Element of NAT : (pr1 InvPairFunc) . (k + 1) = (pr1 InvPairFunc) . s } ; ::_thesis: s1 in NAT then ex s being Element of NAT st ( s = s1 & (pr1 InvPairFunc) . (k + 1) = (pr1 InvPairFunc) . s ) ; hence s1 in NAT ; ::_thesis: verum end; k + 1 in { s where s is Element of NAT : (pr1 InvPairFunc) . (k + 1) = (pr1 InvPairFunc) . s } ; then reconsider N0 = { s where s is Element of NAT : (pr1 InvPairFunc) . (k + 1) = (pr1 InvPairFunc) . s } as non empty Subset of NAT by A2; given m0 being Nat such that A3: for Sets being SetSequence of X for Cvr being Covering of Sets,F holds (Partial_Sums (vol (M,(On Cvr)))) . k <= (Partial_Sums (Volume (M,Cvr))) . m0 ; ::_thesis: S1[k + 1] take m = m0 + ((pr1 InvPairFunc) . (k + 1)); ::_thesis: for Sets being SetSequence of X for Cvr being Covering of Sets,F holds (Partial_Sums (vol (M,(On Cvr)))) . (k + 1) <= (Partial_Sums (Volume (M,Cvr))) . m let Sets be SetSequence of X; ::_thesis: for Cvr being Covering of Sets,F holds (Partial_Sums (vol (M,(On Cvr)))) . (k + 1) <= (Partial_Sums (Volume (M,Cvr))) . m let Cvr be Covering of Sets,F; ::_thesis: (Partial_Sums (vol (M,(On Cvr)))) . (k + 1) <= (Partial_Sums (Volume (M,Cvr))) . m defpred S2[ Element of NAT , Function] means ( ( $1 = (pr1 InvPairFunc) . (k + 1) implies for m being Element of NAT holds $2 . m = (Cvr . $1) . m ) & ( $1 <> (pr1 InvPairFunc) . (k + 1) implies for m being Element of NAT holds $2 . m = {} ) ); defpred S3[ Element of NAT , Function] means ( ( $1 <> (pr1 InvPairFunc) . (k + 1) implies for m being Element of NAT holds $2 . m = (Cvr . $1) . m ) & ( $1 = (pr1 InvPairFunc) . (k + 1) implies for m being Element of NAT holds $2 . m = {} ) ); A4: for n being Element of NAT ex y being Element of Funcs (NAT,(bool X)) st S2[n,y] proof let n be Element of NAT ; ::_thesis: ex y being Element of Funcs (NAT,(bool X)) st S2[n,y] A5: now__::_thesis:_(_n_=_(pr1_InvPairFunc)_._(k_+_1)_implies_ex_y_being_Element_of_Funcs_(NAT,(bool_X))_st_S2[n,y]_) reconsider y = Cvr . n as Element of Funcs (NAT,(bool X)) by FUNCT_2:8; assume A6: n = (pr1 InvPairFunc) . (k + 1) ; ::_thesis: ex y being Element of Funcs (NAT,(bool X)) st S2[n,y] take y = y; ::_thesis: S2[n,y] thus S2[n,y] by A6; ::_thesis: verum end; ( n <> (pr1 InvPairFunc) . (k + 1) implies S2[n,y] ) by FUNCOP_1:7; hence ex y being Element of Funcs (NAT,(bool X)) st S2[n,y] by A5; ::_thesis: verum end; consider Cvr0 being Function of NAT,(Funcs (NAT,(bool X))) such that A7: for n being Element of NAT holds S2[n,Cvr0 . n] from FUNCT_2:sch_3(A4); A8: for n being Nat holds Cvr0 . n is Covering of D . n,F proof let n be Nat; ::_thesis: Cvr0 . n is Covering of D . n,F consider FSets0 being Function such that A9: Cvr0 . n = FSets0 and A10: ( dom FSets0 = NAT & rng FSets0 c= bool X ) by FUNCT_2:def_2; reconsider FSets0 = FSets0 as SetSequence of X by A10, FUNCT_2:2; for s being Nat holds FSets0 . s in F proof let s be Nat; ::_thesis: FSets0 . s in F A11: s in NAT by ORDINAL1:def_12; A12: now__::_thesis:_(_n_=_(pr1_InvPairFunc)_._(k_+_1)_implies_FSets0_._s_in_F_) assume n = (pr1 InvPairFunc) . (k + 1) ; ::_thesis: FSets0 . s in F then FSets0 . s = (Cvr . n) . s by A7, A9, A11; hence FSets0 . s in F ; ::_thesis: verum end; n in NAT by ORDINAL1:def_12; then ( n <> (pr1 InvPairFunc) . (k + 1) implies FSets0 . s = {} ) by A7, A9, A11; hence FSets0 . s in F by A12, PROB_1:4; ::_thesis: verum end; then A13: FSets0 is Set_Sequence of F by Def2; n in NAT by ORDINAL1:def_12; then D . n = {} by FUNCOP_1:7; then D . n c= union (rng FSets0) by XBOOLE_1:2; hence Cvr0 . n is Covering of D . n,F by A9, A13, Def3; ::_thesis: verum end; A14: for n being Element of NAT ex y being Element of Funcs (NAT,(bool X)) st S3[n,y] proof let n be Element of NAT ; ::_thesis: ex y being Element of Funcs (NAT,(bool X)) st S3[n,y] A15: now__::_thesis:_(_n_<>_(pr1_InvPairFunc)_._(k_+_1)_implies_ex_y_being_Element_of_Funcs_(NAT,(bool_X))_st_S3[n,y]_) reconsider y = Cvr . n as Element of Funcs (NAT,(bool X)) by FUNCT_2:8; assume A16: n <> (pr1 InvPairFunc) . (k + 1) ; ::_thesis: ex y being Element of Funcs (NAT,(bool X)) st S3[n,y] take y = y; ::_thesis: S3[n,y] thus S3[n,y] by A16; ::_thesis: verum end; ( n = (pr1 InvPairFunc) . (k + 1) implies S3[n,y] ) by FUNCOP_1:7; hence ex y being Element of Funcs (NAT,(bool X)) st S3[n,y] by A15; ::_thesis: verum end; consider Cvr1 being Function of NAT,(Funcs (NAT,(bool X))) such that A17: for n being Element of NAT holds S3[n,Cvr1 . n] from FUNCT_2:sch_3(A14); for n being Nat holds Cvr1 . n is Covering of D . n,F proof let n be Nat; ::_thesis: Cvr1 . n is Covering of D . n,F consider FSets1 being Function such that A18: Cvr1 . n = FSets1 and A19: ( dom FSets1 = NAT & rng FSets1 c= bool X ) by FUNCT_2:def_2; reconsider FSets1 = FSets1 as Function of NAT,(bool X) by A19, FUNCT_2:2; for s being Nat holds FSets1 . s in F proof let s be Nat; ::_thesis: FSets1 . s in F A20: s in NAT by ORDINAL1:def_12; A21: n in NAT by ORDINAL1:def_12; A22: now__::_thesis:_(_n_<>_(pr1_InvPairFunc)_._(k_+_1)_implies_FSets1_._s_in_F_) assume n <> (pr1 InvPairFunc) . (k + 1) ; ::_thesis: FSets1 . s in F then FSets1 . s = (Cvr . n) . s by A17, A18, A21, A20; hence FSets1 . s in F ; ::_thesis: verum end; ( n = (pr1 InvPairFunc) . (k + 1) implies FSets1 . s = {} ) by A17, A18, A20; hence FSets1 . s in F by A22, PROB_1:4; ::_thesis: verum end; then A23: FSets1 is Set_Sequence of F by Def2; n in NAT by ORDINAL1:def_12; then D . n = {} by FUNCOP_1:7; then D . n c= union (rng FSets1) by XBOOLE_1:2; hence Cvr1 . n is Covering of D . n,F by A18, A23, Def3; ::_thesis: verum end; then reconsider Cvr1 = Cvr1 as Covering of D,F by Def4; reconsider Cvr0 = Cvr0 as Covering of D,F by A8, Def4; set PSv1 = Partial_Sums (vol (M,(On Cvr1))); (On Cvr1) . (k + 1) = (Cvr1 . ((pr1 InvPairFunc) . (k + 1))) . ((pr2 InvPairFunc) . (k + 1)) by Def10 .= {} by A17 ; then A24: (vol (M,(On Cvr1))) . (k + 1) = M . {} by Def5 .= 0 by VALUED_0:def_19 ; set PSv0 = Partial_Sums (vol (M,(On Cvr0))); set PSv = Partial_Sums (vol (M,(On Cvr))); defpred S4[ Element of N0, Element of NAT ] means $2 = (pr2 InvPairFunc) . $1; A25: for s being Element of N0 ex y being Element of NAT st S4[s,y] ; consider SOS being Function of N0,NAT such that A26: for s being Element of N0 holds S4[s,SOS . s] from FUNCT_2:sch_3(A25); A27: for s being Element of NAT holds ( ( s in N0 implies (vol (M,(On Cvr0))) . s = ((vol (M,(Cvr0 . ((pr1 InvPairFunc) . (k + 1))))) * SOS) . s ) & ( not s in N0 implies (vol (M,(On Cvr0))) . s = 0 ) ) proof let s be Element of NAT ; ::_thesis: ( ( s in N0 implies (vol (M,(On Cvr0))) . s = ((vol (M,(Cvr0 . ((pr1 InvPairFunc) . (k + 1))))) * SOS) . s ) & ( not s in N0 implies (vol (M,(On Cvr0))) . s = 0 ) ) thus ( s in N0 implies (vol (M,(On Cvr0))) . s = ((vol (M,(Cvr0 . ((pr1 InvPairFunc) . (k + 1))))) * SOS) . s ) ::_thesis: ( not s in N0 implies (vol (M,(On Cvr0))) . s = 0 ) proof A28: (vol (M,(On Cvr0))) . s = M . ((On Cvr0) . s) by Def5; assume A29: s in N0 ; ::_thesis: (vol (M,(On Cvr0))) . s = ((vol (M,(Cvr0 . ((pr1 InvPairFunc) . (k + 1))))) * SOS) . s then ( ex s1 being Element of NAT st ( s1 = s & (pr1 InvPairFunc) . (k + 1) = (pr1 InvPairFunc) . s1 ) & (pr2 InvPairFunc) . s = SOS . s ) by A26; then (vol (M,(On Cvr0))) . s = M . ((Cvr0 . ((pr1 InvPairFunc) . (k + 1))) . (SOS . s)) by A28, Def10; then (vol (M,(On Cvr0))) . s = (vol (M,(Cvr0 . ((pr1 InvPairFunc) . (k + 1))))) . (SOS . s) by Def5; hence (vol (M,(On Cvr0))) . s = ((vol (M,(Cvr0 . ((pr1 InvPairFunc) . (k + 1))))) * SOS) . s by A29, FUNCT_2:15; ::_thesis: verum end; assume not s in N0 ; ::_thesis: (vol (M,(On Cvr0))) . s = 0 then A30: not (pr1 InvPairFunc) . (k + 1) = (pr1 InvPairFunc) . s ; (vol (M,(On Cvr0))) . s = M . ((On Cvr0) . s) by Def5 .= M . ((Cvr0 . ((pr1 InvPairFunc) . s)) . ((pr2 InvPairFunc) . s)) by Def10 .= M . {} by A7, A30 ; hence (vol (M,(On Cvr0))) . s = 0 by VALUED_0:def_19; ::_thesis: verum end; now__::_thesis:_for_s1,_s2_being_set_st_s1_in_N0_&_s2_in_N0_&_SOS_._s1_=_SOS_._s2_holds_ s1_=_s2 let s1, s2 be set ; ::_thesis: ( s1 in N0 & s2 in N0 & SOS . s1 = SOS . s2 implies s1 = s2 ) assume that A31: ( s1 in N0 & s2 in N0 ) and A32: SOS . s1 = SOS . s2 ; ::_thesis: s1 = s2 A33: ( ex s11 being Element of NAT st ( s11 = s1 & (pr1 InvPairFunc) . (k + 1) = (pr1 InvPairFunc) . s11 ) & ex s22 being Element of NAT st ( s22 = s2 & (pr1 InvPairFunc) . (k + 1) = (pr1 InvPairFunc) . s22 ) ) by A31; A34: ( InvPairFunc . s1 = [((pr1 InvPairFunc) . s1),((pr2 InvPairFunc) . s1)] & InvPairFunc . s2 = [((pr1 InvPairFunc) . s2),((pr2 InvPairFunc) . s2)] ) by A31, FUNCT_2:119; ( SOS . s1 = (pr2 InvPairFunc) . s1 & SOS . s2 = (pr2 InvPairFunc) . s2 ) by A26, A31; hence s1 = s2 by A32, A33, A34, FUNCT_2:19, NAGATA_2:2; ::_thesis: verum end; then A35: SOS is one-to-one by FUNCT_2:19; (Ser (vol (M,(On Cvr1)))) . (k + 1) = ((Ser (vol (M,(On Cvr1)))) . k) + ((vol (M,(On Cvr1))) . (k + 1)) by SUPINF_2:44 .= (Ser (vol (M,(On Cvr1)))) . k by A24, XXREAL_3:4 ; then (Partial_Sums (vol (M,(On Cvr1)))) . (k + 1) = (Ser (vol (M,(On Cvr1)))) . k by Th1; then A36: (Partial_Sums (vol (M,(On Cvr1)))) . (k + 1) = (Partial_Sums (vol (M,(On Cvr1)))) . k by Th1; for s being Element of NAT holds 0. <= (Volume (M,Cvr0)) . s by Th5; then A37: Volume (M,Cvr0) is nonnegative by SUPINF_2:39; then (Volume (M,Cvr0)) . ((pr1 InvPairFunc) . (k + 1)) <= (Ser (Volume (M,Cvr0))) . ((pr1 InvPairFunc) . (k + 1)) by MEASURE7:2; then A38: SUM (vol (M,(Cvr0 . ((pr1 InvPairFunc) . (k + 1))))) <= (Ser (Volume (M,Cvr0))) . ((pr1 InvPairFunc) . (k + 1)) by Def6; A39: m0 is Element of NAT by ORDINAL1:def_12; then (Ser (Volume (M,Cvr0))) . ((pr1 InvPairFunc) . (k + 1)) <= (Ser (Volume (M,Cvr0))) . m by A37, SUPINF_2:41; then A40: SUM (vol (M,(Cvr0 . ((pr1 InvPairFunc) . (k + 1))))) <= (Ser (Volume (M,Cvr0))) . m by A38, XXREAL_0:2; vol (M,(Cvr0 . ((pr1 InvPairFunc) . (k + 1)))) is nonnegative by Th4; then SUM (vol (M,(On Cvr0))) <= SUM (vol (M,(Cvr0 . ((pr1 InvPairFunc) . (k + 1))))) by A35, A27, MEASURE7:11; then A41: SUM (vol (M,(On Cvr0))) <= (Ser (Volume (M,Cvr0))) . m by A40, XXREAL_0:2; (Ser (vol (M,(On Cvr0)))) . (k + 1) <= SUM (vol (M,(On Cvr0))) by Th4, MEASURE7:6; then (Ser (vol (M,(On Cvr0)))) . (k + 1) <= (Ser (Volume (M,Cvr0))) . m by A41, XXREAL_0:2; then (Partial_Sums (vol (M,(On Cvr0)))) . (k + 1) <= (Ser (Volume (M,Cvr0))) . m by Th1; then A42: (Partial_Sums (vol (M,(On Cvr0)))) . (k + 1) <= (Partial_Sums (Volume (M,Cvr0))) . m by Th1; for s being Element of NAT holds 0. <= (Volume (M,Cvr1)) . s by Th5; then A43: Volume (M,Cvr1) is nonnegative by SUPINF_2:39; then ( m0 <= m & Partial_Sums (Volume (M,Cvr1)) is non-decreasing ) by MESFUNC9:16, NAT_1:11; then A44: (Partial_Sums (Volume (M,Cvr1))) . m0 <= (Partial_Sums (Volume (M,Cvr1))) . m by A39, RINFSUP2:7; A45: for n being Element of NAT holds (vol (M,(On Cvr))) . n = ((vol (M,(On Cvr0))) . n) + ((vol (M,(On Cvr1))) . n) proof let n be Element of NAT ; ::_thesis: (vol (M,(On Cvr))) . n = ((vol (M,(On Cvr0))) . n) + ((vol (M,(On Cvr1))) . n) set n1 = (pr1 InvPairFunc) . n; set n2 = (pr2 InvPairFunc) . n; A46: ( (vol (M,(On Cvr0))) . n = M . ((On Cvr0) . n) & (vol (M,(On Cvr1))) . n = M . ((On Cvr1) . n) ) by Def5; (vol (M,(On Cvr))) . n = M . ((On Cvr) . n) by Def5; then A47: (vol (M,(On Cvr))) . n = M . ((Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n)) by Def10; percases ( (pr1 InvPairFunc) . n = (pr1 InvPairFunc) . (k + 1) or (pr1 InvPairFunc) . n <> (pr1 InvPairFunc) . (k + 1) ) ; supposeA48: (pr1 InvPairFunc) . n = (pr1 InvPairFunc) . (k + 1) ; ::_thesis: (vol (M,(On Cvr))) . n = ((vol (M,(On Cvr0))) . n) + ((vol (M,(On Cvr1))) . n) (On Cvr1) . n = (Cvr1 . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) by Def10 .= {} by A17, A48 ; then A49: M . ((On Cvr1) . n) = 0 by VALUED_0:def_19; (On Cvr0) . n = (Cvr0 . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) by Def10 .= (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) by A7, A48 ; hence (vol (M,(On Cvr))) . n = ((vol (M,(On Cvr0))) . n) + ((vol (M,(On Cvr1))) . n) by A46, A47, A49, XXREAL_3:4; ::_thesis: verum end; supposeA50: (pr1 InvPairFunc) . n <> (pr1 InvPairFunc) . (k + 1) ; ::_thesis: (vol (M,(On Cvr))) . n = ((vol (M,(On Cvr0))) . n) + ((vol (M,(On Cvr1))) . n) (On Cvr0) . n = (Cvr0 . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) by Def10 .= {} by A7, A50 ; then A51: M . ((On Cvr0) . n) = 0 by VALUED_0:def_19; (On Cvr1) . n = (Cvr1 . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) by Def10 .= (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) by A17, A50 ; hence (vol (M,(On Cvr))) . n = ((vol (M,(On Cvr0))) . n) + ((vol (M,(On Cvr1))) . n) by A46, A47, A51, XXREAL_3:4; ::_thesis: verum end; end; end; ( vol (M,(On Cvr0)) is nonnegative & vol (M,(On Cvr1)) is nonnegative ) by Th4; then (Ser (vol (M,(On Cvr)))) . (k + 1) = ((Ser (vol (M,(On Cvr0)))) . (k + 1)) + ((Ser (vol (M,(On Cvr1)))) . (k + 1)) by A45, MEASURE7:3; then (Partial_Sums (vol (M,(On Cvr)))) . (k + 1) = ((Ser (vol (M,(On Cvr0)))) . (k + 1)) + ((Ser (vol (M,(On Cvr1)))) . (k + 1)) by Th1; then (Partial_Sums (vol (M,(On Cvr)))) . (k + 1) = ((Partial_Sums (vol (M,(On Cvr0)))) . (k + 1)) + ((Ser (vol (M,(On Cvr1)))) . (k + 1)) by Th1; then A52: (Partial_Sums (vol (M,(On Cvr)))) . (k + 1) = ((Partial_Sums (vol (M,(On Cvr0)))) . (k + 1)) + ((Partial_Sums (vol (M,(On Cvr1)))) . (k + 1)) by Th1; (Partial_Sums (vol (M,(On Cvr1)))) . k <= (Partial_Sums (Volume (M,Cvr1))) . m0 by A3; then A53: (Partial_Sums (vol (M,(On Cvr1)))) . (k + 1) <= (Partial_Sums (Volume (M,Cvr1))) . m by A36, A44, XXREAL_0:2; for n being Element of NAT holds (Volume (M,Cvr)) . n = ((Volume (M,Cvr0)) . n) + ((Volume (M,Cvr1)) . n) proof let n be Element of NAT ; ::_thesis: (Volume (M,Cvr)) . n = ((Volume (M,Cvr0)) . n) + ((Volume (M,Cvr1)) . n) A54: now__::_thesis:_(_n_<>_(pr1_InvPairFunc)_._(k_+_1)_implies_SUM_(vol_(M,(Cvr_._n)))_=_(SUM_(vol_(M,(Cvr0_._n))))_+_(SUM_(vol_(M,(Cvr1_._n))))_) assume A55: n <> (pr1 InvPairFunc) . (k + 1) ; ::_thesis: SUM (vol (M,(Cvr . n))) = (SUM (vol (M,(Cvr0 . n)))) + (SUM (vol (M,(Cvr1 . n)))) for s being Element of NAT holds (vol (M,(Cvr0 . n))) . s = 0. proof let s be Element of NAT ; ::_thesis: (vol (M,(Cvr0 . n))) . s = 0. (Cvr0 . n) . s = {} by A7, A55; then M . ((Cvr0 . n) . s) = 0 by VALUED_0:def_19; hence (vol (M,(Cvr0 . n))) . s = 0. by Def5; ::_thesis: verum end; then A56: SUM (vol (M,(Cvr0 . n))) = 0. by MEASURE7:1; for s being Element of NAT holds ( (vol (M,(Cvr1 . n))) . s <= (vol (M,(Cvr . n))) . s & (vol (M,(Cvr . n))) . s <= (vol (M,(Cvr1 . n))) . s ) proof let s be Element of NAT ; ::_thesis: ( (vol (M,(Cvr1 . n))) . s <= (vol (M,(Cvr . n))) . s & (vol (M,(Cvr . n))) . s <= (vol (M,(Cvr1 . n))) . s ) ( (vol (M,(Cvr1 . n))) . s = M . ((Cvr1 . n) . s) & (vol (M,(Cvr . n))) . s = M . ((Cvr . n) . s) ) by Def5; hence ( (vol (M,(Cvr1 . n))) . s <= (vol (M,(Cvr . n))) . s & (vol (M,(Cvr . n))) . s <= (vol (M,(Cvr1 . n))) . s ) by A17, A55; ::_thesis: verum end; then ( SUM (vol (M,(Cvr1 . n))) <= SUM (vol (M,(Cvr . n))) & SUM (vol (M,(Cvr . n))) <= SUM (vol (M,(Cvr1 . n))) ) by SUPINF_2:43; then SUM (vol (M,(Cvr . n))) = SUM (vol (M,(Cvr1 . n))) by XXREAL_0:1; hence SUM (vol (M,(Cvr . n))) = (SUM (vol (M,(Cvr0 . n)))) + (SUM (vol (M,(Cvr1 . n)))) by A56, XXREAL_3:4; ::_thesis: verum end; A57: now__::_thesis:_(_n_=_(pr1_InvPairFunc)_._(k_+_1)_implies_SUM_(vol_(M,(Cvr_._n)))_=_(SUM_(vol_(M,(Cvr0_._n))))_+_(SUM_(vol_(M,(Cvr1_._n))))_) assume A58: n = (pr1 InvPairFunc) . (k + 1) ; ::_thesis: SUM (vol (M,(Cvr . n))) = (SUM (vol (M,(Cvr0 . n)))) + (SUM (vol (M,(Cvr1 . n)))) for s being Element of NAT holds (vol (M,(Cvr1 . n))) . s = 0 proof let s be Element of NAT ; ::_thesis: (vol (M,(Cvr1 . n))) . s = 0 (Cvr1 . n) . s = {} by A17, A58; then M . ((Cvr1 . n) . s) = 0 by VALUED_0:def_19; hence (vol (M,(Cvr1 . n))) . s = 0 by Def5; ::_thesis: verum end; then A59: SUM (vol (M,(Cvr1 . n))) = 0 by MEASURE7:1; for s being Element of NAT holds ( (vol (M,(Cvr . n))) . s <= (vol (M,(Cvr0 . n))) . s & (vol (M,(Cvr0 . n))) . s <= (vol (M,(Cvr . n))) . s ) proof let s be Element of NAT ; ::_thesis: ( (vol (M,(Cvr . n))) . s <= (vol (M,(Cvr0 . n))) . s & (vol (M,(Cvr0 . n))) . s <= (vol (M,(Cvr . n))) . s ) (vol (M,(Cvr0 . n))) . s = M . ((Cvr0 . n) . s) by Def5 .= M . ((Cvr . n) . s) by A7, A58 ; hence ( (vol (M,(Cvr . n))) . s <= (vol (M,(Cvr0 . n))) . s & (vol (M,(Cvr0 . n))) . s <= (vol (M,(Cvr . n))) . s ) by Def5; ::_thesis: verum end; then ( SUM (vol (M,(Cvr . n))) <= SUM (vol (M,(Cvr0 . n))) & SUM (vol (M,(Cvr0 . n))) <= SUM (vol (M,(Cvr . n))) ) by SUPINF_2:43; then SUM (vol (M,(Cvr . n))) = SUM (vol (M,(Cvr0 . n))) by XXREAL_0:1; hence SUM (vol (M,(Cvr . n))) = (SUM (vol (M,(Cvr0 . n)))) + (SUM (vol (M,(Cvr1 . n)))) by A59, XXREAL_3:4; ::_thesis: verum end; ( (Volume (M,Cvr)) . n = SUM (vol (M,(Cvr . n))) & (Volume (M,Cvr0)) . n = SUM (vol (M,(Cvr0 . n))) ) by Def6; hence (Volume (M,Cvr)) . n = ((Volume (M,Cvr0)) . n) + ((Volume (M,Cvr1)) . n) by A57, A54, Def6; ::_thesis: verum end; then (Ser (Volume (M,Cvr))) . m = ((Ser (Volume (M,Cvr0))) . m) + ((Ser (Volume (M,Cvr1))) . m) by A37, A43, MEASURE7:3; then (Partial_Sums (Volume (M,Cvr))) . m = ((Ser (Volume (M,Cvr0))) . m) + ((Ser (Volume (M,Cvr1))) . m) by Th1 .= ((Partial_Sums (Volume (M,Cvr0))) . m) + ((Ser (Volume (M,Cvr1))) . m) by Th1 .= ((Partial_Sums (Volume (M,Cvr0))) . m) + ((Partial_Sums (Volume (M,Cvr1))) . m) by Th1 ; hence (Partial_Sums (vol (M,(On Cvr)))) . (k + 1) <= (Partial_Sums (Volume (M,Cvr))) . m by A42, A53, A52, XXREAL_3:36; ::_thesis: verum end; A60: S1[ 0 ] proof take m = (pr1 InvPairFunc) . 0; ::_thesis: for Sets being SetSequence of X for Cvr being Covering of Sets,F holds (Partial_Sums (vol (M,(On Cvr)))) . 0 <= (Partial_Sums (Volume (M,Cvr))) . m let Sets be SetSequence of X; ::_thesis: for Cvr being Covering of Sets,F holds (Partial_Sums (vol (M,(On Cvr)))) . 0 <= (Partial_Sums (Volume (M,Cvr))) . m let Cvr be Covering of Sets,F; ::_thesis: (Partial_Sums (vol (M,(On Cvr)))) . 0 <= (Partial_Sums (Volume (M,Cvr))) . m for n being Element of NAT holds 0 <= (Volume (M,Cvr)) . n by Th5; then Volume (M,Cvr) is nonnegative by SUPINF_2:39; then (Volume (M,Cvr)) . m <= (Ser (Volume (M,Cvr))) . m by MEASURE7:2; then A61: (Volume (M,Cvr)) . m <= (Partial_Sums (Volume (M,Cvr))) . m by Th1; ( (vol (M,(On Cvr))) . 0 = M . ((On Cvr) . 0) & (vol (M,(Cvr . ((pr1 InvPairFunc) . 0)))) . ((pr2 InvPairFunc) . 0) = M . ((Cvr . ((pr1 InvPairFunc) . 0)) . ((pr2 InvPairFunc) . 0)) ) by Def5; then (vol (M,(On Cvr))) . 0 <= (vol (M,(Cvr . ((pr1 InvPairFunc) . 0)))) . ((pr2 InvPairFunc) . 0) by Def10; then (vol (M,(On Cvr))) . 0 <= SUM (vol (M,(Cvr . ((pr1 InvPairFunc) . 0)))) by Th4, MEASURE6:3; then ( (Partial_Sums (vol (M,(On Cvr)))) . 0 = (vol (M,(On Cvr))) . 0 & (vol (M,(On Cvr))) . 0 <= (Volume (M,Cvr)) . ((pr1 InvPairFunc) . 0) ) by Def6, MESFUNC9:def_1; hence (Partial_Sums (vol (M,(On Cvr)))) . 0 <= (Partial_Sums (Volume (M,Cvr))) . m by A61, XXREAL_0:2; ::_thesis: verum end; thus for k being Element of NAT holds S1[k] from NAT_1:sch_1(A60, A1); ::_thesis: verum end; theorem Th7: :: MEASURE8:7 for X being set for F being Field_Subset of X for M being Measure of F for Sets being SetSequence of X for Cvr being Covering of Sets,F holds inf (Svc (M,(union (rng Sets)))) <= SUM (Volume (M,Cvr)) proof let X be set ; ::_thesis: for F being Field_Subset of X for M being Measure of F for Sets being SetSequence of X for Cvr being Covering of Sets,F holds inf (Svc (M,(union (rng Sets)))) <= SUM (Volume (M,Cvr)) let F be Field_Subset of X; ::_thesis: for M being Measure of F for Sets being SetSequence of X for Cvr being Covering of Sets,F holds inf (Svc (M,(union (rng Sets)))) <= SUM (Volume (M,Cvr)) let M be Measure of F; ::_thesis: for Sets being SetSequence of X for Cvr being Covering of Sets,F holds inf (Svc (M,(union (rng Sets)))) <= SUM (Volume (M,Cvr)) let Sets be SetSequence of X; ::_thesis: for Cvr being Covering of Sets,F holds inf (Svc (M,(union (rng Sets)))) <= SUM (Volume (M,Cvr)) let Cvr be Covering of Sets,F; ::_thesis: inf (Svc (M,(union (rng Sets)))) <= SUM (Volume (M,Cvr)) set Q = SUM (vol (M,(On Cvr))); for x being ext-real number st x in rng (Ser (vol (M,(On Cvr)))) holds ex y being ext-real number st ( y in rng (Ser (Volume (M,Cvr))) & x <= y ) proof let x be ext-real number ; ::_thesis: ( x in rng (Ser (vol (M,(On Cvr)))) implies ex y being ext-real number st ( y in rng (Ser (Volume (M,Cvr))) & x <= y ) ) assume x in rng (Ser (vol (M,(On Cvr)))) ; ::_thesis: ex y being ext-real number st ( y in rng (Ser (Volume (M,Cvr))) & x <= y ) then consider n being Element of NAT such that A1: x = (Ser (vol (M,(On Cvr)))) . n by FUNCT_2:113; consider m being Nat such that A2: for Sets being SetSequence of X for G being Covering of Sets,F holds (Partial_Sums (vol (M,(On G)))) . n <= (Partial_Sums (Volume (M,G))) . m by Th6; take (Ser (Volume (M,Cvr))) . m ; ::_thesis: ( (Ser (Volume (M,Cvr))) . m in rng (Ser (Volume (M,Cvr))) & x <= (Ser (Volume (M,Cvr))) . m ) A3: for Sets being SetSequence of X for G being Covering of Sets,F holds (Ser (vol (M,(On G)))) . n <= (Ser (Volume (M,G))) . m proof let Sets be SetSequence of X; ::_thesis: for G being Covering of Sets,F holds (Ser (vol (M,(On G)))) . n <= (Ser (Volume (M,G))) . m let G be Covering of Sets,F; ::_thesis: (Ser (vol (M,(On G)))) . n <= (Ser (Volume (M,G))) . m (Partial_Sums (vol (M,(On G)))) . n <= (Partial_Sums (Volume (M,G))) . m by A2; then (Ser (vol (M,(On G)))) . n <= (Partial_Sums (Volume (M,G))) . m by Th1; hence (Ser (vol (M,(On G)))) . n <= (Ser (Volume (M,G))) . m by Th1; ::_thesis: verum end; m in NAT by ORDINAL1:def_12; hence ( (Ser (Volume (M,Cvr))) . m in rng (Ser (Volume (M,Cvr))) & x <= (Ser (Volume (M,Cvr))) . m ) by A1, A3, FUNCT_2:4; ::_thesis: verum end; then A4: SUM (vol (M,(On Cvr))) <= SUM (Volume (M,Cvr)) by XXREAL_2:63; SUM (vol (M,(On Cvr))) in Svc (M,(union (rng Sets))) by Def7; then inf (Svc (M,(union (rng Sets)))) <= SUM (vol (M,(On Cvr))) by XXREAL_2:3; hence inf (Svc (M,(union (rng Sets)))) <= SUM (Volume (M,Cvr)) by A4, XXREAL_0:2; ::_thesis: verum end; theorem Th8: :: MEASURE8:8 for X being set for F being Field_Subset of X for A being Subset of X st A in F holds (A,({} X)) followed_by ({} X) is Covering of A,F proof let X be set ; ::_thesis: for F being Field_Subset of X for A being Subset of X st A in F holds (A,({} X)) followed_by ({} X) is Covering of A,F let F be Field_Subset of X; ::_thesis: for A being Subset of X st A in F holds (A,({} X)) followed_by ({} X) is Covering of A,F let A be Subset of X; ::_thesis: ( A in F implies (A,({} X)) followed_by ({} X) is Covering of A,F ) reconsider Sets = (A,({} X)) followed_by ({} X) as SetSequence of X ; A1: Sets . 0 = A by FUNCT_7:122; A2: Sets . 1 = {} X by FUNCT_7:123; assume A3: A in F ; ::_thesis: (A,({} X)) followed_by ({} X) is Covering of A,F for n being Nat holds Sets . n in F proof let n be Nat; ::_thesis: Sets . n in F percases ( n = 0 or n = 1 or n > 1 ) by NAT_1:25; suppose n = 0 ; ::_thesis: Sets . n in F hence Sets . n in F by A3, FUNCT_7:122; ::_thesis: verum end; suppose n = 1 ; ::_thesis: Sets . n in F hence Sets . n in F by A2, PROB_1:4; ::_thesis: verum end; suppose n > 1 ; ::_thesis: Sets . n in F then Sets . n = {} by FUNCT_7:124; hence Sets . n in F by PROB_1:4; ::_thesis: verum end; end; end; then reconsider Sets = Sets as Set_Sequence of F by Def2; A c= union (rng Sets) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in union (rng Sets) ) dom Sets = NAT by FUNCT_2:def_1; then A4: Sets . 0 in rng Sets by FUNCT_1:3; assume x in A ; ::_thesis: x in union (rng Sets) hence x in union (rng Sets) by A1, A4, TARSKI:def_4; ::_thesis: verum end; hence (A,({} X)) followed_by ({} X) is Covering of A,F by Def3; ::_thesis: verum end; theorem Th9: :: MEASURE8:9 for X being set for F being Field_Subset of X for M being Measure of F for A being set st A in F holds (C_Meas M) . A <= M . A proof let X be set ; ::_thesis: for F being Field_Subset of X for M being Measure of F for A being set st A in F holds (C_Meas M) . A <= M . A let F be Field_Subset of X; ::_thesis: for M being Measure of F for A being set st A in F holds (C_Meas M) . A <= M . A let M be Measure of F; ::_thesis: for A being set st A in F holds (C_Meas M) . A <= M . A let A9 be set ; ::_thesis: ( A9 in F implies (C_Meas M) . A9 <= M . A9 ) assume A1: A9 in F ; ::_thesis: (C_Meas M) . A9 <= M . A9 then reconsider A = A9 as Subset of X ; reconsider Aseq = (A,({} X)) followed_by ({} X) as Set_Sequence of F by A1, Th8; A2: Aseq . 1 = {} X by FUNCT_7:123; A3: Aseq . 0 = A by FUNCT_7:122; A c= union (rng Aseq) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in union (rng Aseq) ) dom Aseq = NAT by FUNCT_2:def_1; then A4: Aseq . 0 in rng Aseq by FUNCT_1:3; assume x in A ; ::_thesis: x in union (rng Aseq) hence x in union (rng Aseq) by A3, A4, TARSKI:def_4; ::_thesis: verum end; then reconsider Aseq = Aseq as Covering of A,F by Def3; A5: for n being Element of NAT st n <> 0 holds (vol (M,Aseq)) . n = 0 proof let n be Element of NAT ; ::_thesis: ( n <> 0 implies (vol (M,Aseq)) . n = 0 ) assume n <> 0 ; ::_thesis: (vol (M,Aseq)) . n = 0 then Aseq . n = {} by A2, FUNCT_7:124, NAT_1:25; then (vol (M,Aseq)) . n = M . {} by Def5; hence (vol (M,Aseq)) . n = 0 by VALUED_0:def_19; ::_thesis: verum end; then for n being Element of NAT st 1 <= n holds (vol (M,Aseq)) . n = 0 ; then SUM (vol (M,Aseq)) = (Ser (vol (M,Aseq))) . 1 by Th4, SUPINF_2:48 .= (vol (M,Aseq)) . 0 by A5, MEASURE7:9 ; then SUM (vol (M,Aseq)) = M . (Aseq . 0) by Def5; then A6: M . A in Svc (M,A) by A3, Def7; (C_Meas M) . A = inf (Svc (M,A)) by Def8; hence (C_Meas M) . A9 <= M . A9 by A6, XXREAL_2:3; ::_thesis: verum end; theorem Th10: :: MEASURE8:10 for X being set for F being Field_Subset of X for M being Measure of F holds C_Meas M is nonnegative proof let X be set ; ::_thesis: for F being Field_Subset of X for M being Measure of F holds C_Meas M is nonnegative let F be Field_Subset of X; ::_thesis: for M being Measure of F holds C_Meas M is nonnegative let M be Measure of F; ::_thesis: C_Meas M is nonnegative for r being ext-real number st r in rng (C_Meas M) holds 0 <= r proof let r be ext-real number ; ::_thesis: ( r in rng (C_Meas M) implies 0 <= r ) assume r in rng (C_Meas M) ; ::_thesis: 0 <= r then consider A being set such that A1: A in bool X and A2: (C_Meas M) . A = r by FUNCT_2:11; reconsider A = A as Subset of X by A1; now__::_thesis:_for_p_being_ext-real_number_st_p_in_Svc_(M,A)_holds_ 0_<=_p let p be ext-real number ; ::_thesis: ( p in Svc (M,A) implies 0 <= p ) assume p in Svc (M,A) ; ::_thesis: 0 <= p then ex G being Covering of A,F st p = SUM (vol (M,G)) by Def7; hence 0 <= p by Th4, MEASURE6:2; ::_thesis: verum end; then 0 is LowerBound of Svc (M,A) by XXREAL_2:def_2; then 0 <= inf (Svc (M,A)) by XXREAL_2:def_4; hence 0 <= r by A2, Def8; ::_thesis: verum end; then for r being R_eal st r in rng (C_Meas M) holds 0 <= r ; then rng (C_Meas M) is nonnegative by SUPINF_2:def_9; hence C_Meas M is nonnegative by SUPINF_2:def_16; ::_thesis: verum end; theorem Th11: :: MEASURE8:11 for X being set for F being Field_Subset of X for M being Measure of F holds (C_Meas M) . {} = 0 proof let X be set ; ::_thesis: for F being Field_Subset of X for M being Measure of F holds (C_Meas M) . {} = 0 let F be Field_Subset of X; ::_thesis: for M being Measure of F holds (C_Meas M) . {} = 0 let M be Measure of F; ::_thesis: (C_Meas M) . {} = 0 (C_Meas M) . {} <= M . {} by Th9, PROB_1:4; then A1: (C_Meas M) . {} <= 0 by VALUED_0:def_19; {} X in bool X ; then {} in dom (C_Meas M) by FUNCT_2:def_1; then A2: (C_Meas M) . {} in rng (C_Meas M) by FUNCT_1:3; C_Meas M is nonnegative by Th10; then rng (C_Meas M) is nonnegative by SUPINF_2:def_16; hence (C_Meas M) . {} = 0. by A1, A2, SUPINF_2:def_9; ::_thesis: verum end; theorem Th12: :: MEASURE8:12 for X being set for F being Field_Subset of X for M being Measure of F for A, B being Subset of X st A c= B holds (C_Meas M) . A <= (C_Meas M) . B proof let X be set ; ::_thesis: for F being Field_Subset of X for M being Measure of F for A, B being Subset of X st A c= B holds (C_Meas M) . A <= (C_Meas M) . B let F be Field_Subset of X; ::_thesis: for M being Measure of F for A, B being Subset of X st A c= B holds (C_Meas M) . A <= (C_Meas M) . B let M be Measure of F; ::_thesis: for A, B being Subset of X st A c= B holds (C_Meas M) . A <= (C_Meas M) . B let A, B be Subset of X; ::_thesis: ( A c= B implies (C_Meas M) . A <= (C_Meas M) . B ) assume A1: A c= B ; ::_thesis: (C_Meas M) . A <= (C_Meas M) . B now__::_thesis:_for_r_being_set_st_r_in_Svc_(M,B)_holds_ r_in_Svc_(M,A) let r be set ; ::_thesis: ( r in Svc (M,B) implies r in Svc (M,A) ) assume r in Svc (M,B) ; ::_thesis: r in Svc (M,A) then consider G being Covering of B,F such that A2: SUM (vol (M,G)) = r by Def7; B c= union (rng G) by Def3; then A c= union (rng G) by A1, XBOOLE_1:1; then reconsider G1 = G as Covering of A,F by Def3; SUM (vol (M,G)) = SUM (vol (M,G1)) ; hence r in Svc (M,A) by A2, Def7; ::_thesis: verum end; then A3: Svc (M,B) c= Svc (M,A) by TARSKI:def_3; ( (C_Meas M) . A = inf (Svc (M,A)) & (C_Meas M) . B = inf (Svc (M,B)) ) by Def8; hence (C_Meas M) . A <= (C_Meas M) . B by A3, XXREAL_2:60; ::_thesis: verum end; Lm2: for X being set for F being Field_Subset of X for M being Measure of F for Sets being SetSequence of X st ex n being Nat st (C_Meas M) . (Sets . n) = +infty holds (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets) proof let X be set ; ::_thesis: for F being Field_Subset of X for M being Measure of F for Sets being SetSequence of X st ex n being Nat st (C_Meas M) . (Sets . n) = +infty holds (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets) let F be Field_Subset of X; ::_thesis: for M being Measure of F for Sets being SetSequence of X st ex n being Nat st (C_Meas M) . (Sets . n) = +infty holds (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets) let M be Measure of F; ::_thesis: for Sets being SetSequence of X st ex n being Nat st (C_Meas M) . (Sets . n) = +infty holds (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets) let Sets be SetSequence of X; ::_thesis: ( ex n being Nat st (C_Meas M) . (Sets . n) = +infty implies (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets) ) assume ex n being Nat st (C_Meas M) . (Sets . n) = +infty ; ::_thesis: (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets) then consider N being Nat such that A1: (C_Meas M) . (Sets . N) = +infty ; reconsider N = N as Element of NAT by ORDINAL1:def_12; A2: (C_Meas M) * Sets is nonnegative by Th10, MEASURE1:25; dom Sets = NAT by FUNCT_2:def_1; then ((C_Meas M) * Sets) . N = (C_Meas M) . (Sets . N) by FUNCT_1:13; then SUM ((C_Meas M) * Sets) = +infty by A1, A2, SUPINF_2:45; hence (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets) by XXREAL_0:3; ::_thesis: verum end; theorem Th13: :: MEASURE8:13 for X being set for F being Field_Subset of X for M being Measure of F for Sets being SetSequence of X holds (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets) proof let X be set ; ::_thesis: for F being Field_Subset of X for M being Measure of F for Sets being SetSequence of X holds (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets) let F be Field_Subset of X; ::_thesis: for M being Measure of F for Sets being SetSequence of X holds (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets) let M be Measure of F; ::_thesis: for Sets being SetSequence of X holds (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets) let Sets be SetSequence of X; ::_thesis: (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets) A1: now__::_thesis:_(_(_for_n_being_Element_of_NAT_holds_Svc_(M,(Sets_._n))_<>_{+infty}_)_implies_(C_Meas_M)_._(union_(rng_Sets))_<=_SUM_((C_Meas_M)_*_Sets)_) assume A2: for n being Element of NAT holds Svc (M,(Sets . n)) <> {+infty} ; ::_thesis: (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets) inf (Svc (M,(union (rng Sets)))) <= sup (rng (Ser ((C_Meas M) * Sets))) proof set y = inf (Svc (M,(union (rng Sets)))); set x = sup (rng (Ser ((C_Meas M) * Sets))); A3: (Ser ((C_Meas M) * Sets)) . 0 <= sup (rng (Ser ((C_Meas M) * Sets))) by FUNCT_2:4, XXREAL_2:4; A4: (C_Meas M) * Sets is nonnegative by Th10, MEASURE1:25; then 0 <= ((C_Meas M) * Sets) . 0 by SUPINF_2:39; then A5: 0 <= (Ser ((C_Meas M) * Sets)) . 0 by SUPINF_2:44; assume not inf (Svc (M,(union (rng Sets)))) <= sup (rng (Ser ((C_Meas M) * Sets))) ; ::_thesis: contradiction then consider eps being real number such that A6: 0 < eps and A7: (sup (rng (Ser ((C_Meas M) * Sets)))) + eps < inf (Svc (M,(union (rng Sets)))) by A5, A3, XXREAL_3:49; eps in ExtREAL by XXREAL_0:def_1; then consider E being Function of NAT,ExtREAL such that A8: for n being Element of NAT holds 0 < E . n and A9: SUM E < eps by A6, MEASURE6:4; for n being Element of NAT holds 0 <= E . n by A8; then A10: E is nonnegative by SUPINF_2:39; defpred S1[ Element of NAT , set ] means ex F0 being Covering of Sets . $1,F st ( $2 = F0 & SUM (vol (M,F0)) < (inf (Svc (M,(Sets . $1)))) + (E . $1) ); A11: for n being Element of NAT ex F0 being Element of Funcs (NAT,(bool X)) st S1[n,F0] proof let n be Element of NAT ; ::_thesis: ex F0 being Element of Funcs (NAT,(bool X)) st S1[n,F0] ( C_Meas M is nonnegative & (C_Meas M) . (Sets . n) = inf (Svc (M,(Sets . n))) ) by Def8, Th10; then A12: ( 0 is Real & 0. <= inf (Svc (M,(Sets . n))) ) by SUPINF_2:51; Svc (M,(Sets . n)) <> {+infty} by A2; then not Svc (M,(Sets . n)) c= {+infty} by ZFMISC_1:33; then (Svc (M,(Sets . n))) \ {+infty} <> {} by XBOOLE_1:37; then consider x being set such that A13: x in (Svc (M,(Sets . n))) \ {+infty} by XBOOLE_0:def_1; reconsider x = x as R_eal by A13; not x in {+infty} by A13, XBOOLE_0:def_5; then A14: x <> +infty by TARSKI:def_1; x in Svc (M,(Sets . n)) by A13, XBOOLE_0:def_5; then inf (Svc (M,(Sets . n))) <= x by XXREAL_2:3; then inf (Svc (M,(Sets . n))) < +infty by A14, XXREAL_0:2, XXREAL_0:4; then inf (Svc (M,(Sets . n))) is Real by A12, XXREAL_0:46; then consider S1 being ext-real number such that A15: S1 in Svc (M,(Sets . n)) and A16: S1 < (inf (Svc (M,(Sets . n)))) + (E . n) by A8, MEASURE6:5; consider FS being Covering of Sets . n,F such that A17: S1 = SUM (vol (M,FS)) by A15, Def7; reconsider FS = FS as Element of Funcs (NAT,(bool X)) by FUNCT_2:8; take FS ; ::_thesis: S1[n,FS] thus S1[n,FS] by A16, A17; ::_thesis: verum end; consider FF being Function of NAT,(Funcs (NAT,(bool X))) such that A18: for n being Element of NAT holds S1[n,FF . n] from FUNCT_2:sch_3(A11); A19: for n being Nat holds FF . n is Covering of Sets . n,F proof let n be Nat; ::_thesis: FF . n is Covering of Sets . n,F n in NAT by ORDINAL1:def_12; then ex F0 being Covering of Sets . n,F st ( F0 = FF . n & SUM (vol (M,F0)) < (inf (Svc (M,(Sets . n)))) + (E . n) ) by A18; hence FF . n is Covering of Sets . n,F ; ::_thesis: verum end; deffunc H1( Element of NAT ) -> set = (((C_Meas M) * Sets) . $1) + (E . $1); A20: for x being Element of NAT holds H1(x) is Element of ExtREAL by XXREAL_0:def_1; consider G0 being Function of NAT,ExtREAL such that A21: for n being Element of NAT holds G0 . n = H1(n) from FUNCT_2:sch_9(A20); reconsider FF = FF as Covering of Sets,F by A19, Def4; for n being Element of NAT holds (Volume (M,FF)) . n <= G0 . n proof let n be Element of NAT ; ::_thesis: (Volume (M,FF)) . n <= G0 . n ( ex F0 being Covering of Sets . n,F st ( F0 = FF . n & SUM (vol (M,F0)) < (inf (Svc (M,(Sets . n)))) + (E . n) ) & ((C_Meas M) * Sets) . n = (C_Meas M) . (Sets . n) ) by A18, FUNCT_2:15; then SUM (vol (M,(FF . n))) < (((C_Meas M) * Sets) . n) + (E . n) by Def8; then (Volume (M,FF)) . n < (((C_Meas M) * Sets) . n) + (E . n) by Def6; hence (Volume (M,FF)) . n <= G0 . n by A21; ::_thesis: verum end; then A22: SUM (Volume (M,FF)) <= SUM G0 by SUPINF_2:43; A23: now__::_thesis:_for_n_being_Nat_holds_G0_._n_=_(((C_Meas_M)_*_Sets)_._n)_+_(E_._n) let n be Nat; ::_thesis: G0 . n = (((C_Meas M) * Sets) . n) + (E . n) n is Element of NAT by ORDINAL1:def_12; hence G0 . n = (((C_Meas M) * Sets) . n) + (E . n) by A21; ::_thesis: verum end; (SUM ((C_Meas M) * Sets)) + (SUM E) <= (SUM ((C_Meas M) * Sets)) + eps by A9, XXREAL_3:36; then SUM G0 <= (SUM ((C_Meas M) * Sets)) + eps by A4, A10, A23, Th3; then A24: SUM (Volume (M,FF)) <= (SUM ((C_Meas M) * Sets)) + eps by A22, XXREAL_0:2; inf (Svc (M,(union (rng Sets)))) <= SUM (Volume (M,FF)) by Th7; hence contradiction by A7, A24, XXREAL_0:2; ::_thesis: verum end; hence (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets) by Def8; ::_thesis: verum end; now__::_thesis:_(_ex_n_being_Element_of_NAT_st_Svc_(M,(Sets_._n))_=_{+infty}_implies_(C_Meas_M)_._(union_(rng_Sets))_<=_SUM_((C_Meas_M)_*_Sets)_) assume ex n being Element of NAT st Svc (M,(Sets . n)) = {+infty} ; ::_thesis: (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets) then consider n being Element of NAT such that A25: Svc (M,(Sets . n)) = {+infty} ; inf {+infty} = +infty by XXREAL_2:13; then (C_Meas M) . (Sets . n) = +infty by A25, Def8; hence (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets) by Lm2; ::_thesis: verum end; hence (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets) by A1; ::_thesis: verum end; theorem Th14: :: MEASURE8:14 for X being set for F being Field_Subset of X for M being Measure of F holds C_Meas M is C_Measure of X proof let X be set ; ::_thesis: for F being Field_Subset of X for M being Measure of F holds C_Meas M is C_Measure of X let F be Field_Subset of X; ::_thesis: for M being Measure of F holds C_Meas M is C_Measure of X let M be Measure of F; ::_thesis: C_Meas M is C_Measure of X (C_Meas M) . {} = 0. by Th11; then A1: C_Meas M is zeroed by VALUED_0:def_19; ( C_Meas M is nonnegative & ( for A, B being Subset of X st A c= B holds ( (C_Meas M) . A <= (C_Meas M) . B & ( for F being Function of NAT,(bool X) holds (C_Meas M) . (union (rng F)) <= SUM ((C_Meas M) * F) ) ) ) ) by Th10, Th12, Th13; hence C_Meas M is C_Measure of X by A1, MEASURE4:def_1; ::_thesis: verum end; definition let X be set ; let F be Field_Subset of X; let M be Measure of F; :: original: C_Meas redefine func C_Meas M -> C_Measure of X; correctness coherence C_Meas M is C_Measure of X; by Th14; end; begin definition let X be set ; let F be Field_Subset of X; let M be Measure of F; attrM is completely-additive means :Def11: :: MEASURE8:def 11 for FSets being Sep_Sequence of F st union (rng FSets) in F holds SUM (M * FSets) = M . (union (rng FSets)); end; :: deftheorem Def11 defines completely-additive MEASURE8:def_11_:_ for X being set for F being Field_Subset of X for M being Measure of F holds ( M is completely-additive iff for FSets being Sep_Sequence of F st union (rng FSets) in F holds SUM (M * FSets) = M . (union (rng FSets)) ); theorem Th15: :: MEASURE8:15 for X being set for F being Field_Subset of X for FSets being Set_Sequence of F holds Partial_Union FSets is Set_Sequence of F proof let X be set ; ::_thesis: for F being Field_Subset of X for FSets being Set_Sequence of F holds Partial_Union FSets is Set_Sequence of F let F be Field_Subset of X; ::_thesis: for FSets being Set_Sequence of F holds Partial_Union FSets is Set_Sequence of F let FSets be Set_Sequence of F; ::_thesis: Partial_Union FSets is Set_Sequence of F defpred S1[ Nat] means (Partial_Union FSets) . $1 in F; A1: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) A2: (Partial_Union FSets) . (k + 1) = ((Partial_Union FSets) . k) \/ (FSets . (k + 1)) by PROB_3:def_2; assume S1[k] ; ::_thesis: S1[k + 1] hence S1[k + 1] by A2, PROB_1:3; ::_thesis: verum end; (Partial_Union FSets) . 0 = FSets . 0 by PROB_3:def_2; then A3: S1[ 0 ] ; for n being Nat holds S1[n] from NAT_1:sch_2(A3, A1); hence Partial_Union FSets is Set_Sequence of F by Def2; ::_thesis: verum end; theorem Th16: :: MEASURE8:16 for X being set for F being Field_Subset of X for FSets being Set_Sequence of F holds Partial_Diff_Union FSets is Set_Sequence of F proof let X be set ; ::_thesis: for F being Field_Subset of X for FSets being Set_Sequence of F holds Partial_Diff_Union FSets is Set_Sequence of F let F be Field_Subset of X; ::_thesis: for FSets being Set_Sequence of F holds Partial_Diff_Union FSets is Set_Sequence of F let FSets be Set_Sequence of F; ::_thesis: Partial_Diff_Union FSets is Set_Sequence of F defpred S1[ Nat] means (Partial_Diff_Union FSets) . $1 in F; A1: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume S1[k] ; ::_thesis: S1[k + 1] Partial_Union FSets is Set_Sequence of F by Th15; then A2: (Partial_Union FSets) . k in F by Def2; (Partial_Diff_Union FSets) . (k + 1) = (FSets . (k + 1)) \ ((Partial_Union FSets) . k) by PROB_3:def_3; hence S1[k + 1] by A2, PROB_1:6; ::_thesis: verum end; (Partial_Diff_Union FSets) . 0 = FSets . 0 by PROB_3:def_3; then A3: S1[ 0 ] ; for n being Nat holds S1[n] from NAT_1:sch_2(A3, A1); hence Partial_Diff_Union FSets is Set_Sequence of F by Def2; ::_thesis: verum end; theorem Th17: :: MEASURE8:17 for X being set for F being Field_Subset of X for A being Subset of X for CA being Covering of A,F st A in F holds ex FSets being Sep_Sequence of F st ( A = union (rng FSets) & ( for n being Nat holds FSets . n c= CA . n ) ) proof let X be set ; ::_thesis: for F being Field_Subset of X for A being Subset of X for CA being Covering of A,F st A in F holds ex FSets being Sep_Sequence of F st ( A = union (rng FSets) & ( for n being Nat holds FSets . n c= CA . n ) ) let F be Field_Subset of X; ::_thesis: for A being Subset of X for CA being Covering of A,F st A in F holds ex FSets being Sep_Sequence of F st ( A = union (rng FSets) & ( for n being Nat holds FSets . n c= CA . n ) ) let A be Subset of X; ::_thesis: for CA being Covering of A,F st A in F holds ex FSets being Sep_Sequence of F st ( A = union (rng FSets) & ( for n being Nat holds FSets . n c= CA . n ) ) let CA be Covering of A,F; ::_thesis: ( A in F implies ex FSets being Sep_Sequence of F st ( A = union (rng FSets) & ( for n being Nat holds FSets . n c= CA . n ) ) ) deffunc H1( Element of NAT ) -> Element of bool X = ((Partial_Diff_Union CA) . $1) /\ A; consider FSets being Function of NAT,(bool X) such that A1: for n being Element of NAT holds FSets . n = H1(n) from FUNCT_2:sch_4(); reconsider FSets = FSets as SetSequence of X ; assume A2: A in F ; ::_thesis: ex FSets being Sep_Sequence of F st ( A = union (rng FSets) & ( for n being Nat holds FSets . n c= CA . n ) ) now__::_thesis:_for_y_being_set_st_y_in_rng_FSets_holds_ y_in_F let y be set ; ::_thesis: ( y in rng FSets implies y in F ) assume y in rng FSets ; ::_thesis: y in F then consider x being set such that A3: x in NAT and A4: FSets . x = y by FUNCT_2:11; reconsider n = x as Element of NAT by A3; A5: FSets . n = ((Partial_Diff_Union CA) . n) /\ A by A1; Partial_Diff_Union CA is Set_Sequence of F by Th16; then (Partial_Diff_Union CA) . n in F by Def2; hence y in F by A2, A4, A5, FINSUB_1:def_2; ::_thesis: verum end; then rng FSets c= F by TARSKI:def_3; then reconsider FSets = FSets as Function of NAT,F by FUNCT_2:6; for m, n being Nat st m <> n holds FSets . m misses FSets . n proof let m, n be Nat; ::_thesis: ( m <> n implies FSets . m misses FSets . n ) n in NAT by ORDINAL1:def_12; then FSets . n = ((Partial_Diff_Union CA) . n) /\ A by A1; then A6: FSets . n c= (Partial_Diff_Union CA) . n by XBOOLE_1:17; m in NAT by ORDINAL1:def_12; then FSets . m = ((Partial_Diff_Union CA) . m) /\ A by A1; then A7: FSets . m c= (Partial_Diff_Union CA) . m by XBOOLE_1:17; assume m <> n ; ::_thesis: FSets . m misses FSets . n then (Partial_Diff_Union CA) . m misses (Partial_Diff_Union CA) . n by PROB_3:def_4; hence FSets . m misses FSets . n by A7, A6, XBOOLE_1:64; ::_thesis: verum end; then reconsider FSets = FSets as Sep_Sequence of F by PROB_3:def_4; now__::_thesis:_for_x_being_set_st_x_in_A_holds_ x_in_union_(rng_FSets) let x be set ; ::_thesis: ( x in A implies x in union (rng FSets) ) assume A8: x in A ; ::_thesis: x in union (rng FSets) A c= union (rng CA) by Def3; then x in union (rng CA) by A8; then x in Union CA by CARD_3:def_4; then x in Union (Partial_Diff_Union CA) by PROB_3:20; then x in union (rng (Partial_Diff_Union CA)) by CARD_3:def_4; then consider E being set such that A9: x in E and A10: E in rng (Partial_Diff_Union CA) by TARSKI:def_4; consider n being set such that A11: n in NAT and A12: (Partial_Diff_Union CA) . n = E by A10, FUNCT_2:11; reconsider n = n as Element of NAT by A11; x in ((Partial_Diff_Union CA) . n) /\ A by A8, A9, A12, XBOOLE_0:def_4; then A13: x in FSets . n by A1; FSets . n in rng FSets by FUNCT_2:4; hence x in union (rng FSets) by A13, TARSKI:def_4; ::_thesis: verum end; then A14: A c= union (rng FSets) by TARSKI:def_3; take FSets ; ::_thesis: ( A = union (rng FSets) & ( for n being Nat holds FSets . n c= CA . n ) ) now__::_thesis:_for_x_being_set_st_x_in_union_(rng_FSets)_holds_ x_in_A let x be set ; ::_thesis: ( x in union (rng FSets) implies x in A ) assume x in union (rng FSets) ; ::_thesis: x in A then consider E being set such that A15: x in E and A16: E in rng FSets by TARSKI:def_4; consider n being set such that A17: n in NAT and A18: FSets . n = E by A16, FUNCT_2:11; reconsider n = n as Element of NAT by A17; x in ((Partial_Diff_Union CA) . n) /\ A by A1, A15, A18; hence x in A by XBOOLE_0:def_4; ::_thesis: verum end; then union (rng FSets) c= A by TARSKI:def_3; hence A = union (rng FSets) by A14, XBOOLE_0:def_10; ::_thesis: for n being Nat holds FSets . n c= CA . n hereby ::_thesis: verum let n be Nat; ::_thesis: FSets . n c= CA . n n in NAT by ORDINAL1:def_12; then FSets . n = ((Partial_Diff_Union CA) . n) /\ A by A1; then A19: FSets . n c= (Partial_Diff_Union CA) . n by XBOOLE_1:17; (Partial_Diff_Union CA) . n c= CA . n by PROB_3:17; hence FSets . n c= CA . n by A19, XBOOLE_1:1; ::_thesis: verum end; end; theorem Th18: :: MEASURE8:18 for X being set for F being Field_Subset of X for M being Measure of F st M is completely-additive holds for A being set st A in F holds M . A = (C_Meas M) . A proof let X be set ; ::_thesis: for F being Field_Subset of X for M being Measure of F st M is completely-additive holds for A being set st A in F holds M . A = (C_Meas M) . A let F be Field_Subset of X; ::_thesis: for M being Measure of F st M is completely-additive holds for A being set st A in F holds M . A = (C_Meas M) . A let M be Measure of F; ::_thesis: ( M is completely-additive implies for A being set st A in F holds M . A = (C_Meas M) . A ) assume A1: M is completely-additive ; ::_thesis: for A being set st A in F holds M . A = (C_Meas M) . A let A be set ; ::_thesis: ( A in F implies M . A = (C_Meas M) . A ) assume A2: A in F ; ::_thesis: M . A = (C_Meas M) . A then reconsider A9 = A as Subset of X ; for x being ext-real number st x in Svc (M,A9) holds M . A <= x proof let x be ext-real number ; ::_thesis: ( x in Svc (M,A9) implies M . A <= x ) assume x in Svc (M,A9) ; ::_thesis: M . A <= x then consider Aseq being Covering of A9,F such that A3: x = SUM (vol (M,Aseq)) by Def7; consider Bseq being Sep_Sequence of F such that A4: A = union (rng Bseq) and A5: for n being Nat holds Bseq . n c= Aseq . n by A2, Th17; for n being Element of NAT holds (M * Bseq) . n <= (vol (M,Aseq)) . n proof let n be Element of NAT ; ::_thesis: (M * Bseq) . n <= (vol (M,Aseq)) . n M . (Bseq . n) <= M . (Aseq . n) by A5, MEASURE1:8; then (M * Bseq) . n <= M . (Aseq . n) by FUNCT_2:15; hence (M * Bseq) . n <= (vol (M,Aseq)) . n by Def5; ::_thesis: verum end; then SUM (M * Bseq) <= SUM (vol (M,Aseq)) by SUPINF_2:43; hence M . A <= x by A1, A2, A3, A4, Def11; ::_thesis: verum end; then M . A is LowerBound of Svc (M,A9) by XXREAL_2:def_2; then M . A <= inf (Svc (M,A9)) by XXREAL_2:def_4; then A6: M . A <= (C_Meas M) . A9 by Def8; (C_Meas M) . A <= M . A by A2, Th9; hence M . A = (C_Meas M) . A by A6, XXREAL_0:1; ::_thesis: verum end; theorem Th19: :: MEASURE8:19 for X being set for A being Subset of X for C being C_Measure of X st ( for B being Subset of X holds (C . (B /\ A)) + (C . (B /\ (X \ A))) <= C . B ) holds A in sigma_Field C proof let X be set ; ::_thesis: for A being Subset of X for C being C_Measure of X st ( for B being Subset of X holds (C . (B /\ A)) + (C . (B /\ (X \ A))) <= C . B ) holds A in sigma_Field C let A be Subset of X; ::_thesis: for C being C_Measure of X st ( for B being Subset of X holds (C . (B /\ A)) + (C . (B /\ (X \ A))) <= C . B ) holds A in sigma_Field C let C be C_Measure of X; ::_thesis: ( ( for B being Subset of X holds (C . (B /\ A)) + (C . (B /\ (X \ A))) <= C . B ) implies A in sigma_Field C ) assume A1: for B being Subset of X holds (C . (B /\ A)) + (C . (B /\ (X \ A))) <= C . B ; ::_thesis: A in sigma_Field C for W, Z being Subset of X st W c= A & Z c= X \ A holds (C . W) + (C . Z) <= C . (W \/ Z) proof let W, Z be Subset of X; ::_thesis: ( W c= A & Z c= X \ A implies (C . W) + (C . Z) <= C . (W \/ Z) ) assume that A2: W c= A and A3: Z c= X \ A ; ::_thesis: (C . W) + (C . Z) <= C . (W \/ Z) set Y = W \/ Z; A4: Z misses A by A3, XBOOLE_1:106; A5: (W \/ Z) /\ (X \ A) = ((W \/ Z) /\ X) \ A by XBOOLE_1:49 .= ((X /\ W) \/ (X /\ Z)) \ A by XBOOLE_1:23 .= (W \/ (X /\ Z)) \ A by XBOOLE_1:28 .= (W \/ Z) \ A by XBOOLE_1:28 .= (W \ A) \/ (Z \ A) by XBOOLE_1:42 .= {} \/ (Z \ A) by A2, XBOOLE_1:37 .= {} \/ Z by A4, XBOOLE_1:83 ; (W \/ Z) /\ A = (A /\ W) \/ (A /\ Z) by XBOOLE_1:23 .= W \/ (A /\ Z) by A2, XBOOLE_1:28 .= W \/ {} by A4, XBOOLE_0:def_7 ; hence (C . W) + (C . Z) <= C . (W \/ Z) by A1, A5; ::_thesis: verum end; hence A in sigma_Field C by MEASURE4:def_2; ::_thesis: verum end; theorem Th20: :: MEASURE8:20 for X being set for F being Field_Subset of X for M being Measure of F holds F c= sigma_Field (C_Meas M) proof let X be set ; ::_thesis: for F being Field_Subset of X for M being Measure of F holds F c= sigma_Field (C_Meas M) let F be Field_Subset of X; ::_thesis: for M being Measure of F holds F c= sigma_Field (C_Meas M) let M be Measure of F; ::_thesis: F c= sigma_Field (C_Meas M) set C = C_Meas M; now__::_thesis:_for_E_being_set_st_E_in_F_holds_ E_in_sigma_Field_(C_Meas_M) let E be set ; ::_thesis: ( E in F implies E in sigma_Field (C_Meas M) ) assume A1: E in F ; ::_thesis: E in sigma_Field (C_Meas M) then reconsider E9 = E as Subset of X ; for A being Subset of X holds ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) <= (C_Meas M) . A proof let A be Subset of X; ::_thesis: ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) <= (C_Meas M) . A set CA = ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))); A2: for seq being Covering of A,F holds ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) <= SUM (vol (M,seq)) proof let seq be Covering of A,F; ::_thesis: ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) <= SUM (vol (M,seq)) deffunc H1( Element of NAT ) -> Element of bool X = (seq . $1) /\ E; consider Bseq being Function of NAT,(bool X) such that A3: for n being Element of NAT holds Bseq . n = H1(n) from FUNCT_2:sch_4(); reconsider Bseq = Bseq as SetSequence of X ; for n being Nat holds Bseq . n in F proof let n be Nat; ::_thesis: Bseq . n in F n in NAT by ORDINAL1:def_12; then Bseq . n = (seq . n) /\ E by A3; hence Bseq . n in F by A1, FINSUB_1:def_2; ::_thesis: verum end; then reconsider Bseq = Bseq as Set_Sequence of F by Def2; A4: for x being set st x in A holds ex n being Element of NAT st x in seq . n proof let x be set ; ::_thesis: ( x in A implies ex n being Element of NAT st x in seq . n ) assume A5: x in A ; ::_thesis: ex n being Element of NAT st x in seq . n A c= union (rng seq) by Def3; then consider B being set such that A6: x in B and A7: B in rng seq by A5, TARSKI:def_4; ex n being Element of NAT st B = seq . n by A7, FUNCT_2:113; hence ex n being Element of NAT st x in seq . n by A6; ::_thesis: verum end; now__::_thesis:_for_x_being_set_st_x_in_A_/\_E9_holds_ x_in_union_(rng_Bseq) let x be set ; ::_thesis: ( x in A /\ E9 implies x in union (rng Bseq) ) assume A8: x in A /\ E9 ; ::_thesis: x in union (rng Bseq) then x in A by XBOOLE_0:def_4; then consider n being Element of NAT such that A9: x in seq . n by A4; x in E9 by A8, XBOOLE_0:def_4; then x in (seq . n) /\ E by A9, XBOOLE_0:def_4; then A10: x in Bseq . n by A3; Bseq . n in rng Bseq by FUNCT_2:4; hence x in union (rng Bseq) by A10, TARSKI:def_4; ::_thesis: verum end; then A /\ E9 c= union (rng Bseq) by TARSKI:def_3; then reconsider Bseq = Bseq as Covering of A /\ E9,F by Def3; deffunc H2( Element of NAT ) -> Element of bool X = (seq . $1) /\ (X \ E); consider Cseq being Function of NAT,(bool X) such that A11: for n being Element of NAT holds Cseq . n = H2(n) from FUNCT_2:sch_4(); reconsider Cseq = Cseq as SetSequence of X ; for n being Nat holds Cseq . n in F proof let n be Nat; ::_thesis: Cseq . n in F X in F by PROB_1:5; then A12: X \ E in F by A1, PROB_1:6; n in NAT by ORDINAL1:def_12; then Cseq . n = (seq . n) /\ (X \ E) by A11; hence Cseq . n in F by A12, FINSUB_1:def_2; ::_thesis: verum end; then reconsider Cseq = Cseq as Set_Sequence of F by Def2; now__::_thesis:_for_x_being_set_st_x_in_A_/\_(X_\_E9)_holds_ x_in_union_(rng_Cseq) let x be set ; ::_thesis: ( x in A /\ (X \ E9) implies x in union (rng Cseq) ) assume A13: x in A /\ (X \ E9) ; ::_thesis: x in union (rng Cseq) then x in A by XBOOLE_0:def_4; then consider n being Element of NAT such that A14: x in seq . n by A4; x in X \ E9 by A13, XBOOLE_0:def_4; then x in (seq . n) /\ (X \ E) by A14, XBOOLE_0:def_4; then A15: x in Cseq . n by A11; Cseq . n in rng Cseq by FUNCT_2:4; hence x in union (rng Cseq) by A15, TARSKI:def_4; ::_thesis: verum end; then A /\ (X \ E9) c= union (rng Cseq) by TARSKI:def_3; then reconsider Cseq = Cseq as Covering of A /\ (X \ E9),F by Def3; A16: for n being Nat holds (vol (M,seq)) . n = ((vol (M,Bseq)) . n) + ((vol (M,Cseq)) . n) proof let n be Nat; ::_thesis: (vol (M,seq)) . n = ((vol (M,Bseq)) . n) + ((vol (M,Cseq)) . n) A17: ( M . (seq . n) = (vol (M,seq)) . n & M . (Bseq . n) = (vol (M,Bseq)) . n ) by Def5; A18: M . (Cseq . n) = (vol (M,Cseq)) . n by Def5; n is Element of NAT by ORDINAL1:def_12; then A19: ( Bseq . n = (seq . n) /\ E & Cseq . n = (seq . n) /\ (X \ E) ) by A3, A11; then (Bseq . n) \/ (Cseq . n) = (seq . n) /\ (E \/ (X \ E)) by XBOOLE_1:23; then (Bseq . n) \/ (Cseq . n) = (seq . n) /\ (E \/ X) by XBOOLE_1:39; then (Bseq . n) \/ (Cseq . n) = (seq . n) /\ X by XBOOLE_1:12; then A20: (Bseq . n) \/ (Cseq . n) = seq . n by XBOOLE_1:28; Bseq . n misses Cseq . n by A19, XBOOLE_1:76, XBOOLE_1:79; hence (vol (M,seq)) . n = ((vol (M,Bseq)) . n) + ((vol (M,Cseq)) . n) by A20, A17, A18, MEASURE1:def_3; ::_thesis: verum end; ( (C_Meas M) . (A /\ (X \ E9)) = inf (Svc (M,(A /\ (X \ E9)))) & SUM (vol (M,Cseq)) in Svc (M,(A /\ (X \ E9))) ) by Def7, Def8; then A21: (C_Meas M) . (A /\ (X \ E9)) <= SUM (vol (M,Cseq)) by XXREAL_2:3; ( (C_Meas M) . (A /\ E9) = inf (Svc (M,(A /\ E9))) & SUM (vol (M,Bseq)) in Svc (M,(A /\ E9)) ) by Def7, Def8; then A22: (C_Meas M) . (A /\ E9) <= SUM (vol (M,Bseq)) by XXREAL_2:3; ( vol (M,Bseq) is nonnegative & vol (M,Cseq) is nonnegative ) by Th4; then SUM (vol (M,seq)) = (SUM (vol (M,Bseq))) + (SUM (vol (M,Cseq))) by A16, Th3; hence ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) <= SUM (vol (M,seq)) by A22, A21, XXREAL_3:36; ::_thesis: verum end; for r being ext-real number st r in Svc (M,A) holds ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) <= r proof let r be ext-real number ; ::_thesis: ( r in Svc (M,A) implies ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) <= r ) assume r in Svc (M,A) ; ::_thesis: ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) <= r then ex G being Covering of A,F st r = SUM (vol (M,G)) by Def7; hence ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) <= r by A2; ::_thesis: verum end; then ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) is LowerBound of Svc (M,A) by XXREAL_2:def_2; then ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) <= inf (Svc (M,A)) by XXREAL_2:def_4; hence ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) <= (C_Meas M) . A by Def8; ::_thesis: verum end; hence E in sigma_Field (C_Meas M) by Th19; ::_thesis: verum end; hence F c= sigma_Field (C_Meas M) by TARSKI:def_3; ::_thesis: verum end; theorem Th21: :: MEASURE8:21 for X being set for F being Field_Subset of X for FSets being Set_Sequence of F for M being Function of F,ExtREAL holds M * FSets is ExtREAL_sequence proof let X be set ; ::_thesis: for F being Field_Subset of X for FSets being Set_Sequence of F for M being Function of F,ExtREAL holds M * FSets is ExtREAL_sequence let F be Field_Subset of X; ::_thesis: for FSets being Set_Sequence of F for M being Function of F,ExtREAL holds M * FSets is ExtREAL_sequence let FSets be Set_Sequence of F; ::_thesis: for M being Function of F,ExtREAL holds M * FSets is ExtREAL_sequence let M be Function of F,ExtREAL; ::_thesis: M * FSets is ExtREAL_sequence now__::_thesis:_for_y_being_set_st_y_in_rng_FSets_holds_ y_in_F let y be set ; ::_thesis: ( y in rng FSets implies y in F ) assume y in rng FSets ; ::_thesis: y in F then ex x being set st ( x in NAT & FSets . x = y ) by FUNCT_2:11; hence y in F by Def2; ::_thesis: verum end; then rng FSets c= F by TARSKI:def_3; then rng FSets c= dom M by FUNCT_2:def_1; then dom (M * FSets) = dom FSets by RELAT_1:27; then dom (M * FSets) = NAT by FUNCT_2:def_1; hence M * FSets is ExtREAL_sequence by FUNCT_2:def_1; ::_thesis: verum end; definition let X be set ; let F be Field_Subset of X; let FSets be Set_Sequence of F; let g be Function of F,ExtREAL; :: original: * redefine funcg * FSets -> ExtREAL_sequence; correctness coherence FSets * g is ExtREAL_sequence; by Th21; end; theorem Th22: :: MEASURE8:22 for X being set for S being SigmaField of X for SSets being SetSequence of S for M being Function of S,ExtREAL holds M * SSets is ExtREAL_sequence proof let X be set ; ::_thesis: for S being SigmaField of X for SSets being SetSequence of S for M being Function of S,ExtREAL holds M * SSets is ExtREAL_sequence let S be SigmaField of X; ::_thesis: for SSets being SetSequence of S for M being Function of S,ExtREAL holds M * SSets is ExtREAL_sequence let SSets be SetSequence of S; ::_thesis: for M being Function of S,ExtREAL holds M * SSets is ExtREAL_sequence let M be Function of S,ExtREAL; ::_thesis: M * SSets is ExtREAL_sequence rng SSets c= S ; then rng SSets c= dom M by FUNCT_2:def_1; then dom (M * SSets) = dom SSets by RELAT_1:27; then dom (M * SSets) = NAT by FUNCT_2:def_1; hence M * SSets is ExtREAL_sequence by FUNCT_2:def_1; ::_thesis: verum end; definition let X be set ; let S be SigmaField of X; let SSets be SetSequence of S; let g be Function of S,ExtREAL; :: original: * redefine funcg * SSets -> ExtREAL_sequence; correctness coherence SSets * g is ExtREAL_sequence; by Th22; end; theorem Th23: :: MEASURE8:23 for F, G being Function of NAT,ExtREAL for n being Nat st ( for m being Nat st m <= n holds F . m <= G . m ) holds (Ser F) . n <= (Ser G) . n proof let F, G be Function of NAT,ExtREAL; ::_thesis: for n being Nat st ( for m being Nat st m <= n holds F . m <= G . m ) holds (Ser F) . n <= (Ser G) . n let n be Nat; ::_thesis: ( ( for m being Nat st m <= n holds F . m <= G . m ) implies (Ser F) . n <= (Ser G) . n ) assume A1: for m being Nat st m <= n holds F . m <= G . m ; ::_thesis: (Ser F) . n <= (Ser G) . n defpred S1[ Nat] means ( ( for m being Nat st m <= $1 holds F . m <= G . m ) implies (Ser F) . $1 <= (Ser G) . $1 ); A2: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) A3: k is Element of NAT by ORDINAL1:def_12; assume A4: S1[k] ; ::_thesis: S1[k + 1] now__::_thesis:_(_(_for_m_being_Nat_st_m_<=_k_+_1_holds_ F_._m_<=_G_._m_)_implies_(Ser_F)_._(k_+_1)_<=_(Ser_G)_._(k_+_1)_) assume A5: for m being Nat st m <= k + 1 holds F . m <= G . m ; ::_thesis: (Ser F) . (k + 1) <= (Ser G) . (k + 1) A6: now__::_thesis:_for_m_being_Nat_st_m_<=_k_holds_ F_._m_<=_G_._m let m be Nat; ::_thesis: ( m <= k implies F . m <= G . m ) assume m <= k ; ::_thesis: F . m <= G . m then m < k + 1 by NAT_1:13; hence F . m <= G . m by A5; ::_thesis: verum end; F . (k + 1) <= G . (k + 1) by A5; then ((Ser F) . k) + (F . (k + 1)) <= ((Ser G) . k) + (G . (k + 1)) by A4, A6, XXREAL_3:36; then (Ser F) . (k + 1) <= ((Ser G) . k) + (G . (k + 1)) by A3, SUPINF_2:44; hence (Ser F) . (k + 1) <= (Ser G) . (k + 1) by A3, SUPINF_2:44; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; now__::_thesis:_(_(_for_m_being_Nat_st_m_<=_0_holds_ F_._m_<=_G_._m_)_implies_(Ser_F)_._0_<=_(Ser_G)_._0_) A7: ( (Ser F) . 0 = F . 0 & (Ser G) . 0 = G . 0 ) by SUPINF_2:44; assume for m being Nat st m <= 0 holds F . m <= G . m ; ::_thesis: (Ser F) . 0 <= (Ser G) . 0 hence (Ser F) . 0 <= (Ser G) . 0 by A7; ::_thesis: verum end; then A8: S1[ 0 ] ; for k being Nat holds S1[k] from NAT_1:sch_2(A8, A2); hence (Ser F) . n <= (Ser G) . n by A1; ::_thesis: verum end; theorem Th24: :: MEASURE8:24 for X being set for C being C_Measure of X for seq being Sep_Sequence of (sigma_Field C) holds ( union (rng seq) in sigma_Field C & C . (union (rng seq)) = Sum (C * seq) ) proof let X be set ; ::_thesis: for C being C_Measure of X for seq being Sep_Sequence of (sigma_Field C) holds ( union (rng seq) in sigma_Field C & C . (union (rng seq)) = Sum (C * seq) ) let C be C_Measure of X; ::_thesis: for seq being Sep_Sequence of (sigma_Field C) holds ( union (rng seq) in sigma_Field C & C . (union (rng seq)) = Sum (C * seq) ) let seq be Sep_Sequence of (sigma_Field C); ::_thesis: ( union (rng seq) in sigma_Field C & C . (union (rng seq)) = Sum (C * seq) ) A1: rng seq c= sigma_Field C by RELAT_1:def_19; then reconsider seq1 = seq as Function of NAT,(bool X) by FUNCT_2:6; A2: for A being Subset of X for n being Element of NAT holds ((Ser (C * (A (/\) seq1))) . n) + (C . (A /\ (X \ (union (rng seq))))) <= C . A proof defpred S1[ Nat] means for A being Subset of X holds C . A >= ((Ser (C * (A (/\) seq1))) . $1) + (C . (A /\ (X \ (union (rng seq))))); let A be Subset of X; ::_thesis: for n being Element of NAT holds ((Ser (C * (A (/\) seq1))) . n) + (C . (A /\ (X \ (union (rng seq))))) <= C . A let n be Element of NAT ; ::_thesis: ((Ser (C * (A (/\) seq1))) . n) + (C . (A /\ (X \ (union (rng seq))))) <= C . A A3: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A4: S1[k] ; ::_thesis: S1[k + 1] A5: now__::_thesis:_for_A_being_Subset_of_X_holds_C_._(A_/\_(X_\_(seq1_._(k_+_1))))_>=_((Ser_(C_*_(A_(/\)_seq1)))_._k)_+_(C_._(A_/\_(X_\_(union_(rng_seq))))) let A be Subset of X; ::_thesis: C . (A /\ (X \ (seq1 . (k + 1)))) >= ((Ser (C * (A (/\) seq1))) . k) + (C . (A /\ (X \ (union (rng seq))))) A6: C . (A /\ (X \ (seq1 . (k + 1)))) >= ((Ser (C * ((A /\ (X \ (seq1 . (k + 1)))) (/\) seq1))) . k) + (C . ((A /\ (X \ (seq1 . (k + 1)))) /\ (X \ (union (rng seq))))) by A4; for m being Nat st m <= k holds (C * (A (/\) seq1)) . m <= (C * ((A /\ (X \ (seq1 . (k + 1)))) (/\) seq1)) . m proof let m be Nat; ::_thesis: ( m <= k implies (C * (A (/\) seq1)) . m <= (C * ((A /\ (X \ (seq1 . (k + 1)))) (/\) seq1)) . m ) reconsider m1 = m as Element of NAT by ORDINAL1:def_12; assume m <= k ; ::_thesis: (C * (A (/\) seq1)) . m <= (C * ((A /\ (X \ (seq1 . (k + 1)))) (/\) seq1)) . m then m < k + 1 by NAT_1:13; then seq1 . m misses seq1 . (k + 1) by PROB_2:def_2; then A7: (seq1 . m) /\ (X \ (seq1 . (k + 1))) = seq1 . m by XBOOLE_1:28, XBOOLE_1:86; ((A /\ (X \ (seq1 . (k + 1)))) (/\) seq1) . m = (A /\ (X \ (seq1 . (k + 1)))) /\ (seq1 . m1) by SETLIM_2:def_5 .= A /\ ((seq1 . m) /\ (X \ (seq1 . (k + 1)))) by XBOOLE_1:16 ; then ((A /\ (X \ (seq1 . (k + 1)))) (/\) seq1) . m = (A (/\) seq1) . m1 by A7, SETLIM_2:def_5; then (C * ((A /\ (X \ (seq1 . (k + 1)))) (/\) seq1)) . m1 = C . ((A (/\) seq1) . m1) by FUNCT_2:15; hence (C * (A (/\) seq1)) . m <= (C * ((A /\ (X \ (seq1 . (k + 1)))) (/\) seq1)) . m by FUNCT_2:15; ::_thesis: verum end; then A8: (Ser (C * (A (/\) seq1))) . k <= (Ser (C * ((A /\ (X \ (seq1 . (k + 1)))) (/\) seq1))) . k by Th23; seq1 . (k + 1) c= union (rng seq) by FUNCT_2:4, ZFMISC_1:74; then (X \ (seq1 . (k + 1))) /\ (X \ (union (rng seq))) = X \ (union (rng seq)) by XBOOLE_1:28, XBOOLE_1:34; then (A /\ (X \ (seq1 . (k + 1)))) /\ (X \ (union (rng seq))) = A /\ (X \ (union (rng seq))) by XBOOLE_1:16; then ((Ser (C * ((A /\ (X \ (seq1 . (k + 1)))) (/\) seq1))) . k) + (C . ((A /\ (X \ (seq1 . (k + 1)))) /\ (X \ (union (rng seq))))) >= ((Ser (C * (A (/\) seq1))) . k) + (C . (A /\ (X \ (union (rng seq))))) by A8, XXREAL_3:36; hence C . (A /\ (X \ (seq1 . (k + 1)))) >= ((Ser (C * (A (/\) seq1))) . k) + (C . (A /\ (X \ (union (rng seq))))) by A6, XXREAL_0:2; ::_thesis: verum end; let A be Subset of X; ::_thesis: C . A >= ((Ser (C * (A (/\) seq1))) . (k + 1)) + (C . (A /\ (X \ (union (rng seq))))) A /\ (X \ (seq1 . (k + 1))) = (A /\ X) \ (seq1 . (k + 1)) by XBOOLE_1:49 .= A \ (seq1 . (k + 1)) by XBOOLE_1:28 ; then A9: C . (A \ (seq1 . (k + 1))) >= ((Ser (C * (A (/\) seq1))) . k) + (C . (A /\ (X \ (union (rng seq))))) by A5; A10: A \ (seq1 . (k + 1)) c= X \ (seq1 . (k + 1)) by XBOOLE_1:33; A11: A \/ (A \ (seq1 . (k + 1))) = A by XBOOLE_1:12, XBOOLE_1:36; ( seq1 . (k + 1) in rng seq & A /\ (seq1 . (k + 1)) c= seq1 . (k + 1) ) by FUNCT_2:4, XBOOLE_1:17; then (C . (A /\ (seq1 . (k + 1)))) + (C . (A \ (seq1 . (k + 1)))) = C . ((A /\ (seq1 . (k + 1))) \/ (A \ (seq1 . (k + 1)))) by A1, A10, MEASURE4:5 .= C . ((A \/ (A \ (seq1 . (k + 1)))) /\ ((seq1 . (k + 1)) \/ (A \ (seq1 . (k + 1))))) by XBOOLE_1:24 .= C . ((A \/ (A \ (seq1 . (k + 1)))) /\ ((seq1 . (k + 1)) \/ A)) by XBOOLE_1:39 ; then (C . (A /\ (seq1 . (k + 1)))) + (C . (A \ (seq1 . (k + 1)))) = C . A by A11, XBOOLE_1:7, XBOOLE_1:28; then A12: C . A >= (((Ser (C * (A (/\) seq1))) . k) + (C . (A /\ (X \ (union (rng seq)))))) + (C . (A /\ (seq1 . (k + 1)))) by A9, XXREAL_3:36; A13: ((Ser (C * (A (/\) seq1))) . k) + (C . (A /\ (seq1 . (k + 1)))) = ((Ser (C * (A (/\) seq1))) . k) + (C . ((A (/\) seq1) . (k + 1))) by SETLIM_2:def_5 .= ((Ser (C * (A (/\) seq1))) . k) + ((C * (A (/\) seq1)) . (k + 1)) by FUNCT_2:15 .= (Ser (C * (A (/\) seq1))) . (k + 1) by SUPINF_2:44 ; A14: C is nonnegative by MEASURE4:def_1; then A15: C * (A (/\) seq1) is nonnegative by MEASURE1:25; then (C * (A (/\) seq1)) . k >= 0 by SUPINF_2:51; then A16: (Ser (C * (A (/\) seq1))) . k > -infty by A15, MEASURE7:2; ( C . (A /\ (X \ (union (rng seq)))) > -infty & C . (A /\ (seq1 . (k + 1))) > -infty ) by A14, SUPINF_2:51; hence C . A >= ((Ser (C * (A (/\) seq1))) . (k + 1)) + (C . (A /\ (X \ (union (rng seq))))) by A16, A12, A13, XXREAL_3:29; ::_thesis: verum end; A17: seq . 0 in sigma_Field C ; now__::_thesis:_for_A_being_Subset_of_X_holds_C_._A_>=_((Ser_(C_*_(A_(/\)_seq1)))_._0)_+_(C_._(A_/\_(X_\_(union_(rng_seq))))) let A be Subset of X; ::_thesis: C . A >= ((Ser (C * (A (/\) seq1))) . 0) + (C . (A /\ (X \ (union (rng seq))))) ( A /\ (seq1 . 0) c= seq1 . 0 & A /\ (X \ (seq1 . 0)) c= X \ (seq1 . 0) ) by XBOOLE_1:17; then A18: (C . (A /\ (seq1 . 0))) + (C . (A /\ (X \ (seq1 . 0)))) = C . ((A /\ (seq1 . 0)) \/ (A /\ (X \ (seq1 . 0)))) by A17, MEASURE4:5 .= C . ((A /\ (seq1 . 0)) \/ ((A /\ X) \ (seq1 . 0))) by XBOOLE_1:49 .= C . ((A /\ (seq1 . 0)) \/ (A \ (seq1 . 0))) by XBOOLE_1:28 .= C . A by XBOOLE_1:51 ; seq1 . 0 c= Union seq1 by ABCMIZ_1:1; then seq . 0 c= union (rng seq) by CARD_3:def_4; then X \ (union (rng seq)) c= X \ (seq . 0) by XBOOLE_1:34; then A /\ (X \ (union (rng seq))) c= A /\ (X \ (seq . 0)) by XBOOLE_1:26; then A19: C . (A /\ (X \ (union (rng seq)))) <= C . (A /\ (X \ (seq . 0))) by MEASURE4:def_1; (Ser (C * (A (/\) seq1))) . 0 = (C * (A (/\) seq1)) . 0 by SUPINF_2:44 .= C . ((A (/\) seq1) . 0) by FUNCT_2:15 .= C . (A /\ (seq1 . 0)) by SETLIM_2:def_5 ; hence C . A >= ((Ser (C * (A (/\) seq1))) . 0) + (C . (A /\ (X \ (union (rng seq))))) by A18, A19, XXREAL_3:36; ::_thesis: verum end; then A20: S1[ 0 ] ; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A20, A3); hence ((Ser (C * (A (/\) seq1))) . n) + (C . (A /\ (X \ (union (rng seq))))) <= C . A ; ::_thesis: verum end; A21: for A being Subset of X holds ( (SUM (C * (A (/\) seq1))) + (C . (A /\ (X \ (union (rng seq))))) <= C . A & C . (A /\ (Union seq1)) <= SUM (C * (A (/\) seq1)) ) proof let A be Subset of X; ::_thesis: ( (SUM (C * (A (/\) seq1))) + (C . (A /\ (X \ (union (rng seq))))) <= C . A & C . (A /\ (Union seq1)) <= SUM (C * (A (/\) seq1)) ) A22: C is nonnegative by MEASURE4:def_1; then A23: C * (A (/\) seq1) is nonnegative by MEASURE1:25; A24: C . (A /\ (X \ (union (rng seq)))) > -infty by A22, SUPINF_2:51; ( ( not C . A = +infty or not C . (A /\ (X \ (union (rng seq)))) = +infty ) implies (SUM (C * (A (/\) seq1))) + (C . (A /\ (X \ (union (rng seq))))) <= C . A ) proof assume A25: ( not C . A = +infty or not C . (A /\ (X \ (union (rng seq)))) = +infty ) ; ::_thesis: (SUM (C * (A (/\) seq1))) + (C . (A /\ (X \ (union (rng seq))))) <= C . A for x being ext-real number st x in rng (Ser (C * (A (/\) seq1))) holds x <= (C . A) - (C . (A /\ (X \ (union (rng seq))))) proof let x be ext-real number ; ::_thesis: ( x in rng (Ser (C * (A (/\) seq1))) implies x <= (C . A) - (C . (A /\ (X \ (union (rng seq))))) ) assume x in rng (Ser (C * (A (/\) seq1))) ; ::_thesis: x <= (C . A) - (C . (A /\ (X \ (union (rng seq))))) then consider i being set such that A26: i in NAT and A27: (Ser (C * (A (/\) seq1))) . i = x by FUNCT_2:11; reconsider i = i as Element of NAT by A26; (C * (A (/\) seq1)) . i >= 0 by A23, SUPINF_2:51; then A28: x > -infty by A23, A27, MEASURE7:2; ( C . (A /\ (X \ (union (rng seq)))) > -infty & ((Ser (C * (A (/\) seq1))) . i) + (C . (A /\ (X \ (union (rng seq))))) <= C . A ) by A2, A22, SUPINF_2:51; hence x <= (C . A) - (C . (A /\ (X \ (union (rng seq))))) by A25, A27, A28, XXREAL_3:56; ::_thesis: verum end; then (C . A) - (C . (A /\ (X \ (union (rng seq))))) is UpperBound of rng (Ser (C * (A (/\) seq1))) by XXREAL_2:def_1; then A29: SUM (C * (A (/\) seq1)) <= (C . A) - (C . (A /\ (X \ (union (rng seq))))) by XXREAL_2:def_3; SUM (C * (A (/\) seq1)) >= 0 by A23, MEASURE6:2; hence (SUM (C * (A (/\) seq1))) + (C . (A /\ (X \ (union (rng seq))))) <= C . A by A24, A29, XXREAL_3:55; ::_thesis: verum end; hence (SUM (C * (A (/\) seq1))) + (C . (A /\ (X \ (union (rng seq))))) <= C . A by XXREAL_0:3; ::_thesis: C . (A /\ (Union seq1)) <= SUM (C * (A (/\) seq1)) C . (union (rng (A (/\) seq1))) <= SUM (C * (A (/\) seq1)) by MEASURE4:def_1; then C . (Union (A (/\) seq1)) <= SUM (C * (A (/\) seq1)) by CARD_3:def_4; hence C . (A /\ (Union seq1)) <= SUM (C * (A (/\) seq1)) by SETLIM_2:38; ::_thesis: verum end; then A30: C . ((union (rng seq)) /\ (Union seq1)) <= SUM (C * ((union (rng seq)) (/\) seq1)) ; for W, Z being Subset of X st W c= Union seq1 & Z c= X \ (Union seq1) holds (C . W) + (C . Z) <= C . (W \/ Z) proof let W, Z be Subset of X; ::_thesis: ( W c= Union seq1 & Z c= X \ (Union seq1) implies (C . W) + (C . Z) <= C . (W \/ Z) ) assume that A31: W c= Union seq1 and A32: Z c= X \ (Union seq1) ; ::_thesis: (C . W) + (C . Z) <= C . (W \/ Z) set A = W \/ Z; A33: (W \/ Z) /\ (X \ (Union seq1)) = Z \/ (W /\ (X \ (Union seq1))) by A32, XBOOLE_1:30; X \ (Union seq1) misses Union seq1 by XBOOLE_1:79; then A34: (X \ (Union seq1)) /\ (Union seq1) = {} by XBOOLE_0:def_7; W /\ (X \ (Union seq1)) c= (Union seq1) /\ (X \ (Union seq1)) by A31, XBOOLE_1:26; then W /\ (X \ (Union seq1)) = {} by A34; then A35: C . Z = C . ((W \/ Z) /\ (X \ (union (rng seq)))) by A33, CARD_3:def_4; Z /\ (Union seq1) c= (X \ (Union seq1)) /\ (Union seq1) by A32, XBOOLE_1:26; then A36: Z /\ (Union seq1) = {} by A34; (W \/ Z) /\ (Union seq1) = W \/ (Z /\ (Union seq1)) by A31, XBOOLE_1:30; then C . W <= SUM (C * ((W \/ Z) (/\) seq1)) by A21, A36; then A37: (C . W) + (C . Z) <= (SUM (C * ((W \/ Z) (/\) seq1))) + (C . ((W \/ Z) /\ (X \ (union (rng seq))))) by A35, XXREAL_3:36; (SUM (C * ((W \/ Z) (/\) seq1))) + (C . ((W \/ Z) /\ (X \ (union (rng seq))))) <= C . (W \/ Z) by A21; hence (C . W) + (C . Z) <= C . (W \/ Z) by A37, XXREAL_0:2; ::_thesis: verum end; then Union seq1 in sigma_Field C by MEASURE4:def_2; hence union (rng seq) in sigma_Field C by CARD_3:def_4; ::_thesis: C . (union (rng seq)) = Sum (C * seq) set Sseq = Ser (C * seq1); union (rng seq) misses X \ (union (rng seq)) by XBOOLE_1:79; then A38: (union (rng seq)) /\ (X \ (union (rng seq))) = {} by XBOOLE_0:def_7; C is zeroed by MEASURE4:def_1; then A39: C . ((union (rng seq)) /\ (X \ (union (rng seq)))) = 0 by A38, VALUED_0:def_19; for n being set st n in NAT holds ((union (rng seq)) (/\) seq1) . n = seq . n proof let n be set ; ::_thesis: ( n in NAT implies ((union (rng seq)) (/\) seq1) . n = seq . n ) assume n in NAT ; ::_thesis: ((union (rng seq)) (/\) seq1) . n = seq . n then reconsider n1 = n as Element of NAT ; seq1 . n1 c= union (rng seq) by FUNCT_2:4, ZFMISC_1:74; then (union (rng seq)) /\ (seq1 . n1) = seq . n by XBOOLE_1:28; hence ((union (rng seq)) (/\) seq1) . n = seq . n by SETLIM_2:def_5; ::_thesis: verum end; then A40: SUM (C * ((union (rng seq)) (/\) seq1)) = sup (Ser (C * seq1)) by FUNCT_2:12; C is nonnegative by MEASURE4:def_1; then C * seq1 is nonnegative by MEASURE1:25; then for m, n being ext-real number st m in dom (Ser (C * seq1)) & n in dom (Ser (C * seq1)) & m <= n holds (Ser (C * seq1)) . m <= (Ser (C * seq1)) . n by MEASURE7:8; then Ser (C * seq1) is non-decreasing by VALUED_0:def_15; then SUM (C * ((union (rng seq)) (/\) seq1)) = lim (Ser (C * seq1)) by A40, RINFSUP2:37; then A41: SUM (C * ((union (rng seq)) (/\) seq1)) = lim (Partial_Sums (C * seq1)) by Th1; (SUM (C * ((union (rng seq)) (/\) seq1))) + (C . ((union (rng seq)) /\ (X \ (union (rng seq))))) <= C . (union (rng seq)) by A21; then ( union (rng seq) = Union seq1 & C . (union (rng seq)) >= Sum (C * seq) ) by A39, A41, CARD_3:def_4, XXREAL_3:4; hence C . (union (rng seq)) = Sum (C * seq) by A30, A41, XXREAL_0:1; ::_thesis: verum end; theorem :: MEASURE8:25 for X being set for C being C_Measure of X for seq being SetSequence of sigma_Field C holds Union seq in sigma_Field C proof let X be set ; ::_thesis: for C being C_Measure of X for seq being SetSequence of sigma_Field C holds Union seq in sigma_Field C let C be C_Measure of X; ::_thesis: for seq being SetSequence of sigma_Field C holds Union seq in sigma_Field C let seq be SetSequence of sigma_Field C; ::_thesis: Union seq in sigma_Field C set Aseq = Partial_Diff_Union seq; rng (Partial_Diff_Union seq) c= sigma_Field C by RELAT_1:def_19; then reconsider Aseq9 = Partial_Diff_Union seq as Function of NAT,(sigma_Field C) by FUNCT_2:6; reconsider Aseq9 = Aseq9 as Sep_Sequence of (sigma_Field C) ; union (rng Aseq9) in sigma_Field C by Th24; then Union (Partial_Diff_Union seq) in sigma_Field C by CARD_3:def_4; hence Union seq in sigma_Field C by PROB_3:36; ::_thesis: verum end; theorem Th26: :: MEASURE8:26 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for SSets being SetSequence of S st SSets is non-descending holds lim (M * SSets) = M . (lim SSets) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for SSets being SetSequence of S st SSets is non-descending holds lim (M * SSets) = M . (lim SSets) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for SSets being SetSequence of S st SSets is non-descending holds lim (M * SSets) = M . (lim SSets) let M be sigma_Measure of S; ::_thesis: for SSets being SetSequence of S st SSets is non-descending holds lim (M * SSets) = M . (lim SSets) let SSets be SetSequence of S; ::_thesis: ( SSets is non-descending implies lim (M * SSets) = M . (lim SSets) ) assume A1: SSets is non-descending ; ::_thesis: lim (M * SSets) = M . (lim SSets) then A2: Partial_Union SSets = SSets by PROB_4:19; rng (Partial_Diff_Union SSets) c= S ; then reconsider Bseq = Partial_Diff_Union SSets as Sep_Sequence of S by FUNCT_2:6; for n being set st n in NAT holds (Ser (M * Bseq)) . n = (M * (Partial_Union SSets)) . n proof defpred S1[ Nat] means (Ser (M * Bseq)) . $1 = (M * (Partial_Union SSets)) . $1; let n be set ; ::_thesis: ( n in NAT implies (Ser (M * Bseq)) . n = (M * (Partial_Union SSets)) . n ) A3: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A4: S1[k] ; ::_thesis: S1[k + 1] A5: ( (Partial_Union (Partial_Diff_Union SSets)) . k = (Partial_Union SSets) . k & (Partial_Diff_Union SSets) . (k + 1) = (SSets . (k + 1)) \ ((Partial_Union SSets) . k) ) by PROB_3:35, PROB_3:def_3; (Ser (M * Bseq)) . (k + 1) = ((Ser (M * Bseq)) . k) + ((M * Bseq) . (k + 1)) by SUPINF_2:44 .= ((M * (Partial_Union SSets)) . k) + (M . ((Partial_Diff_Union SSets) . (k + 1))) by A4, FUNCT_2:15 .= (M . ((Partial_Union SSets) . k)) + (M . ((Partial_Diff_Union SSets) . (k + 1))) by FUNCT_2:15 .= (M . ((Partial_Union (Partial_Diff_Union SSets)) . k)) + (M . ((Partial_Diff_Union SSets) . (k + 1))) by PROB_3:35 ; then (Ser (M * Bseq)) . (k + 1) = M . (((Partial_Union (Partial_Diff_Union SSets)) . k) \/ ((Partial_Diff_Union SSets) . (k + 1))) by A5, MEASURE1:30, XBOOLE_1:79 .= M . ((Partial_Union (Partial_Diff_Union SSets)) . (k + 1)) by PROB_3:def_2 .= M . ((Partial_Union SSets) . (k + 1)) by PROB_3:35 ; hence (Ser (M * Bseq)) . (k + 1) = (M * (Partial_Union SSets)) . (k + 1) by FUNCT_2:15; ::_thesis: verum end; assume n in NAT ; ::_thesis: (Ser (M * Bseq)) . n = (M * (Partial_Union SSets)) . n then reconsider n1 = n as Element of NAT ; (Ser (M * Bseq)) . 0 = (M * Bseq) . 0 by SUPINF_2:44 .= M . ((Partial_Diff_Union SSets) . 0) by FUNCT_2:15 .= M . (SSets . 0) by PROB_3:31 .= M . ((Partial_Union SSets) . 0) by PROB_3:22 ; then A6: S1[ 0 ] by FUNCT_2:15; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A6, A3); then (Ser (M * Bseq)) . n1 = (M * (Partial_Union SSets)) . n1 ; hence (Ser (M * Bseq)) . n = (M * (Partial_Union SSets)) . n ; ::_thesis: verum end; then A7: Ser (M * Bseq) = M * SSets by A2, FUNCT_2:12; reconsider Gseq = Ser (M * Bseq) as ExtREAL_sequence ; M * Bseq is nonnegative by MEASURE1:25; then for m, n being ext-real number st m in dom Gseq & n in dom Gseq & m <= n holds Gseq . m <= Gseq . n by MEASURE7:8; then Gseq is non-decreasing by VALUED_0:def_15; then A8: ( SUM (M * Bseq) = M . (union (rng Bseq)) & lim Gseq = sup Gseq ) by MEASURE1:def_6, RINFSUP2:37; Partial_Union (Partial_Diff_Union SSets) = SSets by A2, PROB_3:35; then Union SSets = Union (Partial_Diff_Union SSets) by PROB_3:30; then lim Gseq = M . (Union SSets) by A8, CARD_3:def_4; hence lim (M * SSets) = M . (lim SSets) by A1, A7, SETLIM_1:63; ::_thesis: verum end; theorem :: MEASURE8:27 for X being set for F being Field_Subset of X for M being Measure of F for FSets being Set_Sequence of F st FSets is non-descending holds M * FSets is non-decreasing proof let X be set ; ::_thesis: for F being Field_Subset of X for M being Measure of F for FSets being Set_Sequence of F st FSets is non-descending holds M * FSets is non-decreasing let F be Field_Subset of X; ::_thesis: for M being Measure of F for FSets being Set_Sequence of F st FSets is non-descending holds M * FSets is non-decreasing let M be Measure of F; ::_thesis: for FSets being Set_Sequence of F st FSets is non-descending holds M * FSets is non-decreasing let FSets be Set_Sequence of F; ::_thesis: ( FSets is non-descending implies M * FSets is non-decreasing ) A1: dom (M * FSets) = NAT by FUNCT_2:def_1; assume A2: FSets is non-descending ; ::_thesis: M * FSets is non-decreasing now__::_thesis:_for_n,_m_being_Element_of_NAT_st_n_<=_m_holds_ (M_*_FSets)_._n_<=_(M_*_FSets)_._m let n, m be Element of NAT ; ::_thesis: ( n <= m implies (M * FSets) . n <= (M * FSets) . m ) assume n <= m ; ::_thesis: (M * FSets) . n <= (M * FSets) . m then A3: FSets . n c= FSets . m by A2, PROB_1:def_5; ( (M * FSets) . n = M . (FSets . n) & (M * FSets) . m = M . (FSets . m) ) by A1, FUNCT_1:12; hence (M * FSets) . n <= (M * FSets) . m by A3, MEASURE1:8; ::_thesis: verum end; then for n, m being Element of NAT st m <= n holds (M * FSets) . m <= (M * FSets) . n ; hence M * FSets is non-decreasing by RINFSUP2:7; ::_thesis: verum end; theorem :: MEASURE8:28 for X being set for F being Field_Subset of X for M being Measure of F for FSets being Set_Sequence of F st FSets is non-ascending holds M * FSets is non-increasing proof let X be set ; ::_thesis: for F being Field_Subset of X for M being Measure of F for FSets being Set_Sequence of F st FSets is non-ascending holds M * FSets is non-increasing let F be Field_Subset of X; ::_thesis: for M being Measure of F for FSets being Set_Sequence of F st FSets is non-ascending holds M * FSets is non-increasing let M be Measure of F; ::_thesis: for FSets being Set_Sequence of F st FSets is non-ascending holds M * FSets is non-increasing let FSets be Set_Sequence of F; ::_thesis: ( FSets is non-ascending implies M * FSets is non-increasing ) A1: dom (M * FSets) = NAT by FUNCT_2:def_1; assume A2: FSets is non-ascending ; ::_thesis: M * FSets is non-increasing now__::_thesis:_for_n,_m_being_Element_of_NAT_st_m_<=_n_holds_ (M_*_FSets)_._n_<=_(M_*_FSets)_._m let n, m be Element of NAT ; ::_thesis: ( m <= n implies (M * FSets) . n <= (M * FSets) . m ) assume m <= n ; ::_thesis: (M * FSets) . n <= (M * FSets) . m then A3: FSets . n c= FSets . m by A2, PROB_1:def_4; ( (M * FSets) . n = M . (FSets . n) & (M * FSets) . m = M . (FSets . m) ) by A1, FUNCT_1:12; hence (M * FSets) . n <= (M * FSets) . m by A3, MEASURE1:8; ::_thesis: verum end; hence M * FSets is non-increasing by RINFSUP2:7; ::_thesis: verum end; theorem Th29: :: MEASURE8:29 for X being set for S being SigmaField of X for M being sigma_Measure of S for SSets being SetSequence of S st SSets is non-descending holds M * SSets is non-decreasing proof let X be set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for SSets being SetSequence of S st SSets is non-descending holds M * SSets is non-decreasing let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for SSets being SetSequence of S st SSets is non-descending holds M * SSets is non-decreasing let M be sigma_Measure of S; ::_thesis: for SSets being SetSequence of S st SSets is non-descending holds M * SSets is non-decreasing let SSets be SetSequence of S; ::_thesis: ( SSets is non-descending implies M * SSets is non-decreasing ) A1: dom (M * SSets) = NAT by FUNCT_2:def_1; assume A2: SSets is non-descending ; ::_thesis: M * SSets is non-decreasing now__::_thesis:_for_n,_m_being_Element_of_NAT_st_n_<=_m_holds_ (M_*_SSets)_._n_<=_(M_*_SSets)_._m let n, m be Element of NAT ; ::_thesis: ( n <= m implies (M * SSets) . n <= (M * SSets) . m ) A3: (M * SSets) . m = M . (SSets . m) by A1, FUNCT_1:12; assume n <= m ; ::_thesis: (M * SSets) . n <= (M * SSets) . m then A4: SSets . n c= SSets . m by A2, PROB_1:def_5; ( rng SSets c= S & (M * SSets) . n = M . (SSets . n) ) by A1, FUNCT_1:12; hence (M * SSets) . n <= (M * SSets) . m by A4, A3, MEASURE1:31; ::_thesis: verum end; then for n, m being Element of NAT st m <= n holds (M * SSets) . m <= (M * SSets) . n ; hence M * SSets is non-decreasing by RINFSUP2:7; ::_thesis: verum end; theorem Th30: :: MEASURE8:30 for X being set for S being SigmaField of X for M being sigma_Measure of S for SSets being SetSequence of S st SSets is non-ascending holds M * SSets is non-increasing proof let X be set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for SSets being SetSequence of S st SSets is non-ascending holds M * SSets is non-increasing let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for SSets being SetSequence of S st SSets is non-ascending holds M * SSets is non-increasing let M be sigma_Measure of S; ::_thesis: for SSets being SetSequence of S st SSets is non-ascending holds M * SSets is non-increasing let SSets be SetSequence of S; ::_thesis: ( SSets is non-ascending implies M * SSets is non-increasing ) A1: dom (M * SSets) = NAT by FUNCT_2:def_1; assume A2: SSets is non-ascending ; ::_thesis: M * SSets is non-increasing now__::_thesis:_for_n,_m_being_Element_of_NAT_st_m_<=_n_holds_ (M_*_SSets)_._n_<=_(M_*_SSets)_._m let n, m be Element of NAT ; ::_thesis: ( m <= n implies (M * SSets) . n <= (M * SSets) . m ) A3: (M * SSets) . m = M . (SSets . m) by A1, FUNCT_1:12; assume m <= n ; ::_thesis: (M * SSets) . n <= (M * SSets) . m then A4: SSets . n c= SSets . m by A2, PROB_1:def_4; ( rng SSets c= S & (M * SSets) . n = M . (SSets . n) ) by A1, FUNCT_1:12; hence (M * SSets) . n <= (M * SSets) . m by A4, A3, MEASURE1:31; ::_thesis: verum end; hence M * SSets is non-increasing by RINFSUP2:7; ::_thesis: verum end; theorem :: MEASURE8:31 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for SSets being SetSequence of S st SSets is non-ascending & M . (SSets . 0) < +infty holds lim (M * SSets) = M . (lim SSets) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for SSets being SetSequence of S st SSets is non-ascending & M . (SSets . 0) < +infty holds lim (M * SSets) = M . (lim SSets) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for SSets being SetSequence of S st SSets is non-ascending & M . (SSets . 0) < +infty holds lim (M * SSets) = M . (lim SSets) let M be sigma_Measure of S; ::_thesis: for SSets being SetSequence of S st SSets is non-ascending & M . (SSets . 0) < +infty holds lim (M * SSets) = M . (lim SSets) let SSets be SetSequence of S; ::_thesis: ( SSets is non-ascending & M . (SSets . 0) < +infty implies lim (M * SSets) = M . (lim SSets) ) assume that A1: SSets is non-ascending and A2: M . (SSets . 0) < +infty ; ::_thesis: lim (M * SSets) = M . (lim SSets) A3: M . ((SSets . 0) \ (lim SSets)) >= 0 by SUPINF_2:51; now__::_thesis:_for_y_being_set_st_y_in_rng_((SSets_._0)_(\)_SSets)_holds_ y_in_S let y be set ; ::_thesis: ( y in rng ((SSets . 0) (\) SSets) implies y in S ) assume y in rng ((SSets . 0) (\) SSets) ; ::_thesis: y in S then consider x being set such that A4: x in NAT and A5: ((SSets . 0) (\) SSets) . x = y by FUNCT_2:11; reconsider x = x as Element of NAT by A4; (SSets . 0) \ (SSets . x) in S ; hence y in S by A5, SETLIM_2:def_7; ::_thesis: verum end; then rng ((SSets . 0) (\) SSets) c= S by TARSKI:def_3; then reconsider Bseq = (SSets . 0) (\) SSets as SetSequence of S by RELAT_1:def_19; deffunc H1( Element of NAT ) -> Element of ExtREAL = (M * SSets) . 0; consider seq1 being Function of NAT,ExtREAL such that A6: for n being Element of NAT holds seq1 . n = H1(n) from FUNCT_2:sch_4(); A7: now__::_thesis:_for_k_being_Nat_holds_seq1_._k_=_((M_*_SSets)_._k)_+_((M_*_Bseq)_._k) let k be Nat; ::_thesis: seq1 . k = ((M * SSets) . k) + ((M * Bseq) . k) reconsider k1 = k as Element of NAT by ORDINAL1:def_12; A8: ( SSets . k1 in S & Bseq . k1 in S ) ; A9: k is Element of NAT by ORDINAL1:def_12; then ( (SSets . k) \/ ((SSets . 0) \ (SSets . k)) = (SSets . 0) \/ (SSets . k) & SSets . k c= SSets . 0 ) by A1, PROB_1:def_4, XBOOLE_1:39; then (SSets . k) \/ ((SSets . 0) \ (SSets . k)) = SSets . 0 by XBOOLE_1:12; then A10: (SSets . k) \/ (Bseq . k) = SSets . 0 by A9, SETLIM_2:def_7; SSets . k misses (SSets . 0) \ (SSets . k) by XBOOLE_1:79; then SSets . k misses Bseq . k by A9, SETLIM_2:def_7; then M . (SSets . 0) = (M . (SSets . k)) + (M . (Bseq . k)) by A10, A8, MEASURE1:30; then (M * SSets) . 0 = (M . (SSets . k)) + (M . (Bseq . k)) by FUNCT_2:15; then seq1 . k = (M . (SSets . k)) + (M . (Bseq . k)) by A6, A9; then seq1 . k = ((M * SSets) . k) + (M . (Bseq . k)) by A9, FUNCT_2:15; hence seq1 . k = ((M * SSets) . k) + ((M * Bseq) . k) by A9, FUNCT_2:15; ::_thesis: verum end; M * SSets is non-increasing by A1, Th30; then A11: M * SSets is convergent by RINFSUP2:36; rng Bseq c= S ; then Bseq is Function of NAT,S by FUNCT_2:6; then A12: M * Bseq is nonnegative by MEASURE2:1; A13: for n being Nat holds seq1 . n = (M * SSets) . 0 proof let n be Nat; ::_thesis: seq1 . n = (M * SSets) . 0 n is Element of NAT by ORDINAL1:def_12; hence seq1 . n = (M * SSets) . 0 by A6; ::_thesis: verum end; A14: rng SSets c= S ; then SSets is Function of NAT,S by FUNCT_2:6; then A15: M * SSets is nonnegative by MEASURE2:1; then A16: -infty < (M * SSets) . 0 by SUPINF_2:51; (inferior_setsequence SSets) . (0 + 1) c= SSets . 0 by A1, SETLIM_1:50; then Intersection SSets c= SSets . 0 by A1, SETLIM_1:52; then lim SSets c= SSets . 0 by A1, SETLIM_1:61; then A17: (SSets . 0) \/ (lim SSets) = SSets . 0 by XBOOLE_1:12; Intersection SSets in S by A14, PROB_1:def_6; then A18: lim SSets in S by A1, SETLIM_1:61; then A19: (SSets . 0) \ (lim SSets) is Element of S by PROB_1:6; then M . (((SSets . 0) \ (lim SSets)) \/ (lim SSets)) = (M . ((SSets . 0) \ (lim SSets))) + (M . (lim SSets)) by A18, MEASURE1:30, XBOOLE_1:79; then A20: M . ((SSets . 0) \/ (lim SSets)) = (M . ((SSets . 0) \ (lim SSets))) + (M . (lim SSets)) by XBOOLE_1:39; (M * SSets) . 0 < +infty by A2, FUNCT_2:15; then A21: (M * SSets) . 0 in REAL by A16, XXREAL_0:14; for n, m being Element of NAT st n <= m holds Bseq . n c= Bseq . m proof let n, m be Element of NAT ; ::_thesis: ( n <= m implies Bseq . n c= Bseq . m ) assume n <= m ; ::_thesis: Bseq . n c= Bseq . m then SSets . m c= SSets . n by A1, PROB_1:def_4; then (SSets . 0) \ (SSets . n) c= (SSets . 0) \ (SSets . m) by XBOOLE_1:34; then Bseq . n c= (SSets . 0) \ (SSets . m) by SETLIM_2:def_7; hence Bseq . n c= Bseq . m by SETLIM_2:def_7; ::_thesis: verum end; then A22: Bseq is non-descending by PROB_1:def_5; then M * Bseq is non-decreasing by Th29; then M * Bseq is convergent by RINFSUP2:37; then lim seq1 = (lim (M * Bseq)) + (lim (M * SSets)) by A11, A12, A15, A7, MESFUNC9:11; then A23: (M * SSets) . 0 = (lim (M * Bseq)) + (lim (M * SSets)) by A21, A13, MESFUNC5:52; lim (M * Bseq) = M . (lim Bseq) by A22, Th26 .= M . ((SSets . 0) \ (lim SSets)) by A1, SETLIM_1:64, SETLIM_2:86 ; then A24: (M . ((SSets . 0) \ (lim SSets))) + (M . (lim SSets)) = (lim (M * SSets)) + (M . ((SSets . 0) \ (lim SSets))) by A20, A17, A23, FUNCT_2:15; A25: M . ((SSets . 0) \ (lim SSets)) <= M . (SSets . 0) by A19, MEASURE1:31, XBOOLE_1:36; then M . ((SSets . 0) \ (lim SSets)) < +infty by A2, XXREAL_0:2; then A26: M . (lim SSets) = ((lim (M * SSets)) + (M . ((SSets . 0) \ (lim SSets)))) - (M . ((SSets . 0) \ (lim SSets))) by A3, A24, XXREAL_3:28; M . ((SSets . 0) \ (lim SSets)) is Real by A2, A25, A3, XXREAL_0:14; hence M . (lim SSets) = lim (M * SSets) by A26, XXREAL_3:22; ::_thesis: verum end; definition let X be set ; let F be Field_Subset of X; let S be SigmaField of X; let m be Measure of F; let M be sigma_Measure of S; predM is_extension_of m means :Def12: :: MEASURE8:def 12 for A being set st A in F holds M . A = m . A; end; :: deftheorem Def12 defines is_extension_of MEASURE8:def_12_:_ for X being set for F being Field_Subset of X for S being SigmaField of X for m being Measure of F for M being sigma_Measure of S holds ( M is_extension_of m iff for A being set st A in F holds M . A = m . A ); theorem :: MEASURE8:32 for X being non empty set for F being Field_Subset of X for m being Measure of F st ex M being sigma_Measure of (sigma F) st M is_extension_of m holds m is completely-additive proof let X be non empty set ; ::_thesis: for F being Field_Subset of X for m being Measure of F st ex M being sigma_Measure of (sigma F) st M is_extension_of m holds m is completely-additive let F be Field_Subset of X; ::_thesis: for m being Measure of F st ex M being sigma_Measure of (sigma F) st M is_extension_of m holds m is completely-additive let m be Measure of F; ::_thesis: ( ex M being sigma_Measure of (sigma F) st M is_extension_of m implies m is completely-additive ) given M being sigma_Measure of (sigma F) such that A1: M is_extension_of m ; ::_thesis: m is completely-additive A2: F c= sigma F by PROB_1:def_9; for Aseq being Sep_Sequence of F st union (rng Aseq) in F holds SUM (m * Aseq) = m . (union (rng Aseq)) proof let Aseq be Sep_Sequence of F; ::_thesis: ( union (rng Aseq) in F implies SUM (m * Aseq) = m . (union (rng Aseq)) ) reconsider Bseq = Aseq as Function of NAT,(sigma F) by A2, FUNCT_2:7; reconsider Bseq = Bseq as Sep_Sequence of (sigma F) ; A3: now__::_thesis:_for_n_being_set_st_n_in_NAT_holds_ (M_*_Bseq)_._n_=_(m_*_Aseq)_._n let n be set ; ::_thesis: ( n in NAT implies (M * Bseq) . n = (m * Aseq) . n ) assume n in NAT ; ::_thesis: (M * Bseq) . n = (m * Aseq) . n then reconsider n9 = n as Element of NAT ; (M * Bseq) . n = M . (Bseq . n9) by FUNCT_2:15; then (M * Bseq) . n = m . (Aseq . n9) by A1, Def12; hence (M * Bseq) . n = (m * Aseq) . n by FUNCT_2:15; ::_thesis: verum end; assume union (rng Aseq) in F ; ::_thesis: SUM (m * Aseq) = m . (union (rng Aseq)) then m . (union (rng Aseq)) = M . (union (rng Aseq)) by A1, Def12; then m . (union (rng Aseq)) = SUM (M * Bseq) by MEASURE1:def_6; hence SUM (m * Aseq) = m . (union (rng Aseq)) by A3, FUNCT_2:12; ::_thesis: verum end; hence m is completely-additive by Def11; ::_thesis: verum end; theorem Th33: :: MEASURE8:33 for X being non empty set for F being Field_Subset of X for m being Measure of F st m is completely-additive holds ex M being sigma_Measure of (sigma F) st ( M is_extension_of m & M = (sigma_Meas (C_Meas m)) | (sigma F) ) proof let X be non empty set ; ::_thesis: for F being Field_Subset of X for m being Measure of F st m is completely-additive holds ex M being sigma_Measure of (sigma F) st ( M is_extension_of m & M = (sigma_Meas (C_Meas m)) | (sigma F) ) let F be Field_Subset of X; ::_thesis: for m being Measure of F st m is completely-additive holds ex M being sigma_Measure of (sigma F) st ( M is_extension_of m & M = (sigma_Meas (C_Meas m)) | (sigma F) ) let m be Measure of F; ::_thesis: ( m is completely-additive implies ex M being sigma_Measure of (sigma F) st ( M is_extension_of m & M = (sigma_Meas (C_Meas m)) | (sigma F) ) ) assume A1: m is completely-additive ; ::_thesis: ex M being sigma_Measure of (sigma F) st ( M is_extension_of m & M = (sigma_Meas (C_Meas m)) | (sigma F) ) set M = (sigma_Meas (C_Meas m)) | (sigma F); A2: F c= sigma_Field (C_Meas m) by Th20; then A3: sigma F c= sigma_Field (C_Meas m) by PROB_1:def_9; then reconsider M = (sigma_Meas (C_Meas m)) | (sigma F) as Function of (sigma F),ExtREAL by FUNCT_2:32; A4: for SS being Sep_Sequence of (sigma F) holds SUM (M * SS) = M . (union (rng SS)) proof let SS be Sep_Sequence of (sigma F); ::_thesis: SUM (M * SS) = M . (union (rng SS)) reconsider SS9 = SS as Sep_Sequence of (sigma_Field (C_Meas m)) by A3, FUNCT_2:7; A5: rng SS c= sigma F by RELAT_1:def_19; M * SS = (sigma_Meas (C_Meas m)) * ((sigma F) |` SS) by MONOID_1:1 .= (sigma_Meas (C_Meas m)) * SS9 by A5, RELAT_1:94 ; then A6: SUM (M * SS) = (sigma_Meas (C_Meas m)) . (union (rng SS9)) by MEASURE1:def_6; union (rng SS) is Element of sigma F by MEASURE1:24; hence SUM (M * SS) = M . (union (rng SS)) by A6, FUNCT_1:49; ::_thesis: verum end; M . {} = (sigma_Meas (C_Meas m)) . {} by FUNCT_1:49, PROB_1:4 .= 0 by VALUED_0:def_19 ; then reconsider M = M as sigma_Measure of (sigma F) by A4, MEASURE1:def_6, MESFUNC5:15, VALUED_0:def_19; take M ; ::_thesis: ( M is_extension_of m & M = (sigma_Meas (C_Meas m)) | (sigma F) ) A7: F c= sigma F by PROB_1:def_9; for A being set st A in F holds M . A = m . A proof let A be set ; ::_thesis: ( A in F implies M . A = m . A ) assume A8: A in F ; ::_thesis: M . A = m . A then reconsider A9 = A as Subset of X ; M . A = (sigma_Meas (C_Meas m)) . A by A7, A8, FUNCT_1:49 .= (C_Meas m) . A9 by A2, A8, MEASURE4:def_3 ; hence M . A = m . A by A1, A8, Th18; ::_thesis: verum end; hence ( M is_extension_of m & M = (sigma_Meas (C_Meas m)) | (sigma F) ) by Def12; ::_thesis: verum end; theorem Th34: :: MEASURE8:34 for X being set for F being Field_Subset of X for M being Measure of F for k being Nat for FSets being Set_Sequence of F st ( for n being Nat holds M . (FSets . n) < +infty ) holds M . ((Partial_Union FSets) . k) < +infty proof let X be set ; ::_thesis: for F being Field_Subset of X for M being Measure of F for k being Nat for FSets being Set_Sequence of F st ( for n being Nat holds M . (FSets . n) < +infty ) holds M . ((Partial_Union FSets) . k) < +infty let F be Field_Subset of X; ::_thesis: for M being Measure of F for k being Nat for FSets being Set_Sequence of F st ( for n being Nat holds M . (FSets . n) < +infty ) holds M . ((Partial_Union FSets) . k) < +infty let M be Measure of F; ::_thesis: for k being Nat for FSets being Set_Sequence of F st ( for n being Nat holds M . (FSets . n) < +infty ) holds M . ((Partial_Union FSets) . k) < +infty let k be Nat; ::_thesis: for FSets being Set_Sequence of F st ( for n being Nat holds M . (FSets . n) < +infty ) holds M . ((Partial_Union FSets) . k) < +infty let FSets be Set_Sequence of F; ::_thesis: ( ( for n being Nat holds M . (FSets . n) < +infty ) implies M . ((Partial_Union FSets) . k) < +infty ) defpred S1[ Nat] means M . ((Partial_Union FSets) . $1) < +infty ; assume A1: for n being Nat holds M . (FSets . n) < +infty ; ::_thesis: M . ((Partial_Union FSets) . k) < +infty A2: now__::_thesis:_for_k_being_Nat_st_S1[k]_holds_ S1[k_+_1] let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) A3: 0 <= M . ((Partial_Union FSets) . k) by SUPINF_2:51; ( M . (FSets . (k + 1)) < +infty & 0 <= M . (FSets . (k + 1)) ) by A1, SUPINF_2:51; then A4: M . (FSets . (k + 1)) in REAL by XXREAL_0:10; assume S1[k] ; ::_thesis: S1[k + 1] then M . ((Partial_Union FSets) . k) in REAL by A3, XXREAL_0:10; then A5: (M . ((Partial_Union FSets) . k)) + (M . (FSets . (k + 1))) in REAL by A4, XREAL_0:def_1; Partial_Union FSets is Set_Sequence of F by Th15; then A6: (Partial_Union FSets) . k in F by Def2; (Partial_Union FSets) . (k + 1) = ((Partial_Union FSets) . k) \/ (FSets . (k + 1)) by PROB_3:def_2; then M . ((Partial_Union FSets) . (k + 1)) <= (M . ((Partial_Union FSets) . k)) + (M . (FSets . (k + 1))) by A6, MEASURE1:10; hence S1[k + 1] by A5, XXREAL_0:9, XXREAL_0:13; ::_thesis: verum end; (Partial_Union FSets) . 0 = FSets . 0 by PROB_3:def_2; then A7: S1[ 0 ] by A1; for k being Nat holds S1[k] from NAT_1:sch_2(A7, A2); hence M . ((Partial_Union FSets) . k) < +infty ; ::_thesis: verum end; theorem :: MEASURE8:35 for X being non empty set for F being Field_Subset of X for m being Measure of F st m is completely-additive & ex Aseq being Set_Sequence of F st ( ( for n being Nat holds m . (Aseq . n) < +infty ) & X = union (rng Aseq) ) holds for M being sigma_Measure of (sigma F) st M is_extension_of m holds M = (sigma_Meas (C_Meas m)) | (sigma F) proof let X be non empty set ; ::_thesis: for F being Field_Subset of X for m being Measure of F st m is completely-additive & ex Aseq being Set_Sequence of F st ( ( for n being Nat holds m . (Aseq . n) < +infty ) & X = union (rng Aseq) ) holds for M being sigma_Measure of (sigma F) st M is_extension_of m holds M = (sigma_Meas (C_Meas m)) | (sigma F) let F be Field_Subset of X; ::_thesis: for m being Measure of F st m is completely-additive & ex Aseq being Set_Sequence of F st ( ( for n being Nat holds m . (Aseq . n) < +infty ) & X = union (rng Aseq) ) holds for M being sigma_Measure of (sigma F) st M is_extension_of m holds M = (sigma_Meas (C_Meas m)) | (sigma F) let m be Measure of F; ::_thesis: ( m is completely-additive & ex Aseq being Set_Sequence of F st ( ( for n being Nat holds m . (Aseq . n) < +infty ) & X = union (rng Aseq) ) implies for M being sigma_Measure of (sigma F) st M is_extension_of m holds M = (sigma_Meas (C_Meas m)) | (sigma F) ) A1: F c= sigma F by PROB_1:def_9; assume m is completely-additive ; ::_thesis: ( for Aseq being Set_Sequence of F holds ( ex n being Nat st not m . (Aseq . n) < +infty or not X = union (rng Aseq) ) or for M being sigma_Measure of (sigma F) st M is_extension_of m holds M = (sigma_Meas (C_Meas m)) | (sigma F) ) then consider M1 being sigma_Measure of (sigma F) such that A2: M1 is_extension_of m and A3: M1 = (sigma_Meas (C_Meas m)) | (sigma F) by Th33; assume ex Aseq being Set_Sequence of F st ( ( for n being Nat holds m . (Aseq . n) < +infty ) & X = union (rng Aseq) ) ; ::_thesis: for M being sigma_Measure of (sigma F) st M is_extension_of m holds M = (sigma_Meas (C_Meas m)) | (sigma F) then consider Aseq being Set_Sequence of F such that A4: for n being Nat holds m . (Aseq . n) < +infty and A5: X = union (rng Aseq) ; let M be sigma_Measure of (sigma F); ::_thesis: ( M is_extension_of m implies M = (sigma_Meas (C_Meas m)) | (sigma F) ) reconsider Bseq = Partial_Union Aseq as Set_Sequence of F by Th15; assume A6: M is_extension_of m ; ::_thesis: M = (sigma_Meas (C_Meas m)) | (sigma F) F c= sigma_Field (C_Meas m) by Th20; then A7: sigma F c= sigma_Field (C_Meas m) by PROB_1:def_9; A8: for B being Subset of X st B in sigma F holds M . B <= M1 . B proof let B be Subset of X; ::_thesis: ( B in sigma F implies M . B <= M1 . B ) assume A9: B in sigma F ; ::_thesis: M . B <= M1 . B A10: for seq being Covering of B,F holds M . B <= SUM (vol (m,seq)) proof let seq be Covering of B,F; ::_thesis: M . B <= SUM (vol (m,seq)) A11: now__::_thesis:_for_n_being_Element_of_NAT_holds_seq_._n_in_sigma_F let n be Element of NAT ; ::_thesis: seq . n in sigma F seq . n in F ; hence seq . n in sigma F by A1; ::_thesis: verum end; now__::_thesis:_for_y_being_set_st_y_in_rng_seq_holds_ y_in_sigma_F let y be set ; ::_thesis: ( y in rng seq implies y in sigma F ) assume y in rng seq ; ::_thesis: y in sigma F then consider x being set such that A12: x in NAT and A13: seq . x = y by FUNCT_2:11; thus y in sigma F by A11, A12, A13; ::_thesis: verum end; then rng seq c= sigma F by TARSKI:def_3; then reconsider seq1 = seq as SetSequence of sigma F by RELAT_1:def_19; A16: rng seq1 c= sigma F ; then reconsider Fseq = seq1 as Function of NAT,(sigma F) by FUNCT_2:6; B c= union (rng seq1) by Def3; then ( Union seq1 in sigma F & B c= Union seq1 ) by CARD_3:def_4, PROB_1:17; then A17: M . B <= M . (Union seq1) by A9, MEASURE1:31; for n being set st n in NAT holds (M * Fseq) . n = (vol (m,seq)) . n proof let n be set ; ::_thesis: ( n in NAT implies (M * Fseq) . n = (vol (m,seq)) . n ) assume A18: n in NAT ; ::_thesis: (M * Fseq) . n = (vol (m,seq)) . n then reconsider n1 = n as Element of NAT ; n1 in dom Fseq by A18, FUNCT_2:def_1; then (M * Fseq) . n = M . (Fseq . n1) by FUNCT_1:13 .= m . (seq . n1) by A6, Def12 ; hence (M * Fseq) . n = (vol (m,seq)) . n by Def5; ::_thesis: verum end; then A19: SUM (M * Fseq) = SUM (vol (m,seq)) by FUNCT_2:12; rng Fseq is N_Sub_set_fam of X by MEASURE1:23; then rng Fseq is N_Measure_fam of sigma F by A16, MEASURE2:def_1; then M . (union (rng Fseq)) <= SUM (M * Fseq) by MEASURE2:11; then M . (Union seq1) <= SUM (vol (m,seq)) by A19, CARD_3:def_4; hence M . B <= SUM (vol (m,seq)) by A17, XXREAL_0:2; ::_thesis: verum end; for r being ext-real number st r in Svc (m,B) holds M . B <= r proof let r be ext-real number ; ::_thesis: ( r in Svc (m,B) implies M . B <= r ) assume r in Svc (m,B) ; ::_thesis: M . B <= r then ex seq being Covering of B,F st r = SUM (vol (m,seq)) by Def7; hence M . B <= r by A10; ::_thesis: verum end; then M . B is LowerBound of Svc (m,B) by XXREAL_2:def_2; then M . B <= inf (Svc (m,B)) by XXREAL_2:def_4; then M . B <= (C_Meas m) . B by Def8; then M . B <= (sigma_Meas (C_Meas m)) . B by A7, A9, MEASURE4:def_3; hence M . B <= M1 . B by A3, A9, FUNCT_1:49; ::_thesis: verum end; A20: for B being set st ex k being Element of NAT st B c= Bseq . k & B in sigma F holds M . B = M1 . B proof let B be set ; ::_thesis: ( ex k being Element of NAT st B c= Bseq . k & B in sigma F implies M . B = M1 . B ) assume ex k being Element of NAT st B c= Bseq . k ; ::_thesis: ( not B in sigma F or M . B = M1 . B ) then consider k being Element of NAT such that A21: B c= Bseq . k ; A22: M . (Bseq . k) = m . (Bseq . k) by A6, Def12; assume A23: B in sigma F ; ::_thesis: M . B = M1 . B then reconsider B9 = B as Subset of X ; A24: ( F c= sigma F & Bseq . k in F ) by PROB_1:def_9; then A25: (Bseq . k) \ B is Element of sigma F by A23, PROB_1:6; then M . ((Bseq . k) \ B) <= M . (Bseq . k) by A24, MEASURE1:31, XBOOLE_1:36; then A26: M . ((Bseq . k) \ B) < +infty by A4, A22, Th34, XXREAL_0:2; (M . B) + (M . ((Bseq . k) \ B)) = M . (B \/ ((Bseq . k) \ B)) by A23, A25, MEASURE1:30, XBOOLE_1:79; then (M . B) + (M . ((Bseq . k) \ B)) = M . ((Bseq . k) \/ B) by XBOOLE_1:39; then A27: (M . B) + (M . ((Bseq . k) \ B)) = M . (Bseq . k) by A21, XBOOLE_1:12; 0 <= M . ((Bseq . k) \ B) by SUPINF_2:51; then A28: M . B = (M . (Bseq . k)) - (M . ((Bseq . k) \ B)) by A27, A26, XXREAL_3:28; A29: M1 . (Bseq . k) = m . (Bseq . k) by A2, Def12; (M1 . B) + (M1 . ((Bseq . k) \ B)) = M1 . (B \/ ((Bseq . k) \ B)) by A23, A25, MEASURE1:30, XBOOLE_1:79; then (M1 . B) + (M1 . ((Bseq . k) \ B)) = M1 . ((Bseq . k) \/ B) by XBOOLE_1:39; then A30: (M1 . B) + (M1 . ((Bseq . k) \ B)) = M1 . (Bseq . k) by A21, XBOOLE_1:12; M1 . ((Bseq . k) \ B) <= M1 . (Bseq . k) by A24, A25, MEASURE1:31, XBOOLE_1:36; then A31: M1 . ((Bseq . k) \ B) < +infty by A4, A29, Th34, XXREAL_0:2; 0 <= M1 . ((Bseq . k) \ B) by SUPINF_2:51; then A32: M1 . B = (M1 . (Bseq . k)) - (M1 . ((Bseq . k) \ B)) by A30, A31, XXREAL_3:28; M . ((Bseq . k) \ B) <= M1 . ((Bseq . k) \ B) by A8, A23, A24, PROB_1:6; then A33: (M1 . (Bseq . k)) - (M1 . ((Bseq . k) \ B)) <= (M . (Bseq . k)) - (M . ((Bseq . k) \ B)) by A29, A22, XXREAL_3:37; M . B9 <= M1 . B9 by A8, A23; hence M . B = M1 . B by A28, A32, A33, XXREAL_0:1; ::_thesis: verum end; for B being set st B in sigma F holds M . B = M1 . B proof let B be set ; ::_thesis: ( B in sigma F implies M . B = M1 . B ) deffunc H1( set ) -> set = B /\ (Bseq . $1); assume A34: B in sigma F ; ::_thesis: M . B = M1 . B then reconsider B9 = B as Subset of X ; A35: for n being set st n in NAT holds H1(n) in bool X proof let n be set ; ::_thesis: ( n in NAT implies H1(n) in bool X ) assume n in NAT ; ::_thesis: H1(n) in bool X then Bseq . n in F by Def2; then (Bseq . n) /\ B c= X /\ X by A34, XBOOLE_1:27; hence H1(n) in bool X ; ::_thesis: verum end; consider Cseq being Function of NAT,(bool X) such that A36: for n being set st n in NAT holds Cseq . n = H1(n) from FUNCT_2:sch_2(A35); reconsider Cseq = Cseq as SetSequence of X ; for n, m being Element of NAT st n <= m holds Cseq . n c= Cseq . m proof let n, m be Element of NAT ; ::_thesis: ( n <= m implies Cseq . n c= Cseq . m ) A37: Bseq is non-descending by PROB_3:11; assume n <= m ; ::_thesis: Cseq . n c= Cseq . m then Bseq . n c= Bseq . m by A37, PROB_1:def_5; then B /\ (Bseq . n) c= B /\ (Bseq . m) by XBOOLE_1:26; then Cseq . n c= B /\ (Bseq . m) by A36; hence Cseq . n c= Cseq . m by A36; ::_thesis: verum end; then A38: Cseq is non-descending by PROB_1:def_5; now__::_thesis:_for_y_being_set_st_y_in_rng_Cseq_holds_ y_in_sigma_F let y be set ; ::_thesis: ( y in rng Cseq implies y in sigma F ) assume y in rng Cseq ; ::_thesis: y in sigma F then consider x being set such that A39: x in NAT and A40: Cseq . x = y by FUNCT_2:11; reconsider x = x as Element of NAT by A39; Bseq . x in F ; then (Bseq . x) /\ B in sigma F by A1, A34, MEASURE1:34; hence y in sigma F by A36, A40; ::_thesis: verum end; then rng Cseq c= sigma F by TARSKI:def_3; then reconsider Cseq = Cseq as SetSequence of sigma F by RELAT_1:def_19; for n being set st n in NAT holds (M1 * (Partial_Union Cseq)) . n = (M * (Partial_Union Cseq)) . n proof let n be set ; ::_thesis: ( n in NAT implies (M1 * (Partial_Union Cseq)) . n = (M * (Partial_Union Cseq)) . n ) assume n in NAT ; ::_thesis: (M1 * (Partial_Union Cseq)) . n = (M * (Partial_Union Cseq)) . n then reconsider n1 = n as Element of NAT ; A41: now__::_thesis:_for_x_being_set_st_x_in_(Partial_Union_Cseq)_._n1_holds_ ex_k_being_Element_of_NAT_st_ (_k_<=_n1_&_x_in_Bseq_._k_) let x be set ; ::_thesis: ( x in (Partial_Union Cseq) . n1 implies ex k being Element of NAT st ( k <= n1 & x in Bseq . k ) ) assume x in (Partial_Union Cseq) . n1 ; ::_thesis: ex k being Element of NAT st ( k <= n1 & x in Bseq . k ) then consider k being Nat such that A42: k <= n1 and A43: x in Cseq . k by PROB_3:13; reconsider k = k as Element of NAT by ORDINAL1:def_12; take k = k; ::_thesis: ( k <= n1 & x in Bseq . k ) x in B /\ (Bseq . k) by A36, A43; hence ( k <= n1 & x in Bseq . k ) by A42, XBOOLE_0:def_4; ::_thesis: verum end; A44: (Partial_Union Cseq) . n1 c= Bseq . n1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Partial_Union Cseq) . n1 or x in Bseq . n1 ) assume x in (Partial_Union Cseq) . n1 ; ::_thesis: x in Bseq . n1 then consider k being Element of NAT such that A45: k <= n1 and A46: x in Bseq . k by A41; Bseq is non-descending by PROB_3:11; then Bseq . k c= Bseq . n1 by A45, PROB_1:def_5; hence x in Bseq . n1 by A46; ::_thesis: verum end; A47: (M1 * (Partial_Union Cseq)) . n = M1 . ((Partial_Union Cseq) . n1) by FUNCT_2:15; A48: rng (Partial_Union Cseq) c= sigma F by RELAT_1:def_19; dom (Partial_Union Cseq) = NAT by PARTFUN1:def_2; then (Partial_Union Cseq) . n1 in rng (Partial_Union Cseq) by FUNCT_1:3; then (M1 * (Partial_Union Cseq)) . n = M . ((Partial_Union Cseq) . n1) by A47, A20, A44, A48; hence (M1 * (Partial_Union Cseq)) . n = (M * (Partial_Union Cseq)) . n by FUNCT_2:15; ::_thesis: verum end; then A49: M1 * (Partial_Union Cseq) = M * (Partial_Union Cseq) by FUNCT_2:12; for n being Element of NAT holds Cseq . n = B9 /\ (Bseq . n) by A36; then Cseq = B9 (/\) Bseq by SETLIM_2:def_5; then Union Cseq = B9 /\ (Union Bseq) by SETLIM_2:38; then Union Cseq = B9 /\ (Union Aseq) by PROB_3:15; then Union Cseq = B9 /\ X by A5, CARD_3:def_4; then A50: B9 = Union Cseq by XBOOLE_1:28; then B9 = lim Cseq by A38, SETLIM_1:63; then M1 . B = lim (M1 * Cseq) by A38, Th26; then M1 . B = lim (M * (Partial_Union Cseq)) by A38, A49, PROB_4:19; then M1 . B = lim (M * Cseq) by A38, PROB_4:19; then M1 . B = M . (lim Cseq) by A38, Th26; hence M1 . B = M . B by A38, A50, SETLIM_1:63; ::_thesis: verum end; hence M = (sigma_Meas (C_Meas m)) | (sigma F) by A3, FUNCT_2:12; ::_thesis: verum end;