:: Set Sequences and Monotone Class
::  by Bo Zhang , Hiroshi Yamazaki and Yatsuka Nakamura
::
:: Received August 12, 2005
:: Copyright (c) 2005 Association of Mizar Users

environ

 vocabularies RELAT_1, PROB_1, SEQ_1, SEQ_2, SETLIM_2, ABSVALUE, VECTSP_1,
      SETWISEO, FINSOP_1, ARYTM_1, ORDINAL2, ARYTM, BOOLE, SUBSET_1, PROB_2,
      SETFAM_1, TARSKI, SEQM_3, FINSUB_1, LATTICES, SERIES_1, RLVECT_1,
      FINSEQ_1, FUNCT_1, PROB_3;
 notations FINSEQ_1, ORDINAL1, CARD_3, FINSUB_1, REAL_1, RELAT_1, TARSKI,
      XBOOLE_0, RVSUM_1, FINSOP_1, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0,
      SETFAM_1, BINOP_1, SETWOP_2, BINOP_2, SETWISEO, NAT_1, COMPLEX1, SEQ_1,
      SEQ_2, RELSET_1, FUNCT_1, FUNCT_2, PROB_1, PROB_2, KURATO_2, SETLIM_2,
      PSCOMP_1, SEQM_3, SETLIM_1, RINFSUP1, SERIES_1, PCOMPS_1;
 constructors REAL_1, NAT_1, SETLIM_2, SUPINF_2, KURATO_2, SETLIM_1, SERIES_1,
      RINFSUP1, SETWISEO, FINSOP_1, PROB_2, BINOP_2, PARTFUN3, SETFAM_1;
 registrations SEQ_1, SUBSET_1, XREAL_0, RELSET_1, ARYTM_3, MEMBERED, ORDINAL2,
      FUNCT_1, PROB_1;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
 definitions TARSKI, XBOOLE_0;
 theorems FUNCT_1, FUNCT_2, SEQ_1, ABSVALUE, SEQ_2, SUBSET_1, NAT_1, TARSKI,
      XBOOLE_0, XBOOLE_1, PROB_2, SETLIM_2, RINFSUP1, RELAT_1, SETFAM_1,
      ZFMISC_1, SEQM_3, CARD_3, SETLIM_1, PROB_1, FINSUB_1, SERIES_1, FINSEQ_1,
      FINSEQ_2, FINSEQ_3, RVSUM_1, FINSOP_1, SETWISEO, BINOP_2, XREAL_1;
 schemes FUNCT_1, NAT_1, RECDEF_1, FINSEQ_1, FINSEQ_2, PARTFUN1;

begin

 reserve n,m,k,i,j for Nat,
         g,q,r,s,t,p for real number,
         x,y,z,X,Y,Z for set,
         A1 for SetSequence of X,
         F1 for FinSequence of bool X,
         RFin for FinSequence of REAL,
         Si for SigmaField of X,
         XSeq,YSeq for SetSequence of Si,
         Omega for non empty set,
         Sigma for SigmaField of Omega,
         ASeq,BSeq for SetSequence of Sigma,
         P for Probability of Sigma;

LM1: for s st 0 < s & t <= p holds t < p+s & t-s < p
proof let s; assume 0<s & t <= p;
  then t+0 < p+s by XREAL_1:10;
  hence thesis by XREAL_1:21;
end;

theorem Th50:
  for f being FinSequence holds not 0 in dom f
proof let f be FinSequence;
  assume 0 in dom f;then
  0 in Seg len f by FINSEQ_1:def 3;
  hence contradiction by FINSEQ_1:3;
end;

theorem Th51:
  for f being FinSequence holds
    n in dom f iff n<>0 & n <= len f
proof
  let f be FinSequence;
  n in dom f iff n>=1 & n <= len f by FINSEQ_3:27;
  hence thesis by NAT_1:39;
end;

theorem Th1:
  for f being Real_Sequence st
  (ex k st for n st k<=n holds f.n=g) holds
    f is convergent & lim f = g
proof
  let f be Real_Sequence;
  given k such that
A1: for n st k<=n holds f.n=g;
A2: now let p such that
B1: 0 < p;
  take k;
  thus for m st k<=m holds abs(f.m-g)<p
  proof let m such that
C1: k<=m;
    f.m = g by C1,A1;
    hence thesis by B1,ABSVALUE:7;
  end;
 end;
 hence f is convergent by SEQ_2:def 6;
 hence thesis by A2,SEQ_2:def 7;
end;

theorem Th2:
  (P * ASeq).n >= 0
proof
A0: ASeq.n is Event of Sigma by PROB_1:57;
  dom (P * ASeq) = NAT by SEQ_1:3;then
  (P * ASeq).n = P.(ASeq.n) by FUNCT_1:22;
  hence thesis by A0,PROB_1:def 13;
end;

theorem Th3:
  ASeq.n c= BSeq.n implies (P * ASeq).n <= (P * BSeq).n
proof
  assume
A1: ASeq.n c= BSeq.n;
  ASeq.n in Sigma & BSeq.n in Sigma by PROB_1:def 9;then
  ASeq.n is Event of Sigma & BSeq.n is Event of Sigma by PROB_1:def 10;then
  P.(ASeq.n) <= P.(BSeq.n) by A1,PROB_1:70;then
  (P * ASeq).n <= P.(BSeq.n) by PROB_2:11;
  hence thesis by PROB_2:11;
end;

theorem Th4:
  ASeq is non-decreasing implies P * ASeq is non-decreasing
proof assume
A0: ASeq is non-decreasing;
A1: dom (P * ASeq) = NAT by SEQ_1:3;
 now let n,m such that
B1: n <= m;
B2: ASeq.n is Event of Sigma & ASeq.m is Event of Sigma by PROB_1:57;
B3: ASeq.n c= ASeq.m by B1,A0,PROB_1:def 7;
  (P * ASeq).n = P.(ASeq.n) & (P * ASeq).m = P.(ASeq.m) by A1,FUNCT_1:22;
  hence (P * ASeq).n <= (P * ASeq).m by B3,B2,PROB_1:70;
 end;
 hence thesis by SEQM_3:12;
end;

theorem Th5:
  ASeq is non-increasing implies P * ASeq is non-increasing
proof assume
A0: ASeq is non-increasing;
A1: dom (P * ASeq) = NAT by SEQ_1:3;
 now let n,m such that
B1: n <= m;
B2: ASeq.n is Event of Sigma & ASeq.m is Event of Sigma by PROB_1:57;
B3: ASeq.m c= ASeq.n by B1,A0,PROB_1:def 6;
  (P * ASeq).n = P.(ASeq.n) & (P * ASeq).m = P.(ASeq.m) by A1,FUNCT_1:22;
  hence (P * ASeq).m <= (P * ASeq).n by B3,B2,PROB_1:70;
 end;
 hence thesis by SEQM_3:14;
end;

definition
  let A1 be Function;
  func Partial_Intersection A1 -> Function means
:def1: dom it = NAT & it.0 = A1.0 &
      for n being Nat holds it.(n+1) = it.n /\ A1.(n+1);
  existence
  proof
    deffunc G(Nat,set) = $2 /\ A1.($1+1);
    ex f being Function st dom f = NAT &
    f.0 = A1.0 & for n being Element of NAT holds f.(n+1) = G(n,f.n)
    from RECDEF_1:sch 3;
    hence thesis;
  end;
  uniqueness
proof
   let S1,S2 be Function such that
A1:dom S1 = NAT & S1.0 = A1.0 &
   for n being Nat holds S1.(n+1) = S1.n /\ A1.(n+1) and
A2:dom S2 = NAT & S2.0 = A1.0 &
   for n being Nat holds S2.(n+1) = S2.n /\ A1.(n+1);
   defpred P[set] means S1.$1 = S2.$1;
   for n being set holds n in NAT implies P[n]
   proof let n be set; assume n in NAT;then
     reconsider n as Nat;
A4:  P[0] by A1,A2;
A5:  for k st P[k] holds P[k+1]
     proof
       let k;
       assume S1.k = S2.k;
       hence S1.(k+1) = S2.k /\ A1.(k+1) by A1
            .= S2.(k+1) by A2;
     end;
     for k being Nat holds P[k] from NAT_1:sch 1(A4,A5);
     then S1.n = S2.n;
     hence thesis;
   end;
   hence thesis by A1,A2,FUNCT_1:9;
 end;
end;

definition
  let X be set, A1 be SetSequence of X;
  redefine func Partial_Intersection A1 -> SetSequence of X;
  coherence
 proof
    defpred P[set] means (Partial_Intersection A1).$1 c= X;
    (Partial_Intersection A1).0 = A1.0 by def1; then
B1: P[0];
B2: for k st P[k] holds P[k+1]
    proof let k; assume (Partial_Intersection A1).k c= X;then
      (Partial_Intersection A1).k /\ A1.(k+1) c= X by XBOOLE_1:108;
      hence thesis by def1;
    end;
B3: for k being Nat holds P[k] from NAT_1:sch 1(B1,B2);
B4: dom Partial_Intersection A1 = NAT by def1;
    rng Partial_Intersection A1 c= bool X
    proof let x be set; assume x in rng Partial_Intersection A1; then
      consider n being set such that
B5:   n in NAT & x = (Partial_Intersection A1).n by B4,FUNCT_1:def 5;
      reconsider n as Nat by B5;
      P[n] by B3;
      hence thesis by B5;
    end;
    hence thesis by B4,FUNCT_2:4;
 end;
end;

definition
  let A1 be Function;
  func Partial_Union A1 -> Function means
:def2: dom it = NAT & it.0 = A1.0 &
      for n being Nat holds it.(n+1) = it.n \/ A1.(n+1);
  existence
  proof
    deffunc G(Nat,set) = $2 \/ A1.($1+1);
    ex f being Function st dom f = NAT &
    f.0 = A1.0 & for n being Element of NAT holds f.(n+1) = G(n,f.n)
    from RECDEF_1:sch 3;
    hence thesis;
  end;
  uniqueness
proof
   let S1,S2 be Function such that
A1:dom S1 = NAT & S1.0 = A1.0 &
   for n being Nat holds S1.(n+1) = S1.n \/ A1.(n+1) and
A2:dom S2 = NAT & S2.0 = A1.0 &
   for n being Nat holds S2.(n+1) = S2.n \/ A1.(n+1);
   defpred P[set] means S1.$1 = S2.$1;
   for n being set holds n in NAT implies P[n]
   proof
     let n be set; assume n in NAT;then
     reconsider n as Nat;
