:: MEASURE3 semantic presentation begin theorem Th1: :: MEASURE3:1 for F1, F2 being Function of NAT,ExtREAL st ( for n being Element of NAT holds (Ser F1) . n <= (Ser F2) . n ) holds SUM F1 <= SUM F2 proof let F1, F2 be Function of NAT,ExtREAL; ::_thesis: ( ( for n being Element of NAT holds (Ser F1) . n <= (Ser F2) . n ) implies SUM F1 <= SUM F2 ) assume A1: for n being Element of NAT holds (Ser F1) . n <= (Ser F2) . n ; ::_thesis: SUM F1 <= SUM F2 A2: for x being ext-real number st x in rng (Ser F1) holds ex y being ext-real number st ( y in rng (Ser F2) & x <= y ) proof let x be ext-real number ; ::_thesis: ( x in rng (Ser F1) implies ex y being ext-real number st ( y in rng (Ser F2) & x <= y ) ) A3: dom (Ser F1) = NAT by FUNCT_2:def_1; assume x in rng (Ser F1) ; ::_thesis: ex y being ext-real number st ( y in rng (Ser F2) & x <= y ) then consider n being set such that A4: n in NAT and A5: x = (Ser F1) . n by A3, FUNCT_1:def_3; reconsider n = n as Element of NAT by A4; reconsider y = (Ser F2) . n as R_eal ; take y ; ::_thesis: ( y in rng (Ser F2) & x <= y ) dom (Ser F2) = NAT by FUNCT_2:def_1; hence ( y in rng (Ser F2) & x <= y ) by A1, A5, FUNCT_1:def_3; ::_thesis: verum end; ( SUM F1 = sup (rng (Ser F1)) & SUM F2 = sup (rng (Ser F2)) ) by SUPINF_2:def_17; hence SUM F1 <= SUM F2 by A2, XXREAL_2:63; ::_thesis: verum end; theorem :: MEASURE3:2 for F1, F2 being Function of NAT,ExtREAL st ( for n being Element of NAT holds (Ser F1) . n = (Ser F2) . n ) holds SUM F1 = SUM F2 proof let F1, F2 be Function of NAT,ExtREAL; ::_thesis: ( ( for n being Element of NAT holds (Ser F1) . n = (Ser F2) . n ) implies SUM F1 = SUM F2 ) assume A1: for n being Element of NAT holds (Ser F1) . n = (Ser F2) . n ; ::_thesis: SUM F1 = SUM F2 then for n being Element of NAT holds (Ser F2) . n <= (Ser F1) . n ; then A2: SUM F2 <= SUM F1 by Th1; for n being Element of NAT holds (Ser F1) . n <= (Ser F2) . n by A1; then SUM F1 <= SUM F2 by Th1; hence SUM F1 = SUM F2 by A2, XXREAL_0:1; ::_thesis: verum end; notation let X be set ; let S be SigmaField of X; synonym N_Sub_fam of S for N_Measure_fam of S; end; definition let X be set ; let S be SigmaField of X; let F be Function of NAT,S; :: original: rng redefine func rng F -> N_Measure_fam of S; coherence rng F is N_Measure_fam of S proof ( rng F is N_Sub_set_fam of X & rng F c= S ) by MEASURE1:23, RELAT_1:def_19; hence rng F is N_Measure_fam of S by MEASURE2:def_1; ::_thesis: verum end; end; theorem :: MEASURE3:3 for X being set for S being SigmaField of X for M being sigma_Measure of S for F being Function of NAT,S for A being Element of S st meet (rng F) c= A & ( for n being Element of NAT holds A c= F . n ) holds M . A = M . (meet (rng F)) proof let X be set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for F being Function of NAT,S for A being Element of S st meet (rng F) c= A & ( for n being Element of NAT holds A c= F . n ) holds M . A = M . (meet (rng F)) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for F being Function of NAT,S for A being Element of S st meet (rng F) c= A & ( for n being Element of NAT holds A c= F . n ) holds M . A = M . (meet (rng F)) let M be sigma_Measure of S; ::_thesis: for F being Function of NAT,S for A being Element of S st meet (rng F) c= A & ( for n being Element of NAT holds A c= F . n ) holds M . A = M . (meet (rng F)) let F be Function of NAT,S; ::_thesis: for A being Element of S st meet (rng F) c= A & ( for n being Element of NAT holds A c= F . n ) holds M . A = M . (meet (rng F)) let A be Element of S; ::_thesis: ( meet (rng F) c= A & ( for n being Element of NAT holds A c= F . n ) implies M . A = M . (meet (rng F)) ) assume that A1: meet (rng F) c= A and A2: for n being Element of NAT holds A c= F . n ; ::_thesis: M . A = M . (meet (rng F)) A c= meet (rng F) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in meet (rng F) ) assume A3: x in A ; ::_thesis: x in meet (rng F) for Y being set st Y in rng F holds x in Y proof let Y be set ; ::_thesis: ( Y in rng F implies x in Y ) A4: dom F = NAT by FUNCT_2:def_1; assume Y in rng F ; ::_thesis: x in Y then ex n being set st ( n in NAT & Y = F . n ) by A4, FUNCT_1:def_3; then A c= Y by A2; hence x in Y by A3; ::_thesis: verum end; hence x in meet (rng F) by SETFAM_1:def_1; ::_thesis: verum end; then A5: M . A <= M . (meet (rng F)) by MEASURE1:31; M . (meet (rng F)) <= M . A by A1, MEASURE1:31; hence M . A = M . (meet (rng F)) by A5, XXREAL_0:1; ::_thesis: verum end; theorem Th4: :: MEASURE3:4 for X being set for S being SigmaField of X for G, F being Function of NAT,S st G . 0 = {} & ( for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds union (rng G) = (F . 0) \ (meet (rng F)) proof let X be set ; ::_thesis: for S being SigmaField of X for G, F being Function of NAT,S st G . 0 = {} & ( for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds union (rng G) = (F . 0) \ (meet (rng F)) let S be SigmaField of X; ::_thesis: for G, F being Function of NAT,S st G . 0 = {} & ( for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds union (rng G) = (F . 0) \ (meet (rng F)) let G, F be Function of NAT,S; ::_thesis: ( G . 0 = {} & ( for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) implies union (rng G) = (F . 0) \ (meet (rng F)) ) assume that A1: G . 0 = {} and A2: for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ; ::_thesis: union (rng G) = (F . 0) \ (meet (rng F)) A3: dom G = NAT by FUNCT_2:def_1; thus union (rng G) c= (F . 0) \ (meet (rng F)) :: according to XBOOLE_0:def_10 ::_thesis: (F . 0) \ (meet (rng F)) c= union (rng G) proof let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in union (rng G) or A in (F . 0) \ (meet (rng F)) ) assume A in union (rng G) ; ::_thesis: A in (F . 0) \ (meet (rng F)) then consider Z being set such that A4: A in Z and A5: Z in rng G by TARSKI:def_4; consider n being set such that A6: n in NAT and A7: Z = G . n by A3, A5, FUNCT_1:def_3; reconsider n = n as Element of NAT by A6; consider k being Nat such that A8: n = k + 1 by A1, A4, A7, NAT_1:6; reconsider k = k as Element of NAT by ORDINAL1:def_12; set Y = F . k; A9: A in (F . 0) \ (F . k) by A2, A4, A7, A8; then ( F . k in rng F & not A in F . k ) by FUNCT_2:4, XBOOLE_0:def_5; then A10: not A in meet (rng F) by SETFAM_1:def_1; A in F . 0 by A9, XBOOLE_0:def_5; hence A in (F . 0) \ (meet (rng F)) by A10, XBOOLE_0:def_5; ::_thesis: verum end; let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in (F . 0) \ (meet (rng F)) or A in union (rng G) ) assume A11: A in (F . 0) \ (meet (rng F)) ; ::_thesis: A in union (rng G) then not A in meet (rng F) by XBOOLE_0:def_5; then A12: ex Y being set st ( Y in rng F & not A in Y ) by SETFAM_1:def_1; A in F . 0 by A11, XBOOLE_0:def_5; then consider Y being set such that A13: A in F . 0 and A14: Y in rng F and A15: not A in Y by A12; dom F = NAT by FUNCT_2:def_1; then consider n being set such that A16: n in NAT and A17: Y = F . n by A14, FUNCT_1:def_3; reconsider n = n as Element of NAT by A16; A in (F . 0) \ (F . n) by A13, A15, A17, XBOOLE_0:def_5; then A18: A in G . (n + 1) by A2; G . (n + 1) in rng G by FUNCT_2:4; hence A in union (rng G) by A18, TARSKI:def_4; ::_thesis: verum end; theorem Th5: :: MEASURE3:5 for X being set for S being SigmaField of X for G, F being Function of NAT,S st G . 0 = {} & ( for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds meet (rng F) = (F . 0) \ (union (rng G)) proof let X be set ; ::_thesis: for S being SigmaField of X for G, F being Function of NAT,S st G . 0 = {} & ( for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds meet (rng F) = (F . 0) \ (union (rng G)) let S be SigmaField of X; ::_thesis: for G, F being Function of NAT,S st G . 0 = {} & ( for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds meet (rng F) = (F . 0) \ (union (rng G)) let G, F be Function of NAT,S; ::_thesis: ( G . 0 = {} & ( for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) implies meet (rng F) = (F . 0) \ (union (rng G)) ) assume that A1: G . 0 = {} and A2: for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ; ::_thesis: meet (rng F) = (F . 0) \ (union (rng G)) A3: for n being Element of NAT holds F . n c= F . 0 proof defpred S1[ Element of NAT ] means F . $1 c= F . 0; A4: 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 A5: F . k c= F . 0 ; ::_thesis: S1[k + 1] F . (k + 1) c= F . k by A2; hence S1[k + 1] by A5, XBOOLE_1:1; ::_thesis: verum end; A6: S1[ 0 ] ; thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A6, A4); ::_thesis: verum end; A7: meet (rng F) c= F . 0 proof set X = the Element of rng F; let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in meet (rng F) or A in F . 0 ) dom F = NAT by FUNCT_2:def_1; then ex n being set st ( n in NAT & F . n = the Element of rng F ) by FUNCT_1:def_3; then A8: the Element of rng F c= F . 0 by A3; assume A in meet (rng F) ; ::_thesis: A in F . 0 then A in the Element of rng F by SETFAM_1:def_1; hence A in F . 0 by A8; ::_thesis: verum end; A9: (F . 0) /\ (meet (rng F)) = (F . 0) \ ((F . 0) \ (meet (rng F))) by XBOOLE_1:48; union (rng G) = (F . 0) \ (meet (rng F)) by A1, A2, Th4; hence meet (rng F) = (F . 0) \ (union (rng G)) by A7, A9, XBOOLE_1:28; ::_thesis: verum end; theorem Th6: :: MEASURE3:6 for X being set for S being SigmaField of X for M being sigma_Measure of S for G, F being Function of NAT,S st M . (F . 0) < +infty & G . 0 = {} & ( for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds M . (meet (rng F)) = (M . (F . 0)) - (M . (union (rng G))) proof let X be set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for G, F being Function of NAT,S st M . (F . 0) < +infty & G . 0 = {} & ( for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds M . (meet (rng F)) = (M . (F . 0)) - (M . (union (rng G))) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for G, F being Function of NAT,S st M . (F . 0) < +infty & G . 0 = {} & ( for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds M . (meet (rng F)) = (M . (F . 0)) - (M . (union (rng G))) let M be sigma_Measure of S; ::_thesis: for G, F being Function of NAT,S st M . (F . 0) < +infty & G . 0 = {} & ( for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds M . (meet (rng F)) = (M . (F . 0)) - (M . (union (rng G))) let G, F be Function of NAT,S; ::_thesis: ( M . (F . 0) < +infty & G . 0 = {} & ( for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) implies M . (meet (rng F)) = (M . (F . 0)) - (M . (union (rng G))) ) assume that A1: M . (F . 0) < +infty and A2: ( G . 0 = {} & ( for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) ) ; ::_thesis: M . (meet (rng F)) = (M . (F . 0)) - (M . (union (rng G))) A3: union (rng G) = (F . 0) \ (meet (rng F)) by A2, Th4; A4: M . ((F . 0) \ (union (rng G))) = M . (meet (rng F)) by A2, Th5; M . ((F . 0) \ (meet (rng F))) <> +infty by A1, MEASURE1:31, XBOOLE_1:36; then M . (union (rng G)) < +infty by A3, XXREAL_0:4; hence M . (meet (rng F)) = (M . (F . 0)) - (M . (union (rng G))) by A3, A4, MEASURE1:32, XBOOLE_1:36; ::_thesis: verum end; theorem Th7: :: MEASURE3:7 for X being set for S being SigmaField of X for M being sigma_Measure of S for G, F being Function of NAT,S st M . (F . 0) < +infty & G . 0 = {} & ( for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds M . (union (rng G)) = (M . (F . 0)) - (M . (meet (rng F))) proof let X be set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for G, F being Function of NAT,S st M . (F . 0) < +infty & G . 0 = {} & ( for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds M . (union (rng G)) = (M . (F . 0)) - (M . (meet (rng F))) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for G, F being Function of NAT,S st M . (F . 0) < +infty & G . 0 = {} & ( for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds M . (union (rng G)) = (M . (F . 0)) - (M . (meet (rng F))) let M be sigma_Measure of S; ::_thesis: for G, F being Function of NAT,S st M . (F . 0) < +infty & G . 0 = {} & ( for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds M . (union (rng G)) = (M . (F . 0)) - (M . (meet (rng F))) let G, F be Function of NAT,S; ::_thesis: ( M . (F . 0) < +infty & G . 0 = {} & ( for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) implies M . (union (rng G)) = (M . (F . 0)) - (M . (meet (rng F))) ) assume that A1: M . (F . 0) < +infty and A2: ( G . 0 = {} & ( for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) ) ; ::_thesis: M . (union (rng G)) = (M . (F . 0)) - (M . (meet (rng F))) A3: meet (rng F) = (F . 0) \ (union (rng G)) by A2, Th5; A4: M . ((F . 0) \ (meet (rng F))) = M . (union (rng G)) by A2, Th4; M . ((F . 0) \ (union (rng G))) <> +infty by A1, MEASURE1:31, XBOOLE_1:36; then M . (meet (rng F)) < +infty by A3, XXREAL_0:4; hence M . (union (rng G)) = (M . (F . 0)) - (M . (meet (rng F))) by A3, A4, MEASURE1:32, XBOOLE_1:36; ::_thesis: verum end; theorem :: MEASURE3:8 for X being set for S being SigmaField of X for M being sigma_Measure of S for G, F being Function of NAT,S st M . (F . 0) < +infty & G . 0 = {} & ( for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds M . (meet (rng F)) = (M . (F . 0)) - (sup (rng (M * G))) proof let X be set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for G, F being Function of NAT,S st M . (F . 0) < +infty & G . 0 = {} & ( for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds M . (meet (rng F)) = (M . (F . 0)) - (sup (rng (M * G))) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for G, F being Function of NAT,S st M . (F . 0) < +infty & G . 0 = {} & ( for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds M . (meet (rng F)) = (M . (F . 0)) - (sup (rng (M * G))) let M be sigma_Measure of S; ::_thesis: for G, F being Function of NAT,S st M . (F . 0) < +infty & G . 0 = {} & ( for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds M . (meet (rng F)) = (M . (F . 0)) - (sup (rng (M * G))) let G, F be Function of NAT,S; ::_thesis: ( M . (F . 0) < +infty & G . 0 = {} & ( for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) implies M . (meet (rng F)) = (M . (F . 0)) - (sup (rng (M * G))) ) assume that A1: M . (F . 0) < +infty and A2: ( G . 0 = {} & ( for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) ) ; ::_thesis: M . (meet (rng F)) = (M . (F . 0)) - (sup (rng (M * G))) for n being Element of NAT holds G . n c= G . (n + 1) by A2, MEASURE2:13; then M . (union (rng G)) = sup (rng (M * G)) by MEASURE2:23; hence M . (meet (rng F)) = (M . (F . 0)) - (sup (rng (M * G))) by A1, A2, Th6; ::_thesis: verum end; theorem Th9: :: MEASURE3:9 for X being set for S being SigmaField of X for M being sigma_Measure of S for G, F being Function of NAT,S st M . (F . 0) < +infty & G . 0 = {} & ( for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds ( M . (F . 0) is Real & inf (rng (M * F)) is Real & sup (rng (M * G)) is Real ) proof let X be set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for G, F being Function of NAT,S st M . (F . 0) < +infty & G . 0 = {} & ( for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds ( M . (F . 0) is Real & inf (rng (M * F)) is Real & sup (rng (M * G)) is Real ) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for G, F being Function of NAT,S st M . (F . 0) < +infty & G . 0 = {} & ( for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds ( M . (F . 0) is Real & inf (rng (M * F)) is Real & sup (rng (M * G)) is Real ) let M be sigma_Measure of S; ::_thesis: for G, F being Function of NAT,S st M . (F . 0) < +infty & G . 0 = {} & ( for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds ( M . (F . 0) is Real & inf (rng (M * F)) is Real & sup (rng (M * G)) is Real ) let G, F be Function of NAT,S; ::_thesis: ( M . (F . 0) < +infty & G . 0 = {} & ( for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) implies ( M . (F . 0) is Real & inf (rng (M * F)) is Real & sup (rng (M * G)) is Real ) ) assume that A1: M . (F . 0) < +infty and A2: G . 0 = {} and A3: for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ; ::_thesis: ( M . (F . 0) is Real & inf (rng (M * F)) is Real & sup (rng (M * G)) is Real ) reconsider P = {} as Element of S by PROB_1:4; M . P <= M . (F . 0) by MEASURE1:31, XBOOLE_1:2; then 0. <= M . (F . 0) by VALUED_0:def_19; hence A4: M . (F . 0) is Real by A1, XXREAL_0:46; ::_thesis: ( inf (rng (M * F)) is Real & sup (rng (M * G)) is Real ) for x being ext-real number st x in rng (M * G) holds x <= M . (F . 0) proof let x be ext-real number ; ::_thesis: ( x in rng (M * G) implies x <= M . (F . 0) ) A5: dom (M * G) = NAT by FUNCT_2:def_1; assume x in rng (M * G) ; ::_thesis: x <= M . (F . 0) then consider n being set such that A6: n in NAT and A7: (M * G) . n = x by A5, FUNCT_1:def_3; reconsider n = n as Element of NAT by A6; A8: x = M . (G . n) by A5, A7, FUNCT_1:12; A9: ( ex k being Nat st n = k + 1 implies x <= M . (F . 0) ) proof given k being Nat such that A10: n = k + 1 ; ::_thesis: x <= M . (F . 0) reconsider k = k as Element of NAT by ORDINAL1:def_12; G . n = (F . 0) \ (F . k) by A3, A10; hence x <= M . (F . 0) by A8, MEASURE1:31, XBOOLE_1:36; ::_thesis: verum end; ( n = 0 implies x <= M . (F . 0) ) by A2, A8, MEASURE1:31, XBOOLE_1:2; hence x <= M . (F . 0) by A9, NAT_1:6; ::_thesis: verum end; then M . (F . 0) is UpperBound of rng (M * G) by XXREAL_2:def_1; then A11: sup (rng (M * G)) <= M . (F . 0) by XXREAL_2:def_3; for x being ext-real number st x in rng (M * F) holds 0. <= x proof let x be ext-real number ; ::_thesis: ( x in rng (M * F) implies 0. <= x ) A12: dom (M * F) = NAT by FUNCT_2:def_1; A13: M * F is V87() by MEASURE2:1; assume x in rng (M * F) ; ::_thesis: 0. <= x then ex n being set st ( n in NAT & (M * F) . n = x ) by A12, FUNCT_1:def_3; hence 0. <= x by A13, SUPINF_2:39; ::_thesis: verum end; then 0. is LowerBound of rng (M * F) by XXREAL_2:def_2; then A14: inf (rng (M * F)) >= 0 by XXREAL_2:def_4; ex x being R_eal st ( x in rng (M * F) & x = M . (F . 0) ) proof take (M * F) . 0 ; ::_thesis: ( (M * F) . 0 in rng (M * F) & (M * F) . 0 = M . (F . 0) ) dom (M * F) = NAT by FUNCT_2:def_1; hence ( (M * F) . 0 in rng (M * F) & (M * F) . 0 = M . (F . 0) ) by FUNCT_1:12, FUNCT_2:4; ::_thesis: verum end; then inf (rng (M * F)) <= M . (F . 0) by XXREAL_2:3; hence inf (rng (M * F)) is Real by A4, A14, XXREAL_0:45; ::_thesis: sup (rng (M * G)) is Real 0. <= sup (rng (M * G)) proof set x = (M * G) . 0; for x being R_eal st x in rng (M * G) holds 0. <= x proof let x be R_eal; ::_thesis: ( x in rng (M * G) implies 0. <= x ) A15: dom (M * G) = NAT by FUNCT_2:def_1; A16: M * G is V87() by MEASURE2:1; assume x in rng (M * G) ; ::_thesis: 0. <= x then ex n being set st ( n in NAT & (M * G) . n = x ) by A15, FUNCT_1:def_3; hence 0. <= x by A16, SUPINF_2:39; ::_thesis: verum end; then A17: 0. <= (M * G) . 0 by FUNCT_2:4; (M * G) . 0 <= sup (rng (M * G)) by FUNCT_2:4, XXREAL_2:4; hence 0. <= sup (rng (M * G)) by A17, XXREAL_0:2; ::_thesis: verum end; hence sup (rng (M * G)) is Real by A4, A11, XXREAL_0:45; ::_thesis: verum end; theorem Th10: :: MEASURE3:10 for X being set for S being SigmaField of X for M being sigma_Measure of S for G, F being Function of NAT,S st M . (F . 0) < +infty & G . 0 = {} & ( for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds sup (rng (M * G)) = (M . (F . 0)) - (inf (rng (M * F))) proof let X be set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for G, F being Function of NAT,S st M . (F . 0) < +infty & G . 0 = {} & ( for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds sup (rng (M * G)) = (M . (F . 0)) - (inf (rng (M * F))) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for G, F being Function of NAT,S st M . (F . 0) < +infty & G . 0 = {} & ( for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds sup (rng (M * G)) = (M . (F . 0)) - (inf (rng (M * F))) let M be sigma_Measure of S; ::_thesis: for G, F being Function of NAT,S st M . (F . 0) < +infty & G . 0 = {} & ( for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds sup (rng (M * G)) = (M . (F . 0)) - (inf (rng (M * F))) let G, F be Function of NAT,S; ::_thesis: ( M . (F . 0) < +infty & G . 0 = {} & ( for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) implies sup (rng (M * G)) = (M . (F . 0)) - (inf (rng (M * F))) ) assume that A1: M . (F . 0) < +infty and A2: G . 0 = {} and A3: for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ; ::_thesis: sup (rng (M * G)) = (M . (F . 0)) - (inf (rng (M * F))) set l = (M . (F . 0)) - (inf (rng (M * F))); for x being ext-real number st x in rng (M * G) holds x <= (M . (F . 0)) - (inf (rng (M * F))) proof let x be ext-real number ; ::_thesis: ( x in rng (M * G) implies x <= (M . (F . 0)) - (inf (rng (M * F))) ) A4: dom (M * G) = NAT by FUNCT_2:def_1; assume x in rng (M * G) ; ::_thesis: x <= (M . (F . 0)) - (inf (rng (M * F))) then consider n being set such that A5: n in NAT and A6: (M * G) . n = x by A4, FUNCT_1:def_3; M * G is V87() by MEASURE2:1; then x >= 0 by A5, A6, SUPINF_2:39; then A7: x > -infty by XXREAL_0:2, XXREAL_0:12; reconsider n = n as Element of NAT by A5; A8: ( n = 0 implies G . n c= F . 0 ) by A2, XBOOLE_1:2; A9: dom (M * F) = NAT by FUNCT_2:def_1; A10: ( n = 0 implies M . ((F . 0) \ (G . n)) in rng (M * F) ) proof assume A11: n = 0 ; ::_thesis: M . ((F . 0) \ (G . n)) in rng (M * F) M . (F . 0) = (M * F) . 0 by A9, FUNCT_1:12; hence M . ((F . 0) \ (G . n)) in rng (M * F) by A2, A11, FUNCT_2:4; ::_thesis: verum end; A12: ( ex k being Nat st n = k + 1 implies M . ((F . 0) \ (G . n)) in rng (M * F) ) proof A13: for n being Element of NAT holds F . n c= F . 0 proof defpred S1[ Element of NAT ] means F . $1 c= F . 0; A14: 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 A15: F . k c= F . 0 ; ::_thesis: S1[k + 1] F . (k + 1) c= F . k by A3; hence S1[k + 1] by A15, XBOOLE_1:1; ::_thesis: verum end; A16: S1[ 0 ] ; thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A16, A14); ::_thesis: verum end; given k being Nat such that A17: n = k + 1 ; ::_thesis: M . ((F . 0) \ (G . n)) in rng (M * F) reconsider k = k as Element of NAT by ORDINAL1:def_12; A18: M . (F . k) = (M * F) . k by A9, FUNCT_1:12; (F . 0) \ (G . n) = (F . 0) \ ((F . 0) \ (F . k)) by A3, A17 .= (F . 0) /\ (F . k) by XBOOLE_1:48 .= F . k by A13, XBOOLE_1:28 ; hence M . ((F . 0) \ (G . n)) in rng (M * F) by A18, FUNCT_2:4; ::_thesis: verum end; A19: ( ex k being Nat st n = k + 1 implies G . n c= F . 0 ) proof given k being Nat such that A20: n = k + 1 ; ::_thesis: G . n c= F . 0 reconsider k = k as Element of NAT by ORDINAL1:def_12; G . n = (F . 0) \ (F . k) by A3, A20; hence G . n c= F . 0 by XBOOLE_1:36; ::_thesis: verum end; A21: x = M . (G . n) by A4, A6, FUNCT_1:12; then x <> +infty by A1, A8, A19, MEASURE1:31, NAT_1:6; then A22: x is Real by A7, XXREAL_0:14; reconsider x = x as R_eal by XXREAL_0:def_1; ( M . (F . 0) is Real & inf (rng (M * F)) is Real ) by A1, A2, A3, Th9; then consider a, b, c being Real such that A23: a = M . (F . 0) and A24: b = x and A25: c = inf (rng (M * F)) by A22; (M . (F . 0)) - x = a - b by A23, A24, SUPINF_2:3; then A26: ((M . (F . 0)) - x) + x = (a - b) + b by A24, SUPINF_2:1 .= M . (F . 0) by A23 ; (inf (rng (M * F))) + x = c + b by A24, A25, SUPINF_2:1; then A27: ((inf (rng (M * F))) + x) - (inf (rng (M * F))) = (b + c) - c by A25, SUPINF_2:3 .= x by A24 ; (M . (F . 0)) - x = M . ((F . 0) \ (G . n)) by A21, A8, A19, A22, MEASURE1:32, NAT_1:6, XXREAL_0:9; then inf (rng (M * F)) <= (M . (F . 0)) - x by A10, A12, NAT_1:6, XXREAL_2:3; then (inf (rng (M * F))) + x <= M . (F . 0) by A26, XXREAL_3:36; hence x <= (M . (F . 0)) - (inf (rng (M * F))) by A27, XXREAL_3:37; ::_thesis: verum end; then A28: (M . (F . 0)) - (inf (rng (M * F))) is UpperBound of rng (M * G) by XXREAL_2:def_1; A29: for n being Element of NAT holds G . n c= G . (n + 1) by A2, A3, MEASURE2:13; for y being UpperBound of rng (M * G) holds (M . (F . 0)) - (inf (rng (M * F))) <= y proof let y be UpperBound of rng (M * G); ::_thesis: (M . (F . 0)) - (inf (rng (M * F))) <= y (M . (F . 0)) - (inf (rng (M * F))) <= y proof for x being ext-real number st x in rng (M * F) holds M . (meet (rng F)) <= x proof let x be ext-real number ; ::_thesis: ( x in rng (M * F) implies M . (meet (rng F)) <= x ) A30: dom (M * F) = NAT by FUNCT_2:def_1; assume x in rng (M * F) ; ::_thesis: M . (meet (rng F)) <= x then consider n being set such that A31: n in NAT and A32: (M * F) . n = x by A30, FUNCT_1:def_3; reconsider n = n as Element of NAT by A31; A33: meet (rng F) c= F . n by FUNCT_2:4, SETFAM_1:3; x = M . (F . n) by A30, A32, FUNCT_1:12; hence M . (meet (rng F)) <= x by A33, MEASURE1:31; ::_thesis: verum end; then M . (meet (rng F)) is LowerBound of rng (M * F) by XXREAL_2:def_2; then A34: M . (meet (rng F)) <= inf (rng (M * F)) by XXREAL_2:def_4; set Q = union (rng G); sup (rng (M * G)) = M . (union (rng G)) by A29, MEASURE2:23; then A35: M . (union (rng G)) <= y by XXREAL_2:def_3; (M . (F . 0)) - (M . (meet (rng F))) = M . (union (rng G)) by A1, A2, A3, Th7; then (M . (F . 0)) - (inf (rng (M * F))) <= M . (union (rng G)) by A34, XXREAL_3:37; hence (M . (F . 0)) - (inf (rng (M * F))) <= y by A35, XXREAL_0:2; ::_thesis: verum end; hence (M . (F . 0)) - (inf (rng (M * F))) <= y ; ::_thesis: verum end; hence sup (rng (M * G)) = (M . (F . 0)) - (inf (rng (M * F))) by A28, XXREAL_2:def_3; ::_thesis: verum end; theorem Th11: :: MEASURE3:11 for X being set for S being SigmaField of X for M being sigma_Measure of S for G, F being Function of NAT,S st M . (F . 0) < +infty & G . 0 = {} & ( for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds inf (rng (M * F)) = (M . (F . 0)) - (sup (rng (M * G))) proof let X be set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for G, F being Function of NAT,S st M . (F . 0) < +infty & G . 0 = {} & ( for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds inf (rng (M * F)) = (M . (F . 0)) - (sup (rng (M * G))) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for G, F being Function of NAT,S st M . (F . 0) < +infty & G . 0 = {} & ( for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds inf (rng (M * F)) = (M . (F . 0)) - (sup (rng (M * G))) let M be sigma_Measure of S; ::_thesis: for G, F being Function of NAT,S st M . (F . 0) < +infty & G . 0 = {} & ( for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds inf (rng (M * F)) = (M . (F . 0)) - (sup (rng (M * G))) let G, F be Function of NAT,S; ::_thesis: ( M . (F . 0) < +infty & G . 0 = {} & ( for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) implies inf (rng (M * F)) = (M . (F . 0)) - (sup (rng (M * G))) ) assume that A1: M . (F . 0) < +infty and A2: G . 0 = {} and A3: for n being Element of NAT holds ( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ; ::_thesis: inf (rng (M * F)) = (M . (F . 0)) - (sup (rng (M * G))) set l = (M . (F . 0)) - (sup (rng (M * G))); for x being ext-real number st x in rng (M * F) holds (M . (F . 0)) - (sup (rng (M * G))) <= x proof let x be ext-real number ; ::_thesis: ( x in rng (M * F) implies (M . (F . 0)) - (sup (rng (M * G))) <= x ) assume A4: x in rng (M * F) ; ::_thesis: (M . (F . 0)) - (sup (rng (M * G))) <= x ( x <> +infty implies (M . (F . 0)) - (sup (rng (M * G))) <= x ) proof A5: dom (M * F) = NAT by FUNCT_2:def_1; then consider n being set such that A6: n in NAT and A7: (M * F) . n = x by A4, FUNCT_1:def_3; M * F is V87() by MEASURE2:1; then A8: 0. <= x by A6, A7, SUPINF_2:39; assume A9: x <> +infty ; ::_thesis: (M . (F . 0)) - (sup (rng (M * G))) <= x reconsider x = x as R_eal by XXREAL_0:def_1; x <= +infty by XXREAL_0:3; then x < +infty by A9, XXREAL_0:1; then A10: x is Real by A8, XXREAL_0:14, XXREAL_0:46; ( M . (F . 0) is Real & sup (rng (M * G)) is Real ) by A1, A2, A3, Th9; then consider a, b, c being Real such that A11: a = M . (F . 0) and A12: b = x and A13: c = sup (rng (M * G)) by A10; (sup (rng (M * G))) + x = c + b by A12, A13, SUPINF_2:1; then A14: ((sup (rng (M * G))) + x) - (sup (rng (M * G))) = (b + c) - c by A13, SUPINF_2:3 .= x by A12 ; reconsider n = n as Element of NAT by A6; A15: dom (M * G) = NAT by FUNCT_2:def_1; A16: (M . (F . 0)) - x <= sup (rng (M * G)) proof set k = n + 1; A17: for n being Element of NAT holds F . n c= F . 0 proof defpred S1[ Element of NAT ] means F . $1 c= F . 0; A18: 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 A19: F . k c= F . 0 ; ::_thesis: S1[k + 1] F . (k + 1) c= F . k by A3; hence S1[k + 1] by A19, XBOOLE_1:1; ::_thesis: verum end; A20: S1[ 0 ] ; thus for k being Element of NAT holds S1[k] from NAT_1:sch_1(A20, A18); ::_thesis: verum end; then M . (F . n) <= M . (F . 0) by MEASURE1:31; then A21: M . (F . n) < +infty by A1, XXREAL_0:2; (M . (F . 0)) - x = (M . (F . 0)) - (M . (F . n)) by A5, A7, FUNCT_1:12 .= M . ((F . 0) \ (F . n)) by A17, A21, MEASURE1:32 .= M . (G . (n + 1)) by A3 ; then (M . (F . 0)) - x = (M * G) . (n + 1) by A15, FUNCT_1:12; hence (M . (F . 0)) - x <= sup (rng (M * G)) by FUNCT_2:4, XXREAL_2:4; ::_thesis: verum end; (M . (F . 0)) - x = a - b by A11, A12, SUPINF_2:3; then ((M . (F . 0)) - x) + x = (a - b) + b by A12, SUPINF_2:1 .= M . (F . 0) by A11 ; then M . (F . 0) <= (sup (rng (M * G))) + x by A16, XXREAL_3:36; hence (M . (F . 0)) - (sup (rng (M * G))) <= x by A14, XXREAL_3:37; ::_thesis: verum end; hence (M . (F . 0)) - (sup (rng (M * G))) <= x by XXREAL_0:4; ::_thesis: verum end; then A22: (M . (F . 0)) - (sup (rng (M * G))) is LowerBound of rng (M * F) by XXREAL_2:def_2; for y being LowerBound of rng (M * F) holds y <= (M . (F . 0)) - (sup (rng (M * G))) proof A23: inf (rng (M * F)) is Real by A1, A2, A3, Th9; ( sup (rng (M * G)) is Real & M . (F . 0) is Real ) by A1, A2, A3, Th9; then consider a, b, c being Real such that A24: a = sup (rng (M * G)) and A25: b = M . (F . 0) and A26: c = inf (rng (M * F)) by A23; (sup (rng (M * G))) + (inf (rng (M * F))) = a + c by A24, A26, SUPINF_2:1; then A27: ((sup (rng (M * G))) + (inf (rng (M * F)))) - (sup (rng (M * G))) = (c + a) - a by A24, SUPINF_2:3 .= inf (rng (M * F)) by A26 ; let y be LowerBound of rng (M * F); ::_thesis: y <= (M . (F . 0)) - (sup (rng (M * G))) consider s, t, r being R_eal such that s = sup (rng (M * G)) and t = (M . (F . 0)) - (inf (rng (M * F))) and A28: r = inf (rng (M * F)) ; A29: sup (rng (M * G)) = (M . (F . 0)) - (inf (rng (M * F))) by A1, A2, A3, Th10; (M . (F . 0)) - (inf (rng (M * F))) = b - c by A25, A26, SUPINF_2:3; then ((M . (F . 0)) - (inf (rng (M * F)))) + r = (b - c) + c by A26, A28, SUPINF_2:1 .= M . (F . 0) by A25 ; hence y <= (M . (F . 0)) - (sup (rng (M * G))) by A29, A28, A27, XXREAL_2:def_4; ::_thesis: verum end; hence inf (rng (M * F)) = (M . (F . 0)) - (sup (rng (M * G))) by A22, XXREAL_2:def_4; ::_thesis: verum end; theorem :: MEASURE3:12 for X being set for S being SigmaField of X for M being sigma_Measure of S for F being Function of NAT,S st ( for n being Element of NAT holds F . (n + 1) c= F . n ) & M . (F . 0) < +infty holds M . (meet (rng F)) = inf (rng (M * F)) proof let X be set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for F being Function of NAT,S st ( for n being Element of NAT holds F . (n + 1) c= F . n ) & M . (F . 0) < +infty holds M . (meet (rng F)) = inf (rng (M * F)) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for F being Function of NAT,S st ( for n being Element of NAT holds F . (n + 1) c= F . n ) & M . (F . 0) < +infty holds M . (meet (rng F)) = inf (rng (M * F)) let M be sigma_Measure of S; ::_thesis: for F being Function of NAT,S st ( for n being Element of NAT holds F . (n + 1) c= F . n ) & M . (F . 0) < +infty holds M . (meet (rng F)) = inf (rng (M * F)) let F be Function of NAT,S; ::_thesis: ( ( for n being Element of NAT holds F . (n + 1) c= F . n ) & M . (F . 0) < +infty implies M . (meet (rng F)) = inf (rng (M * F)) ) assume that A1: for n being Element of NAT holds F . (n + 1) c= F . n and A2: M . (F . 0) < +infty ; ::_thesis: M . (meet (rng F)) = inf (rng (M * F)) consider G being Function of NAT,S such that A3: ( G . 0 = {} & ( for n being Element of NAT holds G . (n + 1) = (F . 0) \ (F . n) ) ) by MEASURE2:9; A4: union (rng G) = (F . 0) \ (meet (rng F)) by A1, A3, Th4; A5: M . ((F . 0) \ (union (rng G))) = M . (meet (rng F)) by A1, A3, Th5; A6: for A being Element of S st A = union (rng G) holds M . (meet (rng F)) = (M . (F . 0)) - (M . A) proof let A be Element of S; ::_thesis: ( A = union (rng G) implies M . (meet (rng F)) = (M . (F . 0)) - (M . A) ) assume A7: A = union (rng G) ; ::_thesis: M . (meet (rng F)) = (M . (F . 0)) - (M . A) M . ((F . 0) \ (meet (rng F))) <> +infty by A2, MEASURE1:31, XBOOLE_1:36; then M . A < +infty by A4, A7, XXREAL_0:4; hence M . (meet (rng F)) = (M . (F . 0)) - (M . A) by A4, A5, A7, MEASURE1:32, XBOOLE_1:36; ::_thesis: verum end; for n being Element of NAT holds G . n c= G . (n + 1) by A1, A3, MEASURE2:13; then M . (union (rng G)) = sup (rng (M * G)) by MEASURE2:23; then M . (meet (rng F)) = (M . (F . 0)) - (sup (rng (M * G))) by A6; hence M . (meet (rng F)) = inf (rng (M * F)) by A1, A2, A3, Th11; ::_thesis: verum end; theorem Th13: :: MEASURE3:13 for X being set for S being SigmaField of X for M being Measure of S for F being Sep_Sequence of S holds SUM (M * F) <= M . (union (rng F)) proof let X be set ; ::_thesis: for S being SigmaField of X for M being Measure of S for F being Sep_Sequence of S holds SUM (M * F) <= M . (union (rng F)) let S be SigmaField of X; ::_thesis: for M being Measure of S for F being Sep_Sequence of S holds SUM (M * F) <= M . (union (rng F)) let M be Measure of S; ::_thesis: for F being Sep_Sequence of S holds SUM (M * F) <= M . (union (rng F)) let F be Sep_Sequence of S; ::_thesis: SUM (M * F) <= M . (union (rng F)) set T = rng F; consider G being Function of NAT,S such that A1: G . 0 = F . 0 and A2: for n being Element of NAT holds G . (n + 1) = (F . (n + 1)) \/ (G . n) by MEASURE2:4; {} is Subset of X by XBOOLE_1:2; then consider H being Function of NAT,(bool X) such that A3: rng H = {(union (rng F)),{}} and A4: H . 0 = union (rng F) and A5: for n being Element of NAT st 0 < n holds H . n = {} by MEASURE1:19; rng H c= S proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in rng H or a in S ) assume a in rng H ; ::_thesis: a in S then ( a = union (rng F) or a = {} ) by A3, TARSKI:def_2; hence a in S by PROB_1:4; ::_thesis: verum end; then reconsider H = H as Function of NAT,S by FUNCT_2:6; defpred S1[ Element of NAT ] means (Ser (M * F)) . $1 = M . (G . $1); A6: dom (M * F) = NAT by FUNCT_2:def_1; A7: for n being Element of NAT holds (G . n) /\ (F . (n + 1)) = {} proof let n be Element of NAT ; ::_thesis: (G . n) /\ (F . (n + 1)) = {} A8: for n, k being Element of NAT st n < k holds (G . n) /\ (F . k) = {} proof defpred S2[ Element of NAT ] means for k being Element of NAT st $1 < k holds (G . $1) /\ (F . k) = {} ; A9: for n being Element of NAT st S2[n] holds S2[n + 1] proof let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] ) assume A10: for k being Element of NAT st n < k holds (G . n) /\ (F . k) = {} ; ::_thesis: S2[n + 1] let k be Element of NAT ; ::_thesis: ( n + 1 < k implies (G . (n + 1)) /\ (F . k) = {} ) assume A11: n + 1 < k ; ::_thesis: (G . (n + 1)) /\ (F . k) = {} then A12: n < k by NAT_1:13; F . (n + 1) misses F . k by A11, PROB_2:def_2; then A13: (F . (n + 1)) /\ (F . k) = {} by XBOOLE_0:def_7; (G . (n + 1)) /\ (F . k) = ((F . (n + 1)) \/ (G . n)) /\ (F . k) by A2 .= ((F . (n + 1)) /\ (F . k)) \/ ((G . n) /\ (F . k)) by XBOOLE_1:23 ; hence (G . (n + 1)) /\ (F . k) = {} by A10, A12, A13; ::_thesis: verum end; A14: S2[ 0 ] proof let k be Element of NAT ; ::_thesis: ( 0 < k implies (G . 0) /\ (F . k) = {} ) assume 0 < k ; ::_thesis: (G . 0) /\ (F . k) = {} then F . 0 misses F . k by PROB_2:def_2; hence (G . 0) /\ (F . k) = {} by A1, XBOOLE_0:def_7; ::_thesis: verum end; thus for n being Element of NAT holds S2[n] from NAT_1:sch_1(A14, A9); ::_thesis: verum end; n < n + 1 by NAT_1:13; hence (G . n) /\ (F . (n + 1)) = {} by A8; ::_thesis: verum end; A15: 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] ) (G . k) /\ (F . (k + 1)) = {} by A7; then A16: G . k misses F . (k + 1) by XBOOLE_0:def_7; assume (Ser (M * F)) . k = M . (G . k) ; ::_thesis: S1[k + 1] then (Ser (M * F)) . (k + 1) = (M . (G . k)) + ((M * F) . (k + 1)) by SUPINF_2:44; then (Ser (M * F)) . (k + 1) = (M . (G . k)) + (M . (F . (k + 1))) by A6, FUNCT_1:12 .= M . ((F . (k + 1)) \/ (G . k)) by A16, MEASURE1:def_3 .= M . (G . (k + 1)) by A2 ; hence S1[k + 1] ; ::_thesis: verum end; (Ser (M * F)) . 0 = (M * F) . 0 by SUPINF_2:44; then A17: S1[ 0 ] by A1, A6, FUNCT_1:12; A18: for n being Element of NAT holds S1[n] from NAT_1:sch_1(A17, A15); defpred S2[ Element of NAT ] means (Ser (M * H)) . $1 = M . (union (rng F)); A19: for n being Element of NAT st S2[n] holds S2[n + 1] proof let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] ) 0 <= n by NAT_1:2; then 0 < n + 1 by NAT_1:13; then A20: H . (n + 1) = {} by A5; dom (M * H) = NAT by FUNCT_2:def_1; then (M * H) . (n + 1) = M . {} by A20, FUNCT_1:12; then A21: (M * H) . (n + 1) = 0. by VALUED_0:def_19; assume (Ser (M * H)) . n = M . (union (rng F)) ; ::_thesis: S2[n + 1] then (Ser (M * H)) . (n + 1) = (M . (union (rng F))) + ((M * H) . (n + 1)) by SUPINF_2:44; hence S2[n + 1] by A21, XXREAL_3:4; ::_thesis: verum end; ( (Ser (M * H)) . 0 = (M * H) . 0 & dom (M * H) = NAT ) by FUNCT_2:def_1, SUPINF_2:44; then A22: S2[ 0 ] by A4, FUNCT_1:12; A23: for n being Element of NAT holds S2[n] from NAT_1:sch_1(A22, A19); A24: for r being Element of NAT st 1 <= r holds (M * H) . r = 0. proof let r be Element of NAT ; ::_thesis: ( 1 <= r implies (M * H) . r = 0. ) assume 1 <= r ; ::_thesis: (M * H) . r = 0. then 0 + 1 <= r ; then 0 < r by NAT_1:13; then A25: H . r = {} by A5; dom (M * H) = NAT by FUNCT_2:def_1; then (M * H) . r = M . {} by A25, FUNCT_1:12; hence (M * H) . r = 0. by VALUED_0:def_19; ::_thesis: verum end; A26: for n being Element of NAT holds G . n c= union (rng F) proof defpred S3[ Element of NAT ] means G . $1 c= union (rng F); A27: for n being Element of NAT st S3[n] holds S3[n + 1] proof let n be Element of NAT ; ::_thesis: ( S3[n] implies S3[n + 1] ) assume A28: G . n c= union (rng F) ; ::_thesis: S3[n + 1] ( G . (n + 1) = (F . (n + 1)) \/ (G . n) & F . (n + 1) c= union (rng F) ) by A2, FUNCT_2:4, ZFMISC_1:74; hence S3[n + 1] by A28, XBOOLE_1:8; ::_thesis: verum end; A29: S3[ 0 ] by A1, FUNCT_2:4, ZFMISC_1:74; thus for n being Element of NAT holds S3[n] from NAT_1:sch_1(A29, A27); ::_thesis: verum end; A30: for n being Element of NAT holds (Ser (M * F)) . n <= (Ser (M * H)) . n proof let n be Element of NAT ; ::_thesis: (Ser (M * F)) . n <= (Ser (M * H)) . n (Ser (M * F)) . n = M . (G . n) by A18; then (Ser (M * F)) . n <= M . (union (rng F)) by A26, MEASURE1:8; hence (Ser (M * F)) . n <= (Ser (M * H)) . n by A23; ::_thesis: verum end; M * H is V87() by MEASURE1:25; then SUM (M * H) = (Ser (M * H)) . 1 by A24, SUPINF_2:48; then SUM (M * H) = M . (union (rng F)) by A23; hence SUM (M * F) <= M . (union (rng F)) by A30, Th1; ::_thesis: verum end; theorem :: MEASURE3:14 for X being set for S being SigmaField of X for M being Measure of S st ( for F being Sep_Sequence of S holds M . (union (rng F)) <= SUM (M * F) ) holds M is sigma_Measure of S proof let X be set ; ::_thesis: for S being SigmaField of X for M being Measure of S st ( for F being Sep_Sequence of S holds M . (union (rng F)) <= SUM (M * F) ) holds M is sigma_Measure of S let S be SigmaField of X; ::_thesis: for M being Measure of S st ( for F being Sep_Sequence of S holds M . (union (rng F)) <= SUM (M * F) ) holds M is sigma_Measure of S let M be Measure of S; ::_thesis: ( ( for F being Sep_Sequence of S holds M . (union (rng F)) <= SUM (M * F) ) implies M is sigma_Measure of S ) assume A1: for F being Sep_Sequence of S holds M . (union (rng F)) <= SUM (M * F) ; ::_thesis: M is sigma_Measure of S for F being Sep_Sequence of S holds SUM (M * F) = M . (union (rng F)) proof let F be Sep_Sequence of S; ::_thesis: SUM (M * F) = M . (union (rng F)) ( M . (union (rng F)) <= SUM (M * F) & SUM (M * F) <= M . (union (rng F)) ) by A1, Th13; hence SUM (M * F) = M . (union (rng F)) by XXREAL_0:1; ::_thesis: verum end; hence M is sigma_Measure of S by MEASURE1:def_6; ::_thesis: verum end; definition let X be set ; let S be SigmaField of X; let M be sigma_Measure of S; predM is_complete S means :Def1: :: MEASURE3:def 1 for A being Subset of X for B being set st B in S & A c= B & M . B = 0. holds A in S; end; :: deftheorem Def1 defines is_complete MEASURE3:def_1_:_ for X being set for S being SigmaField of X for M being sigma_Measure of S holds ( M is_complete S iff for A being Subset of X for B being set st B in S & A c= B & M . B = 0. holds A in S ); definition let X be set ; let S be SigmaField of X; let M be sigma_Measure of S; mode thin of M -> Subset of X means :Def2: :: MEASURE3:def 2 ex B being set st ( B in S & it c= B & M . B = 0. ); existence ex b1 being Subset of X ex B being set st ( B in S & b1 c= B & M . B = 0. ) proof reconsider A = {} as Subset of X by XBOOLE_1:2; take A ; ::_thesis: ex B being set st ( B in S & A c= B & M . B = 0. ) take B = {} ; ::_thesis: ( B in S & A c= B & M . B = 0. ) thus B in S by PROB_1:4; ::_thesis: ( A c= B & M . B = 0. ) thus A c= B ; ::_thesis: M . B = 0. thus M . B = 0. by VALUED_0:def_19; ::_thesis: verum end; end; :: deftheorem Def2 defines thin MEASURE3:def_2_:_ for X being set for S being SigmaField of X for M being sigma_Measure of S for b4 being Subset of X holds ( b4 is thin of M iff ex B being set st ( B in S & b4 c= B & M . B = 0. ) ); definition let X be set ; let S be SigmaField of X; let M be sigma_Measure of S; func COM (S,M) -> non empty Subset-Family of X means :Def3: :: MEASURE3:def 3 for A being set holds ( A in it iff ex B being set st ( B in S & ex C being thin of M st A = B \/ C ) ); existence ex b1 being non empty Subset-Family of X st for A being set holds ( A in b1 iff ex B being set st ( B in S & ex C being thin of M st A = B \/ C ) ) proof A1: ex B being set st ( B in S & {} c= B & M . B = 0. ) proof consider B being set such that A2: ( B = {} & B in S ) by PROB_1:4; take B ; ::_thesis: ( B in S & {} c= B & M . B = 0. ) thus ( B in S & {} c= B & M . B = 0. ) by A2, VALUED_0:def_19; ::_thesis: verum end; A3: {} is Subset of X by XBOOLE_1:2; A4: for A being set st A = {} holds ex B being set st ( B in S & ex C being thin of M st A = B \/ C ) proof reconsider C = {} as thin of M by A3, A1, Def2; let A be set ; ::_thesis: ( A = {} implies ex B being set st ( B in S & ex C being thin of M st A = B \/ C ) ) consider B being set such that A5: B = {} and A6: B in S by PROB_1:4; assume A = {} ; ::_thesis: ex B being set st ( B in S & ex C being thin of M st A = B \/ C ) then A = B \/ C by A5; hence ex B being set st ( B in S & ex C being thin of M st A = B \/ C ) by A6; ::_thesis: verum end; defpred S1[ set ] means for A being set st A = $1 holds ex B being set st ( B in S & ex C being thin of M st A = B \/ C ); consider D being set such that A7: for y being set holds ( y in D iff ( y in bool X & S1[y] ) ) from XBOOLE_0:sch_1(); A8: for A being set holds ( A in D iff ex B being set st ( B in S & ex C being thin of M st A = B \/ C ) ) proof let A be set ; ::_thesis: ( A in D iff ex B being set st ( B in S & ex C being thin of M st A = B \/ C ) ) A9: ( A in D iff ( A in bool X & ( for y being set st y = A holds ex B being set st ( B in S & ex C being thin of M st y = B \/ C ) ) ) ) by A7; ( ex B being set st ( B in S & ex C being thin of M st A = B \/ C ) implies A in D ) proof assume A10: ex B being set st ( B in S & ex C being thin of M st A = B \/ C ) ; ::_thesis: A in D then A c= X by XBOOLE_1:8; hence A in D by A9, A10; ::_thesis: verum end; hence ( A in D iff ex B being set st ( B in S & ex C being thin of M st A = B \/ C ) ) by A7; ::_thesis: verum end; A11: D c= bool X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D or x in bool X ) assume x in D ; ::_thesis: x in bool X hence x in bool X by A7; ::_thesis: verum end; {} c= X by XBOOLE_1:2; then reconsider D = D as non empty Subset-Family of X by A7, A11, A4; take D ; ::_thesis: for A being set holds ( A in D iff ex B being set st ( B in S & ex C being thin of M st A = B \/ C ) ) thus for A being set holds ( A in D iff ex B being set st ( B in S & ex C being thin of M st A = B \/ C ) ) by A8; ::_thesis: verum end; uniqueness for b1, b2 being non empty Subset-Family of X st ( for A being set holds ( A in b1 iff ex B being set st ( B in S & ex C being thin of M st A = B \/ C ) ) ) & ( for A being set holds ( A in b2 iff ex B being set st ( B in S & ex C being thin of M st A = B \/ C ) ) ) holds b1 = b2 proof let D1, D2 be non empty Subset-Family of X; ::_thesis: ( ( for A being set holds ( A in D1 iff ex B being set st ( B in S & ex C being thin of M st A = B \/ C ) ) ) & ( for A being set holds ( A in D2 iff ex B being set st ( B in S & ex C being thin of M st A = B \/ C ) ) ) implies D1 = D2 ) assume that A12: for A being set holds ( A in D1 iff ex B being set st ( B in S & ex C being thin of M st A = B \/ C ) ) and A13: for A being set holds ( A in D2 iff ex B being set st ( B in S & ex C being thin of M st A = B \/ C ) ) ; ::_thesis: D1 = D2 for A being set holds ( A in D1 iff A in D2 ) proof let A be set ; ::_thesis: ( A in D1 iff A in D2 ) thus ( A in D1 implies A in D2 ) ::_thesis: ( A in D2 implies A in D1 ) proof assume A in D1 ; ::_thesis: A in D2 then ex B being set st ( B in S & ex C being thin of M st A = B \/ C ) by A12; hence A in D2 by A13; ::_thesis: verum end; assume A in D2 ; ::_thesis: A in D1 then ex B being set st ( B in S & ex C being thin of M st A = B \/ C ) by A13; hence A in D1 by A12; ::_thesis: verum end; hence D1 = D2 by TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def3 defines COM MEASURE3:def_3_:_ for X being set for S being SigmaField of X for M being sigma_Measure of S for b4 being non empty Subset-Family of X holds ( b4 = COM (S,M) iff for A being set holds ( A in b4 iff ex B being set st ( B in S & ex C being thin of M st A = B \/ C ) ) ); definition let X be set ; let S be SigmaField of X; let M be sigma_Measure of S; let A be Element of COM (S,M); func MeasPart A -> non empty Subset-Family of X means :Def4: :: MEASURE3:def 4 for B being set holds ( B in it iff ( B in S & B c= A & A \ B is thin of M ) ); existence ex b1 being non empty Subset-Family of X st for B being set holds ( B in b1 iff ( B in S & B c= A & A \ B is thin of M ) ) proof defpred S1[ set ] means for t being set st t = $1 holds ( t in S & t c= A & A \ t is thin of M ); consider D being set such that A1: for t being set holds ( t in D iff ( t in bool X & S1[t] ) ) from XBOOLE_0:sch_1(); A2: for B being set holds ( B in D iff ( B in S & B c= A & A \ B is thin of M ) ) proof let B be set ; ::_thesis: ( B in D iff ( B in S & B c= A & A \ B is thin of M ) ) ( B in S & B c= A & A \ B is thin of M implies B in D ) proof assume that A3: B in S and A4: ( B c= A & A \ B is thin of M ) ; ::_thesis: B in D for t being set st t = B holds ( t in S & t c= A & A \ t is thin of M ) by A3, A4; hence B in D by A1, A3; ::_thesis: verum end; hence ( B in D iff ( B in S & B c= A & A \ B is thin of M ) ) by A1; ::_thesis: verum end; A5: D c= bool X proof let B be set ; :: according to TARSKI:def_3 ::_thesis: ( not B in D or B in bool X ) assume B in D ; ::_thesis: B in bool X then B in S by A2; hence B in bool X ; ::_thesis: verum end; D <> {} proof consider B being set such that A6: B in S and A7: ex C being thin of M st A = B \/ C by Def3; consider C being thin of M such that A8: A = B \/ C by A7; consider E being set such that A9: E in S and A10: C c= E and A11: M . E = 0. by Def2; A \ B = C \ B by A8, XBOOLE_1:40; then A \ B c= C by XBOOLE_1:36; then A \ B c= E by A10, XBOOLE_1:1; then A12: A \ B is thin of M by A9, A11, Def2; B c= A by A8, XBOOLE_1:7; hence D <> {} by A2, A6, A12; ::_thesis: verum end; then reconsider D = D as non empty Subset-Family of X by A5; take D ; ::_thesis: for B being set holds ( B in D iff ( B in S & B c= A & A \ B is thin of M ) ) thus for B being set holds ( B in D iff ( B in S & B c= A & A \ B is thin of M ) ) by A2; ::_thesis: verum end; uniqueness for b1, b2 being non empty Subset-Family of X st ( for B being set holds ( B in b1 iff ( B in S & B c= A & A \ B is thin of M ) ) ) & ( for B being set holds ( B in b2 iff ( B in S & B c= A & A \ B is thin of M ) ) ) holds b1 = b2 proof let D1, D2 be non empty Subset-Family of X; ::_thesis: ( ( for B being set holds ( B in D1 iff ( B in S & B c= A & A \ B is thin of M ) ) ) & ( for B being set holds ( B in D2 iff ( B in S & B c= A & A \ B is thin of M ) ) ) implies D1 = D2 ) assume that A13: for B being set holds ( B in D1 iff ( B in S & B c= A & A \ B is thin of M ) ) and A14: for B being set holds ( B in D2 iff ( B in S & B c= A & A \ B is thin of M ) ) ; ::_thesis: D1 = D2 for B being set holds ( B in D1 iff B in D2 ) proof let B be set ; ::_thesis: ( B in D1 iff B in D2 ) thus ( B in D1 implies B in D2 ) ::_thesis: ( B in D2 implies B in D1 ) proof assume A15: B in D1 ; ::_thesis: B in D2 then A16: A \ B is thin of M by A13; ( B in S & B c= A ) by A13, A15; hence B in D2 by A14, A16; ::_thesis: verum end; assume A17: B in D2 ; ::_thesis: B in D1 then A18: A \ B is thin of M by A14; ( B in S & B c= A ) by A14, A17; hence B in D1 by A13, A18; ::_thesis: verum end; hence D1 = D2 by TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def4 defines MeasPart MEASURE3:def_4_:_ for X being set for S being SigmaField of X for M being sigma_Measure of S for A being Element of COM (S,M) for b5 being non empty Subset-Family of X holds ( b5 = MeasPart A iff for B being set holds ( B in b5 iff ( B in S & B c= A & A \ B is thin of M ) ) ); theorem Th15: :: MEASURE3:15 for X being set for S being SigmaField of X for M being sigma_Measure of S for F being Function of NAT,(COM (S,M)) ex G being Function of NAT,S st for n being Element of NAT holds G . n in MeasPart (F . n) proof let X be set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for F being Function of NAT,(COM (S,M)) ex G being Function of NAT,S st for n being Element of NAT holds G . n in MeasPart (F . n) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for F being Function of NAT,(COM (S,M)) ex G being Function of NAT,S st for n being Element of NAT holds G . n in MeasPart (F . n) let M be sigma_Measure of S; ::_thesis: for F being Function of NAT,(COM (S,M)) ex G being Function of NAT,S st for n being Element of NAT holds G . n in MeasPart (F . n) let F be Function of NAT,(COM (S,M)); ::_thesis: ex G being Function of NAT,S st for n being Element of NAT holds G . n in MeasPart (F . n) defpred S1[ Element of NAT , set ] means for n being Element of NAT for y being set st n = $1 & y = $2 holds y in MeasPart (F . n); A1: for t being Element of NAT ex A being Element of S st S1[t,A] proof let t be Element of NAT ; ::_thesis: ex A being Element of S st S1[t,A] set A = the Element of MeasPart (F . t); reconsider A = the Element of MeasPart (F . t) as Element of S by Def4; take A ; ::_thesis: S1[t,A] thus S1[t,A] ; ::_thesis: verum end; ex G being Function of NAT,S st for t being Element of NAT holds S1[t,G . t] from FUNCT_2:sch_3(A1); then consider G being Function of NAT,S such that A2: for t, n being Element of NAT for y being set st n = t & y = G . t holds y in MeasPart (F . n) ; take G ; ::_thesis: for n being Element of NAT holds G . n in MeasPart (F . n) thus for n being Element of NAT holds G . n in MeasPart (F . n) by A2; ::_thesis: verum end; theorem Th16: :: MEASURE3:16 for X being set for S being SigmaField of X for M being sigma_Measure of S for F being Function of NAT,(COM (S,M)) for G being Function of NAT,S ex H being Function of NAT,(bool X) st for n being Element of NAT holds H . n = (F . n) \ (G . n) proof let X be set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for F being Function of NAT,(COM (S,M)) for G being Function of NAT,S ex H being Function of NAT,(bool X) st for n being Element of NAT holds H . n = (F . n) \ (G . n) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for F being Function of NAT,(COM (S,M)) for G being Function of NAT,S ex H being Function of NAT,(bool X) st for n being Element of NAT holds H . n = (F . n) \ (G . n) let M be sigma_Measure of S; ::_thesis: for F being Function of NAT,(COM (S,M)) for G being Function of NAT,S ex H being Function of NAT,(bool X) st for n being Element of NAT holds H . n = (F . n) \ (G . n) let F be Function of NAT,(COM (S,M)); ::_thesis: for G being Function of NAT,S ex H being Function of NAT,(bool X) st for n being Element of NAT holds H . n = (F . n) \ (G . n) let G be Function of NAT,S; ::_thesis: ex H being Function of NAT,(bool X) st for n being Element of NAT holds H . n = (F . n) \ (G . n) defpred S1[ Element of NAT , set ] means for n being Element of NAT for y being set st n = $1 & y = $2 holds y = (F . n) \ (G . n); A1: for t being Element of NAT ex A being Subset of X st S1[t,A] proof let t be Element of NAT ; ::_thesis: ex A being Subset of X st S1[t,A] F . t is Element of COM (S,M) ; then reconsider A = (F . t) \ (G . t) as Subset of X by XBOOLE_1:1; take A ; ::_thesis: S1[t,A] thus S1[t,A] ; ::_thesis: verum end; ex H being Function of NAT,(bool X) st for t being Element of NAT holds S1[t,H . t] from FUNCT_2:sch_3(A1); then consider H being Function of NAT,(bool X) such that A2: for t, n being Element of NAT for y being set st n = t & y = H . t holds y = (F . n) \ (G . n) ; take H ; ::_thesis: for n being Element of NAT holds H . n = (F . n) \ (G . n) thus for n being Element of NAT holds H . n = (F . n) \ (G . n) by A2; ::_thesis: verum end; theorem Th17: :: MEASURE3:17 for X being set for S being SigmaField of X for M being sigma_Measure of S for F being Function of NAT,(bool X) st ( for n being Element of NAT holds F . n is thin of M ) holds ex G being Function of NAT,S st for n being Element of NAT holds ( F . n c= G . n & M . (G . n) = 0. ) proof let X be set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for F being Function of NAT,(bool X) st ( for n being Element of NAT holds F . n is thin of M ) holds ex G being Function of NAT,S st for n being Element of NAT holds ( F . n c= G . n & M . (G . n) = 0. ) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for F being Function of NAT,(bool X) st ( for n being Element of NAT holds F . n is thin of M ) holds ex G being Function of NAT,S st for n being Element of NAT holds ( F . n c= G . n & M . (G . n) = 0. ) let M be sigma_Measure of S; ::_thesis: for F being Function of NAT,(bool X) st ( for n being Element of NAT holds F . n is thin of M ) holds ex G being Function of NAT,S st for n being Element of NAT holds ( F . n c= G . n & M . (G . n) = 0. ) let F be Function of NAT,(bool X); ::_thesis: ( ( for n being Element of NAT holds F . n is thin of M ) implies ex G being Function of NAT,S st for n being Element of NAT holds ( F . n c= G . n & M . (G . n) = 0. ) ) defpred S1[ Element of NAT , set ] means for n being Element of NAT for y being set st n = $1 & y = $2 holds ( y in S & F . n c= y & M . y = 0. ); assume A1: for n being Element of NAT holds F . n is thin of M ; ::_thesis: ex G being Function of NAT,S st for n being Element of NAT holds ( F . n c= G . n & M . (G . n) = 0. ) A2: for t being Element of NAT ex A being Element of S st S1[t,A] proof let t be Element of NAT ; ::_thesis: ex A being Element of S st S1[t,A] F . t is thin of M by A1; then consider A being set such that A3: A in S and A4: ( F . t c= A & M . A = 0. ) by Def2; reconsider A = A as Element of S by A3; take A ; ::_thesis: S1[t,A] thus S1[t,A] by A4; ::_thesis: verum end; ex G being Function of NAT,S st for t being Element of NAT holds S1[t,G . t] from FUNCT_2:sch_3(A2); then consider G being Function of NAT,S such that A5: for t, n being Element of NAT for y being set st n = t & y = G . t holds ( y in S & F . n c= y & M . y = 0. ) ; take G ; ::_thesis: for n being Element of NAT holds ( F . n c= G . n & M . (G . n) = 0. ) thus for n being Element of NAT holds ( F . n c= G . n & M . (G . n) = 0. ) by A5; ::_thesis: verum end; theorem Th18: :: MEASURE3:18 for X being set for S being SigmaField of X for M being sigma_Measure of S for D being non empty Subset-Family of X st ( for A being set holds ( A in D iff ex B being set st ( B in S & ex C being thin of M st A = B \/ C ) ) ) holds D is SigmaField of X proof let X be set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for D being non empty Subset-Family of X st ( for A being set holds ( A in D iff ex B being set st ( B in S & ex C being thin of M st A = B \/ C ) ) ) holds D is SigmaField of X let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for D being non empty Subset-Family of X st ( for A being set holds ( A in D iff ex B being set st ( B in S & ex C being thin of M st A = B \/ C ) ) ) holds D is SigmaField of X let M be sigma_Measure of S; ::_thesis: for D being non empty Subset-Family of X st ( for A being set holds ( A in D iff ex B being set st ( B in S & ex C being thin of M st A = B \/ C ) ) ) holds D is SigmaField of X let D be non empty Subset-Family of X; ::_thesis: ( ( for A being set holds ( A in D iff ex B being set st ( B in S & ex C being thin of M st A = B \/ C ) ) ) implies D is SigmaField of X ) assume A1: for A being set holds ( A in D iff ex B being set st ( B in S & ex C being thin of M st A = B \/ C ) ) ; ::_thesis: D is SigmaField of X A2: for K being N_Sub_set_fam of X st K c= D holds union K in D proof let K be N_Sub_set_fam of X; ::_thesis: ( K c= D implies union K in D ) consider F being Function of NAT,(bool X) such that A3: K = rng F by SUPINF_2:def_8; assume A4: K c= D ; ::_thesis: union K in D A5: for n being Element of NAT holds F . n in D proof let n be Element of NAT ; ::_thesis: F . n in D F . n in K by A3, FUNCT_2:4; hence F . n in D by A4; ::_thesis: verum end; A6: for n being Element of NAT ex B being set st ( B in S & ex C being thin of M st F . n = B \/ C ) proof let n be Element of NAT ; ::_thesis: ex B being set st ( B in S & ex C being thin of M st F . n = B \/ C ) F . n in D by A5; hence ex B being set st ( B in S & ex C being thin of M st F . n = B \/ C ) by A1; ::_thesis: verum end; for n being Element of NAT holds F . n in COM (S,M) proof let n be Element of NAT ; ::_thesis: F . n in COM (S,M) ex B being set st ( B in S & ex C being thin of M st F . n = B \/ C ) by A6; hence F . n in COM (S,M) by Def3; ::_thesis: verum end; then A7: for n being set st n in NAT holds F . n in COM (S,M) ; A8: dom F = NAT by FUNCT_2:def_1; then reconsider F = F as Function of NAT,(COM (S,M)) by A7, FUNCT_2:3; consider G being Function of NAT,S such that A9: for n being Element of NAT holds G . n in MeasPart (F . n) by Th15; consider H being Function of NAT,(bool X) such that A10: for n being Element of NAT holds H . n = (F . n) \ (G . n) by Th16; A11: for n being Element of NAT holds ( G . n in S & G . n c= F . n & (F . n) \ (G . n) is thin of M ) proof let n be Element of NAT ; ::_thesis: ( G . n in S & G . n c= F . n & (F . n) \ (G . n) is thin of M ) G . n in MeasPart (F . n) by A9; hence ( G . n in S & G . n c= F . n & (F . n) \ (G . n) is thin of M ) by Def4; ::_thesis: verum end; for n being Element of NAT holds H . n is thin of M proof let n be Element of NAT ; ::_thesis: H . n is thin of M (F . n) \ (G . n) is thin of M by A11; hence H . n is thin of M by A10; ::_thesis: verum end; then consider L being Function of NAT,S such that A12: for n being Element of NAT holds ( H . n c= L . n & M . (L . n) = 0. ) by Th17; ex B being set st ( B in S & ex C being thin of M st union K = B \/ C ) proof set B = union (rng G); take union (rng G) ; ::_thesis: ( union (rng G) in S & ex C being thin of M st union K = (union (rng G)) \/ C ) A13: union (rng G) c= union (rng F) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (rng G) or x in union (rng F) ) assume x in union (rng G) ; ::_thesis: x in union (rng F) then consider Z being set such that A14: x in Z and A15: Z in rng G by TARSKI:def_4; dom G = NAT by FUNCT_2:def_1; then consider n being set such that A16: n in NAT and A17: Z = G . n by A15, FUNCT_1:def_3; reconsider n = n as Element of NAT by A16; set P = F . n; A18: G . n c= F . n by A11; ex P being set st ( P in rng F & x in P ) proof take F . n ; ::_thesis: ( F . n in rng F & x in F . n ) thus ( F . n in rng F & x in F . n ) by A8, A14, A17, A18, FUNCT_1:def_3; ::_thesis: verum end; hence x in union (rng F) by TARSKI:def_4; ::_thesis: verum end; ex C being thin of M st union K = (union (rng G)) \/ C proof for A being set st A in rng L holds A is measure_zero of M proof let A be set ; ::_thesis: ( A in rng L implies A is measure_zero of M ) assume A19: A in rng L ; ::_thesis: A is measure_zero of M dom L = NAT by FUNCT_2:def_1; then A20: ex n being set st ( n in NAT & A = L . n ) by A19, FUNCT_1:def_3; rng L c= S by MEASURE2:def_1; then reconsider A = A as Element of S by A19; M . A = 0. by A12, A20; hence A is measure_zero of M by MEASURE1:def_7; ::_thesis: verum end; then union (rng L) is measure_zero of M by MEASURE2:14; then A21: M . (union (rng L)) = 0. by MEASURE1:def_7; set C = (union K) \ (union (rng G)); A22: union K = ((union K) \ (union (rng G))) \/ ((union (rng F)) /\ (union (rng G))) by A3, XBOOLE_1:51 .= (union (rng G)) \/ ((union K) \ (union (rng G))) by A13, XBOOLE_1:28 ; reconsider C = (union K) \ (union (rng G)) as Subset of X ; A23: C c= union (rng H) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C or x in union (rng H) ) assume A24: x in C ; ::_thesis: x in union (rng H) then x in union (rng F) by A3, XBOOLE_0:def_5; then consider Z being set such that A25: x in Z and A26: Z in rng F by TARSKI:def_4; consider n being set such that A27: n in NAT and A28: Z = F . n by A8, A26, FUNCT_1:def_3; reconsider n = n as Element of NAT by A27; A29: not x in union (rng G) by A24, XBOOLE_0:def_5; not x in G . n proof dom G = NAT by FUNCT_2:def_1; then A30: G . n in rng G by FUNCT_1:def_3; assume x in G . n ; ::_thesis: contradiction hence contradiction by A29, A30, TARSKI:def_4; ::_thesis: verum end; then A31: x in (F . n) \ (G . n) by A25, A28, XBOOLE_0:def_5; ex Z being set st ( x in Z & Z in rng H ) proof take H . n ; ::_thesis: ( x in H . n & H . n in rng H ) dom H = NAT by FUNCT_2:def_1; hence ( x in H . n & H . n in rng H ) by A10, A31, FUNCT_1:def_3; ::_thesis: verum end; hence x in union (rng H) by TARSKI:def_4; ::_thesis: verum end; union (rng H) c= union (rng L) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (rng H) or x in union (rng L) ) assume x in union (rng H) ; ::_thesis: x in union (rng L) then consider Z being set such that A32: x in Z and A33: Z in rng H by TARSKI:def_4; dom H = NAT by FUNCT_2:def_1; then consider n being set such that A34: n in NAT and A35: Z = H . n by A33, FUNCT_1:def_3; reconsider n = n as Element of NAT by A34; n in dom L by A34, FUNCT_2:def_1; then A36: L . n in rng L by FUNCT_1:def_3; H . n c= L . n by A12; hence x in union (rng L) by A32, A35, A36, TARSKI:def_4; ::_thesis: verum end; then C c= union (rng L) by A23, XBOOLE_1:1; then C is thin of M by A21, Def2; then consider C being thin of M such that A37: union K = (union (rng G)) \/ C by A22; take C ; ::_thesis: union K = (union (rng G)) \/ C thus union K = (union (rng G)) \/ C by A37; ::_thesis: verum end; hence ( union (rng G) in S & ex C being thin of M st union K = (union (rng G)) \/ C ) ; ::_thesis: verum end; hence union K in D by A1; ::_thesis: verum end; for A being set st A in D holds X \ A in D proof let A be set ; ::_thesis: ( A in D implies X \ A in D ) assume A38: A in D ; ::_thesis: X \ A in D ex Q being set st ( Q in S & ex W being thin of M st X \ A = Q \/ W ) proof consider B being set such that A39: B in S and A40: ex C being thin of M st A = B \/ C by A1, A38; set P = X \ B; consider C being thin of M such that A41: A = B \/ C by A40; consider G being set such that A42: G in S and A43: C c= G and A44: M . G = 0. by Def2; set Q = (X \ B) \ G; A45: X \ A = (X \ B) \ C by A41, XBOOLE_1:41; A46: ex W being thin of M st X \ A = ((X \ B) \ G) \/ W proof set W = (X \ B) /\ (G \ C); (X \ B) /\ (G \ C) c= X \ B by XBOOLE_1:17; then reconsider W = (X \ B) /\ (G \ C) as Subset of X by XBOOLE_1:1; reconsider W = W as thin of M by A42, A44, Def2; take W ; ::_thesis: X \ A = ((X \ B) \ G) \/ W thus X \ A = ((X \ B) \ G) \/ W by A43, A45, XBOOLE_1:117; ::_thesis: verum end; take (X \ B) \ G ; ::_thesis: ( (X \ B) \ G in S & ex W being thin of M st X \ A = ((X \ B) \ G) \/ W ) X \ B in S by A39, MEASURE1:def_1; hence ( (X \ B) \ G in S & ex W being thin of M st X \ A = ((X \ B) \ G) \/ W ) by A42, A46, MEASURE1:6; ::_thesis: verum end; hence X \ A in D by A1; ::_thesis: verum end; then reconsider D9 = D as non empty compl-closed sigma-additive Subset-Family of X by A2, MEASURE1:def_1, MEASURE1:def_5; D9 is SigmaField of X ; hence D is SigmaField of X ; ::_thesis: verum end; registration let X be set ; let S be SigmaField of X; let M be sigma_Measure of S; cluster COM (S,M) -> non empty compl-closed sigma-additive ; coherence ( COM (S,M) is sigma-additive & COM (S,M) is compl-closed & not COM (S,M) is empty ) proof for A being set holds ( A in COM (S,M) iff ex B being set st ( B in S & ex C being thin of M st A = B \/ C ) ) by Def3; hence ( COM (S,M) is sigma-additive & COM (S,M) is compl-closed & not COM (S,M) is empty ) by Th18; ::_thesis: verum end; end; theorem Th19: :: MEASURE3:19 for X being set for S being SigmaField of X for M being sigma_Measure of S for B1, B2 being set st B1 in S & B2 in S holds for C1, C2 being thin of M st B1 \/ C1 = B2 \/ C2 holds M . B1 = M . B2 proof let X be set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for B1, B2 being set st B1 in S & B2 in S holds for C1, C2 being thin of M st B1 \/ C1 = B2 \/ C2 holds M . B1 = M . B2 let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for B1, B2 being set st B1 in S & B2 in S holds for C1, C2 being thin of M st B1 \/ C1 = B2 \/ C2 holds M . B1 = M . B2 let M be sigma_Measure of S; ::_thesis: for B1, B2 being set st B1 in S & B2 in S holds for C1, C2 being thin of M st B1 \/ C1 = B2 \/ C2 holds M . B1 = M . B2 let B1, B2 be set ; ::_thesis: ( B1 in S & B2 in S implies for C1, C2 being thin of M st B1 \/ C1 = B2 \/ C2 holds M . B1 = M . B2 ) assume A1: ( B1 in S & B2 in S ) ; ::_thesis: for C1, C2 being thin of M st B1 \/ C1 = B2 \/ C2 holds M . B1 = M . B2 let C1, C2 be thin of M; ::_thesis: ( B1 \/ C1 = B2 \/ C2 implies M . B1 = M . B2 ) assume A2: B1 \/ C1 = B2 \/ C2 ; ::_thesis: M . B1 = M . B2 then A3: B1 c= B2 \/ C2 by XBOOLE_1:7; A4: B2 c= B1 \/ C1 by A2, XBOOLE_1:7; consider D1 being set such that A5: D1 in S and A6: C1 c= D1 and A7: M . D1 = 0. by Def2; A8: B1 \/ C1 c= B1 \/ D1 by A6, XBOOLE_1:9; consider D2 being set such that A9: D2 in S and A10: C2 c= D2 and A11: M . D2 = 0. by Def2; A12: B2 \/ C2 c= B2 \/ D2 by A10, XBOOLE_1:9; reconsider B1 = B1, B2 = B2, D1 = D1, D2 = D2 as Element of S by A1, A5, A9; A13: ( M . (B1 \/ D1) <= (M . B1) + (M . D1) & (M . B1) + (M . D1) = M . B1 ) by A7, MEASURE1:33, XXREAL_3:4; M . B2 <= M . (B1 \/ D1) by A4, A8, MEASURE1:31, XBOOLE_1:1; then A14: M . B2 <= M . B1 by A13, XXREAL_0:2; A15: ( M . (B2 \/ D2) <= (M . B2) + (M . D2) & (M . B2) + (M . D2) = M . B2 ) by A11, MEASURE1:33, XXREAL_3:4; M . B1 <= M . (B2 \/ D2) by A3, A12, MEASURE1:31, XBOOLE_1:1; then M . B1 <= M . B2 by A15, XXREAL_0:2; hence M . B1 = M . B2 by A14, XXREAL_0:1; ::_thesis: verum end; definition let X be set ; let S be SigmaField of X; let M be sigma_Measure of S; func COM M -> sigma_Measure of (COM (S,M)) means :Def5: :: MEASURE3:def 5 for B being set st B in S holds for C being thin of M holds it . (B \/ C) = M . B; existence ex b1 being sigma_Measure of (COM (S,M)) st for B being set st B in S holds for C being thin of M holds b1 . (B \/ C) = M . B proof set B = {} ; defpred S1[ set , set ] means for x, y being set st x in COM (S,M) & x = $1 & y = $2 holds for B being set st B in S holds for C being thin of M st x = B \/ C holds y = M . B; A1: ex B1 being set st ( B1 in S & {} c= B1 & M . B1 = 0. ) proof take {} ; ::_thesis: ( {} in S & {} c= {} & M . {} = 0. ) thus ( {} in S & {} c= {} & M . {} = 0. ) by PROB_1:4, VALUED_0:def_19; ::_thesis: verum end; {} is Subset of X by XBOOLE_1:2; then reconsider C = {} as thin of M by A1, Def2; A2: for x being set st x in COM (S,M) holds ex y being set st ( y in ExtREAL & S1[x,y] ) proof let x be set ; ::_thesis: ( x in COM (S,M) implies ex y being set st ( y in ExtREAL & S1[x,y] ) ) assume x in COM (S,M) ; ::_thesis: ex y being set st ( y in ExtREAL & S1[x,y] ) then consider B being set such that A3: ( B in S & ex C being thin of M st x = B \/ C ) by Def3; take M . B ; ::_thesis: ( M . B in ExtREAL & S1[x,M . B] ) thus ( M . B in ExtREAL & S1[x,M . B] ) by A3, Th19; ::_thesis: verum end; consider comM being Function of (COM (S,M)),ExtREAL such that A4: for x being set st x in COM (S,M) holds S1[x,comM . x] from FUNCT_2:sch_1(A2); A5: for B being set st B in S holds for C being thin of M holds comM . (B \/ C) = M . B proof let B be set ; ::_thesis: ( B in S implies for C being thin of M holds comM . (B \/ C) = M . B ) assume A6: B in S ; ::_thesis: for C being thin of M holds comM . (B \/ C) = M . B let C be thin of M; ::_thesis: comM . (B \/ C) = M . B B \/ C in COM (S,M) by A6, Def3; hence comM . (B \/ C) = M . B by A4, A6; ::_thesis: verum end; A7: for F being Sep_Sequence of (COM (S,M)) holds SUM (comM * F) = comM . (union (rng F)) proof let F be Sep_Sequence of (COM (S,M)); ::_thesis: SUM (comM * F) = comM . (union (rng F)) consider G being Function of NAT,S such that A8: for n being Element of NAT holds G . n in MeasPart (F . n) by Th15; consider H being Function of NAT,(bool X) such that A9: for n being Element of NAT holds H . n = (F . n) \ (G . n) by Th16; A10: for n being Element of NAT holds ( G . n in S & G . n c= F . n & (F . n) \ (G . n) is thin of M ) proof let n be Element of NAT ; ::_thesis: ( G . n in S & G . n c= F . n & (F . n) \ (G . n) is thin of M ) G . n in MeasPart (F . n) by A8; hence ( G . n in S & G . n c= F . n & (F . n) \ (G . n) is thin of M ) by Def4; ::_thesis: verum end; for n being Element of NAT holds H . n is thin of M proof let n be Element of NAT ; ::_thesis: H . n is thin of M (F . n) \ (G . n) is thin of M by A10; hence H . n is thin of M by A9; ::_thesis: verum end; then consider L being Function of NAT,S such that A11: for n being Element of NAT holds ( H . n c= L . n & M . (L . n) = 0. ) by Th17; A12: for n, m being set st n <> m holds G . n misses G . m proof let n, m be set ; ::_thesis: ( n <> m implies G . n misses G . m ) A13: dom F = NAT by FUNCT_2:def_1 .= dom G by FUNCT_2:def_1 ; for n being set holds G . n c= F . n proof let n be set ; ::_thesis: G . n c= F . n percases ( n in dom F or not n in dom F ) ; suppose n in dom F ; ::_thesis: G . n c= F . n hence G . n c= F . n by A10; ::_thesis: verum end; supposeA14: not n in dom F ; ::_thesis: G . n c= F . n then F . n = {} by FUNCT_1:def_2 .= G . n by A13, A14, FUNCT_1:def_2 ; hence G . n c= F . n ; ::_thesis: verum end; end; end; then A15: ( G . n c= F . n & G . m c= F . m ) ; assume n <> m ; ::_thesis: G . n misses G . m then F . n misses F . m by PROB_2:def_2; then (F . n) /\ (F . m) = {} by XBOOLE_0:def_7; then (G . n) /\ (G . m) = {} by A15, XBOOLE_1:3, XBOOLE_1:27; hence G . n misses G . m by XBOOLE_0:def_7; ::_thesis: verum end; consider B being set such that A16: B = union (rng G) ; A17: dom F = NAT by FUNCT_2:def_1; A18: B c= union (rng F) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in union (rng F) ) assume x in B ; ::_thesis: x in union (rng F) then consider Z being set such that A19: x in Z and A20: Z in rng G by A16, TARSKI:def_4; dom G = NAT by FUNCT_2:def_1; then consider n being set such that A21: n in NAT and A22: Z = G . n by A20, FUNCT_1:def_3; reconsider n = n as Element of NAT by A21; set P = F . n; A23: G . n c= F . n by A10; ex P being set st ( P in rng F & x in P ) proof take F . n ; ::_thesis: ( F . n in rng F & x in F . n ) thus ( F . n in rng F & x in F . n ) by A17, A19, A22, A23, FUNCT_1:def_3; ::_thesis: verum end; hence x in union (rng F) by TARSKI:def_4; ::_thesis: verum end; A24: ex C being thin of M st union (rng F) = B \/ C proof for A being set st A in rng L holds A is measure_zero of M proof let A be set ; ::_thesis: ( A in rng L implies A is measure_zero of M ) assume A25: A in rng L ; ::_thesis: A is measure_zero of M dom L = NAT by FUNCT_2:def_1; then A26: ex n being set st ( n in NAT & A = L . n ) by A25, FUNCT_1:def_3; rng L c= S by MEASURE2:def_1; then reconsider A = A as Element of S by A25; M . A = 0. by A11, A26; hence A is measure_zero of M by MEASURE1:def_7; ::_thesis: verum end; then union (rng L) is measure_zero of M by MEASURE2:14; then A27: M . (union (rng L)) = 0. by MEASURE1:def_7; set C = (union (rng F)) \ B; A28: union (rng F) = ((union (rng F)) \ B) \/ ((union (rng F)) /\ B) by XBOOLE_1:51 .= B \/ ((union (rng F)) \ B) by A18, XBOOLE_1:28 ; reconsider C = (union (rng F)) \ B as Subset of X ; A29: C c= union (rng H) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C or x in union (rng H) ) assume A30: x in C ; ::_thesis: x in union (rng H) then x in union (rng F) by XBOOLE_0:def_5; then consider Z being set such that A31: x in Z and A32: Z in rng F by TARSKI:def_4; consider n being set such that A33: n in NAT and A34: Z = F . n by A17, A32, FUNCT_1:def_3; reconsider n = n as Element of NAT by A33; A35: not x in union (rng G) by A16, A30, XBOOLE_0:def_5; not x in G . n proof dom G = NAT by FUNCT_2:def_1; then A36: G . n in rng G by FUNCT_1:def_3; assume x in G . n ; ::_thesis: contradiction hence contradiction by A35, A36, TARSKI:def_4; ::_thesis: verum end; then A37: x in (F . n) \ (G . n) by A31, A34, XBOOLE_0:def_5; ex Z being set st ( x in Z & Z in rng H ) proof take H . n ; ::_thesis: ( x in H . n & H . n in rng H ) dom H = NAT by FUNCT_2:def_1; hence ( x in H . n & H . n in rng H ) by A9, A37, FUNCT_1:def_3; ::_thesis: verum end; hence x in union (rng H) by TARSKI:def_4; ::_thesis: verum end; union (rng H) c= union (rng L) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (rng H) or x in union (rng L) ) assume x in union (rng H) ; ::_thesis: x in union (rng L) then consider Z being set such that A38: x in Z and A39: Z in rng H by TARSKI:def_4; dom H = NAT by FUNCT_2:def_1; then consider n being set such that A40: n in NAT and A41: Z = H . n by A39, FUNCT_1:def_3; reconsider n = n as Element of NAT by A40; n in dom L by A40, FUNCT_2:def_1; then A42: L . n in rng L by FUNCT_1:def_3; H . n c= L . n by A11; hence x in union (rng L) by A38, A41, A42, TARSKI:def_4; ::_thesis: verum end; then C c= union (rng L) by A29, XBOOLE_1:1; then C is thin of M by A27, Def2; then consider C being thin of M such that A43: union (rng F) = B \/ C by A28; take C ; ::_thesis: union (rng F) = B \/ C thus union (rng F) = B \/ C by A43; ::_thesis: verum end; reconsider G = G as Sep_Sequence of S by A12, PROB_2:def_2; A44: for n being Element of NAT holds comM . (F . n) = M . (G . n) proof let n be Element of NAT ; ::_thesis: comM . (F . n) = M . (G . n) (F . n) \ (G . n) is thin of M by A10; then consider C being thin of M such that A45: C = (F . n) \ (G . n) ; F . n = ((F . n) /\ (G . n)) \/ ((F . n) \ (G . n)) by XBOOLE_1:51 .= (G . n) \/ C by A10, A45, XBOOLE_1:28 ; hence comM . (F . n) = M . (G . n) by A5; ::_thesis: verum end; A46: for n being Element of NAT holds (comM * F) . n = (M * G) . n proof let n be Element of NAT ; ::_thesis: (comM * F) . n = (M * G) . n (comM * F) . n = comM . (F . n) by FUNCT_2:15 .= M . (G . n) by A44 .= (M * G) . n by FUNCT_2:15 ; hence (comM * F) . n = (M * G) . n ; ::_thesis: verum end; then for n being Element of NAT holds (M * G) . n <= (comM * F) . n ; then A47: SUM (M * G) <= SUM (comM * F) by SUPINF_2:43; for n being Element of NAT holds (comM * F) . n <= (M * G) . n by A46; then SUM (comM * F) <= SUM (M * G) by SUPINF_2:43; then ( SUM (M * G) = M . (union (rng G)) & SUM (comM * F) = SUM (M * G) ) by A47, MEASURE1:def_6, XXREAL_0:1; hence SUM (comM * F) = comM . (union (rng F)) by A5, A16, A24; ::_thesis: verum end; A48: for x being Element of COM (S,M) holds 0. <= comM . x proof let x be Element of COM (S,M); ::_thesis: 0. <= comM . x consider B being set such that A49: B in S and A50: ex C being thin of M st x = B \/ C by Def3; reconsider B = B as Element of S by A49; comM . x = M . B by A4, A50; hence 0. <= comM . x by MEASURE1:def_2; ::_thesis: verum end; {} = {} \/ C ; then comM . {} = M . {} by A5, PROB_1:4 .= 0. by VALUED_0:def_19 ; then reconsider comM = comM as sigma_Measure of (COM (S,M)) by A48, A7, MEASURE1:def_2, MEASURE1:def_6, VALUED_0:def_19; take comM ; ::_thesis: for B being set st B in S holds for C being thin of M holds comM . (B \/ C) = M . B thus for B being set st B in S holds for C being thin of M holds comM . (B \/ C) = M . B by A5; ::_thesis: verum end; uniqueness for b1, b2 being sigma_Measure of (COM (S,M)) st ( for B being set st B in S holds for C being thin of M holds b1 . (B \/ C) = M . B ) & ( for B being set st B in S holds for C being thin of M holds b2 . (B \/ C) = M . B ) holds b1 = b2 proof let M1, M2 be sigma_Measure of (COM (S,M)); ::_thesis: ( ( for B being set st B in S holds for C being thin of M holds M1 . (B \/ C) = M . B ) & ( for B being set st B in S holds for C being thin of M holds M2 . (B \/ C) = M . B ) implies M1 = M2 ) assume that A51: for B being set st B in S holds for C being thin of M holds M1 . (B \/ C) = M . B and A52: for B being set st B in S holds for C being thin of M holds M2 . (B \/ C) = M . B ; ::_thesis: M1 = M2 for x being set st x in COM (S,M) holds M1 . x = M2 . x proof let x be set ; ::_thesis: ( x in COM (S,M) implies M1 . x = M2 . x ) assume x in COM (S,M) ; ::_thesis: M1 . x = M2 . x then consider B being set such that A53: ( B in S & ex C being thin of M st x = B \/ C ) by Def3; M1 . x = M . B by A51, A53 .= M2 . x by A52, A53 ; hence M1 . x = M2 . x ; ::_thesis: verum end; hence M1 = M2 by FUNCT_2:12; ::_thesis: verum end; end; :: deftheorem Def5 defines COM MEASURE3:def_5_:_ for X being set for S being SigmaField of X for M being sigma_Measure of S for b4 being sigma_Measure of (COM (S,M)) holds ( b4 = COM M iff for B being set st B in S holds for C being thin of M holds b4 . (B \/ C) = M . B ); theorem :: MEASURE3:20 for X being set for S being SigmaField of X for M being sigma_Measure of S holds COM M is_complete COM (S,M) proof let X be set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S holds COM M is_complete COM (S,M) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S holds COM M is_complete COM (S,M) let M be sigma_Measure of S; ::_thesis: COM M is_complete COM (S,M) for A being Subset of X for B being set st B in COM (S,M) & A c= B & (COM M) . B = 0. holds A in COM (S,M) proof let A be Subset of X; ::_thesis: for B being set st B in COM (S,M) & A c= B & (COM M) . B = 0. holds A in COM (S,M) let B be set ; ::_thesis: ( B in COM (S,M) & A c= B & (COM M) . B = 0. implies A in COM (S,M) ) assume A1: B in COM (S,M) ; ::_thesis: ( not A c= B or not (COM M) . B = 0. or A in COM (S,M) ) assume that A2: A c= B and A3: (COM M) . B = 0. ; ::_thesis: A in COM (S,M) ex B1 being set st ( B1 in S & ex C1 being thin of M st A = B1 \/ C1 ) proof take {} ; ::_thesis: ( {} in S & ex C1 being thin of M st A = {} \/ C1 ) consider B2 being set such that A4: B2 in S and A5: ex C2 being thin of M st B = B2 \/ C2 by A1, Def3; A6: M . B2 = 0. by A3, A4, A5, Def5; consider C2 being thin of M such that A7: B = B2 \/ C2 by A5; set C1 = (A /\ B2) \/ (A /\ C2); consider D2 being set such that A8: D2 in S and A9: C2 c= D2 and A10: M . D2 = 0. by Def2; set O = B2 \/ D2; A /\ C2 c= C2 by XBOOLE_1:17; then A11: ( A /\ B2 c= B2 & A /\ C2 c= D2 ) by A9, XBOOLE_1:1, XBOOLE_1:17; ex O being set st ( O in S & (A /\ B2) \/ (A /\ C2) c= O & M . O = 0. ) proof reconsider B2 = B2, D2 = D2 as Element of S by A4, A8; reconsider O1 = B2 \/ D2 as Element of S by A4, A8, FINSUB_1:def_1; take B2 \/ D2 ; ::_thesis: ( B2 \/ D2 in S & (A /\ B2) \/ (A /\ C2) c= B2 \/ D2 & M . (B2 \/ D2) = 0. ) ( M . (B2 \/ D2) <= 0. + 0. & 0. <= M . O1 ) by A6, A10, MEASURE1:33, MEASURE1:def_2; hence ( B2 \/ D2 in S & (A /\ B2) \/ (A /\ C2) c= B2 \/ D2 & M . (B2 \/ D2) = 0. ) by A11, XBOOLE_1:13, XXREAL_0:1; ::_thesis: verum end; then A12: (A /\ B2) \/ (A /\ C2) is thin of M by Def2; A = A /\ (B2 \/ C2) by A2, A7, XBOOLE_1:28 .= {} \/ ((A /\ B2) \/ (A /\ C2)) by XBOOLE_1:23 ; hence ( {} in S & ex C1 being thin of M st A = {} \/ C1 ) by A12, PROB_1:4; ::_thesis: verum end; hence A in COM (S,M) by Def3; ::_thesis: verum end; hence COM M is_complete COM (S,M) by Def1; ::_thesis: verum end;