:: The Relevance of Measure and Probability and Definition of Completeness
:: of Probability
::  by Bo Zhang , Hiroshi Yamazaki and Yatsuka Nakamura
::
:: Received November 23, 2005
:: Copyright (c) 2005-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SUBSET_1, PROB_1, XBOOLE_0, TARSKI, FUNCT_1, RELAT_1,
      NAT_1, PROB_2, FUNCOP_1, FUNCT_7, CARD_1, XXREAL_0, ARYTM_3, ZFMISC_1,
      CARD_3, EQREL_1, RPR_1, ARYTM_1, SERIES_1, SEQ_2, ORDINAL2, PROB_3,
      SUPINF_2, REAL_1, XXREAL_2, SUPINF_1, ORDINAL1, MEASURE1, MEASURE6,
      VALUED_0, SETFAM_1, MEASURE3, PROB_4, SEQ_4;
 notations TARSKI, XBOOLE_0, REAL_1, CARD_3, ORDINAL1, MEASURE3, SUPINF_2,
      XXREAL_0, XXREAL_2, NAT_1, SEQ_2, SETFAM_1, FUNCT_1, RELSET_1, SUBSET_1,
      NUMBERS, SUPINF_1, PARTFUN1, FUNCT_2, FUNCT_7, PROB_1, PROB_3, MEASURE1,
      FUNCOP_1, SEQM_3, SERIES_1, RINFSUP1, ZFMISC_1, MEASURE6, PROB_2;
 constructors REAL_1, SERIES_1, MEASURE3, MEASURE6, PARTFUN3, KURATO_0,
      RINFSUP1, PROB_3, SEQ_1, SUPINF_1, FUNCT_7, RELSET_1, COMSEQ_2;
 registrations SUBSET_1, RELAT_1, ORDINAL1, FUNCT_2, NUMBERS, XXREAL_0,
      XREAL_0, NAT_1, MEMBERED, MEASURE1, MEASURE3, VALUED_0, SEQ_2, SEQ_4,
      FUNCT_7, PROB_1, RELSET_1, PROB_3;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
 definitions TARSKI, XBOOLE_0, SERIES_1, SUBSET_1, PROB_3;
 theorems FUNCT_1, FUNCT_2, SEQ_1, SEQ_2, XREAL_1, NAT_1, TARSKI, XBOOLE_0,
      XBOOLE_1, PROB_2, RINFSUP1, SUPINF_2, SEQM_3, CARD_3, SETLIM_1, PROB_1,
      SERIES_1, PROB_3, MEASURE1, MEASURE3, MEASURE6, ZFMISC_1, XXREAL_0,
      ORDINAL1, NUMBERS, XXREAL_2, FUNCT_7, DYNKIN, VALUED_0, FUNCOP_1,
      RELAT_1;
 schemes FUNCT_2, NAT_1, XBOOLE_0;

begin

reserve n,m,k for Element of NAT,
  x,X for set,
  A1 for SetSequence of X,
  Si for SigmaField of X,
  XSeq for SetSequence of Si;
reserve Omega for non empty set,
  Sigma for SigmaField of Omega,
  ASeq for SetSequence of Sigma,
  P for Probability of Sigma;

Lm1: for A,B,C being set holds C c= B implies A \ C = (A \ B) \/ (A /\ (B \ C)
)
proof
  let A,B,C be set;
  assume
A1: C c= B;
  thus A \ C c= (A \ B) \/ (A /\ (B \ C))
  proof
    let x be set;
    assume x in A \ C;
    then x in A & not x in B or x in A & x in B & not x in C by XBOOLE_0:def 5;
    then x in A \ B or x in A & x in B \ C by XBOOLE_0:def 5;
    then x in A \ B or x in A /\ (B \ C) by XBOOLE_0:def 4;
    hence thesis by XBOOLE_0:def 3;
  end;
  let x be set;
  assume x in (A \ B) \/ (A /\ (B \ C));
  then x in A \ B or x in (A /\ (B \ C)) by XBOOLE_0:def 3;
  then
A2: x in A \ B or x in A & x in B \ C by XBOOLE_0:def 4;
  then not x in C by A1,XBOOLE_0:def 5;
  hence thesis by A2,XBOOLE_0:def 5;
end;

definition
  let X,Si,XSeq,n;
  redefine func XSeq.n -> Element of Si;
  coherence
  proof
    thus XSeq.n is Element of Si;
  end;
end;

theorem Th1:
  rng XSeq c= Si
proof
  let x;
  assume x in rng XSeq;
  then ex n st x = XSeq.n by SETLIM_1:4;
  hence thesis;
end;

theorem Th2:
  for f being Function holds f is SetSequence of Si iff f is Function of NAT,Si
proof
  let f be Function;
  thus f is SetSequence of Si implies f is Function of NAT,Si
  proof
    assume f is SetSequence of Si;
    then reconsider f as SetSequence of Si;
    rng f c= Si & dom f = NAT by Th1,FUNCT_2:def 1;
    hence thesis by FUNCT_2:2;
  end;
  assume
A1: f is Function of NAT,Si;
  then reconsider f as SetSequence of X by FUNCT_2:7;
  f is SetSequence of Si by A1;
  hence thesis;
end;

scheme
  LambdaSigmaSSeq { X() -> set, Si() -> SigmaField of X(), F(set) -> Element
  of Si() } : ex f being SetSequence of Si() st for n holds f.n = F(n) proof
  ex f being SetSequence of X() st for n holds f.n = F(n) from FUNCT_2:sch
  4;
  then consider f be SetSequence of X() such that
A1: for n holds f.n = F(n);
  for n being Nat holds f.n in Si()
  proof
    let n be Nat;
    n in NAT by ORDINAL1:def 12;
    then f.n = F(n) by A1;
    hence thesis;
  end;
  then rng f c= Si() by NAT_1:52;
  then reconsider f as SetSequence of Si() by RELAT_1:def 19;
  take f;
  thus thesis by A1;
end;

registration
  let X;
  cluster disjoint_valued for SetSequence of X;
  existence
  proof
    take A1 = NAT --> {}X;
    for m,n being Nat st m <> n holds A1.m misses A1.n
    proof
      let m,n be Nat;
      m in NAT by ORDINAL1:def 12;
      then A1.m = {} by FUNCOP_1:7;
      hence thesis by XBOOLE_1:65;
    end;
    hence thesis by PROB_3:def 4;
  end;
end;

registration
  let X,Si;
  cluster disjoint_valued for SetSequence of Si;
  existence
  proof
    reconsider MSi = Si as SigmaField of X;
    set f = the disjoint_valued Function of NAT,MSi;
    reconsider f as SetSequence of Si by Th2;
    take f;
    thus thesis;
  end;
end;

theorem Th3:
  for A, B being Subset of X st A misses B holds (A,B) followed_by
  {} is disjoint_valued
proof
  let A,B be Subset of X;
  reconsider A1 = (A,B) followed_by {}X as SetSequence of X;
  assume
A1: A misses B;
  A1 is disjoint_valued
  proof
A2: A1.1 = B by FUNCT_7:123;
    let m,n be Nat such that
A3: m <> n;
A4: A1.0 = A by FUNCT_7:122;
    per cases;
    suppose
A5:   m = 0;
      then n >= 1 by A3,NAT_1:14;
      then
A6:   n + 1 > 1 by NAT_1:13;
      per cases by A6,NAT_1:22;
      suppose
        n > 1;
        then A1.n = {} by FUNCT_7:124;
        hence thesis by XBOOLE_1:65;
      end;
      suppose
        n = 1;
        hence thesis by A1,A4,A5,FUNCT_7:123;
      end;
    end;
    suppose
A7:   m <> 0 & m = 1;
      n >= 1 or n <= 1;
      then
A8:   n + 1 > 1 or n < 1 + 1 by NAT_1:13;
      per cases by A3,A7,A8,NAT_1:14,22;
      suppose
        n > 1;
        then A1.n = {} by FUNCT_7:124;
        hence thesis by XBOOLE_1:65;
      end;
      suppose
        n = 0;
        hence thesis by A1,A4,A2,A7;
      end;
    end;
    suppose
A9:   m <> 0 & m <> 1;
      then m >= 1 by NAT_1:14;
      then m +1 > 1 by NAT_1:13;
      then A1.m = {} by A9,FUNCT_7:124,NAT_1:22;
      hence thesis by XBOOLE_1:65;
    end;
  end;
  hence thesis;
end;

theorem Th4:
  for S being non empty set holds S is SigmaField of X iff S c=
  bool X & (for A1 being SetSequence of X st rng A1 c= S holds Union A1 in S) &
  for A being Subset of X st A in S holds A` in S
proof
  let S be non empty set;
  thus S is SigmaField of X implies S c= bool X & (for A1 being SetSequence of
X st rng A1 c= S holds Union A1 in S) & for A being Subset of X st A in S holds
  A` in S
  proof
    assume S is SigmaField of X;
    then reconsider S as SigmaField of X;
    for A1 being SetSequence of X st rng A1 c= S holds Union A1 in S
    proof
      let A1 be SetSequence of X;
      assume rng A1 c= S;
      then reconsider A1 as SetSequence of S by RELAT_1:def 19;
      Union A1 in S by PROB_1:17;
      hence thesis;
    end;
    hence thesis by PROB_1:15;
  end;
  assume that