A4:  P[0] by A1,A2;
A5:  for k st P[k] holds P[k+1]
     proof
       let k;
       assume S1.k = S2.k;
       hence S1.(k+1) = S2.k \/ A1.(k+1) by A1
            .= S2.(k+1) by A2;
     end;
     for k being Nat holds P[k] from NAT_1:sch 1(A4,A5);
     then S1.n = S2.n;
     hence thesis;
   end;
   hence thesis by A1,A2,FUNCT_1:9;
 end;
end;

definition
  let X be set, A1 be SetSequence of X;
  redefine func Partial_Union A1 -> SetSequence of X;
  coherence
 proof
    defpred P[set] means (Partial_Union A1).$1 c= X;
    (Partial_Union A1).0 = A1.0 by def2; then
B1: P[0];
B2: for k st P[k] holds P[k+1]
    proof let k; assume (Partial_Union A1).k c= X;then
      (Partial_Union A1).k \/ A1.(k+1) c= X by XBOOLE_1:8;
      hence thesis by def2;
    end;
B3: for k being Nat holds P[k] from NAT_1:sch 1(B1,B2);
B4: dom Partial_Union A1 = NAT by def2;
    rng Partial_Union A1 c= bool X
    proof let x be set; assume x in rng Partial_Union A1; then
      consider n being set such that
B5:   n in NAT & x = (Partial_Union A1).n by B4,FUNCT_1:def 5;
      reconsider n as Nat by B5;
      P[n] by B3;
      hence thesis by B5;
    end;
    hence thesis by B4,FUNCT_2:4;
 end;
end;

theorem Th8:
  (Partial_Intersection A1).n c= A1.n
proof
  per cases by NAT_1:22;
  suppose n = 0;
    hence thesis by def1;
  end;
  suppose ex k st n = k+1;then
    consider k such that
B1: n = k+1;
    (Partial_Intersection A1).(k+1) = (Partial_Intersection A1).k /\ A1.(k+1)
      by def1;
    hence (Partial_Intersection A1).n c= A1.n by B1,XBOOLE_1:17;
  end;
end;

theorem Th9:
  A1.n c= (Partial_Union A1).n
proof
  per cases by NAT_1:22;
  suppose n = 0;
    hence thesis by def2;
  end;
  suppose ex k st n = k+1;then
    consider k such that
B1: n = k+1;
    (Partial_Union A1).(k+1) = (Partial_Union A1).k \/ A1.(k+1) by def2;
    hence A1.n c= (Partial_Union A1).n by B1,XBOOLE_1:7;
  end;
end;

theorem Th10:
  Partial_Intersection A1 is non-increasing
proof
 now let n;
 (Partial_Intersection A1).(n+1) = (Partial_Intersection A1).n /\ A1.(n+1)
  by def1;
 hence (Partial_Intersection A1).(n+1) c= (Partial_Intersection A1).n
  by XBOOLE_1:17;
 end;
 hence thesis by PROB_2:14;
end;

theorem Th11:
  Partial_Union A1 is non-decreasing
proof
  now let n;
    (Partial_Union A1).(n+1) = (Partial_Union A1).n \/ A1.(n+1) by def2;
    hence (Partial_Union A1).n c= (Partial_Union A1).(n+1) by XBOOLE_1:7;
  end;
  hence thesis by PROB_2:15;
end;

theorem Th12:
  x in (Partial_Intersection A1).n iff for k st k <= n holds x in A1.k
proof
 thus x in (Partial_Intersection A1).n implies for k st k <= n holds x in A1.k
 proof assume
B1: x in (Partial_Intersection A1).n;
    for k st k <= n holds x in A1.k
    proof let k such that
C1:   k <= n;
      Partial_Intersection A1 is non-increasing by Th10;then
C2:   (Partial_Intersection A1).n c= (Partial_Intersection A1).k
        by C1,PROB_1:def 6;
      (Partial_Intersection A1).k c= A1.k by Th8;then
      (Partial_Intersection A1).n c= A1.k by C2,XBOOLE_1:1;
      hence thesis by B1;
    end;
    hence thesis;
  end;
  defpred P[Nat] means (for k st k <= $1 holds x in A1.k) implies
    x in (Partial_Intersection A1).$1;
A1: P[0]
    proof assume for k st k <= 0 holds x in A1.k;then
      x in A1.0;
      hence thesis by def1;
    end;
A2: for i st P[i] holds P[i+1]
    proof let i such that
E1:   (for k st k <= i holds x in A1.k) implies
        x in (Partial_Intersection A1).i;assume
E2:   for k st k <= i+1 holds x in A1.k;
E3:   now let k such that
    F1: k <= i;
        k <= i+1 by F1,NAT_1:37;
        hence x in A1.k by E2;
      end;
  E4: x in A1.(i+1) by E2;
      (Partial_Intersection A1).(i+1) =
        (Partial_Intersection A1).i /\ A1.(i+1) by def1;
      hence thesis by E1,E3,E4,XBOOLE_0:def 3;
    end;
   for n holds P[n] from NAT_1:sch 1(A1,A2);
   hence thesis;
end;

theorem Th13:
  x in (Partial_Union A1).n iff ex k st k <= n & x in A1.k
proof
  defpred P[Nat] means (x in (Partial_Union A1).$1 implies
   ex k st k <= $1 & x in A1.k);
  B1: P[0]
    proof assume C0: x in (Partial_Union A1).0;
      take 0;
      thus thesis by C0,def2;
    end;
  B2: for i st P[i] holds P[i+1]
    proof let i such that
D1: x in (Partial_Union A1).i implies ex k st k <= i & x in A1.k;
    assume
D2: x in (Partial_Union A1).(i+1);
D3: (Partial_Union A1).(i+1) = (Partial_Union A1).i \/ A1.(i+1) by def2;
    now per cases by D2,D3,XBOOLE_0:def 2;
     case x in (Partial_Union A1).i;then
       consider k such that
   E1: k <= i & x in A1.k by D1;
       take k;
       k <= i+1 by E1,NAT_1:37;
       hence ex k st k <= i+1 & x in A1.k by E1;
     end;
     case x in A1.(i+1);
       hence ex k st k <= i+1 & x in A1.k;
     end;
    end;
     hence thesis;
    end;
  for n holds P[n] from NAT_1:sch 1(B1,B2);
  hence x in (Partial_Union A1).n implies ex k st k <= n & x in A1.k;
  given i such that
A2: i <= n and
A3: x in A1.i;
    A1.i c= (Partial_Union A1).i by Th9;then
A4: x in (Partial_Union A1).i by A3;
     Partial_Union A1 is non-decreasing by Th11;then
     (Partial_Union A1).i c= (Partial_Union A1).n by A2,PROB_1:def 7;
 hence thesis by A4;
end;

theorem Th14:
  Intersection Partial_Intersection A1 = Intersection A1
proof
 thus Intersection Partial_Intersection A1 c= Intersection A1
 proof
   let x; assume
A1: x in Intersection Partial_Intersection A1;
   for n holds x in A1.n
   proof let n;
     x in (Partial_Intersection A1).n by A1,PROB_1:29;
     hence thesis by Th12;
   end;
   hence thesis by PROB_1:29;
 end;
    let x; assume
B1: x in Intersection A1;
    for n holds x in (Partial_Intersection A1).n
    proof let n;
      for k st k <= n holds x in A1.k by B1,PROB_1:29;
      hence thesis by Th12;
    end;
    hence thesis by PROB_1:29;
end;

theorem Th15:
  Union Partial_Union A1 = Union A1
proof
  thus Union Partial_Union A1 c= Union A1
  proof
    let x be set; assume x in Union Partial_Union A1;then
    consider n such that
A1: x in (Partial_Union A1).n by PROB_1:25;
    consider k such that
A2: k <= n & x in A1.k by A1,Th13;
    thus thesis by A2,PROB_1:25;
  end;
    let x be set;
    assume x in Union A1;then
    consider n such that
B1: x in A1.n by PROB_1:25;
    x in (Partial_Union A1).n by B1,Th13;
    hence thesis by PROB_1:25;
end;

definition let A1 be Function;
  func Partial_Diff_Union A1 -> Function means
:def3:  dom it = NAT & it.0 = A1.0 &
  for n being Nat holds it.(n+1) = A1.(n+1) \ (Partial_Union A1).n;
  existence
  proof
    deffunc G(Nat,set) = A1.($1+1) \ (Partial_Union A1).$1;
    ex f being Function st dom f = NAT &
    f.0 = A1.0 & for n being Element of NAT holds f.(n+1) = G(n,f.n)
    from RECDEF_1:sch 3;
    hence thesis;
  end;
  uniqueness
proof
   let S1,S2 be Function such that
A1:dom S1 = NAT & S1.0 = A1.0 &
   for n being Nat holds S1.(n+1) = A1.(n+1) \ (Partial_Union A1).n and
A2:dom S2 = NAT & S2.0 = A1.0 &
   for n being Nat holds S2.(n+1) = A1.(n+1) \ (Partial_Union A1).n;
   defpred P[set] means S1.$1 = S2.$1;
   for n being set holds n in NAT implies P[n]
   proof let n be set; assume n in NAT;then
     reconsider n as Nat;
 A4: P[0] by A1,A2;
 A5: for k st P[k] holds P[k+1]
     proof let k; assume S1.k = S2.k;
       thus S1.(k+1) = A1.(k+1) \ (Partial_Union A1).k by A1
             .= S2.(k+1) by A2;
     end;
     for k being Nat holds P[k] from NAT_1:sch 1(A4,A5);
     then S1.n = S2.n;
     hence thesis;
   end;
   hence thesis by A1,A2,FUNCT_1:9;
 end;
end;

definition
  let X be set, A1 be SetSequence of X;
  redefine func Partial_Diff_Union A1 -> SetSequence of X;
  coherence
 proof
    defpred P[set] means (Partial_Diff_Union A1).$1 c= X;
    (Partial_Diff_Union A1).0 = A1.0 by def3; then
B1: P[0];
B2: for k st P[k] holds P[k+1]
    proof let k;
      A1.(k+1) \ (Partial_Union A1).k c= X by XBOOLE_1:109;
      hence thesis by def3;
    end;
B3: for k being Nat holds P[k] from NAT_1:sch 1(B1,B2);
B4: dom Partial_Diff_Union A1 = NAT by def3;
    rng Partial_Diff_Union A1 c= bool X
    proof let x be set; assume x in rng Partial_Diff_Union A1; then
      consider n being set such that
B5:   n in NAT & x = (Partial_Diff_Union A1).n by B4,FUNCT_1:def 5;
      reconsider n as Nat by B5;
      P[n] by B3;
      hence thesis by B5;
    end;
    hence thesis by B4,FUNCT_2:4;
 end;
end;

theorem Th17:
  x in (Partial_Diff_Union A1).n iff
    x in A1.n & for k st k < n holds not x in A1.k
