prob_3.miz



    begin

    reserve n,m,k,i for Nat,

g,s,t,p for Real,

x,y,z for object,

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: 8;

      hence thesis by XREAL_1: 19;

    end;

    theorem :: PROB_3:1

    

     Th1: for f be 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: 1;

    end;

    theorem :: PROB_3:2

    

     Th2: for f be 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: 25;

      hence thesis by NAT_1: 14;

    end;

    theorem :: PROB_3:3

    

     Th3: for f be 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

         A3: 0 < p;

        take k;

        let m be Nat;

        assume k <= m;

        then (f . m) = g by A1;

        hence |.((f . m) - g).| < p by A3, ABSVALUE: 2;

      end;

      hence f is convergent by SEQ_2:def 6;

      hence thesis by A2, SEQ_2:def 7;

    end;

    theorem :: PROB_3:4

    

     Th4: ((P * ASeq) . n) >= 0

    proof

      

       A1: n in NAT by ORDINAL1:def 12;

      ( dom (P * ASeq)) = NAT by SEQ_1: 1;

      then ((P * ASeq) . n) = (P . (ASeq . n)) by A1, FUNCT_1: 12;

      hence thesis by PROB_1:def 8;

    end;

    theorem :: PROB_3:5

    

     Th5: (ASeq . n) c= (BSeq . n) implies ((P * ASeq) . n) <= ((P * BSeq) . n)

    proof

      

       A1: n in NAT by ORDINAL1:def 12;

      assume (ASeq . n) c= (BSeq . n);

      then (P . (ASeq . n)) <= (P . (BSeq . n)) by PROB_1: 34;

      then ((P * ASeq) . n) <= (P . (BSeq . n)) by A1, FUNCT_2: 15;

      hence thesis by A1, FUNCT_2: 15;

    end;

    theorem :: PROB_3:6

    

     Th6: ASeq is non-descending implies (P * ASeq) is non-decreasing

    proof

      

       A1: ( dom (P * ASeq)) = NAT by SEQ_1: 1;

      assume

       A2: ASeq is non-descending;

      now

        let n,m be Nat;

        assume n <= m;

        then

         A3: (ASeq . n) c= (ASeq . m) by A2, PROB_1:def 5;

        reconsider nn = n, mm = m as Element of NAT by ORDINAL1:def 12;

        ((P * ASeq) . nn) = (P . (ASeq . nn)) & ((P * ASeq) . mm) = (P . (ASeq . mm)) by A1, FUNCT_1: 12;

        hence ((P * ASeq) . n) <= ((P * ASeq) . m) by A3, PROB_1: 34;

      end;

      hence thesis by SEQM_3: 6;

    end;

    theorem :: PROB_3:7

    

     Th7: ASeq is non-ascending implies (P * ASeq) is non-increasing

    proof

      

       A1: ( dom (P * ASeq)) = NAT by SEQ_1: 1;

      assume

       A2: ASeq is non-ascending;

      now

        let n,m be Nat;

        assume n <= m;

        then

         A3: (ASeq . m) c= (ASeq . n) by A2, PROB_1:def 4;

        reconsider nn = n, mm = m as Element of NAT by ORDINAL1:def 12;

        ((P * ASeq) . nn) = (P . (ASeq . nn)) & ((P * ASeq) . mm) = (P . (ASeq . mm)) by A1, FUNCT_1: 12;

        hence ((P * ASeq) . m) <= ((P * ASeq) . n) by A3, PROB_1: 34;

      end;

      hence thesis by SEQM_3: 8;

    end;

    definition

      let X be set, A1 be SetSequence of X;

      :: PROB_3:def1

      func Partial_Intersection A1 -> SetSequence of X means

      : Def1: (it . 0 ) = (A1 . 0 ) & for n be Nat holds (it . (n + 1)) = ((it . n) /\ (A1 . (n + 1)));

      existence

      proof

        defpred P[ set, set, set] means for x,y be Subset of X, s be Nat holds s = $1 & x = $2 & y = $3 implies y = (x /\ (A1 . (s + 1)));

        

         A1: for n be Nat holds for x be Subset of X holds ex y be Subset of X st P[n, x, y]

        proof

          let n be Nat;

          let x be Subset of X;

          take (x /\ (A1 . (n + 1)));

          thus thesis;

        end;

        consider F be SetSequence of X such that

         A2: (F . 0 ) = (A1 . 0 ) and

         A3: for n be Nat holds P[n, (F . n), (F . (n + 1))] from RECDEF_1:sch 2( A1);

        take F;

        thus (F . 0 ) = (A1 . 0 ) by A2;

        let n be Nat;

        reconsider n as Element of NAT by ORDINAL1:def 12;

         P[n, (F . n), (F . (n + 1))] by A3;

        hence thesis;

      end;

      uniqueness

      proof

        let S1,S2 be SetSequence of X such that

         A4: (S1 . 0 ) = (A1 . 0 ) and

         A5: for n be Nat holds (S1 . (n + 1)) = ((S1 . n) /\ (A1 . (n + 1))) and

         A6: (S2 . 0 ) = (A1 . 0 ) and

         A7: for n be Nat holds (S2 . (n + 1)) = ((S2 . n) /\ (A1 . (n + 1)));

        defpred P[ object] means (S1 . $1) = (S2 . $1);

        for n be object holds n in NAT implies P[n]

        proof

          let n be object;

          assume n in NAT ;

          then

          reconsider n as Element of NAT ;

          

           A8: 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 A5

            .= (S2 . (k + 1)) by A7;

          end;

          

           A9: P[ 0 ] by A4, A6;

          for k be Nat holds P[k] from NAT_1:sch 2( A9, A8);

          then (S1 . n) = (S2 . n);

          hence thesis;

        end;

        hence thesis;

      end;

    end

    definition

      let X be set, A1 be SetSequence of X;

      :: PROB_3:def2

      func Partial_Union A1 -> SetSequence of X means

      : Def2: (it . 0 ) = (A1 . 0 ) & for n be Nat holds (it . (n + 1)) = ((it . n) \/ (A1 . (n + 1)));

      existence

      proof

        defpred P[ set, set, set] means for x,y be Subset of X, s be Nat holds (s = $1 & x = $2 & y = $3 implies y = (x \/ (A1 . (s + 1))));

        

         A1: for n be Nat holds for x be Subset of X holds ex y be Subset of X st P[n, x, y]

        proof

          let n be Nat;

          let x be Subset of X;

          take (x \/ (A1 . (n + 1)));

          thus thesis;

        end;

        consider F be SetSequence of X such that

         A2: (F . 0 ) = (A1 . 0 ) and

         A3: for n be Nat holds P[n, (F . n), (F . (n + 1))] from RECDEF_1:sch 2( A1);

        take F;

        thus (F . 0 ) = (A1 . 0 ) by A2;

        let n be Nat;

        reconsider n as Element of NAT by ORDINAL1:def 12;

         P[n, (F . n), (F . (n + 1))] by A3;

        hence thesis;

      end;

      uniqueness

      proof

        let S1,S2 be SetSequence of X such that

         A4: (S1 . 0 ) = (A1 . 0 ) and

         A5: for n be Nat holds (S1 . (n + 1)) = ((S1 . n) \/ (A1 . (n + 1))) and

         A6: (S2 . 0 ) = (A1 . 0 ) and

         A7: for n be Nat holds (S2 . (n + 1)) = ((S2 . n) \/ (A1 . (n + 1)));

        defpred P[ object] means (S1 . $1) = (S2 . $1);

        for n be object holds n in NAT implies P[n]

        proof

          let n be object;

          assume n in NAT ;

          then

          reconsider n as Element of NAT ;

          

           A8: 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 A5

            .= (S2 . (k + 1)) by A7;

          end;

          

           A9: P[ 0 ] by A4, A6;

          for k be Nat holds P[k] from NAT_1:sch 2( A9, A8);

          then (S1 . n) = (S2 . n);

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: PROB_3:8

    

     Th8: (( Partial_Intersection A1) . n) c= (A1 . n)

    proof

      per cases by NAT_1: 6;

        suppose n = 0 ;

        hence thesis by Def1;

      end;

        suppose ex k be Nat st n = (k + 1);

        then

        consider k such that

         A1: n = (k + 1);

        (( Partial_Intersection A1) . (k + 1)) = ((( Partial_Intersection A1) . k) /\ (A1 . (k + 1))) by Def1;

        hence thesis by A1, XBOOLE_1: 17;

      end;

    end;

    theorem :: PROB_3:9

    

     Th9: (A1 . n) c= (( Partial_Union A1) . n)

    proof

      per cases by NAT_1: 6;

        suppose n = 0 ;

        hence thesis by Def2;

      end;

        suppose ex k be Nat st n = (k + 1);

        then

        consider k such that

         A1: n = (k + 1);

        (( Partial_Union A1) . (k + 1)) = ((( Partial_Union A1) . k) \/ (A1 . (k + 1))) by Def2;

        hence thesis by A1, XBOOLE_1: 7;

      end;

    end;

    theorem :: PROB_3:10

    

     Th10: ( Partial_Intersection A1) is non-ascending

    proof

      now

        let n be Nat;

        (( 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: 6;

    end;

    theorem :: PROB_3:11

    

     Th11: ( Partial_Union A1) is non-descending

    proof

      now

        let n be Nat;

        (( 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: 7;

    end;

    theorem :: PROB_3:12

    

     Th12: for x be object holds x in (( Partial_Intersection A1) . n) iff for k st k <= n holds x in (A1 . k)

    proof

      let x be object;

      defpred P[ Nat] means (for k st k <= $1 holds x in (A1 . k)) implies x in (( Partial_Intersection A1) . $1);

      

       A1: for i st P[i] holds P[(i + 1)]

      proof

        let i such that

         A2: (for k st k <= i holds x in (A1 . k)) implies x in (( Partial_Intersection A1) . i);

        assume for k st k <= (i + 1) holds x in (A1 . k);

        then

         A3: (for k st k <= i holds x in (A1 . k)) & x in (A1 . (i + 1)) by NAT_1: 12;

        (( Partial_Intersection A1) . (i + 1)) = ((( Partial_Intersection A1) . i) /\ (A1 . (i + 1))) by Def1;

        hence thesis by A2, A3, XBOOLE_0:def 4;

      end;

      thus x in (( Partial_Intersection A1) . n) implies for k st k <= n holds x in (A1 . k)

      proof

        assume

         A4: x in (( Partial_Intersection A1) . n);

        for k st k <= n holds x in (A1 . k)

        proof

          

           A5: ( Partial_Intersection A1) is non-ascending by Th10;

          let k such that

           A6: k <= n;

          

           A7: (( Partial_Intersection A1) . k) c= (A1 . k) by Th8;

          (( Partial_Intersection A1) . n) c= (( Partial_Intersection A1) . k) by A6, A5, PROB_1:def 4;

          then (( Partial_Intersection A1) . n) c= (A1 . k) by A7;

          hence thesis by A4;

        end;

        hence thesis;

      end;

      

       A8: P[ 0 ]

      proof

        assume for k st k <= 0 holds x in (A1 . k);

        then x in (A1 . 0 );

        hence thesis by Def1;

      end;

      for n holds P[n] from NAT_1:sch 2( A8, A1);

      hence thesis;

    end;

    theorem :: PROB_3:13

    

     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));

      

       A1: for i st P[i] holds P[(i + 1)]

      proof

        let i such that

         A2: x in (( Partial_Union A1) . i) implies ex k st k <= i & x in (A1 . k);

        assume

         A3: x in (( Partial_Union A1) . (i + 1));

        

         A4: (( Partial_Union A1) . (i + 1)) = ((( Partial_Union A1) . i) \/ (A1 . (i + 1))) by Def2;

        now

          per cases by A3, A4, XBOOLE_0:def 3;

            case x in (( Partial_Union A1) . i);

            then

            consider k such that

             A5: k <= i & x in (A1 . k) by A2;

            take k;

            thus thesis by A5, NAT_1: 12;

          end;

            case x in (A1 . (i + 1));

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      

       A6: P[ 0 ]

      proof

        assume

         A7: x in (( Partial_Union A1) . 0 );

        take 0 ;

        thus thesis by A7, Def2;

      end;

      for n holds P[n] from NAT_1:sch 2( A6, A1);

      hence x in (( Partial_Union A1) . n) implies ex k st k <= n & x in (A1 . k);

      given i such that

       A8: i <= n and

       A9: x in (A1 . i);

      (A1 . i) c= (( Partial_Union A1) . i) by Th9;

      then

       A10: x in (( Partial_Union A1) . i) by A9;

      

       A11: ( Partial_Union A1) is non-descending by Th11;

      (( Partial_Union A1) . i) c= (( Partial_Union A1) . n) by A8, A11, PROB_1:def 5;

      hence thesis by A10;

    end;

    theorem :: PROB_3:14

    

     Th14: ( Intersection ( Partial_Intersection A1)) = ( Intersection A1)

    proof

      thus ( Intersection ( Partial_Intersection A1)) c= ( Intersection A1)

      proof

        let x be object;

        assume

         A1: x in ( Intersection ( Partial_Intersection A1));

        for n be Nat holds x in (A1 . n)

        proof

          let n be Nat;

          x in (( Partial_Intersection A1) . n) by A1, PROB_1: 13;

          hence thesis by Th12;

        end;

        hence thesis by PROB_1: 13;

      end;

      let x be object;

      assume

       A2: x in ( Intersection A1);

      for n be Nat holds x in (( Partial_Intersection A1) . n)

      proof

        let n be Nat;

        for k st k <= n holds x in (A1 . k) by A2, PROB_1: 13;

        hence thesis by Th12;

      end;

      hence thesis by PROB_1: 13;

    end;

    theorem :: PROB_3:15

    

     Th15: ( Union ( Partial_Union A1)) = ( Union A1)

    proof

      thus ( Union ( Partial_Union A1)) c= ( Union A1)

      proof

        let x be object;

        assume x in ( Union ( Partial_Union A1));

        then

        consider n be Nat such that

         A1: x in (( Partial_Union A1) . n) by PROB_1: 12;

        consider k such that k <= n and

         A2: x in (A1 . k) by A1, Th13;

        thus thesis by A2, PROB_1: 12;

      end;

      let x be object;

      assume x in ( Union A1);

      then

      consider n be Nat such that

       A3: x in (A1 . n) by PROB_1: 12;

      x in (( Partial_Union A1) . n) by A3, Th13;

      hence thesis by PROB_1: 12;

    end;

    definition

      let X be set, A1 be SetSequence of X;

      :: PROB_3:def3

      func Partial_Diff_Union A1 -> SetSequence of X means

      : Def3: (it . 0 ) = (A1 . 0 ) & for n be Nat holds (it . (n + 1)) = ((A1 . (n + 1)) \ (( Partial_Union A1) . n));

      existence

      proof

        defpred P[ set, set, set] means for x,y be Subset of X, s be Nat holds (s = $1 & x = $2 & y = $3 implies y = ((A1 . (s + 1)) \ (( Partial_Union A1) . s)));

        set A = (A1 . 0 );

        

         A1: for n be Nat holds for x be Subset of X holds ex y be Subset of X st P[n, x, y]

        proof

          let n be Nat;

          let x be Subset of X;

          take ((A1 . (n + 1)) \ (( Partial_Union A1) . n));

          thus thesis;

        end;

        consider F be SetSequence of X such that

         A2: (F . 0 ) = A & for n be Nat holds P[n, (F . n), (F . (n + 1))] from RECDEF_1:sch 2( A1);

        for n holds (F . (n + 1)) = ((A1 . (n + 1)) \ (( Partial_Union A1) . n))

        proof

          let n;

          reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

          for x,y be Subset of X, s be Nat holds s = n1 & x = (F . n1) & y = (F . (n1 + 1)) implies y = ((A1 . (s + 1)) \ (( Partial_Union A1) . s)) by A2;

          hence thesis;

        end;

        hence thesis by A2;

      end;

      uniqueness

      proof

        let S1,S2 be SetSequence of X such that

         A3: (S1 . 0 ) = (A1 . 0 ) and

         A4: for n be Nat holds (S1 . (n + 1)) = ((A1 . (n + 1)) \ (( Partial_Union A1) . n)) and

         A5: (S2 . 0 ) = (A1 . 0 ) and

         A6: for n be Nat holds (S2 . (n + 1)) = ((A1 . (n + 1)) \ (( Partial_Union A1) . n));

        defpred P[ object] means (S1 . $1) = (S2 . $1);

        for n be object holds n in NAT implies P[n]

        proof

          let n be object;

          assume n in NAT ;

          then

          reconsider n as Element of NAT ;

          

           A7: 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 A4

            .= (S2 . (k + 1)) by A6;

          end;

          

           A8: P[ 0 ] by A3, A5;

          for k be Nat holds P[k] from NAT_1:sch 2( A8, A7);

          then (S1 . n) = (S2 . n);

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: PROB_3:16

    

     Th16: 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

         A1: x in (( Partial_Diff_Union A1) . n);

        now

          per cases by NAT_1: 6;

            case n = 0 ;

            hence thesis by A1, Def3;

          end;

            case ex n1 be Nat st n = (n1 + 1);

            then

            consider n1 be Nat such that

             A2: n = (n1 + 1);

            

             A3: x in ((A1 . (n1 + 1)) \ (( Partial_Union A1) . n1)) by A1, A2, Def3;

            then

             A4: not x in (( Partial_Union A1) . n1) by XBOOLE_0:def 5;

            for k st k < n holds not x in (A1 . k)

            proof

              let k;

              assume k < n;

              then k <= n1 by A2, NAT_1: 13;

              hence thesis by A4, Th13;

            end;

            hence thesis by A2, A3, XBOOLE_0:def 5;

          end;

        end;

        hence thesis;

      end;

      assume that

       A5: x in (A1 . n) and

       A6: for k st k < n holds not x in (A1 . k);

      now

        per cases by NAT_1: 6;

          case n = 0 ;

          hence thesis by A5, Def3;

        end;

          case ex n1 be Nat st n = (n1 + 1);

          then

          consider n1 be Nat such that

           A7: 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: 13;

            hence thesis by A6, A7;

          end;

          then not x in (( Partial_Union A1) . n1) by Th13;

          then x in ((A1 . (n1 + 1)) \ (( Partial_Union A1) . n1)) by A5, A7, XBOOLE_0:def 5;

          hence thesis by A7, Def3;

        end;

      end;

      hence thesis;

    end;

    theorem :: PROB_3:17

    

     Th17: (( Partial_Diff_Union A1) . n) c= (A1 . n) by Th16;

    theorem :: PROB_3:18

    

     Th18: (( 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 Th9, Th17;

      hence thesis;

    end;

    theorem :: PROB_3:19

    

     Th19: ( Partial_Union ( Partial_Diff_Union A1)) = ( Partial_Union A1)

    proof

      for n be Nat 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);

        

         A1: for k be Nat st P[k] holds P[(k + 1)]

        proof

          let k be Nat such that

           A2: (( 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 A2, Def3

          .= ((A1 . (k + 1)) \/ (( Partial_Union A1) . k)) by XBOOLE_1: 39

          .= (( Partial_Union A1) . (k + 1)) by Def2;

        end;

        (( Partial_Union ( Partial_Diff_Union A1)) . 0 ) = (A2 . 0 ) by Def2

        .= (A1 . 0 ) by Def3

        .= (( Partial_Union A1) . 0 ) by Def2;

        then

         A3: P[ 0 ];

        thus for k be Nat holds P[k] from NAT_1:sch 2( A3, A1);

      end;

      hence thesis;

    end;

    theorem :: PROB_3:20

    

     Th20: ( 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 Th19

      .= ( Union A1) by Th15;

    end;

    definition

      let X, A1;

      :: original: disjoint_valued

      redefine

      :: PROB_3:def4

      attr A1 is disjoint_valued means 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 2;

        assume

         A1: for m, n st m <> n holds (A1 . m) misses (A1 . n);

        now

          let x,y be object;

          assume

           A2: x <> y;

          per cases ;

            suppose x in ( dom A1) & y in ( dom A1);

            hence (A1 . x) misses (A1 . y) by A1, A2;

          end;

            suppose not (x in ( dom A1) & y in ( dom A1));

            then (A1 . x) = {} or (A1 . y) = {} by FUNCT_1:def 2;

            hence (A1 . x) misses (A1 . y);

          end;

        end;

        hence thesis by PROB_2:def 2;

      end;

    end

    registration

      let X, A1;

      cluster ( Partial_Diff_Union A1) -> disjoint_valued;

      coherence

      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 be object such that

           A2: x in (( Partial_Diff_Union A1) . n) and

           A3: x in (( Partial_Diff_Union A1) . m) by XBOOLE_0: 3;

          per cases by A1, XXREAL_0: 1;

            suppose m < n;

            then not x in (A1 . m) by A2, Th16;

            hence contradiction by A3, Th16;

          end;

            suppose n < m;

            then not x in (A1 . n) by A3, Th16;

            hence contradiction by A2, Th16;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let X be set, Si be SigmaField of X, XSeq be SetSequence of Si;

      cluster ( Partial_Intersection XSeq) -> Si -valued;

      coherence

      proof

        defpred P[ set] means (( Partial_Intersection XSeq) . $1) in Si;

        

         A1: for k be Nat st P[k] holds P[(k + 1)]

        proof

          let k be Nat;

          assume

           A2: (( Partial_Intersection XSeq) . k) in Si;

          ((( Partial_Intersection XSeq) . k) /\ (XSeq . (k + 1))) is Event of Si by A2, PROB_1: 19;

          then ((( Partial_Intersection XSeq) . k) /\ (XSeq . (k + 1))) in Si;

          hence thesis by Def1;

        end;

        (XSeq . 0 ) in ( rng XSeq) & (( Partial_Intersection XSeq) . 0 ) = (XSeq . 0 ) by Def1, NAT_1: 51;

        then

         A3: P[ 0 ];

        for k be Nat holds P[k] from NAT_1:sch 2( A3, A1);

        then ( rng ( Partial_Intersection XSeq)) c= Si by NAT_1: 52;

        hence thesis;

      end;

    end

    registration

      let X be set, Si be SigmaField of X, XSeq be SetSequence of Si;

      cluster ( Partial_Union XSeq) -> Si -valued;

      coherence

      proof

        defpred P[ set] means (( Partial_Union XSeq) . $1) in Si;

        

         A1: for k be Nat st P[k] holds P[(k + 1)]

        proof

          let k be Nat;

          assume

           A2: (( Partial_Union XSeq) . k) in Si;

          ((( Partial_Union XSeq) . k) \/ (XSeq . (k + 1))) is Event of Si by A2, PROB_1: 21;

          then ((( Partial_Union XSeq) . k) \/ (XSeq . (k + 1))) in Si;

          hence thesis by Def2;

        end;

        (XSeq . 0 ) in ( rng XSeq) & (( Partial_Union XSeq) . 0 ) = (XSeq . 0 ) by Def2, NAT_1: 51;

        then

         A3: P[ 0 ];

        for k be Nat holds P[k] from NAT_1:sch 2( A3, A1);

        then ( rng ( Partial_Union XSeq)) c= Si by NAT_1: 52;

        hence thesis;

      end;

    end

    registration

      let X be set, Si be SigmaField of X, XSeq be SetSequence of Si;

      cluster ( Partial_Diff_Union XSeq) -> Si -valued;

      coherence

      proof

        

         A1: (XSeq . 0 ) in ( rng XSeq) & (( Partial_Diff_Union XSeq) . 0 ) = (XSeq . 0 ) by Def3, NAT_1: 51;

        for m be Nat holds (( Partial_Diff_Union XSeq) . m) in Si

        proof

          let m be Nat;

          now

            per cases by NAT_1: 6;

              case m = 0 ;

              hence thesis by A1;

            end;

              case ex k be Nat st m = (k + 1);

              then

              consider k be Nat such that

               A2: m = (k + 1);

              reconsider k as Element of NAT by ORDINAL1:def 12;

              ((XSeq . (k + 1)) \ (( Partial_Union XSeq) . k)) in Si;

              hence thesis by A2, Def3;

            end;

          end;

          hence thesis;

        end;

        then ( rng ( Partial_Diff_Union XSeq)) c= Si by NAT_1: 52;

        hence thesis;

      end;

    end

    theorem :: PROB_3:21

    YSeq = ( Partial_Intersection XSeq) implies (YSeq . 0 ) = (XSeq . 0 ) & for n holds (YSeq . (n + 1)) = ((YSeq . n) /\ (XSeq . (n + 1))) by Def1;

    theorem :: PROB_3:22

    YSeq = ( Partial_Union XSeq) implies (YSeq . 0 ) = (XSeq . 0 ) & for n holds (YSeq . (n + 1)) = ((YSeq . n) \/ (XSeq . (n + 1))) by Def2;

    theorem :: PROB_3:23

    (( Partial_Intersection XSeq) . n) c= (XSeq . n) by Th8;

    theorem :: PROB_3:24

    (XSeq . n) c= (( Partial_Union XSeq) . n) by Th9;

    theorem :: PROB_3:25

    for x be object holds x in (( Partial_Intersection XSeq) . n) iff for k st k <= n holds x in (XSeq . k)

    proof

      reconsider XSeq as SetSequence of X;

      let x be object;

      x in (( Partial_Intersection XSeq) . n) iff for k st k <= n holds x in (XSeq . k) by Th12;

      hence thesis;

    end;

    theorem :: PROB_3:26

    x in (( Partial_Union XSeq) . n) iff ex k st k <= n & x in (XSeq . k)

    proof

      reconsider XSeq as SetSequence of X;

      x in (( Partial_Union XSeq) . n) iff ex k st k <= n & x in (XSeq . k) by Th13;

      hence thesis;

    end;

    theorem :: PROB_3:27

    ( Partial_Intersection XSeq) is non-ascending by Th10;

    theorem :: PROB_3:28

    ( Partial_Union XSeq) is non-descending by Th11;

    theorem :: PROB_3:29

    ( Intersection ( Partial_Intersection XSeq)) = ( Intersection XSeq) by Th14;

    theorem :: PROB_3:30

    ( Union ( Partial_Union XSeq)) = ( Union XSeq) by Th15;

    theorem :: PROB_3:31

    YSeq = ( Partial_Diff_Union XSeq) implies (YSeq . 0 ) = (XSeq . 0 ) & for n holds (YSeq . (n + 1)) = ((XSeq . (n + 1)) \ (( Partial_Union XSeq) . n)) by Def3;

    theorem :: PROB_3:32

    x in (( Partial_Diff_Union XSeq) . n) iff x in (XSeq . n) & for k st k < n holds not x in (XSeq . k)

    proof

      reconsider XSeq as SetSequence of X;

      x in (( Partial_Diff_Union XSeq) . n) iff x in (XSeq . n) & for k st k < n holds not x in (XSeq . k) by Th16;

      hence thesis;

    end;

    theorem :: PROB_3:33

    (( Partial_Diff_Union XSeq) . n) c= (XSeq . n) by Th17;

    theorem :: PROB_3:34

    (( Partial_Diff_Union XSeq) . n) c= (( Partial_Union XSeq) . n) by Th18;

    theorem :: PROB_3:35

    ( Partial_Union ( Partial_Diff_Union XSeq)) = ( Partial_Union XSeq) by Th19;

    theorem :: PROB_3:36

    ( Union ( Partial_Diff_Union XSeq)) = ( Union XSeq) by Th20;

    theorem :: PROB_3:37

    

     Th37: (P * ( Partial_Union ASeq)) is non-decreasing

    proof

      ( Partial_Union ASeq) is non-descending by Th11;

      hence thesis by Th6;

    end;

    theorem :: PROB_3:38

    (P * ( Partial_Intersection ASeq)) is non-increasing

    proof

      ( Partial_Intersection ASeq) is non-ascending by Th10;

      hence thesis by Th7;

    end;

    theorem :: PROB_3:39

    ( Partial_Sums (P * ASeq)) is non-decreasing

    proof

      for n be Nat holds ((P * ASeq) . n) >= 0 by Th4;

      hence thesis by SERIES_1: 16;

    end;

    theorem :: PROB_3:40

    

     Th40: ((P * ( Partial_Union ASeq)) . 0 ) = (( Partial_Sums (P * ASeq)) . 0 )

    proof

      

       A1: ( dom (P * ASeq)) = NAT by SEQ_1: 1;

      ( dom (P * ( Partial_Union ASeq))) = NAT by SEQ_1: 1;

      

      then

       A2: ((P * ( Partial_Union ASeq)) . 0 ) = (P . (( Partial_Union ASeq) . 0 )) by FUNCT_1: 12

      .= (P . (ASeq . 0 )) by Def2;

      (( Partial_Sums (P * ASeq)) . 0 ) = ((P * ASeq) . 0 ) by SERIES_1:def 1

      .= (P . (ASeq . 0 )) by A1, FUNCT_1: 12;

      hence thesis by A2;

    end;

    theorem :: PROB_3:41

    

     Th41: (P * ( Partial_Union ASeq)) is convergent & ( lim (P * ( Partial_Union ASeq))) = ( upper_bound (P * ( Partial_Union ASeq))) & ( lim (P * ( Partial_Union ASeq))) = (P . ( Union ASeq))

    proof

      

       A1: (P * ( Partial_Union ASeq)) is non-decreasing by Th37;

      

       A2: ( Partial_Union ASeq) is non-descending by Th11;

      then (P * ( Partial_Union ASeq)) is convergent by PROB_2: 10;

      then

       A3: (P * ( Partial_Union ASeq)) is bounded;

      ( lim (P * ( Partial_Union ASeq))) = (P . ( Union ( Partial_Union ASeq))) by A2, PROB_2: 10

      .= (P . ( Union ASeq)) by Th15;

      hence thesis by A2, A3, A1, PROB_2: 10, RINFSUP1: 24;

    end;

    theorem :: PROB_3:42

    

     Th42: 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

       A2: n < m;

      assume (( Partial_Union ASeq) . n) meets (ASeq . m);

      then

      consider x be object such that

       A3: x in (( Partial_Union ASeq) . n) and

       A4: x in (ASeq . m) by XBOOLE_0: 3;

      reconsider ASeq as SetSequence of Omega;

      consider k be Nat such that

       A5: k <= n and

       A6: x in (ASeq . k) by A3, Th13;

      (ASeq . k) misses (ASeq . m) by A1, A2, A5;

      then ((ASeq . k) /\ (ASeq . m)) = {} ;

      hence contradiction by A4, A6, XBOOLE_0:def 4;

    end;

    theorem :: PROB_3:43

    

     Th43: ASeq is disjoint_valued implies ((P * ( Partial_Union ASeq)) . n) = (( Partial_Sums (P * ASeq)) . n)

    proof

      

       A1: ( dom (P * ASeq)) = NAT by SEQ_1: 1;

      defpred P[ Nat] means ((P * ( Partial_Union ASeq)) . $1) = (( Partial_Sums (P * ASeq)) . $1);

      

       A2: ( dom (P * ( Partial_Union ASeq))) = NAT by SEQ_1: 1;

      assume

       A3: ASeq is disjoint_valued;

      

       A4: for k st P[k] holds P[(k + 1)]

      proof

        let k such that

         A5: ((P * ( Partial_Union ASeq)) . k) = (( Partial_Sums (P * ASeq)) . k);

        k < (k + 1) by NAT_1: 13;

        then

         A6: (( Partial_Union ASeq) . k) misses (ASeq . (k + 1)) by A3, Th42;

        reconsider k as Element of NAT by ORDINAL1:def 12;

        

         A7: (( 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 A1, FUNCT_1: 12;

        ((P * ( Partial_Union ASeq)) . (k + 1)) = (P . (( Partial_Union ASeq) . (k + 1))) by A2, FUNCT_1: 12

        .= (P . ((( Partial_Union ASeq) . k) \/ (ASeq . (k + 1)))) by Def2

        .= ((P . (( Partial_Union ASeq) . k)) + (P . (ASeq . (k + 1)))) by A6, PROB_1:def 8

        .= (((P * ( Partial_Union ASeq)) . k) + (P . (ASeq . (k + 1)))) by A2, FUNCT_1: 12;

        hence thesis by A5, A7;

      end;

      

       A8: P[ 0 ] by Th40;

      for k holds P[k] from NAT_1:sch 2( A8, A4);

      hence thesis;

    end;

    theorem :: PROB_3:44

    

     Th44: ASeq is disjoint_valued implies (P * ( Partial_Union ASeq)) = ( Partial_Sums (P * ASeq)) by Th43;

    theorem :: PROB_3:45

    

     Th45: ASeq is disjoint_valued implies ( Partial_Sums (P * ASeq)) is convergent & ( lim ( Partial_Sums (P * ASeq))) = ( upper_bound ( 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 Th44;

      hence thesis by Th41;

    end;

    theorem :: PROB_3:46

    

     Th46: 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 Th45;

      hence thesis by SERIES_1:def 3;

    end;

    definition

      let X, F1, n;

      :: original: .

      redefine

      func F1 . n -> Subset of X ;

      coherence

      proof

        per cases ;

          suppose n in ( dom F1);

          hence thesis by FINSEQ_2: 11;

        end;

          suppose not n in ( dom F1);

          then (F1 . n) = {} by FUNCT_1:def 2;

          hence thesis by SUBSET_1: 1;

        end;

      end;

    end

    theorem :: PROB_3:47

    ex F1 be FinSequence of ( bool X) st for k st k in ( dom F1) holds (F1 . k) = X

    proof

      now

        let n be Element of NAT ;

        set F1 = (n |-> X);

        

         A1: ( dom F1) = ( Seg n) by FUNCOP_1: 13;

        ( rng F1) c= ( bool X)

        proof

          let x be object;

          assume x in ( rng F1);

          then ex i be Nat st i in ( dom F1) & (F1 . i) = x by FINSEQ_2: 10;

          then x = X by A1, FINSEQ_2: 57;

          hence thesis by ZFMISC_1:def 1;

        end;

        then

         A2: F1 is FinSequence of ( bool X) by FINSEQ_1:def 4;

        for k be Nat st k in ( dom F1) holds (F1 . k) = X by A1, FINSEQ_2: 57;

        hence thesis by A2;

      end;

      hence thesis;

    end;

    theorem :: PROB_3:48

    for F1 be FinSequence of ( bool X) holds ( union ( rng F1)) is Subset of X;

    definition

      let X be set, F1 be FinSequence of ( bool X);

      :: original: Union

      redefine

      func Union F1 -> Subset of X ;

      coherence

      proof

        ( Union F1) = ( union ( rng F1)) by CARD_3:def 4;

        hence thesis;

      end;

    end

    theorem :: PROB_3:49

    

     Th49: 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 and

           A3: Z in ( rng F1) by TARSKI:def 4;

          ex i be Nat st i in ( dom F1) & Z = (F1 . i) by A3, FINSEQ_2: 10;

          hence thesis by A2;

        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) and

           A5: x in (F1 . i);

          (F1 . i) in ( rng F1) by A4, FUNCT_1:def 3;

          hence thesis by A5, TARSKI:def 4;

        end;

      end;

      Y = ( Union F1) by CARD_3:def 4;

      hence thesis by A1;

    end;

    definition

      let X, F1;

      :: PROB_3:def5

      func Complement F1 -> FinSequence of ( bool X) means

      : Def5: ( 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 be FinSequence of ( bool X) such that

         A1: ( len f) = ( len F1) & for n be Nat st n in ( dom f) holds (f . n) = F(n) from FINSEQ_2:sch 1;

        take f;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let F2,F3 be FinSequence of ( bool X) such that

         A2: ( len F2) = ( len F1) and

         A3: for n st n in ( dom F2) holds (F2 . n) = ((F1 . n) ` ) and

         A4: ( len F3) = ( len F1) and

         A5: for n st n in ( dom F3) holds (F3 . n) = ((F1 . n) ` );

        ( dom F2) = ( dom F3) & for k be Nat st k in ( dom F2) holds (F2 . k) = (F3 . k)

        proof

          

          thus

           A6: ( dom F2) = ( Seg ( len F3)) by A2, A4, FINSEQ_1:def 3

          .= ( dom F3) by FINSEQ_1:def 3;

          let k be Nat;

          assume

           A7: k in ( dom F2);

          

          hence (F2 . k) = ((F1 . k) ` ) by A3

          .= (F3 . k) by A5, A6, A7;

        end;

        hence thesis by FINSEQ_1: 13;

      end;

    end

    definition

      let X, F1;

      :: PROB_3:def6

      func Intersection F1 -> Subset of X equals

      : Def6: (( Union ( Complement F1)) ` ) if F1 <> {}

      otherwise {} ;

      coherence by SUBSET_1: 1;

      consistency ;

    end

    theorem :: PROB_3:50

    

     Th50: ( dom ( Complement F1)) = ( dom F1)

    proof

      

      thus ( dom ( Complement F1)) = ( Seg ( len ( Complement F1))) by FINSEQ_1:def 3

      .= ( Seg ( len F1)) by Def5

      .= ( dom F1) by FINSEQ_1:def 3;

    end;

    theorem :: PROB_3:51

    

     Th51: for x be object holds F1 <> {} implies (x in ( Intersection F1) iff for k st k in ( dom F1) holds x in (F1 . k))

    proof

      let x be object;

      

       A1: for n st n in ( dom F1) holds (X \ (( Complement F1) . n)) = (F1 . n)

      proof

        let n;

        assume n in ( dom F1);

        then

         A2: n in ( dom ( Complement F1)) by Th50;

        (X \ (( Complement F1) . n)) = ((( Complement F1) . n) ` ) by SUBSET_1:def 4

        .= (((F1 . n) ` ) ` ) by A2, Def5

        .= (F1 . n);

        hence thesis;

      end;

      assume

       A3: F1 <> {} ;

      then

       A4: ( dom F1) <> {} by RELAT_1: 41;

      

       A5: 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 that

           A6: x in X and

           A7: for n st n in ( dom F1) holds not x in (( Complement F1) . n);

          let n such that

           A8: n in ( dom F1);

           not x in (( Complement F1) . n) by A7, A8;

          then x in (X \ (( Complement F1) . n)) by A6, XBOOLE_0:def 5;

          hence x in (F1 . n) by A1, A8;

        end;

        assume

         A9: for n st n in ( dom F1) holds x in (F1 . n);

         A10:

        now

          let n be Element of NAT such that

           A11: n in ( dom F1);

          x in (F1 . n) by A9, A11;

          then x in (X \ (( Complement F1) . n)) by A1, A11;

          hence x in X & not x in (( Complement F1) . n) by XBOOLE_0:def 5;

        end;

        ex a be object st a in ( dom F1) by A4, XBOOLE_0:def 1;

        hence thesis by A10;

      end;

      ( dom ( Complement F1)) = ( dom F1) by Th50;

      then

       A12: 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) by Th49;

      x in (( Union ( Complement F1)) ` ) iff x in (X \ ( Union ( Complement F1))) by SUBSET_1:def 4;

      hence thesis by A3, A12, A5, Def6, XBOOLE_0:def 5;

    end;

    theorem :: PROB_3:52

    

     Th52: F1 <> {} implies (x in ( meet ( rng F1)) iff for n st n in ( dom F1) holds x in (F1 . n))

    proof

      assume F1 <> {} ;

      then

       A1: ( rng F1) <> {} by RELAT_1: 41;

       A2:

      now

        let x;

        assume

         A3: for n st n in ( dom F1) holds x in (F1 . n);

        now

          let Y;

          assume Y in ( rng F1);

          then

          consider n be object such that

           A4: n in ( dom F1) and

           A5: Y = (F1 . n) by FUNCT_1:def 3;

          thus x in Y by A3, A4, A5;

        end;

        hence x in ( meet ( rng F1)) by A1, SETFAM_1:def 1;

      end;

      now

        let x;

        assume

         A6: x in ( meet ( rng F1));

        now

          let k;

          assume k in ( dom F1);

          then (F1 . k) in ( rng F1) by FUNCT_1: 3;

          hence x in (F1 . k) by A6, SETFAM_1:def 1;

        end;

        hence for n st n in ( dom F1) holds x in (F1 . n);

      end;

      hence thesis by A2;

    end;

    theorem :: PROB_3:53

    ( Intersection F1) = ( meet ( rng F1))

    proof

      per cases ;

        suppose

         A1: F1 <> {} ;

        now

          let x be object;

          x in ( Intersection F1) iff for n st n in ( dom F1) holds x in (F1 . n) by A1, Th51;

          hence x in ( Intersection F1) iff x in ( meet ( rng F1)) by A1, Th52;

        end;

        hence thesis by TARSKI: 2;

      end;

        suppose F1 = {} ;

        hence thesis by Def6, RELAT_1: 38, SETFAM_1: 1;

      end;

    end;

    theorem :: PROB_3:54

    

     Th54: for F1 be FinSequence of ( bool X) holds ex A1 be 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

      deffunc G( object) = {} ;

      let F1 be FinSequence of ( bool X);

      defpred P[ object] means $1 in ( dom F1);

      deffunc F( object) = (F1 . $1);

      ex f be Function st ( dom f) = NAT & for k be object 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 be Function such that

       A1: ( dom f) = NAT and

       A2: for x be object st x in NAT holds (x in ( dom F1) implies (f . x) = (F1 . x)) & ( not x in ( dom F1) implies (f . x) = {} );

      

       A3: for x st x in ( dom F1) holds (F1 . x) in ( bool X)

      proof

        let x;

        assume x in ( dom F1);

        then (F1 . x) in ( rng F1) by FUNCT_1: 3;

        hence thesis;

      end;

      for x st x in NAT holds (f . x) in ( bool X)

      proof

        let x;

        assume

         A4: x in NAT ;

        per cases ;

          suppose not x in ( dom F1);

          then (f . x) = {} by A2, A4;

          then (f . x) c= X;

          hence thesis;

        end;

          suppose

           A5: x in ( dom F1);

          then (f . x) = (F1 . x) by A2;

          hence thesis by A3, A5;

        end;

      end;

      then

      reconsider f as SetSequence of X by A1, FUNCT_2: 3;

      take f;

      thus for k st k in ( dom F1) holds (f . k) = (F1 . k) by A2;

      let k;

      k in NAT by ORDINAL1:def 12;

      hence thesis by A2;

    end;

    theorem :: PROB_3:55

    

     Th55: for F1 be FinSequence of ( bool X) holds for A1 be 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) and

       A2: for k st not k in ( dom F1) holds (A1 . k) = {} ;

      thus (A1 . 0 ) = {} by A2, Th1;

      thus ( Union A1) = ( Union F1)

      proof

        thus ( Union A1) c= ( Union F1)

        proof

          let x be object;

          assume x in ( Union A1);

          then

          consider n be Nat such that

           A3: x in (A1 . n) by PROB_1: 12;

          n in ( dom F1) & x in (F1 . n) by A1, A2, A3;

          hence thesis by Th49;

        end;

        let x be object;

        assume x in ( Union F1);

        then

        consider n such that

         A4: n in ( dom F1) & x in (F1 . n) by Th49;

        n in NAT & x in (A1 . n) by A1, A4;

        hence thesis by PROB_1: 12;

      end;

    end;

    definition

      let X be set, Si be SigmaField of X;

      :: original: FinSequence

      redefine

      mode FinSequence of Si -> FinSequence of ( bool X) ;

      coherence

      proof

        let f be FinSequence of Si;

        thus ( rng f) c= ( bool X) by XBOOLE_1: 1;

      end;

    end

    definition

      let X be set, Si be SigmaField of X, FSi be FinSequence of Si, n;

      :: original: .

      redefine

      func FSi . n -> Event of Si ;

      coherence

      proof

        per cases ;

          suppose n in ( dom FSi);

          hence thesis by FINSEQ_2: 11;

        end;

          suppose not n in ( dom FSi);

          then (FSi . n) = {} by FUNCT_1:def 2;

          hence thesis by PROB_1: 22;

        end;

      end;

    end

    theorem :: PROB_3:56

    

     Th56: for FSi be FinSequence of Si holds ex ASeq be 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 be SetSequence of X such that

       A1: for k st k in ( dom FSi) holds (A1 . k) = (FSi . k) and

       A2: for k st not k in ( dom FSi) holds (A1 . k) = {} by Th54;

      for n be Nat holds (A1 . n) in Si

      proof

        let n be Nat;

        per cases ;

          suppose not n in ( dom FSi);

          then (A1 . n) = {} by A2;

          hence thesis by PROB_1: 4;

        end;

          suppose n in ( dom FSi);

          then (A1 . n) = (FSi . n) by A1;

          hence thesis;

        end;

      end;

      then ( rng A1) c= Si by NAT_1: 52;

      then

      reconsider A1 as SetSequence of Si by RELAT_1:def 19;

      take A1;

      thus thesis by A1, A2;

    end;

    theorem :: PROB_3:57

    

     Th57: for FSi be FinSequence of Si holds ( Union FSi) in Si

    proof

      let FSi be FinSequence of Si;

      consider ASeq be 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 Th56;

      reconsider ASeq as SetSequence of X;

      (for k st k in ( dom FSi) holds (ASeq . k) = (FSi . k)) & for k st not k in ( dom FSi) holds (ASeq . k) = {} by A1;

      then ( Union ASeq) = ( Union FSi) by Th55;

      hence thesis by PROB_1: 17;

    end;

    registration

      let X be set, S be SigmaField of X, F be FinSequence of S;

      cluster ( Complement F) -> S -valued;

      coherence

      proof

        set G = ( Complement F);

        let x be object;

        assume x in ( rng G);

        then

        consider y be object such that

         A1: y in ( dom G) and

         A2: x = (G . y) by FUNCT_1:def 3;

        reconsider y as Nat by A1;

        (G . y) = ((F . y) ` ) by A1, Def5;

        then (G . y) is Event of S by PROB_1: 20;

        hence x in S by A2;

      end;

    end

    theorem :: PROB_3:58

    for FSi be FinSequence of Si holds ( Intersection FSi) in Si

    proof

      let FSi be FinSequence of Si;

      per cases ;

        suppose FSi = {} ;

        then ( Intersection FSi) = {} by Def6;

        hence thesis by PROB_1: 4;

      end;

        suppose

         A1: FSi <> {} ;

        ( rng ( Complement FSi)) c= Si;

        then

        reconsider C = ( Complement FSi) as FinSequence of Si by FINSEQ_1:def 4;

        

         A2: ( Union C) in Si by Th57;

        ( Intersection FSi) = (( Union ( Complement FSi)) ` ) by A1, Def6;

        hence thesis by A2, PROB_1:def 1;

      end;

    end;

    reserve FSeq for FinSequence of Sigma;

    theorem :: PROB_3:59

    

     Th59: ( dom (P * FSeq)) = ( dom FSeq)

    proof

      for x be object holds x in ( dom (P * FSeq)) iff x in ( dom FSeq)

      proof

        let x be object;

        thus x in ( dom (P * FSeq)) implies x in ( dom FSeq) by FUNCT_1: 11;

        assume

         A1: x in ( dom FSeq);

        then

        reconsider k = x as Element of NAT ;

        (FSeq . k) in Sigma;

        then (FSeq . k) in ( dom P) by FUNCT_2:def 1;

        hence thesis by A1, FUNCT_1: 11;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: PROB_3:60

    

     Th60: (P * FSeq) is FinSequence of REAL

    proof

      ( dom (P * FSeq)) = ( dom FSeq) by Th59;

      then ex n be Nat 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 ;

      then ( rng RSeq) c= REAL ;

      hence thesis by FINSEQ_1:def 4;

    end;

    definition

      let Omega, Sigma, FSeq, P;

      :: original: *

      redefine

      func P * FSeq -> FinSequence of REAL ;

      coherence by Th60;

    end

    theorem :: PROB_3:61

    

     Th61: ( len (P * FSeq)) = ( len FSeq)

    proof

      ( dom (P * FSeq)) = ( dom FSeq) by Th59;

      then ( Seg ( len (P * FSeq))) = ( dom FSeq) by FINSEQ_1:def 3;

      hence thesis by FINSEQ_1:def 3;

    end;

    theorem :: PROB_3:62

    

     Th62: ( len RFin) = 0 implies ( Sum RFin) = 0

    proof

      assume

       A1: ( len RFin) = 0 ;

       0 in REAL by XREAL_0:def 1;

      then

       A2: addreal is having_a_unity by RVSUM_1: 1, SETWISEO:def 2;

      

      thus ( Sum RFin) = ( addreal $$ RFin) by RVSUM_1:def 12

      .= 0 by A1, A2, BINOP_2: 2, FINSOP_1:def 1;

    end;

    theorem :: PROB_3:63

    

     Th63: ( len RFin) >= 1 implies ex f be 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 sequence of REAL such that

       A1: (f . 1) = (RFin . 1) and

       A2: for n be Nat st 0 <> n & n < ( len RFin) holds (f . (n + 1)) = ( addreal . ((f . n),(RFin . (n + 1)))) and

       A3: ( addreal "**" RFin) = (f . ( len RFin)) by FINSOP_1: 1;

      take f;

      for n st 0 <> n & n < ( len RFin) holds (f . (n + 1)) = ((f . n) + (RFin . (n + 1)))

      proof

        let n;

        reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

        assume that

         A4: 0 <> n and

         A5: n < ( len RFin);

        

        thus (f . (n + 1)) = ( addreal . ((f . n1),(RFin . (n1 + 1)))) by A2, A4, A5

        .= ((f . n) + (RFin . (n + 1))) by BINOP_2:def 9;

      end;

      hence thesis by A1, A3, RVSUM_1:def 12;

    end;

    theorem :: PROB_3:64

    

     Th64: for FSeq be FinSequence of Sigma, ASeq be 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) and

       A2: for k st not k in ( dom FSeq) holds (ASeq . k) = {} ;

      reconsider XSeq = ASeq as SetSequence of Omega;

      (for k st k in ( dom FSeq) holds (XSeq . k) = (FSeq . k)) & for k st not k in ( dom FSeq) holds (XSeq . k) = {} by A1, A2;

      then

       A3: (ASeq . 0 ) = {} by Th55;

      

       A4: ((P * ASeq) . 0 ) = (P . (ASeq . 0 )) by FUNCT_2: 15

      .= 0 by A3, VALUED_0:def 19;

      

       A5: for k st k in ( dom FSeq) holds ((P * ASeq) . k) = ((P * FSeq) . k)

      proof

        let k such that

         A6: k in ( dom FSeq);

        k in NAT by ORDINAL1:def 12;

        

        hence ((P * ASeq) . k) = (P . (ASeq . k)) by FUNCT_2: 15

        .= (P . (FSeq . k)) by A1, A6

        .= ((P * FSeq) . k) by A6, FUNCT_1: 13;

      end;

      1 = ( 0 + 1);

      

      then

       A7: (( 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 A4;

      

       A8: ( 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 1 in ( dom FSeq) by Th2;

        hence (( Partial_Sums (P * ASeq)) . 1) = ((P * FSeq) . 1) by A5, A7;

        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 that m <> 0 and

           A9: m < ( len FSeq);

          reconsider m1 = m as Element of NAT by ORDINAL1:def 12;

          (m + 1) in ( Seg ( len FSeq)) by A9, FINSEQ_3: 11;

          then

           A10: (m + 1) in ( dom FSeq) by FINSEQ_1:def 3;

          

          thus (( Partial_Sums (P * ASeq)) . (m + 1)) = ((( Partial_Sums (P * ASeq)) . m1) + ((P * ASeq) . (m1 + 1))) by SERIES_1:def 1

          .= ((( Partial_Sums (P * ASeq)) . m) + ((P * FSeq) . (m + 1))) by A5, A10;

        end;

      end;

      defpred P[ Nat] means (( Partial_Sums (P * ASeq)) . ((( len FSeq) + 1) + $1)) = (( Partial_Sums (P * ASeq)) . ( len FSeq));

      

       A11: for m be Nat holds ((P * ASeq) . ((( len FSeq) + 1) + m)) = 0

      proof

        set k = (( len FSeq) + 1);

        let m be Nat;

        reconsider m1 = m as Element of NAT by ORDINAL1:def 12;

        (k + m) >= k by NAT_1: 11;

        then ((( len FSeq) + 1) + m) > ( len FSeq) by Lm1;

        then not ((( len FSeq) + 1) + m) in ( dom FSeq) by FINSEQ_3: 25;

        then

         A12: (ASeq . ((( len FSeq) + 1) + m)) = {} by A2;

        

        thus ((P * ASeq) . ((( len FSeq) + 1) + m)) = (P . (ASeq . ((( len FSeq) + 1) + m1))) by FUNCT_2: 15

        .= 0 by A12, VALUED_0:def 19;

      end;

      

       A13: for k st P[k] holds P[(k + 1)]

      proof

        let k such that

         A14: (( Partial_Sums (P * ASeq)) . ((( len FSeq) + 1) + k)) = (( Partial_Sums (P * ASeq)) . ( len FSeq));

        reconsider k1 = k as Element of NAT by ORDINAL1:def 12;

        (( Partial_Sums (P * ASeq)) . (((( len FSeq) + 1) + k) + 1)) = ((( Partial_Sums (P * ASeq)) . ((( len FSeq) + 1) + k1)) + ((P * ASeq) . ((( len FSeq) + 1) + (k1 + 1)))) by SERIES_1:def 1

        .= ((( Partial_Sums (P * ASeq)) . ((( len FSeq) + 1) + k)) + 0 ) by A11;

        hence thesis by A14;

      end;

      now

        let n be Nat;

        (( Partial_Diff_Union ASeq) . n) c= (ASeq . n) by Th17;

        hence ((P * ( Partial_Diff_Union ASeq)) . n) <= ((P * ASeq) . n) by Th5;

      end;

      then

       A15: for n be Nat holds (( Partial_Sums (P * ( Partial_Diff_Union ASeq))) . n) <= (( Partial_Sums (P * ASeq)) . n) by SERIES_1: 14;

      

       A16: ( Partial_Sums (P * ( Partial_Diff_Union ASeq))) is convergent by Th45;

      (( 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 A11;

      then

       A17: P[ 0 ];

      

       A18: for k holds P[k] from NAT_1:sch 2( A17, A13);

      

       A19: for m st (( len FSeq) + 1) <= m holds (( Partial_Sums (P * ASeq)) . m) = (( Partial_Sums (P * ASeq)) . ( len FSeq))

      proof

        let m;

        assume (( len FSeq) + 1) <= m;

        then ex k be Nat st m = ((( len FSeq) + 1) + k) by NAT_1: 10;

        hence thesis by A18;

      end;

      then

       A20: ( lim ( Partial_Sums (P * ASeq))) = (( Partial_Sums (P * ASeq)) . ( len FSeq)) by Th3;

      then

       A21: ( Sum (P * ASeq)) = (( Partial_Sums (P * ASeq)) . ( len FSeq)) by SERIES_1:def 3;

      

       A22: ( Sum (P * FSeq)) = ( Sum (P * ASeq))

      proof

        now

          per cases ;

            suppose ( len FSeq) = 0 ;

            then ( len (P * FSeq)) = 0 & ( Sum (P * ASeq)) = 0 by A4, A21, Th61, SERIES_1:def 1;

            hence thesis by Th62;

          end;

            suppose

             A23: ( len FSeq) <> 0 ;

            then 1 <= ( len FSeq) by NAT_1: 14;

            then

             A24: 1 <= ( len (P * FSeq)) by Th61;

            then

            consider seq1 be Real_Sequence such that

             A25: (seq1 . 1) = ((P * FSeq) . 1) and

             A26: for n st 0 <> n & n < ( len (P * FSeq)) holds (seq1 . (n + 1)) = ((seq1 . n) + ((P * FSeq) . (n + 1))) and

             A27: ( Sum (P * FSeq)) = (seq1 . ( len (P * FSeq))) by Th63;

            defpred P[ object, object] 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 be 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

              

               A28: for x be object st x in NAT holds ex y be object st P[x, y]

              proof

                let x be object;

                assume x in NAT ;

                then

                reconsider n = x as Element of 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;

              consider f be Function such that

               A29: ( dom f) = NAT & for x be object st x in NAT holds P[x, (f . x)] from CLASSES1:sch 1( A28);

              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 A29;

                hence (f . x) is real;

              end;

              then

              reconsider f as Real_Sequence by A29, SEQ_1: 1;

              take seq = f;

              let n;

              n in NAT by ORDINAL1:def 12;

              then 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 A29;

              hence thesis;

            end;

            then

            consider seq2 be Real_Sequence such that

             A30: 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))));

            defpred P[ Nat] means (seq2 . $1) = (( Partial_Sums (P * ASeq)) . $1);

            

             A31: for k st P[k] holds P[(k + 1)]

            proof

              let k such that

               A32: P[k];

              now

                per cases ;

                  case k = 0 ;

                  thus (seq2 . 1) = (( Partial_Sums (P * ASeq)) . 1) by A8, A23, A24, A25, A30, NAT_1: 14;

                end;

                  case

                   A33: k <> 0 & k <= (( len (P * FSeq)) - 1);

                  then

                   A34: (k + 0 ) < ((( len (P * FSeq)) - 1) + 1) by XREAL_1: 8;

                  then

                   A35: k < ( len FSeq) by Th61;

                  (k + 1) <= ((( len (P * FSeq)) - 1) + 1) by A33, XREAL_1: 7;

                  

                  hence (seq2 . (k + 1)) = (seq1 . (k + 1)) by A30

                  .= ((seq1 . k) + ((P * FSeq) . (k + 1))) by A26, A33, A34

                  .= ((( Partial_Sums (P * ASeq)) . k) + ((P * FSeq) . (k + 1))) by A30, A32, A33, A34

                  .= (( Partial_Sums (P * ASeq)) . (k + 1)) by A8, A33, A35, NAT_1: 14;

                end;

                  case k <> 0 & not k <= (( len (P * FSeq)) - 1);

                  then

                   A36: (k + 1) > ((( len (P * FSeq)) - 1) + 1) by XREAL_1: 8;

                  then (k + 1) >= (( len (P * FSeq)) + 1) by NAT_1: 13;

                  then

                  consider i be Nat such that

                   A37: (k + 1) = ((( len (P * FSeq)) + 1) + i) by NAT_1: 10;

                  

                  thus (seq2 . (k + 1)) = (( Partial_Sums (P * ASeq)) . ( len (P * FSeq))) by A30, A36

                  .= (( Partial_Sums (P * ASeq)) . ( len FSeq)) by Th61

                  .= (( Partial_Sums (P * ASeq)) . ((( len FSeq) + 1) + i)) by A18

                  .= (( Partial_Sums (P * ASeq)) . (k + 1)) by A37, Th61;

                end;

              end;

              hence thesis;

            end;

            (seq2 . 0 ) = ((P * ASeq) . 0 ) by A4, A30

            .= (( Partial_Sums (P * ASeq)) . 0 ) by SERIES_1:def 1;

            then

             A38: P[ 0 ];

            

             A39: for k holds P[k] from NAT_1:sch 2( A38, A31);

            ( len (P * FSeq)) <> 0 by A23, Th61;

            then (seq2 . ( len (P * FSeq))) = ( Sum (P * FSeq)) by A27, A30;

            

            hence ( Sum (P * FSeq)) = (( Partial_Sums (P * ASeq)) . ( len (P * FSeq))) by A39

            .= ( Sum (P * ASeq)) by A21, Th61;

          end;

        end;

        hence thesis;

      end;

      ( Partial_Sums (P * ASeq)) is convergent by A19, Th3;

      then ( lim ( Partial_Sums (P * ( Partial_Diff_Union ASeq)))) <= ( lim ( Partial_Sums (P * ASeq))) by A16, A15, SEQ_2: 18;

      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 Th46;

      hence thesis by A19, A20, A22, Th3, Th20, SERIES_1:def 3;

    end;

    theorem :: PROB_3:65

    (P . ( Union FSeq)) <= ( Sum (P * FSeq)) & (FSeq is disjoint_valued implies (P . ( Union FSeq)) = ( Sum (P * FSeq)))

    proof

      consider ASeq be SetSequence of Sigma such that

       A1: for k st k in ( dom FSeq) holds (ASeq . k) = (FSeq . k) and

       A2: for k st not k in ( dom FSeq) holds (ASeq . k) = {} by Th56;

      reconsider XSeq = ASeq as SetSequence of Omega;

      

       A3: (for k st k in ( dom FSeq) holds (XSeq . k) = (FSeq . k)) & for k st not k in ( dom FSeq) holds (XSeq . k) = {} by A1, A2;

      then (P . ( Union ASeq)) = (P . ( Union FSeq)) by Th55;

      then (P . ( Union FSeq)) <= ( Sum (P * ASeq)) by A1, A2, Th64;

      hence (P . ( Union FSeq)) <= ( Sum (P * FSeq)) by A1, A2, Th64;

      assume

       A4: FSeq is disjoint_valued;

      

       A5: FSeq is disjoint_valued implies ASeq is disjoint_valued

      proof

        assume

         A6: FSeq is disjoint_valued;

        for m,n be Nat st m <> n holds (ASeq . m) misses (ASeq . n)

        proof

          let m,n be Nat such that

           A7: m <> n;

          per cases ;

            suppose

             A8: m in ( dom FSeq) & n in ( dom FSeq);

            (FSeq . m) misses (FSeq . n) by A6, A7, PROB_2:def 2;

            then (ASeq . m) misses (FSeq . n) by A1, A8;

            hence thesis by A1, A8;

          end;

            suppose not (m in ( dom FSeq) & n in ( dom FSeq));

            then (ASeq . m) = {} or (ASeq . n) = {} by A2;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      

      thus (P . ( Union FSeq)) = (P . ( Union ASeq)) by Th55, A3

      .= ( Sum (P * ASeq)) by A5, A4, Th46

      .= ( Sum (P * FSeq)) by A1, A2, Th64;

    end;

    definition

      ::$Canceled

      let X;

      let IT be Subset-Family of X;

      :: PROB_3:def9

      attr IT is non-decreasing-closed means

      : Def7: for A1 be SetSequence of X st A1 is non-descending & ( rng A1) c= IT holds ( Union A1) in IT;

      :: PROB_3:def10

      attr IT is non-increasing-closed means

      : Def8: for A1 be SetSequence of X st A1 is non-ascending & ( rng A1) c= IT holds ( Intersection A1) in IT;

    end

    theorem :: PROB_3:66

    

     Th66: for IT be Subset-Family of X holds IT is non-decreasing-closed iff for A1 be SetSequence of X st A1 is non-descending & ( rng A1) c= IT holds ( lim A1) in IT

    proof

      let IT be Subset-Family of X;

      thus IT is non-decreasing-closed implies for A1 be SetSequence of X st A1 is non-descending & ( rng A1) c= IT holds ( lim A1) in IT

      proof

        assume

         A1: IT is non-decreasing-closed;

        now

          let A1 be SetSequence of X;

          assume that

           A2: A1 is non-descending and

           A3: ( rng A1) c= IT;

          ( Union A1) in IT by A1, A2, A3;

          hence ( lim A1) in IT by A2, SETLIM_1: 63;

        end;

        hence thesis;

      end;

      assume

       A4: for A1 be SetSequence of X st A1 is non-descending & ( rng A1) c= IT holds ( lim A1) in IT;

      for A1 be SetSequence of X st A1 is non-descending & ( rng A1) c= IT holds ( Union A1) in IT

      proof

        let A1 be SetSequence of X;

        assume that

         A5: A1 is non-descending and

         A6: ( rng A1) c= IT;

        ( lim A1) in IT by A4, A5, A6;

        hence thesis by A5, SETLIM_1: 63;

      end;

      hence thesis;

    end;

    theorem :: PROB_3:67

    

     Th67: for IT be Subset-Family of X holds IT is non-increasing-closed iff for A1 be SetSequence of X st A1 is non-ascending & ( rng A1) c= IT holds ( lim A1) in IT

    proof

      let IT be Subset-Family of X;

      thus IT is non-increasing-closed implies for A1 be SetSequence of X st A1 is non-ascending & ( rng A1) c= IT holds ( lim A1) in IT

      proof

        assume

         A1: IT is non-increasing-closed;

        now

          let A1 be SetSequence of X;

          assume that

           A2: A1 is non-ascending and

           A3: ( rng A1) c= IT;

          ( Intersection A1) in IT by A1, A2, A3;

          hence ( lim A1) in IT by A2, SETLIM_1: 64;

        end;

        hence thesis;

      end;

      assume

       A4: for A1 be SetSequence of X st A1 is non-ascending & ( rng A1) c= IT holds ( lim A1) in IT;

      for A1 be SetSequence of X st A1 is non-ascending & ( rng A1) c= IT holds ( Intersection A1) in IT

      proof

        let A1 be SetSequence of X;

        assume that

         A5: A1 is non-ascending and

         A6: ( rng A1) c= IT;

        ( lim A1) in IT by A4, A5, A6;

        hence thesis by A5, SETLIM_1: 64;

      end;

      hence thesis;

    end;

    theorem :: PROB_3:68

    

     Th68: ( bool X) is non-decreasing-closed & ( bool X) is non-increasing-closed;

    registration

      let X;

      cluster non-decreasing-closed non-increasing-closed for Subset-Family of X;

      existence

      proof

        take ( bool X);

        thus thesis;

      end;

    end

    definition

      let X;

      mode MonotoneClass of X is non-decreasing-closed non-increasing-closed Subset-Family of X;

    end

    theorem :: PROB_3:69

    

     Th69: Z is MonotoneClass of X iff Z c= ( bool X) & for A1 be SetSequence of X st A1 is monotone & ( rng A1) c= Z holds ( lim A1) in Z

    proof

      thus Z is MonotoneClass of X implies Z c= ( bool X) & for A1 be SetSequence of X st A1 is monotone & ( rng A1) c= Z holds ( lim A1) in Z

      proof

        assume

         A1: Z is MonotoneClass of X;

        then

        reconsider Z as Subset-Family of X;

        for A1 be SetSequence of X st A1 is monotone & ( rng A1) c= Z holds ( lim A1) in Z

        proof

          let A1 be SetSequence of X;

          assume that

           A2: A1 is monotone and

           A3: ( rng A1) c= Z;

          per cases by A2, SETLIM_1:def 1;

            suppose A1 is non-descending;

            hence thesis by A1, A3, Th66;

          end;

            suppose A1 is non-ascending;

            hence thesis by A1, A3, Th67;

          end;

        end;

        hence thesis;

      end;

      assume that

       A4: Z c= ( bool X) and

       A5: for A1 be SetSequence of X st A1 is monotone & ( rng A1) c= Z holds ( lim A1) in Z;

      reconsider Z as Subset-Family of X by A4;

      

       A6: for A1 be SetSequence of X st A1 is non-ascending & ( rng A1) c= Z holds ( lim A1) in Z

      proof

        let A1 be SetSequence of X;

        assume

         A7: A1 is non-ascending & ( rng A1) c= Z;

        A1 is monotone & ( rng A1) c= Z implies ( lim A1) in Z by A5;

        hence thesis by A7, SETLIM_1:def 1;

      end;

      for A1 be SetSequence of X st A1 is non-descending & ( rng A1) c= Z holds ( lim A1) in Z

      proof

        let A1 be SetSequence of X;

        assume

         A8: A1 is non-descending & ( rng A1) c= Z;

        A1 is monotone & ( rng A1) c= Z implies ( lim A1) in Z by A5;

        hence thesis by A8, SETLIM_1:def 1;

      end;

      hence thesis by A6, Th66, Th67;

    end;

    theorem :: PROB_3:70

    

     Th70: for F be 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;

        

         A1: for A1 be SetSequence of X st A1 is non-descending & ( rng A1) c= F holds ( Union A1) in F

        proof

          let A1 be SetSequence of X;

          assume that A1 is non-descending and

           A2: ( rng A1) c= F;

          reconsider A2 = A1 as SetSequence of F by A2, RELAT_1:def 19;

          ( Union A2) in F by PROB_1: 17;

          hence thesis;

        end;

        F is non-increasing-closed by PROB_1:def 6;

        hence thesis by A1, Def7;

      end;

      assume

       A3: F is MonotoneClass of X;

      for A1 be SetSequence of X st ( rng A1) c= F holds ( Intersection A1) in F

      proof

        let A1 such that

         A4: ( rng A1) c= F;

        set A2 = ( Partial_Intersection A1);

        defpred P[ Nat] means (A2 . $1) in F;

        

         A5: for k st P[k] holds P[(k + 1)]

        proof

          let k;

          assume

           A6: (A2 . k) in F;

          (A1 . (k + 1)) in ( rng A1) & (A2 . (k + 1)) = ((A2 . k) /\ (A1 . (k + 1))) by Def1, NAT_1: 51;

          hence (A2 . (k + 1)) in F by A4, A6, FINSUB_1:def 2;

        end;

        (A1 . 0 ) in ( rng A1) & (A2 . 0 ) = (A1 . 0 ) by Def1, NAT_1: 51;

        then

         A7: P[ 0 ] by A4;

        for k holds P[k] from NAT_1:sch 2( A7, A5);

        then

         A8: ( rng A2) c= F by NAT_1: 52;

        A2 is non-ascending by Th10;

        then ( Intersection A2) in F by A3, A8, Def8;

        hence thesis by Th14;

      end;

      hence thesis by PROB_1:def 6;

    end;

    theorem :: PROB_3:71

    ( bool Omega) is MonotoneClass of Omega by Th68;

    definition

      let Omega;

      let X be Subset-Family of Omega;

      :: PROB_3:def11

      func monotoneclass (X) -> MonotoneClass of Omega means

      : Def9: X c= it & for Z st X c= Z & Z is MonotoneClass of Omega holds it c= Z;

      existence

      proof

        set V = { M where M be Subset-Family of Omega : X c= M & M is MonotoneClass of Omega };

        set Y = ( meet V);

        

         A1: for Z st Z in V holds X c= Z

        proof

          let Z;

          assume Z in V;

          then ex M be Subset-Family of Omega st Z = M & X c= M & M is MonotoneClass of Omega;

          hence thesis;

        end;

        ( bool Omega) is MonotoneClass of Omega by Th68;

        then

         A2: ( bool Omega) in V;

        for MSeq be SetSequence of Omega st MSeq is monotone & ( rng MSeq) c= Y holds ( lim MSeq) in Y

        proof

          let MSeq be SetSequence of Omega such that

           A3: MSeq is monotone and

           A4: ( rng MSeq) c= Y;

          now

            let Z;

            assume

             A5: Z in V;

            now

              let n be Nat;

              (MSeq . n) in ( rng MSeq) by NAT_1: 51;

              hence (MSeq . n) in Z by A4, A5, SETFAM_1:def 1;

            end;

            then

             A6: ( rng MSeq) c= Z by NAT_1: 52;

            ex M be Subset-Family of Omega st Z = M & X c= M & M is MonotoneClass of Omega by A5;

            hence ( lim MSeq) in Z by A3, A6, Th69;

          end;

          hence thesis by A2, SETFAM_1:def 1;

        end;

        then

        reconsider Y as MonotoneClass of Omega by A2, Th69, SETFAM_1: 3;

        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: 3;

        end;

        hence thesis by A2, A1, SETFAM_1: 5;

      end;

      uniqueness ;

    end

    theorem :: PROB_3:72

    

     Th72: for Z be Field_Subset of Omega holds ( monotoneclass Z) is Field_Subset of Omega

    proof

      let Z be Field_Subset of Omega;

      

       A1: Z c= ( monotoneclass Z) by Def9;

      then

      reconsider Z1 = ( monotoneclass Z) as non empty Subset-Family of Omega;

      

       A2: for y,Y be set st Y = { x where x be Element of Z1 : (y \ x) in Z1 & (x \ y) in Z1 & (x /\ y) in Z1 } holds for z be set st z in Y holds z in Z1 & (y \ z) in Z1 & (z \ y) in Z1 & (z /\ y) in Z1

      proof

        let y,Y be set;

        assume

         A3: Y = { x where x be Element of Z1 : (y \ x) in Z1 & (x \ y) in Z1 & (x /\ y) in Z1 };

        thus for z be set st z in Y holds z in Z1 & (y \ z) in Z1 & (z \ y) in Z1 & (z /\ y) in Z1

        proof

          let z be set;

          assume z in Y;

          then ex z1 be Element of Z1 st z = z1 & (y \ z1) in Z1 & (z1 \ y) in Z1 & (z1 /\ y) in Z1 by A3;

          hence thesis;

        end;

      end;

      

       A4: for y be Element of Z1, Y st Y = { x where x be 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

         A5: Y = { x where x be Element of Z1 : (y \ x) in Z1 & (x \ y) in Z1 & (x /\ y) in Z1 };

        

         A6: for A1 be SetSequence of Omega st A1 is monotone & ( rng A1) c= Y holds ( lim A1) in Y

        proof

          let A1 be SetSequence of Omega such that

           A7: A1 is monotone and

           A8: ( rng A1) c= Y;

          

           A9: A1 is convergent by A7, SETLIM_1: 65;

          for n holds (A1 . n) in Z1

          proof

            let n;

            (A1 . n) in ( rng A1) by NAT_1: 51;

            hence thesis by A2, A5, A8;

          end;

          then ( rng A1) c= Z1 by NAT_1: 52;

          then

           A10: ( lim A1) is Element of Z1 by A7, Th69;

          for n holds ((A1 (\) y) . n) in Z1

          proof

            let n be Nat;

            (A1 . n) in ( rng A1) by NAT_1: 51;

            then n in NAT & ((A1 . n) \ y) in Z1 by A2, A5, A8, ORDINAL1:def 12;

            hence thesis by SETLIM_2:def 8;

          end;

          then

           A11: ( rng (A1 (\) y)) c= Z1 by NAT_1: 52;

          for n holds ((y (/\) A1) . n) in Z1

          proof

            let n;

            (A1 . n) in ( rng A1) by NAT_1: 51;

            then n in NAT & (y /\ (A1 . n)) in Z1 by A2, A5, A8, ORDINAL1:def 12;

            hence thesis by SETLIM_2:def 5;

          end;

          then

           A12: ( rng (y (/\) A1)) c= Z1 by NAT_1: 52;

          (y (/\) A1) is monotone by A7, SETLIM_2: 23;

          then ( lim (y (/\) A1)) in Z1 by A12, Th69;

          then

           A13: (y /\ ( lim A1)) in Z1 by A9, SETLIM_2: 92;

          for n holds ((y (\) A1) . n) in Z1

          proof

            let n;

            (A1 . n) in ( rng A1) by NAT_1: 51;

            then n in NAT & (y \ (A1 . n)) in Z1 by A2, A5, A8, ORDINAL1:def 12;

            hence thesis by SETLIM_2:def 7;

          end;

          then

           A14: ( rng (y (\) A1)) c= Z1 by NAT_1: 52;

          (y (\) A1) is monotone by A7, SETLIM_2: 29;

          then ( lim (y (\) A1)) in Z1 by A14, Th69;

          then

           A15: (y \ ( lim A1)) in Z1 by A9, SETLIM_2: 94;

          (A1 (\) y) is monotone by A7, SETLIM_2: 32;

          then ( lim (A1 (\) y)) in Z1 by A11, Th69;

          then (( lim A1) \ y) in Z1 by A9, SETLIM_2: 95;

          hence thesis by A5, A10, A15, A13;

        end;

        for z be object holds z in Y implies z in Z1 by A2, A5;

        then Y c= Z1;

        hence thesis by A6, Th69, XBOOLE_1: 1;

      end;

      

       A16: for y be Element of Z, Y st Y = { x where x be 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

         A17: Y = { x where x be Element of Z1 : (y \ x) in Z1 & (x \ y) in Z1 & (x /\ y) in Z1 };

        

         A18: Z c= Y

        proof

          let z be object;

          reconsider zz = z as set by TARSKI: 1;

          assume

           A19: z in Z;

          then

           A20: (zz /\ y) in Z by FINSUB_1:def 2;

          (zz \ y) in Z & (y \ zz) in Z by A19, PROB_1: 6;

          hence thesis by A1, A17, A19, A20;

        end;

        y in Z;

        then Y is MonotoneClass of Omega by A1, A4, A17;

        hence thesis by A18, Def9;

      end;

      

       A21: for y be Element of Z1, Y st Y = { x where x be 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

         A22: Y = { x where x be Element of Z1 : (y \ x) in Z1 & (x \ y) in Z1 & (x /\ y) in Z1 };

        

         A23: Z c= Y

        proof

          let z be object;

          reconsider zz = z as set by TARSKI: 1;

          set Y1 = { x where x be Element of Z1 : (zz \ x) in Z1 & (x \ zz) in Z1 & (x /\ zz) in Z1 };

          assume

           A24: z in Z;

          then

           A25: Z1 c= Y1 by A16;

          

           A26: y in Z1;

          then

           A27: (zz /\ y) in Z1 by A2, A25;

          (zz \ y) in Z1 & (y \ zz) in Z1 by A2, A25, A26;

          hence thesis by A1, A22, A24, A27;

        end;

        Y is MonotoneClass of Omega by A4, A22;

        hence thesis by A23, Def9;

      end;

      

       A28: for y be Subset of Omega st y in Z1 holds (y ` ) in Z1

      proof

        Omega in Z by PROB_1: 5;

        then

         A29: Omega in Z1 by A1;

        let y be Subset of Omega such that

         A30: y in Z1;

        set Y = { x where x be Element of Z1 : (y \ x) in Z1 & (x \ y) in Z1 & (x /\ y) in Z1 };

        Z1 c= Y by A21, A30;

        then (Omega \ y) in Z1 by A2, A29;

        hence thesis by SUBSET_1:def 4;

      end;

      now

        let y,z be set;

        assume that

         A31: y in Z1 and

         A32: z in Z1;

        set Y = { x where x be Element of Z1 : (y \ x) in Z1 & (x \ y) in Z1 & (x /\ y) in Z1 };

        Z1 c= Y by A21, A31;

        hence (y /\ z) in Z1 by A2, A32;

      end;

      hence thesis by A28, FINSUB_1:def 2, PROB_1:def 1;

    end;

    theorem :: PROB_3:73

    for Z be Field_Subset of Omega holds ( sigma Z) = ( monotoneclass Z)

    proof

      let Z be Field_Subset of Omega;

      ( monotoneclass Z) is Field_Subset of Omega by Th72;

      then

       A1: ( monotoneclass Z) is SigmaField of Omega by Th70;

      Z c= ( monotoneclass Z) by Def9;

      hence ( sigma Z) c= ( monotoneclass Z) by A1, PROB_1:def 9;

      ( sigma Z) is MonotoneClass of Omega & Z c= ( sigma Z) by Th70, PROB_1:def 9;

      hence thesis by Def9;

    end;