A1: S c= bool X and
A2: for A1 being SetSequence of X st rng A1 c= S holds Union A1 in S and
A3: for A being Subset of X st A in S holds A` in S;
  for A1 being SetSequence of X st rng A1 c= S holds Intersection A1 in S
  proof
    let A1 be SetSequence of X such that
A4: rng A1 c= S;
    for n being Nat holds (Complement A1).n in S
    proof
      let n be Nat;
      reconsider n1=n as Element of NAT by ORDINAL1:def 12;
      A1.n in rng A1 by NAT_1:51;
      then (A1.n1)` in S by A3,A4;
      hence thesis by PROB_1:def 2;
    end;
    then rng Complement A1 c= S by NAT_1:52;
    then (Union Complement A1)` in S by A2,A3;
    hence thesis by PROB_1:def 3;
  end;
  hence thesis by A1,A3,PROB_1:15;
end;

theorem Th5:
  for A,B being Event of Sigma holds P.(A \ B) = P.(A \/ B) - P.B
proof
  let A,B be Event of Sigma;
  P.(A \/ B) - P.B = P.B + P.(A \ B) - P.B by PROB_1:36;
  hence thesis;
end;

theorem Th6:
  for A,B being Event of Sigma st A c= B & P.B = 0 holds P.A = 0
proof
  let A,B be Event of Sigma;
  assume A c= B & P.B = 0;
  then P.A <= 0 by PROB_1:34;
  hence thesis by PROB_1:def 8;
end;

theorem Th7:
  (for n holds P.(ASeq.n) = 0) iff P.(Union ASeq) = 0
proof
  hereby
    assume
A1: for n holds P.(ASeq.n) = 0;
    for n holds Partial_Sums(P * ASeq).n = 0
    proof
      defpred P[Element of NAT] means Partial_Sums(P * ASeq).$1 = 0;
A2:   for k st P[k] holds P[k+1]
      proof
        let k such that
A3:     P[k];
        thus Partial_Sums(P * ASeq).(k+1) = Partial_Sums(P * ASeq).k + (P *
        ASeq).(k+1) by SERIES_1:def 1
          .= 0 + P.(ASeq.(k+1)) by A3,FUNCT_2:15
          .= 0 by A1;
      end;
      Partial_Sums(P * ASeq).0 = (P * ASeq).0 by SERIES_1:def 1
        .= P.(ASeq.0) by FUNCT_2:15
        .= 0 by A1;
      then
A4:   P[0];
      thus for k holds P[k] from NAT_1:sch 1(A4,A2);
    end;
    then for n st 0 <= n holds Partial_Sums(P * ASeq).n = 0;
    then
A5: Partial_Sums(P * ASeq) is convergent & lim Partial_Sums(P * ASeq) = 0
    by PROB_1:1;
    now
      let n;
      (Partial_Diff_Union ASeq).n c= ASeq.n by PROB_3:33;
      hence (P * Partial_Diff_Union ASeq).n <= (P * ASeq).n by PROB_3:5;
    end;
    then
A6: for n holds (Partial_Sums(P * Partial_Diff_Union ASeq)).n <= (
    Partial_Sums(P * ASeq)).n by SERIES_1:14;
    Partial_Sums(P * Partial_Diff_Union ASeq) is convergent by PROB_3:45;
    then Sum (P * Partial_Diff_Union ASeq) <= 0 by A5,A6,SEQ_2:18;
    then P.(Union Partial_Diff_Union ASeq) <= 0 by PROB_3:46;
    then
A7: P.(Union ASeq) <= 0 by PROB_3:36;
    Union ASeq is Event of Sigma by PROB_1:26;
    hence P.(Union ASeq) = 0 by A7,PROB_1:def 8;
  end;
  assume
A8: P.(Union ASeq) = 0;
  hereby
    reconsider Y2 = Union ASeq as Event of Sigma by PROB_1:26;
    let n;
    reconsider Y1 = ASeq.n as Event of Sigma;
    ASeq.n in rng ASeq by SETLIM_1:4;
    then ASeq.n c= union rng ASeq by ZFMISC_1:74;
    then Y1 c= Y2 by CARD_3:def 4;
    hence P.(ASeq.n) = 0 by A8,Th6;
  end;
end;

theorem Th8:
  (for A being set st A in rng ASeq holds P.A = 0) iff P.(union rng ASeq) = 0
proof
  hereby
    assume
A1: for A being set st A in rng ASeq holds P.A = 0;
    for n holds P.(ASeq.n) = 0
    proof
      let n;
      ASeq.n in rng ASeq by SETLIM_1:4;
      hence thesis by A1;
    end;
    then P.(Union ASeq) = 0 by Th7;
    hence P.(union rng ASeq) = 0 by CARD_3:def 4;
  end;
  assume P.(union rng ASeq) = 0;
  then
A2: P.(Union ASeq) = 0 by CARD_3:def 4;
  hereby
    let A be set;
    assume A in rng ASeq;
    then ex n1 being Element of NAT st A = ASeq.n1 by SETLIM_1:4;
    hence P.A = 0 by A2,Th7;
  end;
end;

theorem Th9:
  for seq being Function of NAT,REAL, Eseq being Function of NAT,
  ExtREAL st seq = Eseq holds Partial_Sums seq = Ser Eseq
proof
  let seq be Function of NAT,REAL, Eseq be Function of NAT,ExtREAL such that
A1: seq = Eseq;
  reconsider Ps = Partial_Sums seq as Function of NAT, ExtREAL by FUNCT_2:7
,NUMBERS:31;
  defpred P[Element of NAT] means Ps.$1 = (Ser Eseq).$1;
A2: for k st P[k] holds P[k+1]
  proof
    let k such that
A3: Ps.k = (Ser Eseq).k;
    Ps.k = (Partial_Sums seq).k;
    then reconsider Psk = Ps.k as Real;
    Ps.(k+1) = Psk + seq.(k+1) & (Ser Eseq).(k+1) = (Ser Eseq).k + Eseq.(k
    +1) by SERIES_1:def 1,SUPINF_2:44;
    hence thesis by A1,A3,SUPINF_2:1;
  end;
  Ps.0 = Eseq.0 by A1,SERIES_1:def 1
    .= (Ser Eseq).0 by SUPINF_2:44;
  then
A4: P[0];
  for k holds P[k] from NAT_1:sch 1(A4,A2);
  hence thesis by FUNCT_2:63;
end;

theorem Th10:
  for seq being Function of NAT,REAL, Eseq being Function of NAT,
  ExtREAL st seq = Eseq & seq is bounded_above
  holds upper_bound seq = sup rng Eseq
proof
  let seq be Function of NAT,REAL, Eseq be Function of NAT,ExtREAL such that
A1: seq = Eseq and
A2: seq is bounded_above;
  reconsider s = upper_bound seq as R_eal by XXREAL_0:def 1;
A3: dom Eseq = NAT by FUNCT_2:def 1;
A4: rng Eseq <> {-infty}
  proof
    assume rng Eseq = {-infty};
    then reconsider k1 = -infty as Element of rng Eseq by TARSKI:def 1;
    consider n1 being set such that
A5: n1 in NAT and
    Eseq.n1 = k1 by A3,FUNCT_1:def 3;
    reconsider n1 as Element of NAT by A5;
    seq.n1 = k1 by A1;
    hence contradiction;
  end;
  for x being ext-real number holds x in rng Eseq implies x <= s
  proof
    let x be ext-real number;
    assume x in rng Eseq;
    then ex n1 being set st n1 in NAT & Eseq.n1 = x by A3,FUNCT_1:def 3;
    hence thesis by A1,A2,RINFSUP1:7;
  end;
  then
A6: s is UpperBound of rng Eseq by XXREAL_2:def 1;
  then
A7: rng Eseq is bounded_above by XXREAL_2:def 10;
A8: s <= sup rng Eseq
  proof
    reconsider r1=sup rng Eseq as Real by A7,A4,XXREAL_2:57;
    sup rng Eseq is UpperBound of rng Eseq by XXREAL_2:def 3;
    then for n holds seq.n <= r1 by A1,A3,FUNCT_1:3,XXREAL_2:def 1;
    hence thesis by RINFSUP1:9;
  end;
  sup rng Eseq <= s by A6,XXREAL_2:def 3;
  hence thesis by A8,XXREAL_0:1;
end;

theorem Th11:
  for seq being Function of NAT,REAL, Eseq being Function of NAT,
  ExtREAL st seq = Eseq & seq is bounded_below
   holds lower_bound seq = inf rng Eseq
proof
  let seq be Function of NAT,REAL, Eseq be Function of NAT,ExtREAL such that
A1: seq = Eseq and
A2: seq is bounded_below;
  reconsider s=lower_bound seq as R_eal by XXREAL_0:def 1;
A3: dom Eseq = NAT by FUNCT_2:def 1;
A4: rng Eseq <> {+infty}
  proof
    assume rng Eseq = {+infty};
    then reconsider k1 = +infty as Element of rng Eseq by TARSKI:def 1;
    consider n1 being set such that
A5: n1 in NAT and
    Eseq.n1 = k1 by A3,FUNCT_1:def 3;
    reconsider n1 as Element of NAT by A5;
    seq.n1 = k1 by A1;
    hence contradiction;
  end;
  for x being ext-real number holds x in rng Eseq implies s <= x
  proof
    let x be ext-real number;
    assume x in rng Eseq;
    then ex n1 being set st n1 in NAT & Eseq.n1 = x by A3,FUNCT_1:def 3;
    hence thesis by A1,A2,RINFSUP1:8;
  end;
  then
A6: s is LowerBound of rng Eseq by XXREAL_2:def 2;
  then
A7: rng Eseq is bounded_below by XXREAL_2:def 9;
A8: inf rng Eseq <= s
  proof
    reconsider r1=inf rng Eseq as Real by A7,A4,XXREAL_2:58;
    inf rng Eseq is LowerBound of rng Eseq by XXREAL_2:def 4;
    then for n holds r1 <= seq.n by A1,A3,FUNCT_1:3,XXREAL_2:def 2;
    hence thesis by RINFSUP1:10;
  end;
  s <= inf rng Eseq by A6,XXREAL_2:def 4;
  hence thesis by A8,XXREAL_0:1;
end;

theorem Th12:
  for seq being Function of NAT,REAL, Eseq being Function of NAT,
  ExtREAL st seq = Eseq & seq is nonnegative summable holds Sum seq = SUM Eseq
proof
  let seq be Function of NAT,REAL, Eseq be Function of NAT,ExtREAL such that
A1: seq = Eseq and
A2: seq is nonnegative summable;
A3: for n holds seq.n >= 0 by A2,RINFSUP1:def 3;
  Partial_Sums seq is convergent by A2,SERIES_1:def 2;
  then
A4: Partial_Sums seq is bounded;
  then upper_bound Partial_Sums seq = sup rng Ser Eseq by A1,Th9,Th10;
  then upper_bound Partial_Sums seq = SUM Eseq by SUPINF_2:def 17;
  hence thesis by A4,A3,RINFSUP1:24,SERIES_1:16;
end;

theorem Th13:
  P is sigma_Measure of Sigma
proof
  set Z = Sigma;
  reconsider P1 = P as Function of Z,ExtREAL by FUNCT_2:7,NUMBERS:31;
  for x being R_eal holds x in rng P1 implies 0. <= x
  proof
    let x be R_eal;
    assume
A1: x in rng P1;
    dom P1 = Sigma by FUNCT_2:def 1;
    then consider y being set such that
A2: y in Sigma and
A3: P1.y = x by A1,FUNCT_1:def 3;
    reconsider y1=y as Event of Sigma by A2;
    0 <= P.y1 by PROB_1:def 8;
    hence thesis by A3;
  end;
  then
A4: rng P1 is nonnegative by SUPINF_2:def 9;
  for F being Sep_Sequence of Z holds SUM(P1 * F) = P1.(union rng F)
  proof
    let F be Sep_Sequence of Z;
    reconsider F2=F as disjoint_valued SetSequence of Sigma by Th2;
    for n holds (P * F2).n >= 0 by PROB_3:4;
    then
A5: P * F2 is nonnegative by RINFSUP1:def 3;
    Partial_Sums(P * F2) is convergent by PROB_3:45;
    then P * F2 is summable by SERIES_1:def 2;
    then P.(Union F2) = Sum(P * F2) & Sum(P * F2) = SUM(P1 * F) by A5,Th12,
PROB_3:46;
    hence thesis by CARD_3:def 4;
  end;
  hence thesis by A4,MEASURE1:def 6,SUPINF_2:def 16;
end;

definition
  let Omega,Sigma,P;
  func P2M(P) -> sigma_Measure of Sigma equals
  P;
  coherence by Th13;
end;

theorem Th14:
  for X being non empty set, S being SigmaField of X, M being
  sigma_Measure of S st M.X = R_EAL(1) holds M is Probability of S
proof
  let X be non empty set, S be SigmaField of X, M be sigma_Measure of S such
  that
A1: M.X = R_EAL(1);
A2: for A being Element of S holds M.A <= R_EAL(1)
  proof
    reconsider X as Element of S by PROB_1:5;
    let A be Element of S;
    M.A <= M.X by MEASURE1:31;
    hence thesis by A1;
  end;
A3: for x st x in S holds M.x in REAL
  proof
    let x;
    assume x in S;
    then reconsider x as Element of S;
A4: R_EAL(1) is Real & 0 is Real by MEASURE6:def 1;
    0. <= M.x & M.x <= R_EAL(1) by A2,MEASURE1:def 2;
    hence thesis by A4,XXREAL_0:45;
  end;
  dom M = S by FUNCT_2:def 1;
  then reconsider P1 = M as Function of S,REAL by A3,FUNCT_2:3;
  reconsider P1 as Function of S,REAL;
A5: for ASeq being SetSequence of S st ASeq is non-ascending holds P1 *
  ASeq is convergent & lim (P1 * ASeq) = P1.Intersection ASeq
  proof
    let ASeq be SetSequence of S such that
A6: ASeq is non-ascending;
    for n holds 0 <= (P1 * ASeq).n
    proof
      let n;
      reconsider A = ASeq.n as Event of S;
      0 <= P1.A & dom (P1 * ASeq) = NAT by MEASURE1:def 2,SEQ_1:1;
      hence thesis by FUNCT_1:12;
    end;
    then
A7: P1*ASeq is bounded_below by RINFSUP1:10;
    reconsider F = ASeq as Function of NAT,S by Th2;
A8: for n being Element of NAT holds F.(n+1) c= F.n by A6,PROB_2:6;
A9: M.(F.0) <+infty by A3,XXREAL_0:9;
    now
      let n;
      dom (M*F) = NAT by FUNCT_2:def 1;
      then
A10:  (M*F).n = M.(F.n) & (M*F).(n+1) = M.(F.(n+1)) by FUNCT_1:12;
      F.(n+1) c= F.n by A6,PROB_2:6;
      hence (P1*ASeq).(n+1) <= (P1*ASeq).n by A10,MEASURE1:31;
    end;
    then
A11: P1*ASeq is non-increasing by SEQM_3:def 9;
    then lim (P1*ASeq) = lower_bound (P1*ASeq) by A7,RINFSUP1:25
      .= inf(rng (M*F)) by A7,Th11;
    then lim (P1 * ASeq) = M.(meet rng F) by A8,A9,MEASURE3:12
      .= P1.Intersection ASeq by SETLIM_1:8;
    hence thesis by A7,A11;
  end;
A12: for A,B being Event of S st A misses B holds P1.(A \/ B) = P1.A + P1.B
  proof
    let A,B be Event of S such that
A13: A misses B;
    reconsider A, B as Element of S;
    reconsider A2 = A, B2 = B as Element of S;
    P1.(A \/ B) = M.A2 + M.B2 by A13,MEASURE1:30
      .= P1.A + P1.B by SUPINF_2:1;
    hence thesis;
  end;
  ( for A being Event of S holds 0 <= P1.A)& P1.X = 1 by A1,MEASURE1:def 2
,MEASURE6:def 1;
  hence thesis by A12,A5,PROB_1:def 8;
end;

definition
  let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
  assume
A1: M.X = R_EAL(1);
  func M2P(M) -> Probability of S equals
  M;
  coherence by A1,Th14;
end;

Lm2: A1 is non-descending implies for n holds (Partial_Union A1).n = A1.n
proof
  defpred P[Element of NAT] means (Partial_Union A1).$1 = A1.$1;
  assume
A1: A1 is non-descending;
A2: for k st P[k] holds P[k+1]
  proof
    let k such that
A3: P[k];
A4: A1.k c= A1.(k+1) by A1,PROB_2:7;
    thus (Partial_Union A1).(k+1) = A1.k \/ A1.(k+1) by A3,PROB_3:def 2
      .= A1.(k+1) by A4,XBOOLE_1:12;
  end;
A5: P[0] by PROB_3:def 2;
  thus for k holds P[k] from NAT_1:sch 1(A5,A2);
end;

theorem Th15:
  A1 is non-descending implies Partial_Union A1 = A1
proof
  assume A1 is non-descending;
  then for n holds (Partial_Union A1).n = A1.n by Lm2;
  hence thesis by FUNCT_2:63;
end;

theorem Th16:
  A1 is non-descending implies (Partial_Diff_Union A1).0 = A1.0 &
  for n holds (Partial_Diff_Union A1).(n+1) = A1.(n+1) \ A1.n
proof
  assume
A1: A1 is non-descending;
  thus (Partial_Diff_Union A1).0 = A1.0 by PROB_3:def 3;
  thus for n holds (Partial_Diff_Union A1).(n+1) = A1.(n+1) \ A1.n
  proof
    let n;
    thus (Partial_Diff_Union A1).(n+1) = A1.(n+1) \ (Partial_Union A1).n by
PROB_3:def 3
      .= A1.(n+1) \ A1.n by A1,Lm2;
  end;
end;

theorem
  A1 is non-descending implies for n holds A1.(n+1) = (
  Partial_Diff_Union A1).(n+1) \/ A1.n
proof
  assume
A1: A1 is non-descending;
  thus for n holds A1.(n+1) = (Partial_Diff_Union A1).(n+1) \/ A1.n
  proof
    let n;
A2: A1.n c= A1.(n+1) by A1,PROB_2:7;
    thus (Partial_Diff_Union A1).(n+1) \/ A1.n = (A1.(n+1) \ (Partial_Union A1
    ).n) \/ A1.n by PROB_3:def 3
      .= (A1.(n+1) \ A1.n) \/ A1.n by A1,Lm2
      .= A1.(n+1) \/ A1.n by XBOOLE_1:39
      .= A1.(n+1) by A2,XBOOLE_1:12;
  end;
end;

theorem Th18:
  A1 is non-descending implies for n holds (Partial_Diff_Union A1)
  .(n+1) misses A1.n
proof
  assume
A1: A1 is non-descending;
  let n;
  (Partial_Diff_Union A1).(n+1) = A1.(n+1) \ A1.n by A1,Th16;
  hence thesis by XBOOLE_1:79;
end;

theorem
  XSeq is non-descending implies Partial_Union XSeq = XSeq by Th15;

theorem
  XSeq is non-descending implies (Partial_Diff_Union XSeq).0 = XSeq.0 &
  for n holds (Partial_Diff_Union XSeq).(n+1) = XSeq.(n+1) \ XSeq.n by Th16;

theorem
  XSeq is non-descending implies for n holds (Partial_Diff_Union XSeq).
  (n+1) misses XSeq.n by Th18;

definition
  let Omega,Sigma,P;
  pred P is_complete Sigma means
  :Def3:
  for A being Subset of Omega for B
  being set st B in Sigma holds (A c= B & P.B=0 implies A in Sigma);
end;

theorem
  P is_complete Sigma iff P2M(P) is_complete Sigma
proof
  hereby
    assume P is_complete Sigma;
    then
    for A being Subset of Omega for B being set st B in Sigma holds (A c=
    B & (P2M P).B = 0. implies A in Sigma) by Def3;
    hence P2M(P) is_complete Sigma by MEASURE3:def 1;
  end;
  assume P2M(P) is_complete Sigma;
  then
  for A being Subset of Omega for B being set st B in Sigma holds (A c= B
  & P.B=0 implies A in Sigma) by MEASURE3:def 1;
  hence thesis by Def3;
end;

definition
  let Omega,Sigma,P;
  mode thin of P -> Subset of Omega means
    :Def4:
    ex A being set st A in Sigma & it c= A & P.A = 0;
  existence
  proof
    reconsider B = {} as Subset of Omega by XBOOLE_1:2;
    take B;
    take A={};
    thus A in Sigma by PROB_1:4;
    thus B c= A;
    thus thesis by VALUED_0:def 19;
  end;
end;

theorem Th23:
  for Y being Subset of Omega holds Y is thin of P iff Y is thin of P2M(P)
proof
  let Y be Subset of Omega;
  hereby
    assume Y is thin of P;
    then ex A be set st A in Sigma & Y c= A & P.A = 0 by Def4;
    hence Y is thin of P2M(P) by MEASURE3:def 2;
  end;
  assume Y is thin of P2M(P);
  then ex B be set st B in Sigma & Y c= B & (P2M(P)).B = 0. by MEASURE3:def 2;
  hence thesis by Def4;
end;

theorem Th24:
  {} is thin of P
proof
  P.{} = 0 & {} in Sigma by PROB_1:4,VALUED_0:def 19;
  hence thesis by Def4;
end;

theorem Th25:
  for B1,B2 being set st B1 in Sigma & B2 in Sigma holds for C1,C2
  being thin of P holds B1 \/ C1 = B2 \/ C2 implies P.B1 = P.B2
proof
  let B1,B2 be set;
  assume
A1: B1 in Sigma & B2 in Sigma;
  let C1,C2 be thin of P;
  assume
A2: B1 \/ C1 = B2 \/ C2;
  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 Sigma and
A6: C1 c= D1 and
A7: P.D1 = 0 by Def4;
A8: B1 \/ C1 c= B1 \/ D1 by A6,XBOOLE_1:9;
  consider D2 being set such that
A9: D2 in Sigma and
A10: C2 c= D2 and
A11: P.D2 = 0 by Def4;
A12: B2 \/ C2 c= B2 \/ D2 by A10,XBOOLE_1:9;
  reconsider B1,B2,D1,D2 as Event of Sigma by A1,A5,A9;
A13: P.(B1 \/ D1) <= P.B1 + P.D1 by PROB_1:39;
  P.B2 <= P.(B1 \/ D1) by A4,A8,PROB_1:34,XBOOLE_1:1;
  then
A14: P.B2 <= P.B1 by A7,A13,XXREAL_0:2;
A15: P.(B2 \/ D2) <= P.B2 + P.D2 by PROB_1:39;
  P.B1 <= P.(B2 \/ D2) by A3,A12,PROB_1:34,XBOOLE_1:1;
  then P.B1 <= P.B2 by A11,A15,XXREAL_0:2;
  hence thesis by A14,XXREAL_0:1;
end;

definition
  let Omega,Sigma,P;
  func COM(Sigma,P) -> non empty Subset-Family of Omega means
  :Def5:
  for A
being set holds A in it iff ex B being set st B in Sigma & ex C being thin of P
  st A = B \/ C;
  existence
  proof
A1: {} is thin of P by Th24;
A2: for A being set st A = {} holds ex B being set st B in Sigma & ex C
    being thin of P st A = B \/ C
    proof
      let A be set;
      consider B being set such that
A3:   B = {} and
A4:   B in Sigma by PROB_1:4;
      consider C being thin of P such that
A5:   C = {} by A1;
      assume A = {};
      then A = B \/ C by A3,A5;
      hence thesis by A4;
    end;
    defpred P[set] means for A being set st A = $1 holds ex B being set st B
    in Sigma & ex C being thin of P st A = B \/ C;
    consider D being set such that
A6: for y being set holds y in D iff y in bool Omega & P[y] from
    XBOOLE_0:sch 1;
A7: for A being set holds (A in D iff ex B being set st (B in Sigma & ex C
    being thin of P st A = B \/ C) )
    proof
      let A be set;
A8:   A in D iff (A in bool Omega & for y being set holds (y = A implies
ex B being set st (B in Sigma & ex C being thin of P st y = B \/ C) )) by A6;
      (ex B being set st (B in Sigma & ex C being thin of P st A = B \/ C)
      ) implies A in D
      proof
        assume
A9:     ex B being set st (B in Sigma & ex C being thin of P st A = B \/ C);
        then A c= Omega by XBOOLE_1:8;
        hence thesis by A8,A9;
      end;
      hence thesis by A6;
    end;
A10: D c= bool Omega
    proof
      let x be set;
      assume x in D;
      hence thesis by A6;
    end;
    {} c= Omega by XBOOLE_1:2;
    then reconsider D as non empty Subset-Family of Omega by A6,A10,A2;
    take D;
    thus thesis by A7;
  end;
  uniqueness
  proof
    let D1,D2 be non empty Subset-Family of Omega such that
A11: for A being set holds (A in D1 iff ex B being set st (B in Sigma
    & ex C being thin of P st A = B \/ C) ) and
A12: for A being set holds (A in D2 iff ex B being set st (B in Sigma
    & ex C being thin of P st A = B \/ C) );
    for A being set holds A in D1 iff A in D2
    proof
      let A be set;
      thus A in D1 implies A in D2
      proof
        assume A in D1;
        then ex B being set st (B in Sigma & ex C being thin of P st A = B \/
        C) by A11;
        hence thesis by A12;
      end;
      assume A in D2;
      then
      ex B being set st (B in Sigma & ex C being thin of P st A = B \/ C)
      by A12;
      hence thesis by A11;
    end;
    hence thesis by TARSKI:1;
  end;
end;

theorem Th26:
  for C being thin of P holds C in COM(Sigma,P)
proof
  let C be thin of P;
  reconsider B = {} as Element of Sigma by PROB_1:4;
  B \/ C in COM(Sigma,P) by Def5;
  hence thesis;
end;

theorem Th27:
  COM(Sigma,P) = COM(Sigma,P2M P)
proof
A1: COM( Sigma,P2M P) c= COM(Sigma,P)
  proof
    let x;
    assume x in COM( Sigma,P2M P);
    then consider B being set such that
A2: B in Sigma and
A3: ex C being thin of P2M(P) st x = B \/ C by MEASURE3:def 3;
    consider C being thin of P2M(P) such that
A4: x = B \/ C by A3;
    reconsider C1=C as thin of P by Th23;
    x = B \/ C1 by A4;
    hence thesis by A2,Def5;
  end;
  COM(Sigma,P) c= COM(Sigma,P2M P)
  proof
    let x;
    assume x in COM(Sigma,P);
    then consider B being set such that
A5: B in Sigma and
A6: ex C being thin of P st x = B \/ C by Def5;
    consider C being thin of P such that
A7: x = B \/ C by A6;
    reconsider C1=C as thin of P2M(P) by Th23;
    x = B \/ C1 by A7;
    hence thesis by A5,MEASURE3:def 3;
  end;
  hence thesis by A1,XBOOLE_0:def 10;
end;

definition
  let Omega,Sigma,P;
  let A be Element of COM(Sigma,P);
  func P_COM2M_COM(A) -> Element of COM(Sigma,P2M(P)) equals
  A;
  correctness by Th27;
end;

theorem Th28:
  Sigma c= COM(Sigma,P)
proof
  reconsider C={} as thin of P by Th24;
  let A be set such that
A1: A in Sigma;
  A = A \/ C;
  hence thesis by A1,Def5;
end;

definition
  let Omega,Sigma,P;
  let A be Element of COM(Sigma,P);
  func ProbPart(A) -> non empty Subset-Family of Omega means
  :Def7:
  for B
  being set holds (B in it iff B in Sigma & B c= A & A \ B is thin of P );
  existence
  proof
    defpred P[set] means for t being set holds t = $1 implies t in Sigma & t
    c= A & A \ t is thin of P;
    consider D being set such that
A1: for t being set holds t in D iff t in bool Omega & P[t] from
    XBOOLE_0:sch 1;
A2: for B being set holds B in D iff B in Sigma & B c= A & A \ B is thin of P
    proof
      let B be set;
      B in Sigma & B c= A & A \ B is thin of P implies B in D
      proof
        assume that
A3:     B in Sigma and
A4:     B c= A & A \ B is thin of P;
        for t being set holds t = B implies t in Sigma & t c= A & A \ t is
        thin of P by A3,A4;
        hence thesis by A1,A3;
      end;
      hence thesis by A1;
    end;
A5: D c= bool Omega
    proof
      let B be set;
      assume B in D;
      then B in Sigma by A2;
      hence thesis;
    end;
    D <> {}
    proof
      consider B being set such that
A6:   B in Sigma and
A7:   ex C being thin of P st A = B \/ C by Def5;
      consider C being thin of P such that
A8:   A = B \/ C by A7;
      consider E being set such that
A9:   E in Sigma and
A10:  C c= E and
A11:  P.E = 0 by Def4;
      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 P by A9,A11,Def4;
      B c= A by A8,XBOOLE_1:7;
      hence thesis by A2,A6,A12;
    end;
    then reconsider D as non empty Subset-Family of Omega by A5;
    take D;
    thus thesis by A2;
  end;
  uniqueness
  proof
    let D1,D2 be non empty Subset-Family of Omega such that
A13: for B being set holds B in D1 iff B in Sigma & B c= A & A \ B is
    thin of P and
A14: for B being set holds B in D2 iff B in Sigma & B c= A & A \ B is
    thin of P;
    for B being set holds B in D1 iff B in D2
    proof
      let B be set;
      thus B in D1 implies B in D2
      proof
        assume
A15:    B in D1;
        then
A16:    A \ B is thin of P by A13;
        B in Sigma & B c= A by A13,A15;
        hence thesis by A14,A16;
      end;
      assume
A17:  B in D2;
      then
A18:  A \ B is thin of P by A14;
      B in Sigma & B c= A by A14,A17;
      hence thesis by A13,A18;
    end;
    hence thesis by TARSKI:1;
  end;
end;

theorem
  for A being Element of COM(Sigma,P) holds ProbPart(A) = MeasPart(
  P_COM2M_COM(A))
proof
  let A be Element of COM(Sigma,P);
A1: MeasPart(P_COM2M_COM(A)) c= ProbPart(A)
  proof
    let x be set such that
A2: x in MeasPart(P_COM2M_COM A);
    P_COM2M_COM(A) \ x is thin of P2M(P) by A2,MEASURE3:def 4;
    then
A3: A \ x is thin of P by Th23;
    x in Sigma & x c= P_COM2M_COM(A) by A2,MEASURE3:def 4;
    hence thesis by A3,Def7;
  end;
  ProbPart(A) c= MeasPart(P_COM2M_COM(A))
  proof
    let x be set such that
A4: x in ProbPart(A);
    A \ x is thin of P by A4,Def7;
    then
A5: P_COM2M_COM(A) \ x is thin of P2M(P) by Th23;
    x in Sigma & x c= A by A4,Def7;
    hence thesis by A5,MEASURE3:def 4;
  end;
  hence thesis by A1,XBOOLE_0:def 10;
end;

theorem
  for A being Element of COM(Sigma,P) holds for A1,A2 being set st A1 in
  ProbPart(A) & A2 in ProbPart(A) holds P.A1 = P.A2
proof
  let A be Element of COM(Sigma,P);
  let A1,A2 be set such that
A1: A1 in ProbPart(A) and
A2: A2 in ProbPart(A);
  reconsider C1 = A \ A1, C2 = A \ A2 as thin of P by A1,A2,Def7;
A3: A2 c= A by A2,Def7;
  A1 c= A by A1,Def7;
  then
A4: A1 \/ C1 = A by XBOOLE_1:45
    .= A2 \/ C2 by A3,XBOOLE_1:45;
  A1 in Sigma & A2 in Sigma by A1,A2,Def7;
  hence thesis by A4,Th25;
end;

theorem Th31:
  for F being Function of NAT,COM(Sigma,P) holds ex BSeq being
  SetSequence of Sigma st for n holds BSeq.n in ProbPart(F.n)
proof
  let F be Function of NAT,COM(Sigma,P);
  defpred P[Element of NAT, set] means for n being Element of NAT for y being
  set holds (n = $1 & y = $2 implies y in ProbPart(F.n));
A1: for t being Element of NAT ex A being Element of Sigma st P[t,A]
  proof
    let t be Element of NAT;
    set A = the Element of ProbPart(F.t);
    reconsider A as Element of Sigma by Def7;
    take A;
    thus thesis;
  end;
  ex G being Function of NAT,Sigma st for t being Element of NAT holds P[t
  ,G.t] from FUNCT_2:sch 3(A1);
  then consider G being Function of NAT,Sigma such that
A2: for t being Element of NAT holds for n being Element of NAT for y
  being set holds (n = t & y = G.t implies y in ProbPart(F.n));
  reconsider BSeq = G as SetSequence of Omega by FUNCT_2:7;
  reconsider BSeq as SetSequence of Sigma;
  take BSeq;
  thus thesis by A2;
end;

theorem Th32:
  for F being Function of NAT,COM(Sigma,P), BSeq being SetSequence
of Sigma holds ex CSeq being SetSequence of Omega st for n holds CSeq.n = F.n \
  BSeq.n
proof
  let F be Function of NAT,COM(Sigma,P), G be SetSequence of Sigma;
  defpred P[Element of NAT, set] means for n being Element of NAT for y being
  set holds (n = $1 & y = $2 implies y = F.n \ G.n);
A1: for t being Element of NAT ex A being Element of bool Omega st P[t,A]
  proof
    let t be Element of NAT;
    F.t is Element of COM(Sigma,P);
    then reconsider A = F.t \ G.t as Element of bool Omega by XBOOLE_1:1;
    take A;
    thus thesis;
  end;
  ex H being Function of NAT,bool Omega st for t being Element of NAT
  holds P[t,H.t] from FUNCT_2:sch 3(A1);
  then consider H being Function of NAT,bool Omega such that
A2: for t being Element of NAT holds for n being Element of NAT for y
  being set holds n = t & y = H.t implies y = F.n \ G.n;
  take H;
  thus thesis by A2;
end;

theorem Th33:
  for BSeq being SetSequence of Omega st (for n holds BSeq.n is
  thin of P) holds ex CSeq being SetSequence of Sigma st for n holds BSeq.n c=
  CSeq.n & P.(CSeq.n) = 0
proof
  let BSeq be SetSequence of Omega;
  defpred P[Element of NAT, set] means for n being Element of NAT for y being
  set holds (n = $1 & y = $2 implies y in Sigma & BSeq.n c= y & P.y = 0);
  assume
A1: for n holds BSeq.n is thin of P;
A2: for t being Element of NAT ex A being Element of Sigma st P[t,A]
  proof
    let t be Element of NAT;
    BSeq.t is thin of P by A1;
    then consider A being set such that
A3: A in Sigma and
A4: BSeq.t c= A & P.A = 0 by Def4;
    reconsider A as Element of Sigma by A3;
    take A;
    thus thesis by A4;
  end;
  ex G being Function of NAT,Sigma st for t being Element of NAT holds P[t
  ,G.t] from FUNCT_2:sch 3(A2);
  then consider G being Function of NAT,Sigma such that
A5: for t being Element of NAT holds for n being Element of NAT for y
  being set holds (n = t & y = G.t implies y in Sigma & BSeq.n c= y & P.y = 0);
  reconsider CSeq = G as SetSequence of Omega by FUNCT_2:7;
  reconsider CSeq as SetSequence of Sigma;
  take CSeq;
  thus thesis by A5;
end;

theorem Th34:
  for D being non empty Subset-Family of Omega holds (for A being
set holds (A in D iff ex B being set st B in Sigma & ex C being thin of P st A
  = B \/ C)) implies D is SigmaField of Omega
proof
  let D be non empty Subset-Family of Omega;
  assume
A1: for A being set holds A in D iff ex B being set st B in Sigma & ex C
  being thin of P st A = B \/ C;
A2: for A1 being SetSequence of Omega st rng A1 c= D holds Union A1 in D
  proof
    let A1 be SetSequence of Omega;
    reconsider F = A1 as Function of NAT,bool Omega;
A3: dom F = NAT by FUNCT_2:def 1;
    assume
A4: rng A1 c= D;
A5: for n holds ex B being set st B in Sigma & ex C being thin of P st F.
    n = B \/ C
    proof
      let n;
      F.n in rng F by NAT_1:51;
      hence thesis by A1,A4;
    end;
    for n holds F.n in COM(Sigma,P)
    proof
      let n;
      ex B being set st (B in Sigma & ex C being thin of P st F.n = B \/
      C) by A5;
      hence thesis by Def5;
    end;
    then for n being set st n in NAT holds F.n in COM(Sigma,P);
    then reconsider F as Function of NAT,COM(Sigma,P) by A3,FUNCT_2:3;
    consider BSeq being SetSequence of Sigma such that
A6: for n holds BSeq.n in ProbPart(F.n) by Th31;
    consider CSeq being SetSequence of Omega such that
A7: for n holds CSeq.n = F.n \ BSeq.n by Th32;
A8: for n being Element of NAT holds BSeq.n in Sigma & BSeq.n c= F.n & F.
    n \ BSeq.n is thin of P
    proof
      let n be Element of NAT;
      BSeq.n in ProbPart(F.n) by A6;
      hence thesis by Def7;
    end;
    for n holds CSeq.n is thin of P
    proof
      let n be Element of NAT;
      F.n \ BSeq.n is thin of P by A8;
      hence thesis by A7;
    end;
    then consider DSeq being SetSequence of Sigma such that
A9: for n holds CSeq.n c= DSeq.n & P.(DSeq.n) = 0 by Th33;
A10: Union A1 = union rng A1 by CARD_3:def 4;
    ex B being set st B in Sigma & ex C being thin of P st Union A1 = B \/ C
    proof
      set B = union rng BSeq;
      take B;
A11:  union rng BSeq c= union rng F
      proof
        let x be set;
        assume x in union rng BSeq;
        then consider Z being set such that
A12:    x in Z and
A13:    Z in rng BSeq by TARSKI:def 4;
        dom BSeq = NAT by FUNCT_2:def 1;
        then consider n being set such that
A14:    n in NAT and
A15:    Z = BSeq.n by A13,FUNCT_1:def 3;
        reconsider n as Element of NAT by A14;
        set P = F.n;
A16:    BSeq.n c= P by A8;
        ex P being set st P in rng F & x in P
        proof
          take P;
          thus thesis by A3,A12,A15,A16,FUNCT_1:def 3;
        end;
        hence thesis by TARSKI:def 4;
      end;
A17:  ex C being thin of P st Union A1 = B \/ C
      proof
        set C = Union A1 \ B;
        Union DSeq in Sigma by PROB_1:17;
        then
A18:    union rng DSeq in Sigma by CARD_3:def 4;
A19:    C c= union rng CSeq
        proof
          let x be set;
          assume
A20:      x in C;
          then x in union rng F by A10,XBOOLE_0:def 5;
          then consider Z being set such that
A21:      x in Z and
A22:      Z in rng F by TARSKI:def 4;
          consider n being set such that
A23:      n in NAT and
A24:      Z = F.n by A3,A22,FUNCT_1:def 3;
          reconsider n as Element of NAT by A23;
A25:      not x in union rng BSeq by A20,XBOOLE_0:def 5;
          not x in BSeq.n
          proof
            dom BSeq = NAT by FUNCT_2:def 1;
            then
A26:        BSeq.n in rng BSeq by FUNCT_1:def 3;
            assume x in BSeq.n;
            hence thesis by A25,A26,TARSKI:def 4;
          end;
          then
A27:      x in F.n \ BSeq.n by A21,A24,XBOOLE_0:def 5;
          ex Z being set st x in Z & Z in rng CSeq
          proof
            take CSeq.n;
            dom CSeq = NAT by FUNCT_2:def 1;
            hence thesis by A7,A27,FUNCT_1:def 3;
          end;
          hence thesis by TARSKI:def 4;
        end;
        for A being set holds A in rng DSeq implies P.A = 0
        proof
          let A be set;
A28:      dom DSeq = NAT by FUNCT_2:def 1;
          assume A in rng DSeq;
          then ex n being set st n in NAT & A = DSeq.n by A28,FUNCT_1:def 3;
          hence thesis by A9;
        end;
        then
A29:    P.(union rng DSeq) = 0 by Th8;
        union rng CSeq c= union rng DSeq
        proof
          let x be set;
          assume x in union rng CSeq;
          then consider Z being set such that
A30:      x in Z and
A31:      Z in rng CSeq by TARSKI:def 4;
          dom CSeq = NAT by FUNCT_2:def 1;
          then consider n being set such that
A32:      n in NAT and
A33:      Z = CSeq.n by A31,FUNCT_1:def 3;
          reconsider n as Element of NAT by A32;
          n in dom DSeq by A32,FUNCT_2:def 1;
          then
A34:      DSeq.n in rng DSeq by FUNCT_1:def 3;
          CSeq.n c= DSeq.n by A9;
          hence thesis by A30,A33,A34,TARSKI:def 4;
        end;
        then C c= union rng DSeq by A19,XBOOLE_1:1;
        then
A35:    C is thin of P by A29,A18,Def4;
        Union A1 = C \/ union rng F /\ union rng BSeq by A10,XBOOLE_1:51
          .= B \/ C by A11,XBOOLE_1:28;
        then consider C being thin of P such that
A36:    Union A1 = B \/ C by A35;
        take C;
        thus thesis by A36;
      end;
      Union BSeq in Sigma by PROB_1:17;
      hence thesis by A17,CARD_3:def 4;
    end;
    hence thesis by A1;
  end;
  for A being Subset of Omega holds A in D implies A` in D
  proof
    let A be Subset of Omega;
    assume