proof
  thus x in (Partial_Diff_Union A1).n implies
    x in A1.n & for k st k < n holds not x in A1.k
  proof assume
B1: x in (Partial_Diff_Union A1).n;
   now per cases by NAT_1:22;
   case n = 0;
     hence thesis by B1,def3,NAT_1:18;
   end;
   case ex n1 being Nat st n = n1 + 1;then
     consider n1 being Nat such that
BC1: n = n1+1;
BC11:x in A1.(n1+1) \ (Partial_Union A1).n1 by B1,BC1,def3;then
BC2: x in A1.n & not x in (Partial_Union A1).n1 by BC1,XBOOLE_0:def 4;
     for k st k < n holds not x in A1.k
     proof let k; assume k < n; then
       k <= n1 by BC1,NAT_1:38;
       hence thesis by BC2,Th13;
     end;
     hence thesis by BC11,BC1,XBOOLE_0:def 4;
   end;
   end;
  hence thesis;
  end;
  assume
A1: x in A1.n & for k st k < n holds not x in A1.k;
  now per cases by NAT_1:22;
   case n = 0;
     hence thesis by A1,def3;
   end;
   case ex n1 being Nat st n = n1 + 1;then
    consider n1 being Nat such that
AC1: n = n1+1;
    for k st k <= n1 holds not x in A1.k
    proof let k; assume k <= n1; then
      k < n1+1 by NAT_1:38;
      hence thesis by A1,AC1;
    end;then
    not x in (Partial_Union A1).n1 by Th13;then
    x in A1.(n1+1) \ (Partial_Union A1).n1 by A1,AC1,XBOOLE_0:def 4;
    hence thesis by AC1,def3;
   end;
   end;
 hence thesis;
end;

theorem Th18:
  (Partial_Diff_Union A1).n c= A1.n
proof
  x in (Partial_Diff_Union A1).n implies x in A1.n by Th17;
  hence thesis by TARSKI:def 3;
end;

theorem Th19:
  (Partial_Diff_Union A1).n c= (Partial_Union A1).n
proof
  (Partial_Diff_Union A1).n c= A1.n & A1.n c= (Partial_Union A1).n
    by Th18,Th9;
  hence thesis by XBOOLE_1:1;
end;

theorem Th20:
  Partial_Union (Partial_Diff_Union A1) = Partial_Union A1
proof
 for n holds (Partial_Union (Partial_Diff_Union A1)).n
    = (Partial_Union A1).n
 proof
   set A2 = Partial_Diff_Union A1;
   defpred P[set] means
    (Partial_Union A2).$1 = (Partial_Union A1).$1;
   (Partial_Union (Partial_Diff_Union A1)).0 = A2.0 by def2
       .= A1.0 by def3 .= (Partial_Union A1).0 by def2; then
B1:P[0];
B2:for k st P[k] holds P[k+1]
   proof let k such that
C1:  (Partial_Union A2).k = (Partial_Union A1).k;
     thus (Partial_Union A2).(k+1)
       = A2.(k+1) \/ (Partial_Union A2).k by def2
      .= (A1.(k+1) \ (Partial_Union A1).k) \/ (Partial_Union A1).k by C1,def3
      .= A1.(k+1) \/ (Partial_Union A1).k by XBOOLE_1:39
      .= (Partial_Union A1).(k+1) by def2;
   end;
   thus for k being Nat holds P[k] from NAT_1:sch 1(B1,B2);
 end;
 hence thesis by FUNCT_2:113;
end;

theorem Th21:
  Union Partial_Diff_Union A1 = Union A1
proof
  thus Union Partial_Diff_Union A1
    = Union Partial_Union (Partial_Diff_Union A1) by Th15
   .= Union Partial_Union A1 by Th20 .= Union A1 by Th15;
end;

definition let X,A1;
  redefine attr A1 is disjoint_valued means
:def4:  for m,n st m <> n holds A1.m misses A1.n;
  compatibility
  proof
    thus A1 is disjoint_valued implies
      for m,n st m <> n holds A1.m misses A1.n by PROB_2:def 3;
    assume A2:for m,n st m <> n holds A1.m misses A1.n;
    now let x,y; assume A3:x <> y;
      per cases;
      suppose x in dom A1 & y in dom A1;
        hence A1.x misses A1.y by A2,A3;
      end;
      suppose not (x in dom A1 & y in dom A1);
        then A1.x = {} or A1.y = {} by FUNCT_1:def 4;
        hence A1.x misses A1.y by XBOOLE_1:65;
      end;
    end;
    hence thesis by PROB_2:def 3;
  end;
end;

theorem Th22:
  Partial_Diff_Union A1 is disjoint_valued
proof
  for m,n st m <> n holds
    (Partial_Diff_Union A1).n misses (Partial_Diff_Union A1).m
  proof let m,n such that
A1: m <> n;
    assume (Partial_Diff_Union A1).n
      meets (Partial_Diff_Union A1).m;then
    consider x being set such that
B2: x in (Partial_Diff_Union A1).n & x in (Partial_Diff_Union A1).m
      by XBOOLE_0:3;
    per cases by A1,XREAL_1:1;
    suppose m < n;then
      not x in A1.m by B2,Th17;
      hence contradiction by B2,Th17;
    end;
    suppose n < m;then
      not x in A1.n by B2,Th17;
      hence contradiction by B2,Th17;
    end;
  end;
  hence thesis by def4;
end;

definition
  let X be set,
      Si be SigmaField of X,
      XSeq be SetSequence of Si;
  redefine func Partial_Intersection XSeq -> SetSequence of Si;
 coherence
  proof
    defpred P[set] means (Partial_Intersection XSeq).$1 in Si;
    (Partial_Intersection XSeq).0 = XSeq.0 by def1; then
B1: P[0] by PROB_1:def 9;
B2: for k st P[k] holds P[k+1]
    proof let k; assume (Partial_Intersection XSeq).k in Si;then
  C1: (Partial_Intersection XSeq).k is Event of Si by PROB_1:def 10;
      XSeq.(k+1) in Si by PROB_1:def 9;then
      XSeq.(k+1) is Event of Si by PROB_1:def 10;then
      (Partial_Intersection XSeq).k /\ XSeq.(k+1) is Event of Si
        by C1,PROB_1:49;then
      (Partial_Intersection XSeq).k /\ XSeq.(k+1) in Si by PROB_1:def 10;
      hence thesis by def1;
    end;
    for k being Nat holds P[k] from NAT_1:sch 1(B1,B2);
    hence thesis by PROB_1:def 9;
  end;
end;

definition let X be set,
               Si be SigmaField of X,
               XSeq be SetSequence of Si;
 redefine func Partial_Union XSeq -> SetSequence of Si;
  coherence
  proof
    defpred P[set] means (Partial_Union XSeq).$1 in Si;
    (Partial_Union XSeq).0 = XSeq.0 by def2; then
B1: P[0] by PROB_1:def 9;
B2: for k st P[k] holds P[k+1]
    proof let k; assume (Partial_Union XSeq).k in Si;then
  C1: (Partial_Union XSeq).k is Event of Si by PROB_1:def 10;
      XSeq.(k+1) in Si by PROB_1:def 9;then
      XSeq.(k+1) is Event of Si by PROB_1:def 10;then
      (Partial_Union XSeq).k \/ XSeq.(k+1) is Event of Si
        by C1,PROB_1:51;then
      (Partial_Union XSeq).k \/ XSeq.(k+1) in Si by PROB_1:def 10;
      hence thesis by def2;
    end;
    for k being Nat holds P[k] from NAT_1:sch 1(B1,B2);
    hence thesis by PROB_1:def 9;
  end;
end;

definition let X be set,
               Si be SigmaField of X,
               XSeq be SetSequence of Si;
  redefine func Partial_Diff_Union XSeq -> SetSequence of Si;
  coherence
  proof
A1: (Partial_Diff_Union XSeq).0 in Si
    proof
      (Partial_Diff_Union XSeq).0 = XSeq.0 by def3;
      hence thesis by PROB_1:def 9;
    end;
    for m being Nat holds (Partial_Diff_Union XSeq).m in Si
    proof let m be Nat;
      now per cases by NAT_1:22;
        case m = 0;
          hence thesis by A1;
        end;
        case ex k st m = k+1;then
          consider k such that
B1:       m = k+1;
          (Partial_Union XSeq).k in Si &
          XSeq.(k+1) in Si by PROB_1:def 9;then
          XSeq.(k+1) \ (Partial_Union XSeq).k in Si by PROB_1:44;
          hence thesis by B1,def3;
        end;
      end;
      hence thesis;
    end;
    hence thesis by PROB_1:def 9;
  end;
end;

theorem Th40:
  (P * Partial_Union ASeq) is non-decreasing
proof
  Partial_Union ASeq is non-decreasing by Th11;
  hence thesis by Th4;
end;

theorem
  (P * Partial_Intersection ASeq) is non-increasing
proof
  Partial_Intersection ASeq is non-increasing by Th10;
  hence thesis by Th5;
end;

theorem
  Partial_Sums(P * ASeq) is non-decreasing
proof
  for n holds (P * ASeq).n >= 0 by Th2;
  hence thesis by SERIES_1:19;
end;

theorem Th43:
  (P * Partial_Union ASeq).0 = Partial_Sums(P * ASeq).0
 proof
B1: dom (P * ASeq) = NAT & dom (P * Partial_Union ASeq) = NAT by SEQ_1:3;
B2: (P * Partial_Union ASeq).0
        = P.((Partial_Union ASeq).0) by B1,FUNCT_1:22
       .= P.(ASeq.0) by def2;
    Partial_Sums(P * ASeq).0 = (P * ASeq).0 by SERIES_1:def 1
       .= P.(ASeq.0) by B1,FUNCT_1:22;
    hence thesis by B2;
 end;

theorem Th44:
  P * Partial_Union ASeq is convergent &
    lim (P * Partial_Union ASeq) = sup (P * Partial_Union ASeq) &
    lim (P * Partial_Union ASeq) = P.Union ASeq
  proof
A1: Partial_Union ASeq is non-decreasing by Th11;then
    P * Partial_Union ASeq is convergent by PROB_2:20;then
    P * Partial_Union ASeq is bounded by SEQ_2:27;then
A3: P * Partial_Union ASeq is bounded_above by SEQ_2:def 5;
A4: P * Partial_Union ASeq is non-decreasing by Th40;
    lim (P * Partial_Union ASeq) = P.Union (Partial_Union ASeq)
       by A1,PROB_2:20
       .= P.Union ASeq by Th15;
   hence thesis by A1,PROB_2:20,A3,A4,RINFSUP1:24;
  end;

theorem Th45:
  ASeq is disjoint_valued implies
    for n,m st n < m holds (Partial_Union ASeq).n misses ASeq.m
  proof assume
A1: ASeq is disjoint_valued;
    let n,m such that
B1: n < m;
    assume (Partial_Union ASeq).n meets ASeq.m;then
    consider x being set such that
B3: x in (Partial_Union ASeq).n & x in ASeq.m by XBOOLE_0:3;
    consider k being Nat such that
B4: k <= n & x in ASeq.k by B3,Th13;
    ASeq.k misses ASeq.m by B1,B4,A1,PROB_2:def 4;then
    ASeq.k /\ ASeq.m = {} by XBOOLE_0:def 7;
    hence contradiction by B3,B4,XBOOLE_0:def 3;
  end;

theorem Th46:
  ASeq is disjoint_valued implies
    (P * Partial_Union ASeq).n = Partial_Sums(P * ASeq).n
  proof assume
A1: ASeq is disjoint_valued;
A2: dom (P * ASeq) = NAT & dom (P * Partial_Union ASeq) = NAT by SEQ_1:3;
    defpred P[Nat] means
      (P * Partial_Union ASeq).$1 = Partial_Sums(P * ASeq).$1;
B1: P[0] by Th43;
B2: for k st P[k] holds P[k+1]
    proof let k such that
BB1:  (P * Partial_Union ASeq).k = Partial_Sums(P * ASeq).k;
      k < k+1 by NAT_1:38;then
BB2:  (Partial_Union ASeq).k misses ASeq.(k+1) by A1,Th45;
BB3:  ASeq.(k+1) is Event of Sigma &
         (Partial_Union ASeq).k is Event of Sigma by PROB_1:57;
BB4:  (P * Partial_Union ASeq).(k+1)
          = P.((Partial_Union ASeq).(k+1)) by A2,FUNCT_1:22
         .= P.((Partial_Union ASeq).k \/ ASeq.(k+1)) by def2
         .= P.((Partial_Union ASeq).k) + P.(ASeq.(k+1))
           by BB3,BB2,PROB_1:def 13
         .= (P * Partial_Union ASeq).k + P.(ASeq.(k+1)) by A2,FUNCT_1:22;
      Partial_Sums(P * ASeq).(k+1)
          =Partial_Sums(P * ASeq).k + (P * ASeq).(k+1) by SERIES_1:def 1
         .=Partial_Sums(P * ASeq).k + P.(ASeq.(k+1)) by A2,FUNCT_1:22;
      hence thesis by BB4,BB1;
    end;
    for k holds P[k] from NAT_1:sch 1(B1,B2);
    hence thesis;
  end;

theorem Th47:
  ASeq is disjoint_valued implies
    (P * Partial_Union ASeq) = Partial_Sums(P * ASeq)
proof assume ASeq is disjoint_valued;then
  (P * Partial_Union ASeq).n = Partial_Sums(P * ASeq).n by Th46;
  hence thesis by FUNCT_2:113;
end;

theorem Th48:
  ASeq is disjoint_valued implies
    Partial_Sums(P * ASeq) is convergent &
    lim Partial_Sums(P * ASeq) = sup Partial_Sums(P * ASeq) &
    lim Partial_Sums(P * ASeq) = P.Union ASeq
proof assume ASeq is disjoint_valued;then
  (P * Partial_Union ASeq) = Partial_Sums(P * ASeq) by Th47;
  hence thesis by Th44;
end;

theorem Th49:
  ASeq is disjoint_valued implies P.(Union ASeq) = Sum(P * ASeq)
proof
  assume ASeq is disjoint_valued;then
  lim Partial_Sums(P * ASeq) = P.Union ASeq by Th48;
  hence thesis by SERIES_1:def 3;
end;

definition let X,F1,n;
  redefine func F1.n -> Subset of X;
  coherence
  proof
    per cases;
    suppose n in dom F1;
      hence thesis by FINSEQ_2:13;
    end;
    suppose not n in dom F1;then
      F1.n = {} by FUNCT_1:def 4;
      hence thesis by SUBSET_1:4;
    end;
  end;
end;

theorem Th52:
  ex F1 being FinSequence of bool X st
    for k st k in dom F1 holds F1.k = X
  proof now let n;
    deffunc P(Nat) = X;
    ex F being FinSequence st len F = n &
      for k st k in Seg n holds F.k = P(k) from FINSEQ_1:sch 2;then
    consider F1 being FinSequence such that
A1: len F1 = n & for k st k in Seg n holds F1.k = X;
A2: Seg len F1 = dom F1 by FINSEQ_1:def 3;
    rng F1 c= bool X
    proof let x; assume x in rng F1;then
      consider i such that
B1:   i in dom F1 & F1.i = x by FINSEQ_2:11;
      x = X by A1,A2,B1;
      hence thesis by ZFMISC_1:def 1;
    end;then
    F1 is FinSequence of bool X by FINSEQ_1:def 4;
    hence thesis by A1,A2;
  end;
  hence thesis;
end;

theorem Th53:
  for F1 being FinSequence of bool X holds union rng F1 is Subset of X
proof let F1 be FinSequence of bool X;
  for Y st Y in rng F1 holds Y c= X
  proof let Y;
A1: rng F1 c= bool X by FINSEQ_1:def 4;
    assume Y in rng F1;
    hence thesis by A1;
  end;
  hence thesis by ZFMISC_1:94;
end;

definition let X be set, F1 be FinSequence of bool X;
  redefine func Union F1 -> Subset of X;
  coherence
  proof
    Union F1 is Subset of X
    proof
      Union F1 = union rng F1 by CARD_3:def 4;
      hence thesis by Th53;
    end; hence thesis;
  end;
end;

theorem Th54:
  x in Union F1 iff ex k st k in dom F1 & x in F1.k
  proof
    set Y = union rng F1;
A1: for x holds x in Y iff ex k st k in dom F1 & x in F1.k
    proof let x;
      thus x in Y implies ex k st k in dom F1 & x in F1.k
      proof assume x in Y;
        then consider Z such that
A2:     x in Z & Z in rng F1 by TARSKI:def 4;
        consider i such that
A3:     i in dom F1 & Z = F1.i by A2,FINSEQ_2:11;
        thus thesis by A2,A3;
      end;
      thus (ex k st k in dom F1 & x in F1.k) implies x in Y
      proof
        given i such that
A4:     i in dom F1 & x in F1.i;
        F1.i in rng F1 by A4,FUNCT_1:def 5;
        hence thesis by A4,TARSKI:def 4;
      end;
    end;
    Y = Union F1 by CARD_3:def 4;
    hence thesis by A1;
  end;

definition let X, F1;
  func Complement F1 -> FinSequence of bool X means
:def8:  len it = len F1 & for n st n in dom it holds it.n = (F1.n)`;
existence
 proof
   deffunc F(Nat) = (F1.$1)`;
   consider f being FinSequence of bool X such that
A1:len f = len F1 &
   for n st n in Seg len F1 holds f.n = F(n) from FINSEQ_2:sch 1;
   take f;
  Seg len F1 = dom f by A1,FINSEQ_1:def 3;
  hence thesis by A1;
  end;
  uniqueness
    proof let F2,F3 be FinSequence of bool X such that
A1: len F2 = len F1 & for n st n in dom F2 holds F2.n = (F1.n)` and
A2: len F3 = len F1 & for n st n in dom F3 holds F3.n = (F1.n)`;
    dom F2 = dom F3 & (for k st k in dom F2 holds F2.k = F3.k)
    proof
B1:   dom F2 = Seg len F3 by FINSEQ_1:def 3,A1,A2
              .= dom F3 by FINSEQ_1:def 3;
      for k st k in dom F2 holds F2.k = F3.k
      proof let k; assume
C1:     k in dom F2;
        hence F2.k = (F1.k)` by A1 .= F3.k by C1,B1,A2;
      end;
      hence thesis by B1;
    end;
    hence thesis by FINSEQ_1:17;
  end;
end;

definition let X, F1;
  func Intersection F1 -> Subset of X equals
:def9: (Union Complement F1)` if F1 <> {}
    otherwise {};
  coherence by SUBSET_1:4;
  consistency;
end;

theorem Th55:
  dom Complement F1 = dom F1
proof
  thus dom Complement F1 = Seg len Complement F1 by FINSEQ_1:def 3
               .= Seg len F1 by def8
               .= dom F1 by FINSEQ_1:def 3;
end;

theorem Th56:
  F1 <> {} implies
    (x in Intersection F1 iff (for k st k in dom F1 holds x in F1.k))
  proof assume
A00: F1 <> {};then
A0:  dom F1 <> {} by RELAT_1:64;
A1:  for n st n in dom F1 holds X \ (Complement F1).n = F1.n
     proof let n; assume n in dom F1; then
B2:    n in dom Complement F1 by Th55;
       X \ (Complement F1).n = ((Complement F1).n)` by SUBSET_1:def 5
                            .= ((F1.n)`)` by B2,def8 .= F1.n;
       hence thesis;
     end;
 A2: x in (Union Complement F1)` iff x in X \ Union Complement F1
        by SUBSET_1:def 5;
 A3: (x in X & (not x in Union (Complement F1))) iff
   (x in X & (for n st n in dom F1 holds not x in (Complement F1).n))
   proof
B1: dom Complement F1 = dom F1 by Th55;
   hence (x in X & (not x in Union (Complement F1))) implies
     (x in X & for n st n in dom F1 holds not x in (Complement F1).n) by Th54;
   thus (x in X & (for n st n in dom F1 holds not x in (Complement F1).n))
    implies (x in X & (not x in Union (Complement F1))) by B1,Th54;
   end;
   (x in X & (for n st n in dom F1 holds not x in (Complement F1).n)) iff
    (for n st n in dom F1 holds x in F1.n)
    proof
      hereby assume
C1:     x in X & (for n st n in dom F1 holds not x in (Complement F1).n);
    let n such that
C2: n in dom F1;
     x in X & not x in (Complement F1).n by C2,C1;then
     x in X \ (Complement F1).n by XBOOLE_0:def 4;
    hence x in F1.n by C2,A1;
    end;
    assume C3:for n st n in dom F1 holds x in F1.n;
C4:  now let n such that
   C5: n in dom F1;
       x in F1.n by C5,C3;
       then x in X \ (Complement F1).n by C5,A1;
       hence x in X & not x in (Complement F1).n by XBOOLE_0:def 4;
     end;
     consider a being set such that
D2:  a in dom F1 by A0,XBOOLE_0:def 1;
     thus thesis by D2,C4;
   end;
  hence thesis by A00,A2,A3,def9,XBOOLE_0:def 4;
end;