A37: A in D;
    ex Q being set st Q in Sigma & ex W being thin of P st Omega \ A = Q \/ W
    proof
      consider B being set such that
A38:  B in Sigma and
A39:  ex C being thin of P st A = B \/ C by A1,A37;
      consider C being thin of P such that
A40:  A = B \/ C by A39;
      reconsider B as Subset of Omega by A38;
      set H = Omega \ B;
      consider G being set such that
A41:  G in Sigma and
A42:  C c= G and
A43:  P.G = 0 by Def4;
      set Q = H \ G;
A44:  Omega \ A = H \ C by A40,XBOOLE_1:41;
A45:  ex W being thin of P st Omega \ A = Q \/ W
      proof
        set W = H /\ (G \ C);
        W c= H by XBOOLE_1:17;
        then reconsider W as Subset of Omega by XBOOLE_1:1;
        reconsider W as thin of P by A41,A43,Def4;
        take W;
        thus thesis by A42,A44,Lm1;
      end;
      take Q;
      B` in Sigma by A38,PROB_1:def 1;
      hence thesis by A41,A45,PROB_1:6;
    end;
    hence thesis by A1;
  end;
  hence thesis by A2,Th4;
end;

registration
  let Omega,Sigma,P;
  cluster COM(Sigma,P) -> compl-closed sigma-multiplicative;
  coherence
  proof
    for A being set holds (A in COM(Sigma,P) iff ex B being set st B in
    Sigma & ex C being thin of P st A=B \/ C ) by Def5;
    hence thesis by Th34;
  end;
end;

definition
  let Omega,Sigma,P;
  redefine mode thin of P -> Event of COM(Sigma,P);
  coherence by Th26;
end;

theorem Th35:
  for A being set holds (A in COM(Sigma,P) iff ex A1,A2 being set
  st A1 in Sigma & A2 in Sigma & A1 c= A & A c= A2 & P.(A2 \ A1) = 0)
proof
  let A be set;
  thus A in COM(Sigma,P) implies ex A1,A2 being set st A1 in Sigma & A2 in
  Sigma & A1 c= A & A c= A2 & P.(A2 \ A1) = 0
  proof
    assume A in COM(Sigma,P);
    then consider B being set such that
A1: B in Sigma and
A2: ex C being thin of P st A = B \/ C by Def5;
    consider C being thin of P such that
A3: A = B \/ C by A2;
    reconsider B as Event of Sigma by A1;
    consider D being set such that
A4: D in Sigma and
A5: C c= D and
A6: P.D = 0 by Def4;
    reconsider D as Event of Sigma by A4;
    reconsider E = D \/ B as Event of Sigma;
A7: P.(D \/ B) <= P.D + P.B by PROB_1:39;
    P.(E \ B) = P.(D \ B) by XBOOLE_1:40
      .= P.(D \/ B) - P.B by Th5;
    then P.(E \ B) <= 0 by A6,A7,XREAL_1:47;
    then
A8: P.(E \ B) = 0 by PROB_1:def 8;
    A c= E by A3,A5,XBOOLE_1:9;
    hence thesis by A2,A8,XBOOLE_1:7;
  end;
  thus (ex A1,A2 being set st A1 in Sigma & A2 in Sigma & A1 c= A & A c= A2 &
  P.(A2 \ A1) = 0) implies A in COM(Sigma,P)
  proof
    given A1,A2 being set such that
A9: A1 in Sigma and
A10: A2 in Sigma and
A11: A1 c= A and
A12: A c= A2 and
A13: P.(A2 \ A1) = 0;
    reconsider A2 as Element of Sigma by A10;
    reconsider A1 as Element of Sigma by A9;
    set C = A \ A1;
A14: C is thin of P
    proof
      reconsider D = A2 \ A1 as Element of Sigma;
A15:  C c= D
      proof
        let x;
        assume x in C;
        then x in A & not x in A1 by XBOOLE_0:def 5;
        hence thesis by A12,XBOOLE_0:def 5;
      end;
      then C c= Omega by XBOOLE_1:1;
      hence thesis by A13,A15,Def4;
    end;
    A = A1 \/ C by A11,XBOOLE_1:45;
    hence thesis by A14,Def5;
  end;
end;

theorem
  for C being non empty Subset-Family of Omega holds (for A being set
holds (A in C iff ex A1,A2 being set st A1 in Sigma & A2 in Sigma & A1 c= A & A
  c= A2 & P.(A2 \ A1) = 0)) implies C = COM(Sigma,P)
proof
  let C be non empty Subset-Family of Omega;
  assume
A1: for A being set holds (A in C iff ex A1,A2 being set st A1 in Sigma
  & A2 in Sigma & A1 c= A & A c= A2 & P.(A2 \ A1) = 0);
  now
    let A be set;
    A in C iff ex A1,A2 being set st A1 in Sigma & A2 in Sigma & A1 c= A &
    A c= A2 & P.(A2 \ A1) = 0 by A1;
    hence A in C iff A in COM(Sigma,P) by Th35;
  end;
  hence thesis by TARSKI:1;
end;

definition
  let Omega,Sigma,P;
  func COM(P) -> Probability of COM(Sigma,P) means
  :Def8:
  for B being set st B in Sigma for C being thin of P holds it.(B \/ C) = P.B;
  existence
  proof
    reconsider C = {} as thin of P by Th24;
    defpred P[set,set] means for x,y being set st x in COM(Sigma,P) holds (x =
$1 & y = $2 implies (for B being set st B in Sigma for C being thin of P holds
    (x = B \/ C implies y = P.B)));
    set B = {};
A1: {} is thin of P by Th24;
A2: for x being set st x in COM(Sigma,P) ex y being set st y in REAL & P[x ,y]
    proof
      let x be set;
      assume x in COM(Sigma,P);
      then consider B being set such that
A3:   B in Sigma & ex C being thin of P st x = B \/ C by Def5;
      take P.B;
      thus thesis by A3,Th25,FUNCT_2:5;
    end;
    consider comP being Function of COM(Sigma,P),REAL such that
A4: for x being set st x in COM(Sigma,P) holds P[x,comP.x] from
    FUNCT_2:sch 1(A2);
A5: for B being set st B in Sigma for C being thin of P holds comP.(B \/ C
    ) = P.B
    proof
      let B be set;
      assume
A6:   B in Sigma;
      let C be thin of P;
      B \/ C in COM(Sigma,P) by A6,Def5;
      hence thesis by A4,A6;
    end;
A7: for BSeq being SetSequence of COM(Sigma,P) st BSeq is disjoint_valued
    holds Sum(comP * BSeq) = comP.(Union BSeq)
    proof
      let BSeq be SetSequence of COM(Sigma,P) such that
A8:   BSeq is disjoint_valued;
      reconsider F = BSeq as Function of NAT,bool Omega;
      rng F c= COM(Sigma,P) by RELAT_1:def 19;
      then reconsider F as Function of NAT,COM(Sigma,P) by FUNCT_2:6;
      consider CSeq being SetSequence of Sigma such that
A9:   for n holds CSeq.n in ProbPart(F.n) by Th31;
      consider B being set such that
A10:  B = union rng CSeq;
      Union CSeq in Sigma by PROB_1:17;
      then reconsider B as Element of Sigma by A10,CARD_3:def 4;
      consider DSeq being SetSequence of Omega such that
A11:  for n holds DSeq.n = F.n \ CSeq.n by Th32;
A12:  for n being Element of NAT holds CSeq.n in Sigma & CSeq.n c= F.n &
      F.n \ CSeq.n is thin of P
      proof
        let n be Element of NAT;
        CSeq.n in ProbPart(F.n) by A9;
        hence thesis by Def7;
      end;
      for n being Element of NAT holds DSeq.n is thin of P
      proof
        let n be Element of NAT;
        F.n \ CSeq.n is thin of P by A12;
        hence thesis by A11;
      end;
      then consider ESeq being SetSequence of Sigma such that
A13:  for n holds DSeq.n c= ESeq.n & P.(ESeq.n) = 0 by Th33;
A14:  dom BSeq = NAT by FUNCT_2:def 1;
A15:  B c= union rng F
      proof
        let x be set;
        assume x in B;
        then consider Z being set such that
A16:    x in Z and
A17:    Z in rng CSeq by A10,TARSKI:def 4;
        dom CSeq = NAT by FUNCT_2:def 1;
        then consider n being set such that
A18:    n in NAT and
A19:    Z = CSeq.n by A17,FUNCT_1:def 3;
        reconsider n as Element of NAT by A18;
        set P = F.n;
A20:    CSeq.n c= P by A12;
        ex P being set st P in rng F & x in P
        proof
          take P;
          thus thesis by A14,A16,A19,A20,FUNCT_1:def 3;
        end;
        hence thesis by TARSKI:def 4;
      end;
A21:  ex C being thin of P st union rng F = B \/ C
      proof
        set C = union rng F \ B;
A22:    union rng F = C \/ union rng F /\ B by XBOOLE_1:51
          .= B \/ C by A15,XBOOLE_1:28;
        reconsider C as Subset of Omega;
A23:    C c= union rng DSeq
        proof
          let x be set;
          assume
A24:      x in C;
          then x in union rng F by 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 A14,A26,FUNCT_1:def 3;
          reconsider n as Element of NAT by A27;
A29:      not x in union rng CSeq by A10,A24,XBOOLE_0:def 5;
          not x in CSeq.n
          proof
            dom CSeq = NAT by FUNCT_2:def 1;
            then
A30:        CSeq.n in rng CSeq by FUNCT_1:def 3;
            assume x in CSeq.n;
            hence thesis by A29,A30,TARSKI:def 4;
          end;
          then
A31:      x in F.n \ CSeq.n by A25,A28,XBOOLE_0:def 5;
          ex Z being set st x in Z & Z in rng DSeq
          proof
            take DSeq.n;
            dom DSeq = NAT by FUNCT_2:def 1;
            hence thesis by A11,A31,FUNCT_1:def 3;
          end;
          hence thesis by TARSKI:def 4;
        end;
        for A being set holds A in rng ESeq implies P.A = 0
        proof
          let A be set;
A32:      dom ESeq = NAT by FUNCT_2:def 1;
          assume A in rng ESeq;
          then ex n being set st n in NAT & A = ESeq.n by A32,FUNCT_1:def 3;
          hence thesis by A13;
        end;
        then
A33:    P.(union rng ESeq) = 0 by Th8;
        Union ESeq in Sigma by PROB_1:17;
        then
A34:    union rng ESeq in Sigma by CARD_3:def 4;
        union rng DSeq c= union rng ESeq
        proof
          let x be set;
          assume x in union rng DSeq;
          then consider Z being set such that
A35:      x in Z and
A36:      Z in rng DSeq by TARSKI:def 4;
          dom DSeq = NAT by FUNCT_2:def 1;
          then consider n being set such that
A37:      n in NAT and
A38:      Z = DSeq.n by A36,FUNCT_1:def 3;
          reconsider n as Element of NAT by A37;
          n in dom ESeq by A37,FUNCT_2:def 1;
          then
A39:      ESeq.n in rng ESeq by FUNCT_1:def 3;
          DSeq.n c= ESeq.n by A13;
          hence thesis by A35,A38,A39,TARSKI:def 4;
        end;
        then C c= union rng ESeq by A23,XBOOLE_1:1;
        then C is thin of P by A34,A33,Def4;
        then consider C being thin of P such that
A40:    union rng F = B \/ C by A22;
        take C;
        thus thesis by A40;
      end;
      for n,m being set st n <> m holds CSeq.n misses CSeq.m
      proof
        let n,m be set;
A41:    dom F = NAT by FUNCT_2:def 1
          .= dom CSeq by FUNCT_2:def 1;
        for n being set holds CSeq.n c= F.n
        proof
          let n be set;
          per cases;
          suppose
            n in dom F;
            hence thesis by A12;
          end;
          suppose
A42:        not n in dom F;
            then F.n = {} by FUNCT_1:def 2
              .= CSeq.n by A41,A42,FUNCT_1:def 2;
            hence thesis;
          end;
        end;
        then
A43:    CSeq.n c= F.n & CSeq.m c= F.m;
        assume n <> m;
        then F.n misses F.m by A8,PROB_2:def 2;
        then F.n /\ F.m = {} by XBOOLE_0:def 7;
        then CSeq.n /\ CSeq.m = {} by A43,XBOOLE_1:3,27;
        hence thesis by XBOOLE_0:def 7;
      end;
      then
A44:  CSeq is disjoint_valued by PROB_2:def 2;
      Sum(comP*F) = comP.(Union F)
      proof
A45:    for n holds comP.(F.n) = P.(CSeq.n)
        proof
          let n;
          F.n \ CSeq.n is thin of P by A12;
          then consider C being thin of P such that
A46:      C = F.n \ CSeq.n;
          F.n = (F.n /\ CSeq.n) \/ (F.n \ CSeq.n) by XBOOLE_1:51
            .= CSeq.n \/ C by A12,A46,XBOOLE_1:28;
          hence thesis by A5;
        end;
        for x being Element of NAT holds (comP*F).x = (P*CSeq).x
        proof
          let x be Element of NAT;
          (comP*F).x = comP.(F.x) by FUNCT_2:15
            .= P.(CSeq.x) by A45
            .= (P*CSeq).x by FUNCT_2:15;
          hence thesis;
        end;
        then
A47:    Sum(comP*F) = Sum(P*CSeq) by FUNCT_2:63;
        comP.(union rng F) = P.(union rng CSeq) by A5,A10,A21;
        then comP.(Union F) = P.(union rng CSeq) by CARD_3:def 4
          .= P.(Union CSeq) by CARD_3:def 4;
        hence thesis by A44,A47,PROB_3:46;
      end;
      hence thesis;
    end;
A48: for x being Element of COM(Sigma,P) holds comP.x >= 0
    proof
      let x be Element of COM(Sigma,P);
      consider B being set such that
A49:  B in Sigma and
A50:  ex C being thin of P st x = B \/ C by Def5;
      reconsider B as Element of Sigma by A49;
      comP.x = P.B by A4,A50;
      hence thesis by PROB_1:def 8;
    end;
    {} = B \/ C;
    then
A51: comP.{} = P.{} by A5,PROB_1:4
      .= 0 by VALUED_0:def 19;
A52: for A,B being Event of COM(Sigma,P) st A misses B holds comP.(A \/ B)
    = comP.A + comP.B
    proof
      let A,B be Event of COM(Sigma,P) such that
A53:  A misses B;
      reconsider A1=A, B1=B as Subset of Omega;
      reconsider BSeq = (A1,B1) followed_by {}Omega as SetSequence of Omega;
A54:  BSeq.1 = B by FUNCT_7:123;
A55:  BSeq.0 = A by FUNCT_7:122;
      for n being Nat holds BSeq.n in COM(Sigma,P)
      proof
        let n be Nat;
        per cases;
        suppose
          n = 0;
          hence thesis by A55;
        end;
        suppose
          n <> 0;
          then n >= 1 by NAT_1:14;
          then
A56:      n + 1 > 1 by NAT_1:13;
          per cases by A56,NAT_1:22;
          suppose
            n > 1;
            then BSeq.n = {} by FUNCT_7:124;
            hence thesis by PROB_1:4;
          end;
          suppose
            n = 1;
            hence thesis by A54;
          end;
        end;
      end;
      then rng BSeq c= COM(Sigma,P) by NAT_1:52;
      then reconsider BSeq as SetSequence of COM(Sigma,P) by RELAT_1:def 19;
      for m st 2<=m holds Partial_Sums(comP * BSeq).m = comP.A + comP.B
      proof
A57:    Partial_Sums(comP * BSeq).0 = (comP * BSeq).0 by SERIES_1:def 1
          .= comP.A by A55,FUNCT_2:15;
        0+1=1;
        then
A58:    Partial_Sums(comP * BSeq).1 = Partial_Sums(comP * BSeq).0 + (
        comP * BSeq).1 by SERIES_1:def 1
          .= comP.A + comP.B by A54,A57,FUNCT_2:15;
A59:    for n holds Partial_Sums(comP * BSeq).(2+n) = comP.A + comP.B
        proof
          defpred P[Element of NAT] means Partial_Sums(comP * BSeq).(2+$1) =
          comP.A + comP.B;
A60:      for k st P[k] holds P[k+1]
          proof
            let k such that
A61:        P[k];
A62:        2+k+1 > 0+1 by XREAL_1:8;
            thus Partial_Sums(comP * BSeq).(2+(k+1)) = Partial_Sums(comP *
            BSeq).(2+k) + (comP * BSeq).(2+k+1) by SERIES_1:def 1
              .= comP.A + comP.B + comP.(BSeq.(2+k+1)) by A61,FUNCT_2:15
              .= comP.A + comP.B + comP.{} by A62,FUNCT_7:124
              .= comP.A + comP.B by A51;
          end;
          2=1+1;
          then Partial_Sums(comP * BSeq).(2+0) = Partial_Sums(comP * BSeq).1+
          (comP * BSeq).2 by SERIES_1:def 1
            .= comP.A + comP.B + comP.(BSeq.2) by A58,FUNCT_2:15
            .= comP.A + comP.B + comP.{} by FUNCT_7:124
            .= comP.A + comP.B by A51;
          then
A63:      P[0];
          thus for k holds P[k] from NAT_1:sch 1(A63,A60);
        end;
        let m;
        assume 2 <= m;
        then consider k being Nat such that
A64:    m=2+k by NAT_1:10;
        k in NAT by ORDINAL1:def 12;
        hence thesis by A59,A64;
      end;
      then
A65:  Union BSeq = A \/ B & Sum(comP * BSeq) = comP.A + comP.B by DYNKIN:3
,PROB_1:1;
      BSeq is disjoint_valued by A53,Th3;
      hence thesis by A7,A65;
    end;
A66: for A,B being Event of COM(Sigma,P) st A c= B holds comP.(B \ A) =
    comP.B - comP.A
    proof
      let A,B be Event of COM(Sigma,P);
      assume
A67:  A c= B;
      comP.A + comP.(B \ A) = comP.(A \/ (B \ A)) by A52,XBOOLE_1:79
        .= comP.B by A67,XBOOLE_1:45;
      hence thesis;
    end;
A68: for A,B being Event of COM(Sigma,P) st A c= B holds comP.A <= comP.B
    proof
      let A,B be Event of COM(Sigma,P);
      assume A c= B;
      then comP.(B \ A) = comP.B - comP.A by A66;
      then 0 <= comP.B - comP.A by A48;
      then 0 + comP.A <= comP.B by XREAL_1:19;
      hence thesis;
    end;
A69: for BSeq being SetSequence of COM(Sigma,P) st BSeq is non-descending
    holds comP * BSeq is non-decreasing
    proof
      let BSeq be SetSequence of COM(Sigma,P) such that
A70:  BSeq is non-descending;
      for n,m st n <= m holds (comP * BSeq).n <= (comP * BSeq).m
      proof
        let n,m;
        assume n <= m;
        then BSeq.n c= BSeq.m by A70,PROB_1:def 5;
        then comP.(BSeq.n) <= comP.(BSeq.m) by A68;
        then (comP * BSeq).n <= comP.(BSeq.m) by FUNCT_2:15;
        hence thesis by FUNCT_2:15;
      end;
      hence thesis by SEQM_3:6;
    end;
A71: comP.Omega = comP.(B \/ Omega) .= P.Omega by A5,A1,PROB_1:5
      .= 1 by PROB_1:def 8;
A72: for A being Event of COM(Sigma,P) holds comP.A <= 1
    proof
      reconsider B = Omega as Event of COM(Sigma,P) by PROB_1:23;
      let A be Event of COM(Sigma,P);
      comP.A <= comP.B by A68;
      hence thesis by A71;
    end;
A73: for BSeq being SetSequence of COM(Sigma,P) for n holds (comP*BSeq).n <= 1
    proof
      let BSeq be SetSequence of COM(Sigma,P);
      let n;
      (comP*BSeq).n = comP.(BSeq.n) by FUNCT_2:15;
      hence thesis by A72;
    end;
A74: for BSeq being SetSequence of COM(Sigma,P) st BSeq is non-descending
    holds comP * BSeq is bounded_above & comP * BSeq is convergent
    proof
      let BSeq be SetSequence of COM(Sigma,P);
      assume BSeq is non-descending;
      then
A75:  comP * BSeq is non-decreasing by A69;
      for n holds (comP * BSeq).n < 2
      proof
        let n;
        (comP * BSeq).n + 0 < 1 + 1 by A73,XREAL_1:8;
        hence thesis;
      end;
      hence comP * BSeq is bounded_above by SEQ_2:def 3;
      hence thesis by A75;
    end;
    for BSeq being SetSequence of COM(Sigma,P) st BSeq is non-descending
    holds comP * BSeq is convergent & lim (comP * BSeq) = comP.Union BSeq
    proof
      let BSeq be SetSequence of COM(Sigma,P) such that
A76:  BSeq is non-descending;
      reconsider CSeq=Partial_Diff_Union(BSeq) as SetSequence of COM(Sigma,P);
A77:  for n holds Partial_Sums(comP * CSeq).n = (comP * BSeq).n
      proof
        defpred P[Element of NAT] means Partial_Sums(comP * CSeq).$1=(comP *
        BSeq).$1;
A78:    for k st P[k] holds P[k+1]
        proof
          let k such that
A79:      P[k];
A80:      BSeq.k c= BSeq.(k+1) by A76,PROB_2:7;
          thus Partial_Sums(comP * CSeq).(k+1) =(comP * BSeq).k + (comP * CSeq
          ).(k+1) by A79,SERIES_1:def 1
            .=comP.(BSeq.k) + (comP * CSeq).(k+1) by FUNCT_2:15
            .=comP.(BSeq.k) + comP.(CSeq.(k+1)) by FUNCT_2:15
            .=comP.(BSeq.k \/ CSeq.(k+1)) by A52,A76,Th18
            .=comP.(BSeq.k \/ (BSeq.(k+1) \ BSeq.k)) by A76,Th16
            .=comP.(BSeq.k \/ BSeq.(k+1)) by XBOOLE_1:39
            .=comP.(BSeq.(k+1)) by A80,XBOOLE_1:12
            .=(comP * BSeq).(k+1) by FUNCT_2:15;
        end;
        Partial_Sums(comP * CSeq).0 = (comP * CSeq).0 by SERIES_1:def 1
          .= comP.(CSeq.0) by FUNCT_2:15
          .= comP.(BSeq.0) by A76,Th16
          .= (comP * BSeq).0 by FUNCT_2:15;
        then
A81:    P[0];
        thus for k holds P[k] from NAT_1:sch 1(A81,A78);
      end;
      comP.Union BSeq = comP.Union CSeq by PROB_3:36
        .= Sum(comP * CSeq) by A7
        .= lim Partial_Sums(comP * CSeq);
      hence thesis by A74,A76,A77,FUNCT_2:63;
    end;
    then reconsider comP as Probability of COM(Sigma,P) by A48,A71,A52,
PROB_2:10;
    take comP;
    thus thesis by A5;
  end;
  uniqueness
  proof
    let P1,P2 be Probability of COM(Sigma,P) such that
A82: for B being set st B in Sigma for C being thin of P holds P1.(B
    \/ C) = P.B and
A83: for B being set st B in Sigma for C being thin of P holds P2.(B
    \/ C) = P.B;
    for x being set holds x in COM(Sigma,P) implies P1.x = P2.x
   proof
      let x be set;
      assume x in COM(Sigma,P);
      then consider B being set such that
A84:  B in Sigma & ex C being thin of P st x = B \/ C by Def5;
      P1.x = P.B by A82,A84
        .= P2.x by A83,A84;
      hence thesis;
    end;
    hence thesis by FUNCT_2:12;
  end;
end;

theorem
  COM(P) = COM(P2M P)
proof
  set Y = COM(P);
  COM(Sigma,P) = COM(Sigma,P2M P) by Th27;
  then reconsider Y1=P2M(Y) as sigma_Measure of COM(Sigma,P2M(P));
  for B being set st B in Sigma for C being thin of P2M(P) holds Y1.(B \/
  C) = (P2M(P)).B
  proof
    let B be set such that
A1: B in Sigma;
    let C be thin of P2M(P);
    reconsider C1=C as thin of P by Th23;
    Y.(B \/ C1) = P.B by A1,Def8;
    hence thesis;
  end;
  hence thesis by MEASURE3:def 5;
end;

theorem
  COM(P) is_complete COM(Sigma,P)
proof
  for A being Subset of Omega for B being set st B in COM(Sigma,P) & A c=
  B & (COM P).B = 0 holds A in COM(Sigma,P)
  proof
    let A be Subset of Omega;
    let B be set;
    assume
A1: B in COM(Sigma,P);
    assume that
A2: A c= B and
A3: (COM P).B = 0;
    ex B1 being set st (B1 in Sigma & ex C1 being thin of P st A = B1 \/ C1 )
    proof
      take {};
      consider B2 being set such that
A4:   B2 in Sigma and
A5:   ex C2 being thin of P st B = B2 \/ C2 by A1,Def5;
A6:   P.B2 = 0 by A3,A4,A5,Def8;
      consider C2 being thin of P such that
A7:   B = B2 \/ C2 by A5;
      set C1 = (A /\ B2) \/ (A /\ C2);
      consider D2 being set such that
A8:   D2 in Sigma and
A9:   C2 c= D2 and
A10:  P.D2 = 0 by Def4;
      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,17;
      ex O being set st O in Sigma & C1 c= O & P.O = 0
      proof
        reconsider B2,D2 as Element of Sigma by A4,A8;
        take O;
        P.(B2 \/ D2) <= 0 + 0 by A6,A10,PROB_1:39;
        hence thesis by A11,PROB_1:def 8,XBOOLE_1:13;
      end;
      then
A12:  C1 is thin of P by Def4;
      A = A /\ (B2 \/ C2) by A2,A7,XBOOLE_1:28
        .= {} \/ C1 by XBOOLE_1:23;
      hence thesis by A12,PROB_1:4;
    end;
    hence thesis by Def5;
  end;
  hence thesis by Def3;
end;

theorem Th39:
  for A being Event of Sigma holds P.A = (COM P).A
proof
  reconsider C = {} as thin of P by Th24;
  let A be Event of Sigma;
  thus P.A = (COM P).(A \/ C) by Def8
    .= (COM P).A;
end;

theorem Th40:
  for C being thin of P holds (COM P).C = 0
proof
  let C be thin of P;
  consider A being set such that
A1: A in Sigma and
A2: C c= A and
A3: P.A = 0 by Def4;
  reconsider A as Event of Sigma by A1;
A4: (COM P).A = 0 by A3,Th39;
  Sigma c= COM(Sigma,P) by Th28;
  then reconsider A as Event of COM(Sigma,P) by A1;
  (COM P).C <= (COM P).A by A2,PROB_1:34;
  hence thesis by A4,PROB_1:def 8;
end;

theorem
  for A being Element of COM(Sigma,P), B being set st B in ProbPart(A)
  holds P.B = (COM P).A
proof
  let A be Element of COM(Sigma,P), B be set such that
A1: B in ProbPart(A);
  reconsider C = A \ B as thin of P by A1,Def7;
A2: B in Sigma by A1,Def7;
  B c= A by A1,Def7;
  then
A3: A = B \/ C by XBOOLE_1:45;
  Sigma c= COM(Sigma,P) by Th28;
  then reconsider B as Event of COM(Sigma,P) by A2;
  reconsider A as Event of COM(Sigma,P);
  B misses C by XBOOLE_1:79;
  then
A4: (COM P).A = (COM P).B + (COM P).C by A3,PROB_1:def 8
    .= (COM P).B + 0 by Th40
    .= (COM P).B;
  reconsider B as Event of Sigma by A1,Def7;
  (COM P).A = P.B by A4,Th39;
  hence thesis;
end;