theorem Th57:
  F1 <> {} implies
    (x in meet rng F1 iff for n st n in dom F1 holds x in F1.n)
 proof assume F1 <> {};then
 A0: rng F1 <> {} by RELAT_1:64;
A00: now let x; assume
      AA0: x in meet rng F1;
       now let k such that
        B0: k in dom F1;
        F1.k in rng F1 by B0,FUNCT_1:12;
        hence x in F1.k by AA0,SETFAM_1:def 1;
       end;
      hence for n st n in dom F1 holds x in F1.n;
     end;
     now let x;
      assume AA0: for n st n in dom F1 holds x in F1.n;
       now let Y;
        assume Y in rng F1;
        then consider n be set such that
AA2:    n in dom F1 & Y = F1.n by FUNCT_1:def 5;
        thus x in Y by AA0,AA2;
       end;
     hence x in meet rng F1 by A0,SETFAM_1:def 1;
    end;
   hence thesis by A00;
 end;

theorem
  Intersection F1 = meet rng F1
proof
  per cases;
  suppose A1: F1 <> {};
    now let x;
      x in Intersection F1 iff for n st n in dom F1 holds x in F1.n
        by A1,Th56;
      hence x in Intersection F1 iff x in meet rng F1 by A1,Th57;
    end;
    hence thesis by TARSKI:2;
  end;
  suppose F1 = {};
    hence thesis by RELAT_1:60,def9,SETFAM_1:2;
  end;
end;

theorem Th59:
  for F1 being FinSequence of bool X holds
   ex A1 being SetSequence of X st
   ((for k st k in dom F1 holds A1.k = F1.k) &
   (for k st not k in dom F1 holds A1.k = {}))
proof
  let F1 be FinSequence of bool X;
    defpred P[set] means $1 in dom F1;
    deffunc F(set) = F1.$1;
    deffunc G(set) = {};
    ex f being Function st dom f = NAT &
    for k being set st k in NAT holds
    (P[k] implies f.k=F(k)) & (not P[k] implies f.k=G(k)) from PARTFUN1:sch 1;
    then consider f being Function such that
A1: dom f = NAT & for x st x in NAT holds
    (x in dom F1 implies f.x = F1.x) & (not x in dom F1 implies f.x = {});
A2: for x st x in dom F1 holds F1.x in bool X
    proof let x; assume x in dom F1; then
C2:   F1.x in rng F1 by FUNCT_1:12;
      rng F1 c= bool X by FINSEQ_1:def 4;
      hence thesis by C2;
    end;
    for x st x in NAT holds f.x in bool X
    proof
      let x; assume A3: x in NAT;
      per cases;
      suppose not x in dom F1;then
        f.x = {} by A1,A3;then
        f.x c= X by XBOOLE_1:2;
        hence thesis;
      end;
      suppose x in dom F1;then
        f.x = F1.x & F1.x in bool X by A1,A2;
        hence thesis;
      end;
    end;
    then reconsider f as SetSequence of X by A1,FUNCT_2:5;
    take f;
    thus thesis by A1;
  end;

theorem Th60:
  for F1 being FinSequence of bool X for A1 being SetSequence of X st
   ((for k st k in dom F1 holds A1.k = F1.k) &
   (for k st not k in dom F1 holds A1.k = {})) holds
   A1.0={} & Union A1 = Union F1
  proof let F1 be FinSequence of bool X;
        let A1 be SetSequence of X such that
A1: (for k st k in dom F1 holds A1.k = F1.k) &
    (for k st not k in dom F1 holds A1.k = {});
    thus A1.0 = {}
    proof
      not 0 in dom F1 by Th50;
      hence thesis by A1;
    end;
    thus Union A1 = Union F1
    proof
      thus Union A1 c= Union F1
      proof let x;assume x in Union A1;then
        consider n such that
B1:     x in A1.n by PROB_1:25;
B2:     n in dom F1 by A1,B1;then
        x in F1.n by B1,A1;
        hence thesis by B2,Th54;
      end;
      let x;assume x in Union F1;then
      consider n such that
C1:   n in dom F1 & x in F1.n by Th54;
      x in A1.n by C1,A1;
      hence thesis by PROB_1:25;
    end;
  end;

definition let X be set, Si be SigmaField of X;
  mode FinSequence of Si -> FinSequence of bool X means
:def10: for k st k in dom it holds it.k in Si;
 existence
 proof
   consider F1 being FinSequence of bool X such that
A1: for k st k in dom F1 holds F1.k = X by Th52;
   take F1;
   for k st k in dom F1 holds F1.k in Si
   proof let k; assume k in dom F1; then
     F1.k = X by A1;
     hence thesis by PROB_1:43;
   end;
   hence thesis;
 end;
end;

definition let X be set,
               Si be SigmaField of X,
               FSi be FinSequence of Si,n;
  redefine func FSi.n -> Event of Si;
  coherence
  proof
    per cases;
    suppose n in dom FSi;then
      FSi.n in Si by def10;
      hence thesis by PROB_1:def 10;
    end;
    suppose not n in dom FSi;then
      FSi.n = {} by FUNCT_1:def 4;
      hence thesis by PROB_1:52;
    end;
  end;
end;

theorem Th61:
  for FSi being FinSequence of Si holds
  ex ASeq being SetSequence of Si st
  ((for k st k in dom FSi holds ASeq.k = FSi.k) &
  (for k st not k in dom FSi holds ASeq.k = {}))
proof let FSi be FinSequence of Si;
  consider A1 being SetSequence of X such that
A1: (for k st k in dom FSi holds A1.k = FSi.k) &
    (for k st not k in dom FSi holds A1.k = {}) by Th59;
  for n holds A1.n in Si
  proof let n;
    per cases;
    suppose not n in dom FSi;then
      A1.n = {} by A1;
      hence A1.n in Si by PROB_1:42;
    end;
    suppose B2: n in dom FSi;then
      A1.n = FSi.n by A1;
      hence A1.n in Si by B2,def10;
    end;
  end;then
  reconsider A1 as SetSequence of Si by PROB_1:def 9;
  take A1;
  thus thesis by A1;
end;

theorem Th62:
  for FSi being FinSequence of Si holds Union FSi in Si
proof let FSi be FinSequence of Si;
   consider ASeq being SetSequence of Si such that
A1: (for k st k in dom FSi holds ASeq.k = FSi.k) &
    (for k st not k in dom FSi holds ASeq.k = {}) by Th61;
   Union ASeq = Union FSi by A1,Th60;
   hence thesis by PROB_1:46;
end;

definition let X be set,
               S be SigmaField of X,
               F being FinSequence of S;
  func @Complement F -> FinSequence of S equals :def11:
    Complement F;
  coherence
  proof
    now let n; assume n in dom Complement F; then
      (Complement F).n = (F.n)` by def8;
      then (Complement F).n is Event of S by PROB_1:50;
      hence (Complement F).n in S by PROB_1:def 10;
    end; hence thesis by def10;
  end;
end;

theorem
  for FSi being FinSequence of Si holds Intersection FSi in Si
proof let FSi be FinSequence of Si;
  per cases;
  suppose FSi = {};then
    Intersection FSi = {} by def9;
    hence thesis by PROB_1:42;
  end;
  suppose FSi <> {};then
A1: Intersection FSi = (Union Complement FSi)` by def9
                    .= (Union @Complement FSi)` by def11;
    Union @Complement FSi in Si by Th62;
    hence thesis by A1,PROB_1:def 8;
  end;
end;

 reserve FSeq for FinSequence of Sigma;

theorem Th64:
  dom(P * FSeq) = dom FSeq
proof
  for x holds x in dom (P * FSeq) iff x in dom FSeq
  proof let x;
    thus x in dom (P * FSeq) implies x in dom FSeq by FUNCT_1:21;
    assume
B1: x in dom FSeq;then
    reconsider k=x as Nat;
    FSeq.k in Sigma by B1,def10;then
    FSeq.k in dom P by FUNCT_2:def 1;
    hence thesis by B1,FUNCT_1:21;
  end;
  hence thesis by TARSKI:2;
end;

theorem Th65:
  P * FSeq is FinSequence of REAL
  proof
    dom (P * FSeq) = dom FSeq by Th64;then
    ex n st dom (P * FSeq) = Seg n by FINSEQ_1:def 2;then
    reconsider RSeq = (P * FSeq) as FinSequence by FINSEQ_1:def 2;
    rng (P * FSeq) c= REAL
    proof
      rng (P * FSeq) c= rng P & rng P c= REAL by RELAT_1:45;
      hence thesis by XBOOLE_1:1;
    end; then
    rng RSeq c= REAL;
    hence thesis by FINSEQ_1:def 4;
  end;

definition let Omega,Sigma,FSeq,P;
  redefine func P * FSeq -> FinSequence of REAL;
  coherence by Th65;
end;

theorem Th66:
  len (P * FSeq) = len FSeq
proof
  dom(P * FSeq) = dom FSeq by Th64;then
  Seg len (P * FSeq) = dom FSeq by FINSEQ_1:def 3;
  hence thesis by FINSEQ_1:def 3;
end;

theorem Th67:
  len RFin = 0 implies Sum RFin = 0
proof assume
A0: len RFin=0;
A1: addreal is having_a_unity by RVSUM_1:3,SETWISEO:def 2;
    thus Sum(RFin) = addreal $$ RFin by RVSUM_1:def 10
        .= 0 by A1,A0,FINSOP_1:def 1,BINOP_2:2;
end;

theorem Th68:
  len RFin >= 1 implies ex f being Real_Sequence st f.1 = RFin.1 &
    (for n st 0 <> n & n < len RFin holds
    f.(n+1) = f.n+RFin.(n+1)) & Sum(RFin) = f.(len RFin)
  proof assume len RFin >= 1;then
    consider f be Function of NAT,REAL such that
A1: f.1 = RFin.1 &
    (for n st 0 <> n & n < len RFin holds
      f.(n+1) = addreal.(f.n,RFin.(n+1))) &
      addreal "**" RFin = f.(len RFin) by FINSOP_1:2;
A2: for n st 0 <> n & n < len RFin holds f.(n+1) = f.n+ RFin.(n+1)
    proof let n; assume
B1:   0 <> n & n < len RFin; then
      n+1 in Seg len RFin by FINSEQ_3:12;then
      n+1 in dom RFin by FINSEQ_1:def 3;then
B2:   f.n is Real & RFin.(n+1) is Real by FINSEQ_2:13;
      thus f.(n+1) = addreal.(f.n,RFin.(n+1)) by B1,A1
                  .= f.n+ RFin.(n+1) by B2,BINOP_2:def 9;
    end;
    take f;
    thus thesis by A1,A2,RVSUM_1:def 10;
end;

theorem Th69:
 for FSeq being FinSequence of Sigma, ASeq being SetSequence of Sigma st
  ((for k st k in dom FSeq holds ASeq.k = FSeq.k) &
  (for k st not k in dom FSeq holds ASeq.k = {})) holds
   Partial_Sums(P * ASeq) is convergent &
   Sum(P * ASeq) = Partial_Sums(P * ASeq).(len FSeq) &
   P.(Union ASeq) <= Sum(P * ASeq) &
   Sum(P * FSeq) = Sum(P * ASeq)
proof
  let FSeq be FinSequence of Sigma, ASeq be SetSequence of Sigma such that
A1: (for k st k in dom FSeq holds ASeq.k = FSeq.k) &
   (for k st not k in dom FSeq holds ASeq.k = {});
A11: ASeq.0 ={} by A1,Th60;
A2: (P * ASeq).0 = 0 & for m being Nat holds (P * ASeq).((len FSeq + 1) + m)=0
    proof
      thus (P * ASeq).0 = P.(ASeq.0) by PROB_2:11
                       .= 0 by A11,PROB_1:64;
    thus for m being Nat holds (P * ASeq).((len FSeq + 1) + m)=0
    proof
     let m be Nat;
     set k=len FSeq + 1;
     k + m >= k by NAT_1:29;then
     len FSeq + 1 + m > len FSeq by LM1;then
     not len FSeq + 1 + m in dom FSeq by FINSEQ_3:27;then
BB1: ASeq.((len FSeq + 1) + m) = {} by A1;
     thus (P * ASeq).((len FSeq + 1) + m)
            = P.(ASeq.((len FSeq + 1) + m)) by PROB_2:11
           .= 0 by BB1,PROB_1:64;
     end;
    end;
A21: for k st k in dom FSeq holds (P * ASeq).k = (P * FSeq).k
    proof let k such that
BD1:  k in dom FSeq;
      thus (P * ASeq).k = P.(ASeq.k) by PROB_2:11
                 .= P.(FSeq.k) by BD1,A1
                 .= (P * FSeq).k by BD1,FUNCT_1:23;
    end;
    1 = 0+1; then
A30:Partial_Sums(P * ASeq).1
        = Partial_Sums(P * ASeq).0 + (P*ASeq).1 by SERIES_1:def 1
       .= (P*ASeq).0 + (P*ASeq).1 by SERIES_1:def 1
       .= (P * ASeq).1 by A2;
A31: len FSeq >= 1 implies
    Partial_Sums(P * ASeq).1=(P * FSeq).1 & for m st m <> 0 & m < len FSeq
     holds Partial_Sums(P*ASeq).(m+1)=Partial_Sums(P*ASeq).m+(P*FSeq).(m+1)
    proof assume len FSeq >= 1;then
BD1:  1 in dom FSeq by Th51;
      thus Partial_Sums(P * ASeq).1 = (P * FSeq).1 by A30,BD1,A21;
      thus for m st m <> 0 & m < len FSeq holds
        Partial_Sums(P*ASeq).(m+1)=Partial_Sums(P*ASeq).m+(P*FSeq).(m+1)
      proof let m; assume m <> 0 & m < len FSeq; then
        m+1 in Seg len FSeq by FINSEQ_3:12;then
BD3:    m+1 in dom FSeq by FINSEQ_1:def 3;
        thus Partial_Sums(P*ASeq).(m+1)
          = Partial_Sums(P*ASeq).m+(P*ASeq).(m+1) by SERIES_1:def 1
         .= Partial_Sums(P*ASeq).m+(P*FSeq).(m+1) by BD3,A21;
      end;
    end;
    defpred P[Nat] means Partial_Sums(P * ASeq).((len FSeq + 1) + $1)
       = Partial_Sums(P * ASeq).(len FSeq);
    Partial_Sums(P * ASeq).((len FSeq + 1) + 0)
        = Partial_Sums(P * ASeq).(len FSeq) +
    (P * ASeq).((len FSeq + 1) + 0) by SERIES_1:def 1
        .= Partial_Sums(P * ASeq).(len FSeq) + 0 by A2; then
D1: P[0];
D2: for k st P[k] holds P[k+1]
    proof let k such that
DD1:  Partial_Sums(P * ASeq).((len FSeq + 1) + k)
        = Partial_Sums(P * ASeq).(len FSeq);
      Partial_Sums(P * ASeq).((len FSeq + 1 + k)+1)
        = Partial_Sums(P * ASeq).(len FSeq + 1 + k) +
          (P * ASeq).((len FSeq + 1) + (k+1)) by SERIES_1:def 1
       .= Partial_Sums(P * ASeq).(len FSeq + 1 + k) + 0 by A2;
      hence thesis by DD1;
    end;
A3: for k holds P[k] from NAT_1:sch 1(D1,D2);
A6: Partial_Sums(P * ASeq) is convergent &
    Sum(P * ASeq) = Partial_Sums(P * ASeq).(len FSeq)
    proof
      for m st len FSeq + 1 <= m holds
        Partial_Sums(P * ASeq).m = Partial_Sums(P * ASeq).(len FSeq)
      proof let m such that
B1:     len FSeq + 1 <= m;
        consider k such that
   B2:  m = (len FSeq + 1) + k by B1,NAT_1:28;
        thus thesis by B2,A3;
      end;then
      Partial_Sums(P * ASeq) is convergent &
      lim Partial_Sums(P * ASeq) = Partial_Sums(P * ASeq).(len FSeq) by Th1;
      hence thesis by SERIES_1:def 3;
    end;
A8: Sum(P * FSeq) = Sum(P * ASeq)
    proof
      now per cases;
        suppose E1:len FSeq = 0;then
E2:     len (P * FSeq) = 0 by Th66;
        Sum(P * ASeq) = 0 by A2,SERIES_1:def 1,A6,E1;
        hence thesis by E2,Th67;
      end;
      suppose E3:len FSeq <> 0;then
E30:    len (P * FSeq) <> 0 by Th66;
        1 <= len FSeq by E3,NAT_1:39;then
E32:    1 <= len (P * FSeq) by Th66;then
        consider seq1 being Real_Sequence such that
E4:     seq1.1 = (P * FSeq).1 &
        (for n st 0 <> n & n < len (P * FSeq) holds
        seq1.(n+1) = seq1.n+(P * FSeq).(n+1)) &
        Sum(P * FSeq) = seq1.(len (P * FSeq)) by Th68;
        defpred P[set,set] means ex n st (n=$1 &
        (n = 0 implies $2=0) &
        (n <> 0 & n <= len (P * FSeq) implies $2=seq1.n) &
        (n <> 0 & n > len (P * FSeq) implies
        $2=Partial_Sums(P*ASeq).(len(P * FSeq))));
        ex seq being Real_Sequence st for n holds ((n=0 implies seq.n=0) &
        (n<>0 & n <= len (P * FSeq) implies seq.n=seq1.n) &
        (n<>0 & n > len (P * FSeq) implies
        seq.n=Partial_Sums(P*ASeq).(len (P * FSeq))))
        proof
F1:       for x st x in NAT ex y st P[x,y]
          proof let x be set; assume x in NAT;then
            reconsider n=x as Nat;
            now per cases;
            case n=0;
              hence P[x,0];
            end;
            case n <> 0 & n <= len (P * FSeq);
              hence P[x,(seq1.n)];
            end;
            case n <> 0 & not n <= len (P * FSeq);
              hence P[x,Partial_Sums(P*ASeq).(len(P * FSeq))];
            end;
          end;
          hence thesis;
        end;
F2:  for x,y,z st x in NAT & P[x,y] & P[x,z] holds y=z;
     consider f being Function such that
F3:  dom f=NAT &
       for x st x in NAT holds P[x,f.x] from FUNCT_1:sch 2(F2,F1);
     now let x;
     assume x in NAT;
      then ex n st n=x &
       (n = 0 implies f.x=0) &
       (n <> 0 & n <= len (P * FSeq) implies f.x=seq1.n) &
       (n <> 0 & n > len (P * FSeq) implies
        f.x=Partial_Sums(P*ASeq).(len(P * FSeq))) by F3;
       hence f.x is real;
     end;then
     reconsider f as Real_Sequence by F3,SEQ_1:3;
     take seq=f;
     let n;
     ex k st k=n &
     (k=0 implies seq.n=0) &
       (k<>0 & k <= len (P * FSeq) implies seq.n=seq1.k) &
       (k<>0 & k > len (P * FSeq) implies
      seq.n=Partial_Sums(P*ASeq).(len (P * FSeq))) by F3;
     hence thesis;
    end;then
    consider seq2 being Real_Sequence such that
    E6: for n holds (n=0 implies seq2.n=0) &
       (n<>0 & n <= len (P * FSeq) implies seq2.n=seq1.n) &
       (n<>0 & n > len (P * FSeq) implies
        seq2.n=Partial_Sums(P*ASeq).(len (P * FSeq)));
    E7: seq2.(len (P * FSeq)) = Sum(P * FSeq) by E4,E30,E6;
        defpred P[Nat] means seq2.$1 = Partial_Sums(P * ASeq).$1;
        seq2.0 = (P * ASeq).0 by E6,A2
              .= Partial_Sums(P * ASeq).0 by SERIES_1:def 1; then
    G1: P[0];
    G2: for k st P[k] holds P[k+1]
        proof let k such that
     G21: P[k];
          now per cases;
            case k = 0;
            thus seq2.1 = Partial_Sums(P * ASeq).1
              by E3,NAT_1:39,A31,E4,E32,E6;
            end;
            case G23: k <> 0 & k <= len (P * FSeq) -1;then
       G24: k + 0 < (len (P * FSeq) - 1) + 1 by XREAL_1:10;then
       G25: k < len FSeq by Th66;
       G26: k+1 <> 0 by NAT_1:21;
            k+1 <= len (P * FSeq) -1 +1 by G23,XREAL_1:9;
            hence seq2.(k+1) = seq1.(k+1) by G26,E6
              .= seq1.k + (P * FSeq).(k+1) by G23,G24,E4
              .= Partial_Sums(P * ASeq).k + (P * FSeq).(k+1) by G21,G23,G24,E6
              .= Partial_Sums(P * ASeq).(k+1) by E3,NAT_1:39,G23,G25,A31;
            end;
            case k <> 0 & not k <= len (P * FSeq) - 1; then
         G29: k+1 <> 0 & k+1 > len (P * FSeq) - 1 + 1
                by NAT_1:21,XREAL_1:10;then
              k+1 >= len (P * FSeq) + 1 by NAT_1:38;then
              consider i such that
         G30: k+1 = len (P * FSeq) + 1 + i by NAT_1:28;
              thus seq2.(k+1)
                = Partial_Sums(P * ASeq).(len (P * FSeq)) by G29,E6
               .= Partial_Sums(P * ASeq).(len FSeq) by Th66
               .= Partial_Sums(P * ASeq).((len FSeq + 1) + i) by A3
               .= Partial_Sums(P * ASeq).(k+1) by G30,Th66;
            end;
          end;
          hence thesis;
        end;
        for k holds P[k] from NAT_1:sch 1(G1,G2);
        hence Sum(P * FSeq) = Partial_Sums(P * ASeq).(len (P * FSeq)) by E7
                   .= Sum(P * ASeq) by Th66,A6;
     end;
   end;
   hence thesis;
  end;
D0: Partial_Diff_Union ASeq is disjoint_valued by Th22;
D2: Partial_Sums(P * Partial_Diff_Union ASeq) is convergent by D0,Th48;
  now let n;
    (Partial_Diff_Union ASeq).n c= ASeq.n by Th18;
    hence (P * Partial_Diff_Union ASeq).n <= (P * ASeq).n by Th3;
  end; then
  for n holds (Partial_Sums(P * Partial_Diff_Union ASeq)).n
     <= (Partial_Sums(P * ASeq)).n by SERIES_1:17;then
  lim Partial_Sums(P * Partial_Diff_Union ASeq)
     <= lim Partial_Sums(P * ASeq) by A6,D2,SEQ_2:32;then
  Sum (P * Partial_Diff_Union ASeq)
     <= lim Partial_Sums(P * ASeq) by SERIES_1:def 3;then
  Sum (P * Partial_Diff_Union ASeq) <= Sum(P * ASeq) by SERIES_1:def 3;then
  P.(Union Partial_Diff_Union ASeq) <= Sum(P * ASeq) by D0,Th49;
  hence thesis by A6,A8,Th21;
end;

theorem
  P.(Union FSeq) <= Sum(P * FSeq) &
    (FSeq is disjoint_valued implies P.(Union FSeq) = Sum(P * FSeq))
proof
   consider ASeq being SetSequence of Sigma such that
A1:(for k st k in dom FSeq holds ASeq.k = FSeq.k) &
   (for k st not k in dom FSeq holds ASeq.k = {}) by Th61;
   P.(Union ASeq) = P.(Union FSeq) by A1,Th60;then
   P.(Union FSeq) <= Sum(P * ASeq) by A1,Th69;
   hence P.(Union FSeq) <= Sum(P * FSeq) by A1,Th69;
A11: FSeq is disjoint_valued implies ASeq is disjoint_valued
  proof assume
K1: FSeq is disjoint_valued;
    for m,n st m <> n holds ASeq.m misses ASeq.n
    proof let m,n such that
K2:   m <> n;
      per cases;
      suppose K21: m in dom FSeq & n in dom FSeq;
        FSeq.m misses FSeq.n by K2,K1,PROB_2:def 3;then
        ASeq.m misses FSeq.n by K21,A1;
        hence thesis by K21,A1;
      end;
      suppose not (m in dom FSeq & n in dom FSeq);then
        ASeq.m = {} or ASeq.n = {} by A1;
        hence thesis by XBOOLE_1:65;
      end;
    end;
    hence thesis by PROB_2:def 4;
  end;
    assume
J1: FSeq is disjoint_valued;
    thus P.(Union FSeq) = P.(Union ASeq) by A1,Th60
                .= Sum(P * ASeq) by J1,A11,Th49
                .= Sum(P * FSeq) by A1,Th69;
end;

definition let X;
           let IT be Subset-Family of X;
  attr IT is non-decreasing-closed means
:def12: for A1 being SetSequence of X st A1 is non-decreasing &
   (for n holds A1.n in IT) holds Union A1 in IT;
  attr IT is non-increasing-closed means
:def13: for A1 being SetSequence of X st A1 is non-increasing &
   (for n holds A1.n in IT) holds Intersection A1 in IT;
end;

theorem Th71:
  for IT be Subset-Family of X holds
    IT is non-decreasing-closed iff (for A1 being SetSequence of X st
    (A1 is non-decreasing & (for n holds A1.n in IT)) holds lim A1 in IT)
proof let IT be Subset-Family of X;
  thus IT is non-decreasing-closed implies (for A1 being SetSequence of X st
      (A1 is non-decreasing & (for n holds A1.n in IT)) holds lim A1 in IT)
  proof assume
B1: IT is non-decreasing-closed;
    now let A1 be SetSequence of X;assume
  C1: A1 is non-decreasing & (for n holds A1.n in IT);then
      Union A1 in IT by B1,def12;
      hence lim A1 in IT by C1,SETLIM_1:69;
    end;
    hence thesis;
  end;
  assume
A1: for A1 being SetSequence of X st
  A1 is non-decreasing & (for n holds A1.n in IT) holds lim A1 in IT;
  for A1 being SetSequence of X st A1 is non-decreasing &
  (for n holds A1.n in IT) holds Union A1 in IT
  proof let A1 be SetSequence of X;assume
D1: A1 is non-decreasing & (for n holds A1.n in IT);then
    lim A1 in IT by A1;
    hence thesis by D1,SETLIM_1:69;
  end;
  hence thesis by def12;
end;

theorem Th72:
  for IT be Subset-Family of X holds
    IT is non-increasing-closed iff (for A1 being SetSequence of X st
    A1 is non-increasing & (for n holds A1.n in IT) holds lim A1 in IT)
proof let IT be Subset-Family of X;
 thus IT is non-increasing-closed implies (for A1 being SetSequence of X st
      A1 is non-increasing & (for n holds A1.n in IT) holds lim A1 in IT)
  proof assume
B1: IT is non-increasing-closed;
    now let A1 be SetSequence of X;assume
  C1: A1 is non-increasing & (for n holds A1.n in IT);then
      Intersection A1 in IT by B1,def13;
      hence lim A1 in IT by C1,SETLIM_1:70;
    end;
    hence thesis;
  end;
  assume
A1: for A1 being SetSequence of X st
  A1 is non-increasing & (for n holds A1.n in IT) holds lim A1 in IT;
  for A1 being SetSequence of X st A1 is non-increasing &
      (for n holds A1.n in IT) holds Intersection A1 in IT
  proof let A1 be SetSequence of X;assume
D1: A1 is non-increasing & (for n holds A1.n in IT);then
    lim A1 in IT by A1;
    hence thesis by D1,SETLIM_1:70;
  end;
  hence thesis by def13;
end;

theorem Th73:
  bool X is non-decreasing-closed & bool X is non-increasing-closed
proof
  for A1 be SetSequence of X st
    A1 is non-decreasing & for n holds A1.n in bool X holds
      Union A1 in bool X;
  hence bool X is non-decreasing-closed by def12;
  for A1 be SetSequence of X st
    A1 is non-increasing & for n holds A1.n in bool X holds
      Intersection A1 in bool X;
  hence thesis by def13;
end;

definition let X;
  mode MonotoneClass of X -> Subset-Family of X means
:def14: it is non-decreasing-closed & it is non-increasing-closed;
  existence
  proof
    take bool X;
    thus thesis by Th73;
  end;
end;

theorem Th74:
  Z is MonotoneClass of X iff Z c= bool X & (for A1 being SetSequence of X st
    A1 is monotone & (for n holds A1.n in Z) holds lim A1 in Z)
proof
 thus Z is MonotoneClass of X implies Z c= bool X &
  (for A1 being SetSequence of X st
  A1 is monotone & (for n holds A1.n in Z) holds lim A1 in Z)
 proof assume
 B0: Z is MonotoneClass of X;then
     reconsider Z as Subset-Family of X;
 B1: Z is non-decreasing-closed & Z is non-increasing-closed by B0,def14;
     for A1 being SetSequence of X st
     A1 is monotone & (for n holds A1.n in Z) holds lim A1 in Z
     proof let A1 be SetSequence of X;assume
C1:    A1 is monotone & for n holds A1.n in Z;
       per cases by C1,SETLIM_1:def 1;
       suppose A1 is non-decreasing;
         hence lim A1 in Z by B1,C1,Th71;
       end;
       suppose A1 is non-increasing;
         hence lim A1 in Z by B1,C1,Th72;
       end;
     end;
  hence thesis;
 end;
 assume that
A0: Z c= bool X and
A1: for A1 being SetSequence of X st
  A1 is monotone & (for n holds A1.n in Z) holds lim A1 in Z;
 reconsider Z as Subset-Family of X by A0;
 for A1 being SetSequence of X st 
 A1 is non-decreasing & (for n holds A1.n in Z) holds lim A1 in Z
  proof let A1 be SetSequence of X;assume
  D1: A1 is non-decreasing & (for n holds A1.n in Z);
      A1 is monotone & (for n holds A1.n in Z)
       implies lim A1 in Z by A1;
  hence thesis by D1,SETLIM_1:def 1;
  end;then
A2: Z is non-decreasing-closed by Th71;
 for A1 being SetSequence of X st 
 A1 is non-increasing & (for n holds A1.n in Z) holds lim A1 in Z
 proof let A1 be SetSequence of X;assume
  E1: A1 is non-increasing & (for n holds A1.n in Z);
      A1 is monotone & (for n holds A1.n in Z) implies lim A1 in Z by A1;
  hence thesis by E1,SETLIM_1:def 1;
  end;then
 Z is non-increasing-closed by Th72;
 hence thesis by A2,def14;
end;

theorem Th75:
  for F being Field_Subset of X holds
    F is SigmaField of X iff F is MonotoneClass of X
proof let F be Field_Subset of X;
  thus F is SigmaField of X implies F is MonotoneClass of X
  proof assume F is SigmaField of X;then
      reconsider F as SigmaField of X;
      for A1 being SetSequence of X st A1 is non-decreasing &
       (for n holds A1.n in F) holds Union A1 in F
      proof let A1 be SetSequence of X; assume that
      A1: A1 is non-decreasing & for n holds A1.n in F;
          reconsider A2=A1 as SetSequence of F by A1,PROB_1:def 9;
          Union A2 in F by PROB_1:46;
          hence thesis;
      end;then
  B1: F is non-decreasing-closed by def12;
      for A1 being SetSequence of X st A1 is non-increasing &
       (for n holds A1.n in F) holds Intersection A1 in F
       by PROB_1:def 8;then
      F is non-increasing-closed by def13;
   hence thesis by B1,def14;
  end; assume F is MonotoneClass of X;then
A2: F is non-increasing-closed & F is non-decreasing-closed by def14;
  (for A1 being SetSequence of X st
  (for n holds A1.n in F) holds Intersection A1 in F) &
  (for A being Subset of X st A in F holds A` in F)
  proof
    thus (for A1 being SetSequence of X st
      (for n holds A1.n in F) holds Intersection A1 in F)
    proof let A1 such that
D1:   for n holds A1.n in F;
      set A2 = Partial_Intersection A1;
      defpred P[Nat] means A2.$1 in F;
      A2.0 = A1.0 by def1; then
E1:   P[0] by D1;
E2:   for k st P[k] holds P[k+1]
      proof let k;assume
F1:     A2.k in F;
F2:     A1.(k+1) in F by D1;
        A2.(k+1) = A2.k /\ A1.(k+1) by def1;
        hence A2.(k+1) in F by F1,F2,FINSUB_1:def 2;
      end;
D2:   for k holds P[k] from NAT_1:sch 1(E1,E2);
      A2 is non-increasing by Th10;then
      Intersection A2 in F by A2,D2,def13;
      hence thesis by Th14;
    end;
    thus for A being Subset of X st A in F holds A` in F by PROB_1:def 1;
  end;
  hence thesis by PROB_1:def 8;
end;

theorem Th76:
  bool Omega is MonotoneClass of Omega
proof
  bool Omega is non-decreasing-closed &
    bool Omega is non-increasing-closed by Th73;
  hence thesis by def14;
end;

theorem Th77:
  for X being Subset-Family of Omega ex Y being MonotoneClass of Omega st
    X c= Y & for Z st X c= Z & Z is MonotoneClass of Omega holds Y c= Z
  proof let X be Subset-Family of Omega;
    set V = { M where M is Subset-Family of Omega :
      X c= M & M is MonotoneClass of Omega};
    set Y = meet V;
a1: bool Omega in V
    proof
      bool Omega is MonotoneClass of Omega by Th76;
      hence thesis;
    end; then
A1: Y c= bool Omega & V <> {} by SETFAM_1:4;
AA: for Z st Z in V holds X c= Z
    proof let Z; assume Z in V;then
      ex M being Subset-Family of Omega st
        Z = M & X c= M & M is MonotoneClass of Omega;
      hence X c= Z;
    end;
A5: for MSeq being SetSequence of Omega st
      MSeq is monotone & (for n holds MSeq.n in Y) holds lim MSeq in Y
    proof let MSeq be SetSequence of Omega such that
B1:   MSeq is monotone and
B2:   for n holds MSeq.n in Y;
      now let Z; assume
C1:     Z in V;then
C2:     ex M being Subset-Family of Omega st
        Z = M & X c= M & M is MonotoneClass of Omega;
        now let n; MSeq.n in Y by B2;
          hence MSeq.n in Z by C1,SETFAM_1:def 1;
        end;
        hence lim MSeq in Z by B1,C2,Th74;
      end;
      hence thesis by a1,SETFAM_1:def 1;
    end;
    reconsider Y as MonotoneClass of Omega by A1,A5,Th74;
    take Y;
    for Z st X c= Z & Z is MonotoneClass of Omega holds Y c= Z
    proof let Z; assume X c= Z & Z is MonotoneClass of Omega;then
      Z in V;
      hence thesis by SETFAM_1:4;
    end;
    hence thesis by AA,a1,SETFAM_1:6;
  end;

definition let Omega;let X be Subset-Family of Omega;
  func monotoneclass(X) -> MonotoneClass of Omega means :def15:
  X c= it & for Z st X c= Z & Z is MonotoneClass of Omega holds
    it c= Z;
  existence by Th77;
  uniqueness
  proof let R1,R2 be MonotoneClass of Omega such that
A1: X c= R1 & for Z st X c= Z & Z is MonotoneClass of Omega holds R1 c= Z
    and
A2: X c= R2 & for Z st X c= Z & Z is MonotoneClass of Omega holds R2 c= Z;
    thus R1 c= R2 by A1,A2;
    thus thesis by A1,A2;
  end;
end;

theorem Th78:
  for Z being Field_Subset of Omega holds
    monotoneclass(Z) is Field_Subset of Omega
  proof let Z be Field_Subset of Omega;
A0: Z c= monotoneclass(Z) by def15;then
    reconsider Z1=monotoneclass(Z) as non empty Subset-Family of Omega
      by XBOOLE_1:3;
A2: for y,Y st Y = {x where x is Element of Z1:
     y \ x in Z1 & x \ y in Z1 & x /\ y in Z1} holds 
      (for z st z in Y holds 
      z in Z1 & y \ z in Z1 & z \ y in Z1 & z /\ y in Z1)
    proof let y,Y;assume
A21:  Y = {x where x is Element of Z1:
       y \ x in Z1 & x \ y in Z1 & x /\ y in Z1};
      thus (for z st z in Y holds
        z in Z1 & y \ z in Z1 & z \ y in Z1 & z /\ y in Z1)
      proof let z; assume z in Y;then
        consider z1 be Element of Z1 such that
BB1:    z = z1 & y \ z1 in Z1 & z1 \ y in Z1 & z1 /\ y in Z1 by A21;
        thus thesis by BB1;
      end;
    end;
A3: for y being Element of Z1,Y st Y = {x where x is Element of Z1:
      y \ x in Z1 & x \ y in Z1 & x /\ y in Z1} holds
    Y is MonotoneClass of Omega
    proof let y be Element of Z1,Y;assume
B00:  Y = {x where x is Element of Z1:
       y \ x in Z1 & x \ y in Z1 & x /\ y in Z1};
 C1:  Y c= bool Omega
      proof
        z in Y implies z in Z1 by A2,B00;then
        Y c= Z1 by TARSKI:def 3;
        hence thesis by XBOOLE_1:1;
      end;
      Y c= bool Omega & (for A1 being SetSequence of Omega st
      A1 is monotone & (for n holds A1.n in Y) holds lim A1 in Y)
      proof
        for A1 being SetSequence of Omega st
        A1 is monotone & (for n holds A1.n in Y) holds lim A1 in Y
        proof let A1 be SetSequence of Omega such that
D1:       A1 is monotone and
D2:       for n holds A1.n in Y;
          for n holds A1.n in Z1
          proof let n; A1.n in Y by D2;
            hence thesis by B00,A2;
          end; then
D3:       lim A1 in Z1 by D1,Th74;
D4:       A1 is convergent by D1,SETLIM_1:71;
D6:       A1 (\) y is monotone by D1,SETLIM_2:32;
          for n holds (A1 (\) y).n in Z1
          proof let n;
            A1.n in Y by D2;then
            A1.n \ y in Z1 by B00,A2;
            hence thesis by SETLIM_2:def 8;
          end;then
D7:       lim (A1 (\) y) in Z1 by D6,Th74;
D9:       y (\) A1 is monotone by D1,SETLIM_2:29;
          for n holds (y (\) A1).n in Z1
          proof let n;
            A1.n in Y by D2;then
            y \ A1.n in Z1 by B00,A2;
            hence thesis by SETLIM_2:def 7;
          end;then
D10:      lim (y (\) A1) in Z1 by D9,Th74;
D12:      y (/\) A1 is monotone by D1,SETLIM_2:23;
          for n holds (y (/\) A1).n in Z1
          proof let n;
            A1.n in Y by D2;then
            y /\ A1.n in Z1 by B00,A2;
            hence thesis by SETLIM_2:def 5;
          end;then
          lim (y (/\) A1) in Z1 by D12,Th74;then
          lim A1 is Element of Z1 & lim A1 \ y in Z1 & y \ lim A1 in Z1 &
          y /\ lim A1 in Z1 by D3,D7,D4,SETLIM_2:95,D10,SETLIM_2:94,92;
          hence thesis by B00;
        end;
        hence thesis by C1;
      end;
      hence thesis by Th74;
    end;
A4: for y being Element of Z,Y st Y = {x where x is Element of Z1:
     y \ x in Z1 & x \ y in Z1 & x /\ y in Z1} holds Z1 c= Y
    proof let y be Element of Z,Y;assume
E0:   Y = {x where x is Element of Z1:
        y \ x in Z1 & x \ y in Z1 & x /\ y in Z1};
E1:   Z c= Y
      proof let z;assume
E01:    z in Z; then
E02:    z \ y in Z by PROB_1:12;
E03:    y \ z in Z by E01,PROB_1:12;
        z /\ y in Z by E01,FINSUB_1:def 2;
        hence thesis by E01,E02,E03,E0,A0;
      end;
      y in Z;then
      Y is MonotoneClass of Omega by A0,E0,A3;
      hence thesis by E1,def15;
    end;
A5: for y being Element of Z1,Y st Y = {x where x is Element of Z1:
     y \ x in Z1 & x \ y in Z1 & x /\ y in Z1} holds Z1 c= Y
    proof let y be Element of Z1,Y;assume
F0:   Y = {x where x is Element of Z1:
        y \ x in Z1 & x \ y in Z1 & x /\ y in Z1};
F1:   Z c= Y
      proof let z;assume
F01:    z in Z;
        set Y1 = {x where x is Element of Z1:
          z \ x in Z1 & x \ z in Z1 & x /\ z in Z1};
F02:    Z1 c= Y1 by F01,A4;
        y in Z1;then
        z \ y in Z1 & y \ z in Z1 & z /\ y in Z1 by F02,A2;
        hence thesis by F01,A0,F0;
      end;
      Y is MonotoneClass of Omega by F0,A3;
      hence thesis by F1,def15;
    end;
G1: Z1 is cap-closed
    proof now let y,z;assume
G01:  y in Z1 & z in Z1;
      set Y = {x where x is Element of Z1:
      y \ x in Z1 & x \ y in Z1 & x /\ y in Z1};
      Z1 c= Y by G01,A5;
      hence y /\ z in Z1 by A2,G01;
    end;
    hence thesis by FINSUB_1:def 2;
  end;
  for y being Subset of Omega st y in Z1 holds y` in Z1
  proof let y be Subset of Omega such that
G11:y in Z1;
    set Y = {x where x is Element of Z1:
      y \ x in Z1 & x \ y in Z1 & x /\ y in Z1};
    Omega in Z by PROB_1:11;then
G12:Omega in Z1 by A0;
    Z1 c= Y by G11,A5;then
    Omega \ y in Z1 by A2,G12;
    hence thesis by SUBSET_1:def 5;
  end;
  hence thesis by G1,PROB_1:def 1;
end;

theorem
  for Z being Field_Subset of Omega holds sigma Z = monotoneclass Z
proof let Z be Field_Subset of Omega;
  thus sigma Z c= monotoneclass Z
  proof monotoneclass Z is Field_Subset of Omega by Th78;then
A1: monotoneclass Z is SigmaField of Omega by Th75;
    Z c= monotoneclass Z by def15;
    hence thesis by A1,PROB_1:def 14;
  end;
B1: sigma Z is MonotoneClass of Omega by Th75;
    Z c= sigma Z by PROB_1:def 14;
    hence thesis by B1,def15;
end;