kolmog01.miz



    begin

    reserve Omega,I for non empty set;

    reserve Sigma for SigmaField of Omega;

    reserve P for Probability of Sigma;

    reserve D,E,F for Subset-Family of Omega;

    reserve B,sB for non empty Subset of Sigma;

    reserve b for Element of B;

    reserve a for Element of Sigma;

    reserve p,q,u,v for Event of Sigma;

    reserve n,m for Element of NAT ;

    reserve S,S9,X,x,y,z,i,j for set;

    theorem :: KOLMOG01:1

    

     Th1: for f be Function, X be set st X c= ( dom f) holds X <> {} implies ( rng (f | X)) <> {}

    proof

      let f be Function, X be set;

      assume

       A1: X c= ( dom f);

      set x = the Element of X;

      assume X <> {} ;

      then x in X;

      hence thesis by A1, FUNCT_1: 50;

    end;

    theorem :: KOLMOG01:2

    

     Th2: for r be Real st (r * r) = r holds r = 0 or r = 1

    proof

      let r be Real;

      assume (r * r) = r;

      then (r * (r - 1)) = 0 ;

      then r = 0 or (r - 1) = 0 by XCMPLX_1: 6;

      hence thesis;

    end;

    theorem :: KOLMOG01:3

    

     Th3: for X be Subset-Family of Omega st X = {} holds ( sigma X) = { {} , Omega}

    proof

      let X be Subset-Family of Omega;

      

       A1: for A1 be SetSequence of Omega st ( rng A1) c= { {} , Omega} holds ( Union A1) in { {} , Omega}

      proof

        let A1 be SetSequence of Omega;

        assume

         A2: ( rng A1) c= { {} , Omega};

        

         A3: for n be Nat holds ((( Partial_Union A1) . n) = {} or (( Partial_Union A1) . n) = Omega)

        proof

          defpred P[ Nat] means (( Partial_Union A1) . $1) = {} or (( Partial_Union A1) . $1) = Omega;

          let n be Nat;

          

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

          proof

            let k be Nat;

            assume

             A5: (( Partial_Union A1) . k) = {} or (( Partial_Union A1) . k) = Omega;

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

            

             A6: (A1 . (k + 1)) in ( rng A1) by NAT_1: 51;

            per cases by A5, PROB_3:def 2;

              suppose (( Partial_Union A1) . (k + 1)) = ( {} \/ (A1 . (k + 1)));

              hence thesis by A2, A6, TARSKI:def 2;

            end;

              suppose

               A7: (( Partial_Union A1) . (k + 1)) = (Omega \/ (A1 . (k + 1)));

              (A1 . (k + 1)) = {} or (A1 . (k + 1)) = Omega by A2, A6, TARSKI:def 2;

              hence thesis by A7;

            end;

          end;

          (( Partial_Union A1) . 0 ) = (A1 . 0 ) & (A1 . 0 ) in ( rng A1) by NAT_1: 51, PROB_3:def 2;

          then

           A8: P[ 0 ] by A2, TARSKI:def 2;

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

          hence thesis;

        end;

        ( Union ( Partial_Union A1)) = {} or ( Union ( Partial_Union A1)) = Omega

        proof

          per cases ;

            suppose

             A9: for n be Nat holds (( Partial_Union A1) . n) = {} ;

             not ex x be object st x in ( Union ( Partial_Union A1))

            proof

              given x be object such that

               A10: x in ( Union ( Partial_Union A1));

              reconsider x as set by TARSKI: 1;

              ex n be Nat st x in (( Partial_Union A1) . n) by PROB_1: 12, A10;

              hence contradiction by A9;

            end;

            hence thesis by XBOOLE_0:def 1;

          end;

            suppose not for n be Nat holds (( Partial_Union A1) . n) = {} ;

            then

            consider n be Nat such that

             A11: (( Partial_Union A1) . n) <> {} ;

            (( Partial_Union A1) . n) = Omega by A3, A11;

            then for x be object holds x in Omega implies x in ( Union ( Partial_Union A1)) by PROB_1: 12;

            then Omega c= ( Union ( Partial_Union A1));

            hence thesis;

          end;

        end;

        then ( Union A1) = {} or ( Union A1) = Omega by PROB_3: 15;

        hence thesis by TARSKI:def 2;

      end;

      

       A12: for A be Subset of Omega st A in { {} , Omega} holds (A ` ) in { {} , Omega}

      proof

        let A be Subset of Omega;

        assume A in { {} , Omega};

        then A = {} or A = Omega by TARSKI:def 2;

        then (A ` ) = Omega or (A ` ) = {} by XBOOLE_1: 37;

        hence thesis by TARSKI:def 2;

      end;

       {} in ( sigma X) & Omega in ( sigma X) by PROB_1: 4, PROB_1: 5;

      then for x be object holds x in { {} , Omega} implies x in ( sigma X) by TARSKI:def 2;

      then

       A13: { {} , Omega} c= ( sigma X);

      assume X = {} ;

      then

       A14: X c= { {} , Omega};

      for x be object holds x in { {} , Omega} implies x in ( bool Omega)

      proof

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        assume x in { {} , Omega};

        then x = {} or x = Omega by TARSKI:def 2;

        then xx c= Omega;

        hence thesis;

      end;

      then { {} , Omega} is SigmaField of Omega by A1, A12, PROB_4: 4, TARSKI:def 3;

      then ( sigma X) c= { {} , Omega} by A14, PROB_1:def 9;

      hence thesis by A13;

    end;

    definition

      let Omega be non empty set, Sigma be SigmaField of Omega, B be Subset of Sigma, P be Probability of Sigma;

      :: KOLMOG01:def1

      func Indep (B,P) -> Subset of Sigma means

      : Def1: for a be Element of Sigma holds a in it iff for b be Element of B holds (P . (a /\ b)) = ((P . a) * (P . b));

      existence

      proof

        defpred P[ set] means for b be Element of B holds (P . ($1 /\ b)) = ((P . $1) * (P . b));

        consider X such that

         A1: for x holds x in X iff x in Sigma & P[x] from XFAMILY:sch 1;

        for x be object holds x in X implies x in Sigma by A1;

        then

        reconsider X as Subset of Sigma by TARSKI:def 3;

        take X;

        let a be Element of Sigma;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let X1,X2 be Subset of Sigma;

        assume

         A2: for a be Element of Sigma holds a in X1 iff for b be Element of B holds (P . (a /\ b)) = ((P . a) * (P . b));

        assume

         A3: for a be Element of Sigma holds a in X2 iff for b be Element of B holds (P . (a /\ b)) = ((P . a) * (P . b));

        now

          let a be Element of Sigma;

          a in X1 iff for b be Element of B holds (P . (a /\ b)) = ((P . a) * (P . b)) by A2;

          hence a in X1 iff a in X2 by A3;

        end;

        hence thesis by SUBSET_1: 3;

      end;

    end

    theorem :: KOLMOG01:4

    

     Th4: for f be SetSequence of Sigma holds (for n, b holds (P . ((f . n) /\ b)) = ((P . (f . n)) * (P . b))) & f is disjoint_valued implies (P . (b /\ ( Union f))) = ((P . b) * (P . ( Union f)))

    proof

      let f be SetSequence of Sigma;

      reconsider b as Element of Sigma;

      reconsider r = (P . b) as Real;

      for n be Nat holds (( seqIntersection (b,f)) . n) is Event of Sigma

      proof

        let n be Nat;

        

         A1: n in NAT by ORDINAL1:def 12;

        (b /\ (f . n)) is Event of Sigma;

        hence thesis by DYNKIN:def 1, A1;

      end;

      then

      reconsider seqIntf = ( seqIntersection (b,f)) as SetSequence of Sigma by PROB_1: 25;

      for n be Nat holds (( seqIntersection (b,( Partial_Union f))) . n) is Event of Sigma

      proof

        let n be Nat;

        

         A2: n in NAT by ORDINAL1:def 12;

        (b /\ (( Partial_Union f) . n)) is Event of Sigma;

        hence thesis by DYNKIN:def 1, A2;

      end;

      then

      reconsider seqIntPf = ( seqIntersection (b,( Partial_Union f))) as SetSequence of Sigma by PROB_1: 25;

      

       A3: (b /\ ( Union f)) = (b /\ ( Union ( Partial_Union f))) by PROB_3: 15

      .= ( Union seqIntPf) by DYNKIN: 10;

      assume

       A4: for n, b holds (P . ((f . n) /\ b)) = ((P . (f . n)) * (P . b));

      now

        let n be Element of NAT ;

        

        thus ((P * seqIntf) . n) = (P . (seqIntf . n)) by FUNCT_2: 15

        .= (P . ((f . n) /\ b)) by DYNKIN:def 1

        .= ((P . (f . n)) * (P . b)) by A4

        .= (((P * f) . n) * r) by FUNCT_2: 15

        .= ((r (#) (P * f)) . n) by SEQ_1: 9;

      end;

      then

       A5: (P * seqIntf) = (r (#) (P * f)) by FUNCT_2:def 7;

      

       A6: for n, m st n <= m holds x in (( Partial_Union f) . n) implies x in (( Partial_Union f) . m)

      proof

        reconsider Pf = ( Partial_Union f) as SetSequence of Sigma;

        let n, m;

        assume

         A7: n <= m;

        assume

         A8: x in (( Partial_Union f) . n);

        Pf is non-descending by PROB_3: 11;

        then (Pf . n) c= (Pf . m) by A7;

        hence thesis by A8;

      end;

      for n,m be Nat st n <= m holds (( seqIntersection (b,( Partial_Union f))) . n) c= (( seqIntersection (b,( Partial_Union f))) . m)

      proof

        let n,m be Nat;

        assume

         A9: n <= m;

        

         A10: m in NAT by ORDINAL1:def 12;

        

         A11: n in NAT by ORDINAL1:def 12;

        let x be object;

        assume x in (( seqIntersection (b,( Partial_Union f))) . n);

        then

         A12: x in (b /\ (( Partial_Union f) . n)) by DYNKIN:def 1, A11;

        then x in (( Partial_Union f) . n) by XBOOLE_0:def 4;

        then

         A13: x in (( Partial_Union f) . m) by A6, A9, A11, A10;

        x in b by A12, XBOOLE_0:def 4;

        then x in (b /\ (( Partial_Union f) . m)) by A13, XBOOLE_0:def 4;

        hence thesis by DYNKIN:def 1, A10;

      end;

      then

       A14: ( seqIntersection (b,( Partial_Union f))) is non-descending;

      assume

       A15: f is disjoint_valued;

      then

       A16: ( seqIntersection (b,f)) is disjoint_valued by DYNKIN: 9;

      for n holds (( Partial_Union seqIntf) . n) = (( seqIntersection (b,( Partial_Union f))) . n)

      proof

        defpred P[ Nat] means (( Partial_Union seqIntf) . $1) = (( seqIntersection (b,( Partial_Union f))) . $1);

        let n;

        

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

        proof

          let k be Nat such that

           A18: (( Partial_Union seqIntf) . k) = (( seqIntersection (b,( Partial_Union f))) . k);

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

          (( Partial_Union seqIntf) . (k + 1)) = ((( Partial_Union seqIntf) . k) \/ (seqIntf . (k + 1))) by PROB_3:def 2

          .= ((b /\ (( Partial_Union f) . k)) \/ (seqIntf . (k + 1))) by A18, DYNKIN:def 1

          .= ((b /\ (( Partial_Union f) . k)) \/ (b /\ (f . (k + 1)))) by DYNKIN:def 1

          .= (b /\ ((( Partial_Union f) . k) \/ (f . (k + 1)))) by XBOOLE_1: 23

          .= (b /\ (( Partial_Union f) . (k + 1))) by PROB_3:def 2

          .= (( seqIntersection (b,( Partial_Union f))) . (k + 1)) by DYNKIN:def 1;

          hence thesis;

        end;

        (( Partial_Union seqIntf) . 0 ) = (seqIntf . 0 ) by PROB_3:def 2

        .= (b /\ (f . 0 )) by DYNKIN:def 1

        .= (b /\ (( Partial_Union f) . 0 )) by PROB_3:def 2

        .= (( seqIntersection (b,( Partial_Union f))) . 0 ) by DYNKIN:def 1;

        then

         A19: P[ 0 ];

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

        hence thesis;

      end;

      

      then (P * ( seqIntersection (b,( Partial_Union f)))) = (P * ( Partial_Union seqIntf)) by FUNCT_2: 63

      .= ( Partial_Sums (P * seqIntf)) by A16, PROB_3: 44

      .= (r (#) ( Partial_Sums (P * f))) by A5, SERIES_1: 9

      .= (r (#) (P * ( Partial_Union f))) by A15, PROB_3: 44;

      

      then (r * ( lim (P * ( Partial_Union f)))) = ( lim (P * seqIntPf)) by PROB_3: 41, SEQ_2: 8

      .= (P . (b /\ ( Union f))) by A14, A3, PROB_2: 10;

      hence thesis by PROB_3: 41;

    end;

    theorem :: KOLMOG01:5

    

     Th5: ( Indep (B,P)) is Dynkin_System of Omega

    proof

      

       A1: for b holds (P . ( {} /\ b)) = ((P . {} ) * (P . b))

      proof

        let b;

        reconsider b as Event of Sigma;

        (P . ( {} /\ b)) = 0 by VALUED_0:def 19;

        hence thesis;

      end;

      reconsider Indp = ( Indep (B,P)) as Subset-Family of Omega by XBOOLE_1: 1;

       {} is Element of Sigma by PROB_1: 22;

      then

       A2: {} in ( Indep (B,P)) by A1, Def1;

      

       A3: for g be SetSequence of Omega st ( rng g) c= ( Indep (B,P)) & g is disjoint_valued holds ( Union g) in ( Indep (B,P))

      proof

        let g be SetSequence of Omega;

        assume that

         A4: ( rng g) c= ( Indep (B,P)) and

         A5: g is disjoint_valued;

        now

          let n be Nat;

          (g . n) is Element of Sigma

          proof

            per cases ;

              suppose n in ( dom g);

              then (g . n) in ( rng g) by FUNCT_1: 3;

              hence thesis by A4, TARSKI:def 3;

            end;

              suppose not n in ( dom g);

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

              hence thesis by PROB_1: 4;

            end;

          end;

          hence (g . n) is Event of Sigma;

        end;

        then

        reconsider g as SetSequence of Sigma by PROB_1: 25;

        reconsider Ug = ( Union g) as Element of Sigma by PROB_1: 26;

        for n, b holds (P . ((g . n) /\ b)) = ((P . (g . n)) * (P . b))

        proof

          let n, b;

          (g . n) in ( Indep (B,P))

          proof

            per cases ;

              suppose n in ( dom g);

              then (g . n) in ( rng g) by FUNCT_1: 3;

              hence thesis by A4;

            end;

              suppose not n in ( dom g);

              hence thesis by A2, FUNCT_1:def 2;

            end;

          end;

          hence thesis by Def1;

        end;

        then for b holds (P . (Ug /\ b)) = ((P . Ug) * (P . b)) by A5, Th4;

        hence thesis by Def1;

      end;

      for Z be Subset of Omega st Z in ( Indep (B,P)) holds (Z ` ) in ( Indep (B,P))

      proof

        let Z be Subset of Omega;

        assume

         A6: Z in ( Indep (B,P));

        then

        reconsider Z as Event of Sigma;

        reconsider Z9 = (Z ` ) as Element of Sigma by PROB_1: 20;

        for b be Element of B holds (P . ((Z ` ) /\ b)) = ((P . (Z ` )) * (P . b))

        proof

          let b be Element of B;

          (P . (b /\ Z)) = ((P . b) * (P . Z)) by A6, Def1;

          then (b,Z) are_independent_respect_to P by PROB_2:def 4;

          then (b,(( [#] Sigma) \ Z)) are_independent_respect_to P by PROB_2: 25;

          hence thesis by PROB_2:def 4;

        end;

        then Z9 in ( Indep (B,P)) by Def1;

        hence thesis;

      end;

      then Indp is Dynkin_System of Omega by A2, A3, DYNKIN:def 5;

      hence thesis;

    end;

    theorem :: KOLMOG01:6

    

     Th6: for A be Subset-Family of Omega st A is intersection_stable & A c= ( Indep (B,P)) holds ( sigma A) c= ( Indep (B,P))

    proof

      reconsider Indp = ( Indep (B,P)) as Dynkin_System of Omega by Th5;

      let A be Subset-Family of Omega;

      assume A is intersection_stable & A c= ( Indep (B,P));

      then ( sigma A) c= Indp by DYNKIN: 24;

      hence thesis;

    end;

    theorem :: KOLMOG01:7

    

     Th7: for A,B be non empty Subset of Sigma holds A c= ( Indep (B,P)) iff for p, q st p in A & q in B holds (p,q) are_independent_respect_to P

    proof

      let A,B be non empty Subset of Sigma;

       A1:

      now

        assume

         A2: for p, q st p in A & q in B holds (p,q) are_independent_respect_to P;

        thus A c= ( Indep (B,P))

        proof

          let x be object;

          assume

           A3: x in A;

          then

          reconsider x as Event of Sigma;

          for b be Element of B holds (P . (x /\ b)) = ((P . x) * (P . b)) by A2, A3, PROB_2:def 4;

          hence thesis by Def1;

        end;

      end;

      now

        assume

         A4: A c= ( Indep (B,P));

        thus for p, q st p in A & q in B holds (p,q) are_independent_respect_to P

        proof

          let p, q;

          assume that

           A5: p in A and

           A6: q in B;

          reconsider q as Element of B by A6;

          reconsider p as Element of Sigma;

          (P . (p /\ q)) = ((P . p) * (P . q)) by A4, A5, Def1;

          hence thesis by PROB_2:def 4;

        end;

      end;

      hence thesis by A1;

    end;

    theorem :: KOLMOG01:8

    

     Th8: for A,B be non empty Subset of Sigma st A c= ( Indep (B,P)) holds B c= ( Indep (A,P))

    proof

      let A,B be non empty Subset of Sigma;

      assume

       A1: A c= ( Indep (B,P));

      for q, p st q in B & p in A holds (q,p) are_independent_respect_to P by A1, Th7, PROB_2: 19;

      hence thesis by Th7;

    end;

    theorem :: KOLMOG01:9

    

     Th9: for A be Subset-Family of Omega st A is non empty Subset of Sigma & A is intersection_stable holds for B be non empty Subset of Sigma st B is intersection_stable holds A c= ( Indep (B,P)) implies for D, sB st D = B & ( sigma D) = sB holds ( sigma A) c= ( Indep (sB,P))

    proof

      let A be Subset-Family of Omega;

      assume A is non empty Subset of Sigma;

      then

      reconsider sA = ( sigma A) as non empty Subset of Sigma by PROB_1:def 9;

      assume

       A1: A is intersection_stable;

      let B be non empty Subset of Sigma;

      assume

       A2: B is intersection_stable;

      assume A c= ( Indep (B,P));

      then

       A3: ( sigma A) c= ( Indep (B,P)) by A1, Th6;

      let D, sB;

      assume

       A4: D = B & ( sigma D) = sB;

      reconsider B as Subset-Family of Omega by XBOOLE_1: 1;

      B c= ( Indep (sA,P)) by A3, Th8;

      then ( sigma B) c= ( Indep (sA,P)) by A2, Th6;

      hence thesis by A4, Th8;

    end;

    theorem :: KOLMOG01:10

    

     Th10: for E, F st E is non empty Subset of Sigma & E is intersection_stable & F is non empty Subset of Sigma & F is intersection_stable holds (for p, q st p in E & q in F holds (p,q) are_independent_respect_to P) implies for u, v st u in ( sigma E) & v in ( sigma F) holds (u,v) are_independent_respect_to P

    proof

      let E, F;

      assume

       A1: E is non empty Subset of Sigma;

      assume

       A2: E is intersection_stable;

      assume

       A3: F is non empty Subset of Sigma;

      assume

       A4: F is intersection_stable;

      assume

       A5: for p, q st p in E & q in F holds (p,q) are_independent_respect_to P;

      reconsider F as non empty Subset of Sigma by A3;

      reconsider E as non empty Subset of Sigma by A1;

      

       A6: E c= ( Indep (F,P)) by A5, Th7;

      reconsider E, F as Subset-Family of Omega;

      reconsider sF = ( sigma F) as non empty Subset of Sigma by PROB_1:def 9;

      ( sigma E) c= ( Indep (sF,P)) by A2, A4, A6, Th9;

      hence thesis by Th7;

    end;

    definition

      let I be set, Omega be non empty set, Sigma be SigmaField of Omega;

      :: KOLMOG01:def2

      mode ManySortedSigmaField of I,Sigma -> Function of I, ( bool Sigma) means

      : Def2: for i st i in I holds (it . i) is SigmaField of Omega;

      existence

      proof

        set F = (I --> Sigma);

        

         A1: ( rng F) c= ( bool Sigma)

        proof

          let y be object;

          assume y in ( rng F);

          then ex x be object st x in ( dom F) & y = (F . x) by FUNCT_1:def 3;

          then y = Sigma by FUNCOP_1: 7;

          hence thesis by ZFMISC_1:def 1;

        end;

        

         A2: for i st i in I holds (F . i) is SigmaField of Omega by FUNCOP_1: 7;

        ( dom F) = I by FUNCOP_1: 13;

        then F is Function of I, ( bool Sigma) by A1, FUNCT_2: 2;

        hence thesis by A2;

      end;

    end

    definition

      let Omega be non empty set, Sigma be SigmaField of Omega, P be Probability of Sigma, I be set, A be Function of I, Sigma;

      :: KOLMOG01:def3

      pred A is_independent_wrt P means for e be one-to-one FinSequence of I st e <> {} holds ( Product ((P * A) * e)) = (P . ( meet ( rng (A * e))));

    end

    definition

      let Omega be non empty set, Sigma be SigmaField of Omega, I be set, J be Subset of I, F be ManySortedSigmaField of I, Sigma;

      :: KOLMOG01:def4

      mode SigmaSection of J,F -> Function of J, Sigma means

      : Def4: for i st i in J holds (it . i) in (F . i);

      existence

      proof

        set f = (J --> {} );

        

         A1: for i st i in J holds (f . i) in (F . i)

        proof

          let i;

          assume

           A2: i in J;

          then (F . i) is SigmaField of Omega by Def2;

          then {} in (F . i) by PROB_1: 4;

          hence thesis by A2, FUNCOP_1: 7;

        end;

        

         A3: ( dom f) = J by FUNCOP_1: 13;

        ( rng f) c= Sigma

        proof

          let y be object;

          assume y in ( rng f);

          then

          consider i be object such that

           A4: i in J & y = (f . i) by A3, FUNCT_1:def 3;

          y in (F . i) & (F . i) in ( bool Sigma) by A1, A4, FUNCT_2: 5;

          hence thesis;

        end;

        then f is Function of J, Sigma by A3, FUNCT_2: 2;

        hence thesis by A1;

      end;

    end

    definition

      let Omega be non empty set, Sigma be SigmaField of Omega, P be Probability of Sigma, I be set, F be ManySortedSigmaField of I, Sigma;

      :: KOLMOG01:def5

      pred F is_independent_wrt P means for E be finite Subset of I, A be SigmaSection of E, F holds A is_independent_wrt P;

    end

    definition

      let I be set, Omega be non empty set, Sigma be SigmaField of Omega, F be ManySortedSigmaField of I, Sigma, J be Subset of I;

      :: original: |

      redefine

      func F | J -> Function of J, ( bool Sigma) ;

      coherence by FUNCT_2: 32;

    end

    definition

      let I be set, J be Subset of I, Omega be non empty set, Sigma be SigmaField of Omega, F be Function of J, ( bool Sigma);

      :: original: Union

      redefine

      func Union F -> Subset-Family of Omega ;

      coherence

      proof

        for y be object holds y in ( Union F) implies y in ( bool Omega)

        proof

          let y be object;

          assume y in ( Union F);

          then

          consider i be object such that

           A1: i in ( dom F) & y in (F . i) by CARD_5: 2;

          reconsider i as set by TARSKI: 1;

          i in ( dom F) & y in (F . i) by A1;

          hence thesis;

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    definition

      let I be set, Omega be non empty set, Sigma be SigmaField of Omega, F be ManySortedSigmaField of I, Sigma, J be Subset of I;

      :: KOLMOG01:def6

      func sigUn (F,J) -> SigmaField of Omega equals ( sigma ( Union (F | J)));

      coherence ;

    end

    definition

      let I be set, Omega be non empty set, Sigma be SigmaField of Omega, F be ManySortedSigmaField of I, Sigma;

      :: KOLMOG01:def7

      func futSigmaFields (F,I) -> Subset-Family of ( bool Omega) means

      : Def7: for S be Subset-Family of Omega holds S in it iff ex E be finite Subset of I st S = ( sigUn (F,(I \ E)));

      existence

      proof

        defpred P[ set] means ex E be finite Subset of I st $1 = ( sigUn (F,(I \ E)));

        consider X such that

         A1: for x holds x in X iff x in ( bool ( bool Omega)) & P[x] from XFAMILY:sch 1;

        

         A2: X is non empty

        proof

          set Ie = (I \ ( {} I));

          ( sigUn (F,Ie)) in X by A1;

          hence thesis;

        end;

        for x be object holds x in X implies x in ( bool ( bool Omega)) by A1;

        then

        reconsider X as non empty Subset-Family of ( bool Omega) by A2, TARSKI:def 3;

        take X;

        let S be Subset-Family of Omega;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let X1,X2 be Subset-Family of ( bool Omega);

        assume

         A3: for S be Subset-Family of Omega holds S in X1 iff ex E be finite Subset of I st S = ( sigUn (F,(I \ E)));

        assume

         A4: for S be Subset-Family of Omega holds S in X2 iff ex E be finite Subset of I st S = ( sigUn (F,(I \ E)));

        now

          let S be Subset-Family of Omega;

          S in X1 iff ex E be finite Subset of I st S = ( sigUn (F,(I \ E))) by A3;

          hence S in X1 iff S in X2 by A4;

        end;

        hence thesis by SUBSET_1: 3;

      end;

    end

    registration

      let I be set, Omega be non empty set, Sigma be SigmaField of Omega, F be ManySortedSigmaField of I, Sigma;

      cluster ( futSigmaFields (F,I)) -> non empty;

      coherence

      proof

        set Ie = (I \ ( {} I));

        ( sigUn (F,Ie)) in ( futSigmaFields (F,I)) by Def7;

        hence thesis;

      end;

    end

    definition

      let I be set, Omega be non empty set, Sigma be SigmaField of Omega, F be ManySortedSigmaField of I, Sigma;

      :: KOLMOG01:def8

      func tailSigmaField (F,I) -> Subset-Family of Omega equals ( meet ( futSigmaFields (F,I)));

      coherence ;

    end

    registration

      let I be set, Omega be non empty set, Sigma be SigmaField of Omega, F be ManySortedSigmaField of I, Sigma;

      cluster ( tailSigmaField (F,I)) -> non empty;

      coherence

      proof

        for X holds X in ( futSigmaFields (F,I)) implies {} in X

        proof

          let X;

          assume X in ( futSigmaFields (F,I));

          then ex E be finite Subset of I st X = ( sigUn (F,(I \ E))) by Def7;

          hence thesis by PROB_1: 4;

        end;

        hence thesis by SETFAM_1:def 1;

      end;

    end

    definition

      let Omega be non empty set, Sigma be SigmaField of Omega, I be non empty set, J be non empty Subset of I, F be ManySortedSigmaField of I, Sigma;

      :: KOLMOG01:def9

      func MeetSections (J,F) -> Subset-Family of Omega means

      : Def9: for x be Subset of Omega holds x in it iff ex E be non empty finite Subset of I, f be SigmaSection of E, F st E c= J & x = ( meet ( rng f));

      existence

      proof

        defpred P[ set] means ex E be non empty finite Subset of I, f be SigmaSection of E, F st E c= J & $1 = ( meet ( rng f));

        consider X such that

         A1: for x holds x in X iff x in ( bool Omega) & P[x] from XFAMILY:sch 1;

        for x be object holds x in X implies x in ( bool Omega) by A1;

        then

        reconsider X as Subset-Family of Omega by TARSKI:def 3;

        take X;

        let x be Subset of Omega;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let X1,X2 be Subset-Family of Omega;

        assume

         A2: for x be Subset of Omega holds x in X1 iff ex E be non empty finite Subset of I, f be SigmaSection of E, F st E c= J & x = ( meet ( rng f));

        assume

         A3: for x be Subset of Omega holds x in X2 iff ex E be non empty finite Subset of I, f be SigmaSection of E, F st E c= J & x = ( meet ( rng f));

        now

          let x be Subset of Omega;

          x in X1 iff ex E be non empty finite Subset of I, f be SigmaSection of E, F st E c= J & x = ( meet ( rng f)) by A2;

          hence x in X1 iff x in X2 by A3;

        end;

        hence thesis by SUBSET_1: 3;

      end;

    end

    theorem :: KOLMOG01:11

    

     Th11: for F be ManySortedSigmaField of I, Sigma, J be non empty Subset of I holds ( sigma ( MeetSections (J,F))) = ( sigUn (F,J))

    proof

      let F be ManySortedSigmaField of I, Sigma, J be non empty Subset of I;

      

       A1: ( Union (F | J)) c= ( MeetSections (J,F))

      proof

        let x be object;

        assume x in ( Union (F | J));

        then

        consider y such that

         A2: x in y and

         A3: y in ( rng (F | J)) by TARSKI:def 4;

        consider i be object such that

         A4: i in ( dom (F | J)) and

         A5: y = ((F | J) . i) by A3, FUNCT_1:def 3;

        reconsider i as set by TARSKI: 1;

        y = ((F | J) . i) by A5;

        then

        reconsider x as Subset of Omega by A2;

        defpred P[ object, object] means $2 = x & $2 in (F . $1);

        

         A6: {i} c= J by A4, ZFMISC_1: 31;

        then

        reconsider E = {i} as finite Subset of I by XBOOLE_1: 1;

        

         A7: for j be object st j in E holds ex y be object st y in Sigma & P[j, y]

        proof

          let j be object;

          assume

           A8: j in E;

          i in I by A4, TARSKI:def 3;

          then

           A9: (F . i) in ( bool Sigma) by FUNCT_2: 5;

          take y = x;

          y in (F . i) by A2, A4, A5, FUNCT_1: 49;

          hence thesis by A8, A9, TARSKI:def 1;

        end;

        consider g be Function of E, Sigma such that

         A10: for j be object st j in E holds P[j, (g . j)] from FUNCT_2:sch 1( A7);

        for i st i in E holds (g . i) in (F . i) by A10;

        then

        reconsider g as SigmaSection of E, F by Def4;

        ( dom g) = E by FUNCT_2:def 1;

        then

         A11: ( rng g) = {(g . i)} by FUNCT_1: 4;

        i in E by TARSKI:def 1;

        

        then x = (g . i) by A10

        .= ( meet ( rng g)) by A11, SETFAM_1: 10;

        hence thesis by A6, Def9;

      end;

      ( MeetSections (J,F)) c= ( sigma ( Union (F | J)))

      proof

        let x be object;

        assume x in ( MeetSections (J,F));

        then

        consider E be non empty finite Subset of I, f be SigmaSection of E, F such that

         A12: E c= J and

         A13: x = ( meet ( rng f)) by Def9;

        reconsider Ee = E as Element of ( Fin E) by FINSUB_1:def 5;

        for B be Element of ( Fin E) holds ( meet ( rng (f | B))) in ( sigma ( Union (F | J)))

        proof

          defpred P[ set] means ( meet ( rng (f | $1))) in ( sigma ( Union (F | J)));

          let B be Element of ( Fin E);

          

           A14: for B9 be Element of ( Fin E), b be Element of E holds P[B9] & not b in B9 implies P[(B9 \/ {b})]

          proof

            let B9 be Element of ( Fin E), b be Element of E;

            assume that

             A15: ( meet ( rng (f | B9))) in ( sigma ( Union (F | J))) and not b in B9;

            reconsider rfb = ( rng (f | {b})) as set;

            reconsider rfB9 = ( rng (f | B9)) as set;

            reconsider rfB9b = ( rng (f | (B9 \/ {b}))) as set;

            ( rng (f | (B9 \/ {b}))) = ( rng ((f | B9) \/ (f | {b}))) by RELAT_1: 78;

            then

             A16: ( rng (f | (B9 \/ {b}))) = (( rng (f | B9)) \/ ( rng (f | {b}))) by RELAT_1: 12;

            ( dom (F | J)) = J by FUNCT_2:def 1;

            then

             A17: b in ( dom (F | J)) by A12;

            then ((F | J) . b) in ( rng (F | J)) by FUNCT_1:def 3;

            then (F . b) in ( rng (F | J)) by A17, FUNCT_1: 47;

            then

             A18: (F . b) c= ( Union (F | J)) by ZFMISC_1: 74;

            ( Union (F | J)) c= ( sigma ( Union (F | J))) by PROB_1:def 9;

            then

             A19: (F . b) c= ( sigma ( Union (F | J))) by A18;

            b is Element of ( dom f) by FUNCT_2:def 1;

            

            then

             A20: {b} = (( dom f) /\ {b}) by ZFMISC_1: 46

            .= ( dom (f | {b})) by RELAT_1: 61;

            then

             A21: b in ( dom (f | {b})) by TARSKI:def 1;

            ( rng (f | {b})) = {((f | {b}) . b)} by A20, FUNCT_1: 4

            .= {(f . b)} by A21, FUNCT_1: 47;

            then ( meet ( rng (f | {b}))) = (f . b) by SETFAM_1: 10;

            then

             A22: ( meet ( rng (f | {b}))) in (F . b) by Def4;

            per cases ;

              suppose ( rng (f | B9)) = {} ;

              hence thesis by A22, A19, A16;

            end;

              suppose

               A23: not ( rng (f | B9)) = {} ;

              ( dom f) = E & b in {b} by FUNCT_2:def 1, TARSKI:def 1;

              then rfb <> {} by FUNCT_1: 50;

              then ( meet rfB9b) = (( meet rfB9) /\ ( meet rfb)) by A16, A23, SETFAM_1: 9;

              then ( meet ( rng (f | (B9 \/ {b})))) is Event of ( sigma ( Union (F | J))) by A15, A22, A19, PROB_1: 19;

              hence thesis;

            end;

          end;

          ( meet ( rng (f | {} ))) = {} by SETFAM_1:def 1;

          then

           A24: P[( {}. E)] by PROB_1: 4;

          for B1 be Element of ( Fin E) holds P[B1] from SETWISEO:sch 2( A24, A14);

          hence thesis;

        end;

        then ( meet ( rng (f | Ee))) in ( sigma ( Union (F | J)));

        hence thesis by A13;

      end;

      hence ( sigma ( MeetSections (J,F))) c= ( sigUn (F,J)) by PROB_1:def 9;

      ( MeetSections (J,F)) c= ( sigma ( MeetSections (J,F))) by PROB_1:def 9;

      then ( Union (F | J)) c= ( sigma ( MeetSections (J,F))) by A1;

      hence thesis by PROB_1:def 9;

    end;

    theorem :: KOLMOG01:12

    

     Th12: for F be ManySortedSigmaField of I, Sigma, J,K be non empty Subset of I st F is_independent_wrt P & J misses K holds for a,c be Subset of Omega st a in ( MeetSections (J,F)) & c in ( MeetSections (K,F)) holds (P . (a /\ c)) = ((P . a) * (P . c))

    proof

      let F be ManySortedSigmaField of I, Sigma, J,K be non empty Subset of I;

      assume

       A1: F is_independent_wrt P;

      reconsider Si = Sigma as set;

      assume

       A2: J misses K;

      let a,c be Subset of Omega;

      assume that

       A3: a in ( MeetSections (J,F)) and

       A4: c in ( MeetSections (K,F));

      consider E1 be non empty finite Subset of I, f1 be SigmaSection of E1, F such that

       A5: E1 c= J and

       A6: a = ( meet ( rng f1)) by A3, Def9;

      

       A7: f1 is_independent_wrt P by A1;

      consider E2 be non empty finite Subset of I, f2 be SigmaSection of E2, F such that

       A8: E2 c= K and

       A9: c = ( meet ( rng f2)) by A4, Def9;

      

       A10: f2 is_independent_wrt P by A1;

      reconsider rngf1 = ( rng f1), rngf2 = ( rng f2) as set;

      reconsider f1 as Function of E1, rngf1 by FUNCT_2: 6;

      reconsider f2 as Function of E2, rngf2 by FUNCT_2: 6;

      consider m be Nat such that

       A11: (E2,( Seg m)) are_equipotent by FINSEQ_1: 56;

      consider e2 be Function such that

       A12: e2 is one-to-one and

       A13: ( dom e2) = ( Seg m) and

       A14: ( rng e2) = E2 by A11, WELLORD2:def 4;

      

       A15: e2 <> {} by A14;

      reconsider e2 as Function of ( Seg m), E2 by A13, A14, FUNCT_2: 1;

      

       A16: e2 is FinSequence by A13, FINSEQ_1:def 2;

      

       A17: ( rng (f2 * e2)) = ( rng f2) by A14, FUNCT_2: 14;

      reconsider e2 as one-to-one FinSequence of E2 by A12, A14, A16, FINSEQ_1:def 4;

      reconsider f2 as Function of E2, Si;

      deffunc B( object) = (f2 . $1);

      reconsider fe2 = (f2 * e2) as FinSequence of Si;

      ( rng e2) = ( dom f2) by A14, FUNCT_2:def 1;

      then

       A18: ( len fe2) = ( len e2) by FINSEQ_2: 29;

      E2 c= (E1 \/ E2) by XBOOLE_1: 7;

      then

       A19: ( rng e2) c= (E1 \/ E2);

      defpred C[ object] means $1 in E1;

      consider n be Nat such that

       A20: (E1,( Seg n)) are_equipotent by FINSEQ_1: 56;

      consider e1 be Function such that

       A21: e1 is one-to-one and

       A22: ( dom e1) = ( Seg n) and

       A23: ( rng e1) = E1 by A20, WELLORD2:def 4;

      

       A24: e1 <> {} by A23;

      reconsider e1 as Function of ( Seg n), E1 by A22, A23, FUNCT_2: 1;

      

       A25: e1 is FinSequence by A22, FINSEQ_1:def 2;

      

       A26: ( rng (f1 * e1)) = ( rng f1) by A23, FUNCT_2: 14;

      reconsider e1 as one-to-one FinSequence of E1 by A21, A23, A25, FINSEQ_1:def 4;

      reconsider f1 as Function of E1, Si;

      deffunc D( object) = (f1 . $1);

      reconsider fe1 = (f1 * e1) as FinSequence of Si;

      ( rng e1) = ( dom f1) by A23, FUNCT_2:def 1;

      then

       A27: ( len fe1) = ( len e1) by FINSEQ_2: 29;

      consider h be Function such that

       A28: ( dom h) = (E1 \/ E2) & for i be object st i in (E1 \/ E2) holds ( C[i] implies (h . i) = D(i)) & ( not C[i] implies (h . i) = B(i)) from PARTFUN1:sch 1;

      for x be object holds x in ( dom (e1 ^ e2)) implies x in ( dom (h * (e1 ^ e2)))

      proof

        let x be object;

        assume

         A29: x in ( dom (e1 ^ e2));

        ( rng (e1 ^ e2)) = ( dom h) by A23, A14, A28, FINSEQ_1: 31;

        then ((e1 ^ e2) . x) in ( dom h) by A29, FUNCT_1: 3;

        hence thesis by A29, FUNCT_1: 11;

      end;

      then

       A30: ( dom (e1 ^ e2)) c= ( dom (h * (e1 ^ e2)));

      for x be object holds x in ( dom (h * (e1 ^ e2))) implies x in ( dom (e1 ^ e2)) by FUNCT_1: 11;

      then

       A31: ( dom (h * (e1 ^ e2))) c= ( dom (e1 ^ e2));

      

       A32: ( dom (fe1 ^ fe2)) = ( Seg (( len fe1) + ( len fe2))) by FINSEQ_1:def 7

      .= ( dom (e1 ^ e2)) by A27, A18, FINSEQ_1:def 7

      .= ( dom (h * (e1 ^ e2))) by A31, A30;

      for x be object st x in ( dom (fe1 ^ fe2)) holds ((fe1 ^ fe2) . x) = ((h * (e1 ^ e2)) . x)

      proof

        let x be object;

        assume

         A33: x in ( dom (fe1 ^ fe2));

        then

        reconsider x as Element of NAT ;

        per cases ;

          suppose

           A34: x in ( dom fe1);

          then

           A35: ((fe1 ^ fe2) . x) = (fe1 . x) by FINSEQ_1:def 7;

          

           A36: E1 c= (E1 \/ E2) by XBOOLE_1: 7;

          

           A37: x in ( dom e1) by A34, FUNCT_1: 11;

          then (e1 . x) in E1 by A23, FUNCT_1: 3;

          then (h . (e1 . x)) = (f1 . (e1 . x)) by A28, A36;

          then

           A38: ((fe1 ^ fe2) . x) = (h . (e1 . x)) by A34, A35, FUNCT_1: 12;

          ((e1 ^ e2) . x) = (e1 . x) by A37, FINSEQ_1:def 7;

          hence thesis by A32, A33, A38, FUNCT_1: 12;

        end;

          suppose not x in ( dom fe1);

          then

          consider n be Nat such that

           A39: n in ( dom fe2) and

           A40: x = (( len fe1) + n) by A33, FINSEQ_1: 25;

          

           A41: n in ( dom e2) by A39, FUNCT_1: 11;

          then

           A42: (e2 . n) in E2 by A14, FUNCT_1: 3;

          (E1 /\ E2) c= (J /\ K) by A5, A8, XBOOLE_1: 27;

          then (E1 /\ E2) c= {} by A2;

          then (E1 /\ E2) = {} ;

          then E2 = ((E2 \ E1) \/ {} ) by XBOOLE_1: 51;

          then

           A43: not (e2 . n) in E1 by A42, XBOOLE_0:def 5;

          

           A44: E2 c= (E1 \/ E2) by XBOOLE_1: 7;

          ((fe1 ^ fe2) . x) = (fe2 . n) by A39, A40, FINSEQ_1:def 7

          .= (f2 . (e2 . n)) by A39, FUNCT_1: 12

          .= (h . (e2 . n)) by A28, A42, A43, A44

          .= (h . ((e1 ^ e2) . x)) by A27, A40, A41, FINSEQ_1:def 7;

          hence thesis by A32, A33, FUNCT_1: 12;

        end;

      end;

      then

       A45: (fe1 ^ fe2) = (h * (e1 ^ e2)) by A32, FUNCT_1:def 11;

      for i be object st i in (E1 \/ E2) holds (h . i) in Sigma

      proof

        let i be object;

        assume

         A46: i in (E1 \/ E2);

        per cases ;

          suppose

           A47: i in E1;

          then (h . i) = (f1 . i) by A28, A46;

          hence thesis by A47, FUNCT_2: 5;

        end;

          suppose not i in E1;

          then (h . i) = (f2 . i) & i in E2 by A28, A46, XBOOLE_0:def 3;

          hence thesis by FUNCT_2: 5;

        end;

      end;

      then

      reconsider h as Function of (E1 \/ E2), Sigma by A28, FUNCT_2: 3;

      for i st i in (E1 \/ E2) holds (h . i) in (F . i)

      proof

        let i;

        assume

         A48: i in (E1 \/ E2);

        per cases ;

          suppose

           A49: i in E1;

          then (f1 . i) in (F . i) by Def4;

          hence thesis by A28, A48, A49;

        end;

          suppose

           A50: not i in E1;

          then i in E2 by A48, XBOOLE_0:def 3;

          then (f2 . i) in (F . i) by Def4;

          hence thesis by A28, A48, A50;

        end;

      end;

      then

      reconsider h as SigmaSection of (E1 \/ E2), F by Def4;

      

       A51: h is_independent_wrt P by A1;

      E1 c= (E1 \/ E2) by XBOOLE_1: 7;

      then

       A52: ( rng e1) c= (E1 \/ E2);

      reconsider Pfe1 = ((P * f1) * e1), Pfe2 = ((P * f2) * e2) as FinSequence of REAL by FINSEQ_2: 32;

      reconsider e2 as FinSequence of (E1 \/ E2) by A19, FINSEQ_1:def 4;

      reconsider e1 as FinSequence of (E1 \/ E2) by A52, FINSEQ_1:def 4;

      (E1 /\ E2) c= (J /\ K) by A5, A8, XBOOLE_1: 27;

      then (E1 /\ E2) c= {} by A2;

      then (E1 /\ E2) = {} ;

      then ( rng e1) misses ( rng e2) by A23, A14;

      then

      reconsider e12 = (e1 ^ e2) as one-to-one FinSequence of (E1 \/ E2) by FINSEQ_3: 91;

      reconsider e1 as one-to-one FinSequence of E1;

      reconsider fe1 as FinSequence of Si;

      reconsider e2 as FinSequence of E2;

      reconsider fe2 as FinSequence of Si;

      reconsider f1 as Function of E1, Sigma;

      reconsider f2 as Function of E2, Sigma;

      reconsider P as Function of Si, REAL ;

      

       A53: ((P * h) * e12) = (P * (h * (e1 ^ e2))) by RELAT_1: 36

      .= ((P * fe1) ^ (P * fe2)) by A45, FINSEQOP: 9;

      

       A54: (P * fe1) = Pfe1 & (P * fe2) = Pfe2 by RELAT_1: 36;

      reconsider P as Function of Sigma, REAL ;

      

       A55: ( Product ((P * f1) * e1)) = (P . ( meet ( rng (f1 * e1)))) by A24, A7;

      (P . (a /\ c)) = (P . ( meet (( rng f1) \/ ( rng f2)))) by A6, A9, SETFAM_1: 9

      .= (P . ( meet ( rng (fe1 ^ fe2)))) by A26, A17, FINSEQ_1: 31

      .= ( Product (Pfe1 ^ Pfe2)) by A24, A45, A51, A53, A54

      .= (( Product Pfe1) * ( Product Pfe2)) by RVSUM_1: 97

      .= ((P . a) * (P . c)) by A6, A9, A15, A10, A26, A17, A55;

      hence thesis;

    end;

    theorem :: KOLMOG01:13

    

     Th13: for F be ManySortedSigmaField of I, Sigma, J be non empty Subset of I holds ( MeetSections (J,F)) is non empty Subset of Sigma

    proof

      let F be ManySortedSigmaField of I, Sigma, J be non empty Subset of I;

      

       A1: ( MeetSections (J,F)) c= Sigma

      proof

        let X be object;

        assume X in ( MeetSections (J,F));

        then

        consider E be non empty finite Subset of I, f be SigmaSection of E, F such that E c= J and

         A2: X = ( meet ( rng f)) by Def9;

        reconsider Ee = E as Element of ( Fin E) by FINSUB_1:def 5;

        for B be Element of ( Fin E) holds ( meet ( rng (f | B))) in Sigma

        proof

          defpred P[ set] means ( meet ( rng (f | $1))) in Sigma;

          let B be Element of ( Fin E);

          

           A3: for B9 be Element of ( Fin E), b be Element of E holds P[B9] & not b in B9 implies P[(B9 \/ {b})]

          proof

            let B9 be Element of ( Fin E), b be Element of E;

            assume that

             A4: ( meet ( rng (f | B9))) in Sigma and not b in B9;

            

             A5: ( rng (f | (B9 \/ {b}))) = ( rng ((f | B9) \/ (f | {b}))) by RELAT_1: 78

            .= (( rng (f | B9)) \/ ( rng (f | {b}))) by RELAT_1: 12;

            ( dom f) = E & b in {b} by FUNCT_2:def 1, TARSKI:def 1;

            then

             A6: (f . b) in ( rng (f | {b})) by FUNCT_1: 50;

            

             A7: b is Element of ( dom f) by FUNCT_2:def 1;

            then (( dom f) /\ {b}) = {b} by ZFMISC_1: 46;

            then ( dom (f | {b})) = {b} by RELAT_1: 61;

            then

             A8: ( rng (f | {b})) = {((f | {b}) . b)} by FUNCT_1: 4;

            b in {b} by TARSKI:def 1;

            then b in ( dom (f | {b})) by A7, RELAT_1: 57;

            then ( rng (f | {b})) = {(f . b)} by A8, FUNCT_1: 47;

            then

             A9: ( meet ( rng (f | {b}))) is Event of Sigma by SETFAM_1: 10;

            per cases ;

              suppose ( rng (f | B9)) = {} ;

              hence thesis by A9, A5;

            end;

              suppose not ( rng (f | B9)) = {} ;

              then ( meet ( rng (f | (B9 \/ {b})))) = (( meet ( rng (f | B9))) /\ ( meet ( rng (f | {b})))) by A5, A6, SETFAM_1: 9;

              then ( meet ( rng (f | (B9 \/ {b})))) is Event of Sigma by A4, A9, PROB_1: 19;

              hence thesis;

            end;

          end;

          ( meet ( rng (f | {} ))) = {} by SETFAM_1:def 1;

          then

           A10: P[( {}. E)] by PROB_1: 4;

          for B1 be Element of ( Fin E) holds P[B1] from SETWISEO:sch 2( A10, A3);

          hence thesis;

        end;

        then ( meet ( rng (f | Ee))) in Sigma;

        hence thesis by A2;

      end;

      ( MeetSections (J,F)) is non empty set

      proof

        set E = the non empty finite Subset of J;

        consider f be Function such that

         A11: ( dom f) = E and

         A12: ( rng f) = { {} } by FUNCT_1: 5;

        reconsider E as non empty finite Subset of I by XBOOLE_1: 1;

        

         A13: ( meet ( rng f)) = {} by A12, SETFAM_1: 10;

        ( rng f) c= Sigma

        proof

          let y be object;

          assume y in ( rng f);

          then y = {} by A12, TARSKI:def 1;

          hence thesis by PROB_1: 4;

        end;

        then

        reconsider f as Function of E, Sigma by A11, FUNCT_2: 2;

        for i st i in E holds (f . i) in (F . i)

        proof

          let i;

          assume

           A14: i in E;

          then

          reconsider Fi = (F . i) as SigmaField of Omega by Def2;

          (f . i) in ( rng f) by A11, A14, FUNCT_1:def 3;

          then (f . i) = {} by A12, TARSKI:def 1;

          then (f . i) in Fi by PROB_1: 4;

          hence thesis;

        end;

        then

        reconsider f as SigmaSection of E, F by Def4;

        reconsider mrf = ( meet ( rng f)) as Subset of Omega by A13, XBOOLE_1: 2;

        mrf in ( MeetSections (J,F)) by Def9;

        hence thesis;

      end;

      hence thesis by A1;

    end;

    registration

      let I, Omega, Sigma;

      let F be ManySortedSigmaField of I, Sigma, J be non empty Subset of I;

      cluster ( MeetSections (J,F)) -> intersection_stable;

      coherence

      proof

        for x, X st x in ( MeetSections (J,F)) & X in ( MeetSections (J,F)) holds (x /\ X) in ( MeetSections (J,F))

        proof

          let x, X;

          assume that

           A1: x in ( MeetSections (J,F)) and

           A2: X in ( MeetSections (J,F));

          consider E be non empty finite Subset of I, f be SigmaSection of E, F such that

           A3: E c= J and

           A4: x = ( meet ( rng f)) by A1, Def9;

          defpred C[ object] means $1 in E;

          deffunc D( object) = (f . $1);

          consider E9 be non empty finite Subset of I, f9 be SigmaSection of E9, F such that

           A5: E9 c= J and

           A6: X = ( meet ( rng f9)) by A2, Def9;

          deffunc B( object) = (f9 . $1);

          defpred P[ object] means $1 in ((E \ E9) \/ (E9 \ E));

          deffunc G( object) = ((f . $1) /\ (f9 . $1));

          consider h be Function such that

           A7: ( dom h) = (E \/ E9) & for i be object st i in (E \/ E9) holds ( C[i] implies (h . i) = D(i)) & ( not C[i] implies (h . i) = B(i)) from PARTFUN1:sch 1;

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

          consider g be Function such that

           A8: ( dom g) = (E \/ E9) & for i be object st i in (E \/ E9) holds ( P[i] implies (g . i) = F(i)) & ( not P[i] implies (g . i) = G(i)) from PARTFUN1:sch 1;

          

           A9: for i st i in (E \/ E9) holds (g . i) in (F . i)

          proof

            let i;

            assume

             A10: i in (E \/ E9);

            per cases ;

              suppose

               A11: i in ((E \ E9) \/ (E9 \ E));

              (h . i) in (F . i)

              proof

                per cases ;

                  suppose

                   A12: i in E;

                  then (h . i) = (f . i) by A7, A10;

                  hence thesis by A12, Def4;

                end;

                  suppose not i in E;

                  then i in E9 & (h . i) = (f9 . i) by A7, A10, XBOOLE_0:def 3;

                  hence thesis by Def4;

                end;

              end;

              hence thesis by A8, A10, A11;

            end;

              suppose

               A13: not i in ((E \ E9) \/ (E9 \ E));

              reconsider Fi = (F . i) as SigmaField of Omega by A10, Def2;

               not i in (E \+\ E9) by A13;

              then i in E iff i in E9 by XBOOLE_0: 1;

              then (f . i) in (F . i) & (f9 . i) in (F . i) by A10, Def4, XBOOLE_0:def 3;

              then

               A14: ((f . i) /\ (f9 . i)) is Event of Fi by PROB_1: 19;

              (g . i) = ((f . i) /\ (f9 . i)) by A8, A10, A13;

              hence thesis by A14;

            end;

          end;

          ( rng g) c= Sigma

          proof

            let y be object;

            assume y in ( rng g);

            then

            consider i be object such that

             A15: i in ( dom g) & y = (g . i) by FUNCT_1:def 3;

            y in (F . i) & (F . i) in ( bool Sigma) by A8, A9, A15, FUNCT_2: 5;

            hence thesis;

          end;

          then g is Function of (E \/ E9), Sigma by A8, FUNCT_2: 2;

          then

          reconsider g as SigmaSection of (E \/ E9), F by A9, Def4;

          

           A16: (x /\ X) = ( meet ( rng g))

          proof

            

             A17: ( meet ( rng (g | (E /\ E9)))) = (( meet ( rng (f | (E /\ E9)))) /\ ( meet ( rng (f9 | (E /\ E9)))))

            proof

              per cases ;

                suppose

                 A18: (E /\ E9) = {} ;

                then

                 A19: ( meet ( rng (f | (E /\ E9)))) = ( meet ( rng {} )) & ( meet ( rng (f9 | (E /\ E9)))) = ( meet ( rng {} ));

                ( meet ( rng (g | (E /\ E9)))) = ( meet ( rng {} )) by A18

                .= {} by SETFAM_1:def 1;

                hence thesis by A19, SETFAM_1:def 1;

              end;

                suppose not (E /\ E9) = {} ;

                then

                reconsider EnE9 = (E /\ E9) as non empty set;

                reconsider EE9 = EnE9 as Element of ( Fin EnE9) by FINSUB_1:def 5;

                for B be Element of ( Fin EnE9) holds ( meet ( rng (g | B))) = (( meet ( rng (f | B))) /\ ( meet ( rng (f9 | B))))

                proof

                  defpred P[ set] means ( meet ( rng (g | $1))) = (( meet ( rng (f | $1))) /\ ( meet ( rng (f9 | $1))));

                  let B be Element of ( Fin EnE9);

                  

                   A20: for B9 be Element of ( Fin EnE9), b be Element of EnE9 holds P[B9] & not b in B9 implies P[(B9 \/ {b})]

                  proof

                    let B9 be Element of ( Fin EnE9), b be Element of EnE9;

                    assume that

                     A21: ( meet ( rng (g | B9))) = (( meet ( rng (f | B9))) /\ ( meet ( rng (f9 | B9)))) and not b in B9;

                    

                     A22: ( dom (f | {b})) = (( dom f) /\ {b}) by RELAT_1: 61;

                    ( dom f) = E by FUNCT_2:def 1;

                    then

                     A23: (E /\ E9) c= ( dom f) by XBOOLE_1: 17;

                    then b in ( dom f);

                    then

                     A24: ( rng (f | {b})) = {((f | {b}) . b)} by A22, FUNCT_1: 4, ZFMISC_1: 46;

                    b in ((E \ (E \/ E9)) \/ ((E /\ E) /\ E9)) by XBOOLE_0:def 3;

                    then b in (E \ (E \+\ E9)) by XBOOLE_1: 102;

                    then

                     A25: not b in (E \+\ E9) by XBOOLE_0:def 5;

                    

                     A26: b in {b} by TARSKI:def 1;

                    b in ( dom f) by A23;

                    then b in ( dom (f | {b})) by A26, RELAT_1: 57;

                    then

                     A27: ( rng (f | {b})) = {(f . b)} by A24, FUNCT_1: 47;

                    then

                     A28: ( meet ( rng (f | {b}))) = (f . b) by SETFAM_1: 10;

                    

                     A29: (E /\ E9) c= E by XBOOLE_1: 17;

                    

                     A30: ( dom (f9 | {b})) = (( dom f9) /\ {b}) by RELAT_1: 61;

                    ( dom f9) = E9 by FUNCT_2:def 1;

                    then

                     A31: (E /\ E9) c= ( dom f9) by XBOOLE_1: 17;

                    then b in ( dom f9);

                    then

                     A32: ( rng (f9 | {b})) = {((f9 | {b}) . b)} by A30, FUNCT_1: 4, ZFMISC_1: 46;

                    b in ( dom f9) by A31;

                    then b in ( dom (f9 | {b})) by A26, RELAT_1: 57;

                    then

                     A33: ( rng (f9 | {b})) = {(f9 . b)} by A32, FUNCT_1: 47;

                    then

                     A34: ( meet ( rng (f9 | {b}))) = (f9 . b) by SETFAM_1: 10;

                    

                     A35: for g be Function, B9,b be set holds ( meet ( rng (g | (B9 \/ {b})))) = ( meet (( rng (g | B9)) \/ ( rng (g | {b}))))

                    proof

                      let g be Function, B9,b be set;

                      ( rng (g | (B9 \/ {b}))) = ( rng ((g | B9) \/ (g | {b}))) by RELAT_1: 78;

                      hence thesis by RELAT_1: 12;

                    end;

                    E c= ( dom g) by A8, XBOOLE_1: 7;

                    then

                     A36: (E /\ E9) c= ( dom g) by A29;

                    then b is Element of ( dom g);

                    then (( dom g) /\ {b}) = {b} by ZFMISC_1: 46;

                    then ( dom (g | {b})) = {b} by RELAT_1: 61;

                    then

                     A37: ( rng (g | {b})) = {((g | {b}) . b)} by FUNCT_1: 4;

                    b in {b} & b in ( dom g) by A36, TARSKI:def 1;

                    then b in ( dom (g | {b})) by RELAT_1: 57;

                    then

                     A38: ( rng (g | {b})) = {(g . b)} by A37, FUNCT_1: 47;

                    then

                     A39: ( meet ( rng (g | {b}))) = (g . b) by SETFAM_1: 10;

                    E c= (E \/ E9) by XBOOLE_1: 7;

                    then

                     A40: (E /\ E9) c= (E \/ E9) by A29;

                    then b in (E \/ E9);

                    then

                     A41: (g . b) = ((f . b) /\ (f9 . b)) by A8, A25;

                    per cases ;

                      suppose B9 = {} ;

                      hence thesis by A28, A34, A41, A38, SETFAM_1: 10;

                    end;

                      suppose

                       A42: B9 <> {} ;

                      set z = the Element of B9;

                      B9 c= (E /\ E9) by FINSUB_1:def 5;

                      then

                       A43: B9 c= (E \/ E9) by A40;

                      z in B9 by A42;

                      then ( dom (g | B9)) <> {} by A8, A43;

                      then ( rng (g | B9)) <> {} by RELAT_1: 42;

                      then ( meet (( rng (g | B9)) \/ ( rng (g | {b})))) = (( meet ( rng (g | B9))) /\ ( meet ( rng (g | {b})))) by A37, SETFAM_1: 9;

                      

                      then

                       A44: ( meet ( rng (g | (B9 \/ {b})))) = ((( meet ( rng (f | B9))) /\ ( meet ( rng (f9 | B9)))) /\ (g . b)) by A21, A35, A39

                      .= (( meet ( rng (f | B9))) /\ (( meet ( rng (f9 | B9))) /\ ((f . b) /\ (f9 . b)))) by A41, XBOOLE_1: 16

                      .= (( meet ( rng (f | B9))) /\ ((f . b) /\ (( meet ( rng (f9 | B9))) /\ (f9 . b)))) by XBOOLE_1: 16

                      .= ((( meet ( rng (f | B9))) /\ (f . b)) /\ (( meet ( rng (f9 | B9))) /\ (f9 . b))) by XBOOLE_1: 16;

                      B9 c= (E /\ E9) & (E /\ E9) c= E9 by FINSUB_1:def 5, XBOOLE_1: 17;

                      then B9 c= E9;

                      then

                       A45: B9 c= ( dom f9) by FUNCT_2:def 1;

                      B9 c= (E /\ E9) & (E /\ E9) c= E by FINSUB_1:def 5, XBOOLE_1: 17;

                      then B9 c= E;

                      then

                       A46: B9 c= ( dom f) by FUNCT_2:def 1;

                      ( meet ( rng (f | (B9 \/ {b})))) = ( meet (( rng (f | B9)) \/ ( rng (f | {b})))) by A35

                      .= (( meet ( rng (f | B9))) /\ ( meet ( rng (f | {b})))) by A24, A42, A46, SETFAM_1: 9;

                      then

                       A47: (( meet ( rng (f | B9))) /\ (f . b)) = ( meet ( rng (f | (B9 \/ {b})))) by A27, SETFAM_1: 10;

                      ( meet ( rng (f9 | (B9 \/ {b})))) = ( meet (( rng (f9 | B9)) \/ ( rng (f9 | {b})))) by A35

                      .= (( meet ( rng (f9 | B9))) /\ ( meet ( rng (f9 | {b})))) by A32, A42, A45, SETFAM_1: 9;

                      hence thesis by A33, A44, A47, SETFAM_1: 10;

                    end;

                  end;

                  

                   A48: P[( {}. EnE9)];

                  for B1 be Element of ( Fin EnE9) holds P[B1] from SETWISEO:sch 2( A48, A20);

                  hence thesis;

                end;

                then ( meet ( rng (g | EE9))) = (( meet ( rng (f | EE9))) /\ ( meet ( rng (f9 | EE9))));

                hence thesis;

              end;

            end;

            

             A49: for E,E9 be set, g be Function st ( dom g) = (E \/ E9) holds ( rng g) = ((( rng (g | (E /\ E9))) \/ ( rng (g | (E \ E9)))) \/ ( rng (g | (E9 \ E))))

            proof

              let E,E9 be set, g be Function;

              ( rng (g | (E /\ E9))) c= ( rng g) & ( rng (g | (E \ E9))) c= ( rng g) by RELAT_1: 70;

              then

               A50: (( rng (g | (E /\ E9))) \/ ( rng (g | (E \ E9)))) c= ( rng g) by XBOOLE_1: 8;

              assume

               A51: ( dom g) = (E \/ E9);

              thus ( rng g) c= ((( rng (g | (E /\ E9))) \/ ( rng (g | (E \ E9)))) \/ ( rng (g | (E9 \ E))))

              proof

                let y be object;

                assume y in ( rng g);

                then

                consider i be object such that

                 A52: i in ( dom g) and

                 A53: y = (g . i) by FUNCT_1:def 3;

                per cases ;

                  suppose

                   A54: i in ((E \ E9) \/ (E9 \ E));

                  y in ((( rng (g | (E /\ E9))) \/ ( rng (g | (E \ E9)))) \/ ( rng (g | (E9 \ E))))

                  proof

                    per cases ;

                      suppose

                       A55: i in E;

                      

                       A56: (E /\ E9) c= E by XBOOLE_1: 17;

                      (E /\ ((E \ E9) \/ (E9 \ E))) = ((E /\ (E \ E9)) \/ (E /\ (E9 \ E))) by XBOOLE_1: 23

                      .= ((E \ E9) \/ (E /\ (E9 \ E))) by XBOOLE_1: 28

                      .= ((E \ E9) \/ ((E /\ E9) \ E)) by XBOOLE_1: 49

                      .= ((E \ E9) \/ {} ) by A56, XBOOLE_1: 37;

                      then i in (E \ E9) by A54, A55, XBOOLE_0:def 4;

                      then i in (( dom g) /\ (E \ E9)) by A52, XBOOLE_0:def 4;

                      then

                       A57: i in ( dom (g | (E \ E9))) by RELAT_1: 61;

                      then ((g | (E \ E9)) . i) = y by A53, FUNCT_1: 47;

                      then y in ( rng (g | (E \ E9))) by A57, FUNCT_1:def 3;

                      then y in (( rng (g | (E /\ E9))) \/ ( rng (g | (E \ E9)))) by XBOOLE_0:def 3;

                      hence thesis by XBOOLE_0:def 3;

                    end;

                      suppose

                       A58: not i in E;

                      (((E \ E9) \/ (E9 \ E)) \ E) = (((E \ E9) \ E) \/ ((E9 \ E) \ E)) by XBOOLE_1: 42

                      .= ( {} \/ ((E9 \ E) \ E)) by XBOOLE_1: 37

                      .= (E9 \ (E \/ E)) by XBOOLE_1: 41;

                      then i in (E9 \ (E \/ E)) by A54, A58, XBOOLE_0:def 5;

                      then i in (( dom g) /\ (E9 \ E)) by A52, XBOOLE_0:def 4;

                      then

                       A59: i in ( dom (g | (E9 \ E))) by RELAT_1: 61;

                      then ((g | (E9 \ E)) . i) = y by A53, FUNCT_1: 47;

                      then y in ( rng (g | (E9 \ E))) by A59, FUNCT_1:def 3;

                      then y in (( rng (g | (E \ E9))) \/ ( rng (g | (E9 \ E)))) by XBOOLE_0:def 3;

                      then y in (( rng (g | (E /\ E9))) \/ (( rng (g | (E \ E9))) \/ ( rng (g | (E9 \ E))))) by XBOOLE_0:def 3;

                      hence thesis by XBOOLE_1: 4;

                    end;

                  end;

                  hence thesis;

                end;

                  suppose

                   A60: not i in ((E \ E9) \/ (E9 \ E));

                  

                   A61: ((E \/ E9) \ (E \+\ E9)) = (((E \/ E9) \ (E \/ E9)) \/ (((E \/ E9) /\ E) /\ E9)) by XBOOLE_1: 102

                  .= ( {} \/ (((E \/ E9) /\ E) /\ E9)) by XBOOLE_1: 37

                  .= ((E \/ E9) /\ (E /\ E9)) by XBOOLE_1: 16;

                  i in ((E \/ E9) \ (E \+\ E9)) by A51, A52, A60, XBOOLE_0:def 5;

                  then

                   A62: i in ( dom (g | (E /\ E9))) by A51, A61, RELAT_1: 61;

                  then ((g | (E /\ E9)) . i) = y by A53, FUNCT_1: 47;

                  then y in ( rng (g | (E /\ E9))) by A62, FUNCT_1:def 3;

                  then y in (( rng (g | (E /\ E9))) \/ ( rng (g | (E \ E9)))) by XBOOLE_0:def 3;

                  hence thesis by XBOOLE_0:def 3;

                end;

              end;

              ( rng (g | (E9 \ E))) c= ( rng g) by RELAT_1: 70;

              hence thesis by A50, XBOOLE_1: 8;

            end;

            then

             A63: ( rng g) = ((( rng (g | (E /\ E9))) \/ ( rng (g | (E \ E9)))) \/ ( rng (g | (E9 \ E)))) by A8;

            

             A64: ( dom (g | (E9 \ E))) = (( dom g) /\ (E9 \ E)) by RELAT_1: 61

            .= ((E \/ E9) /\ (E9 \ E)) by FUNCT_2:def 1

            .= (((E \/ E9) /\ E9) \ E) by XBOOLE_1: 49

            .= (E9 \ E) by XBOOLE_1: 21;

            

             A65: for i be object st i in ( dom (g | (E9 \ E))) holds ((g | (E9 \ E)) . i) = (f9 . i)

            proof

              let i be object;

              assume

               A66: i in ( dom (g | (E9 \ E)));

              then

               A67: i in ((E \ E9) \/ (E9 \ E)) by A64, XBOOLE_0:def 3;

               not i in E by A64, A66, XBOOLE_0:def 5;

              

              then (f9 . i) = (h . i) by A7, A66

              .= (g . i) by A8, A66, A67;

              hence thesis by A66, FUNCT_1: 47;

            end;

            ( dom (g | (E9 \ E))) = ((E9 /\ E9) \ E) by A64

            .= (E9 /\ (E9 \ E)) by XBOOLE_1: 49

            .= (( dom f9) /\ (E9 \ E)) by FUNCT_2:def 1;

            then

             A68: ( meet ( rng (g | (E9 \ E)))) = ( meet ( rng (f9 | (E9 \ E)))) by A65, FUNCT_1: 46;

            

             A69: ( dom (g | (E \ E9))) = (( dom g) /\ (E \ E9)) by RELAT_1: 61

            .= ((E \/ E9) /\ (E \ E9)) by FUNCT_2:def 1

            .= (((E \/ E9) /\ E) \ E9) by XBOOLE_1: 49

            .= (E \ E9) by XBOOLE_1: 21;

            

             A70: for i be object st i in ( dom (g | (E \ E9))) holds ((g | (E \ E9)) . i) = (f . i)

            proof

              let i be object;

              

               A71: (E \ E9) c= E by XBOOLE_1: 36;

              assume

               A72: i in ( dom (g | (E \ E9)));

              then i in ((E \ E9) \/ (E9 \ E)) by A69, XBOOLE_0:def 3;

              

              then (g . i) = (h . i) by A8, A72

              .= (f . i) by A7, A69, A72, A71;

              hence thesis by A72, FUNCT_1: 47;

            end;

            ( dom (g | (E \ E9))) = ((E /\ E) \ E9) by A69

            .= (E /\ (E \ E9)) by XBOOLE_1: 49

            .= (( dom f) /\ (E \ E9)) by FUNCT_2:def 1;

            then

             A73: ( meet ( rng (g | (E \ E9)))) = ( meet ( rng (f | (E \ E9)))) by A70, FUNCT_1: 46;

            per cases ;

              suppose

               A74: (E /\ E9) = {} ;

              

               A75: (E \ E9) c= E by XBOOLE_1: 36;

              

               A76: E9 c= ( dom g) & E c= ( dom g) by A8, XBOOLE_1: 7;

              

               A77: (E9 \ E) c= E9 by XBOOLE_1: 36;

              

               A78: E misses E9 by A74;

              E c= (E \ E9) by A78, XBOOLE_1: 86;

              then

               A79: E = (E \ E9) by A75;

              E9 c= (E9 \ E) by A78, XBOOLE_1: 86;

              then

               A80: E9 = (E9 \ E) by A77;

              ( rng (g | (E /\ E9))) = {} by A74;

              hence thesis by A4, A6, A73, A68, A63, A80, A79, A76, SETFAM_1: 9;

            end;

              suppose

               A81: not (E /\ E9) = {} ;

              ( meet ( rng g)) = (( meet ( rng f)) /\ ( meet ( rng f9)))

              proof

                per cases ;

                  suppose

                   A82: (E \ E9) = {} ;

                  then

                   A83: ( rng (g | (E \ E9))) = {} ;

                  

                   A84: E c= E9 by A82, XBOOLE_1: 37;

                  

                   A85: (E /\ E9) c= ( dom g) by A8, XBOOLE_1: 29;

                  ( meet ( rng g)) = (( meet ( rng f)) /\ ( meet ( rng f9)))

                  proof

                    per cases ;

                      suppose (E9 \ E) = {} ;

                      then E9 c= E by XBOOLE_1: 37;

                      then

                       A86: E = E9 by A84;

                      thus thesis by A17, A86;

                    end;

                      suppose

                       A87: (E9 \ E) <> {} ;

                      (E9 \ E) c= E9 & E9 c= (E9 \/ E) by XBOOLE_1: 7, XBOOLE_1: 36;

                      then (E9 \ E) c= ( dom g) by A8;

                      then ( meet ( rng g)) = (( meet ( rng (g | (E /\ E9)))) /\ ( meet ( rng (g | (E9 \ E))))) by A63, A81, A83, A85, A87, SETFAM_1: 9;

                      then

                       A88: ( meet ( rng g)) = ((( meet ( rng f)) /\ ( meet ( rng (f9 | (E /\ E9))))) /\ ( meet ( rng (f9 | (E9 \ E))))) by A17, A68, A84, RELSET_1: 19, XBOOLE_1: 19;

                      

                       A89: ( rng (f9 | (E \ E9))) = {} by A82;

                      (E9 \ E) c= E9 by XBOOLE_1: 36;

                      then

                       A90: (E9 \ E) c= ( dom f9) by FUNCT_2:def 1;

                      (E /\ E9) c= E9 by XBOOLE_1: 17;

                      then

                       A91: (E /\ E9) c= ( dom f9) by FUNCT_2:def 1;

                      (E9 \/ E) = E9 & ( dom f9) = E9 by A84, FUNCT_2:def 1, XBOOLE_1: 12;

                      

                      then ( rng f9) = ((( rng (f9 | (E /\ E9))) \/ ( rng (f9 | (E \ E9)))) \/ ( rng (f9 | (E9 \ E)))) by A49

                      .= (( rng (f9 | (E /\ E9))) \/ ( rng (f9 | (E9 \ E)))) by A89;

                      then ( meet ( rng f9)) = (( meet ( rng (f9 | (E /\ E9)))) /\ ( meet ( rng (f9 | (E9 \ E))))) by A81, A87, A91, A90, SETFAM_1: 9;

                      hence thesis by A88, XBOOLE_1: 16;

                    end;

                  end;

                  hence thesis;

                end;

                  suppose

                   A92: not (E \ E9) = {} ;

                  ( meet ( rng g)) = (( meet ( rng f)) /\ ( meet ( rng f9)))

                  proof

                    (E \ E9) c= E & E c= ( dom g) by A8, XBOOLE_1: 7, XBOOLE_1: 36;

                    then

                     A93: ( rng (g | (E \ E9))) <> {} by A92, Th1, XBOOLE_1: 1;

                    

                     A94: (E /\ E9) c= (E \/ E9) by XBOOLE_1: 29;

                    per cases ;

                      suppose

                       A95: (E9 \ E) = {} ;

                      then

                       A96: ( rng (f | (E9 \ E))) = {} ;

                      E9 c= E by A95, XBOOLE_1: 37;

                      then E = (E \/ E9) by XBOOLE_1: 12;

                      then ( dom f) = (E \/ E9) by FUNCT_2:def 1;

                      

                      then

                       A97: ( rng f) = ((( rng (f | (E /\ E9))) \/ ( rng (f | (E \ E9)))) \/ ( rng (f | (E9 \ E)))) by A49

                      .= (( rng (f | (E /\ E9))) \/ ( rng (f | (E \ E9)))) by A96;

                      (E \ E9) c= E by XBOOLE_1: 36;

                      then

                       A98: (E \ E9) c= ( dom f) by FUNCT_2:def 1;

                      E9 c= E by A95, XBOOLE_1: 37;

                      then

                       A99: (f9 | (E /\ E9)) = f9 by RELSET_1: 19, XBOOLE_1: 19;

                      ( dom f) = E by FUNCT_2:def 1;

                      then

                       A100: ( rng (f | (E /\ E9))) <> {} by A81, Th1, XBOOLE_1: 17;

                      ( rng (g | (E9 \ E))) = {} by A95;

                      

                      then ( meet ( rng g)) = (( meet ( rng (g | (E /\ E9)))) /\ ( meet ( rng (g | (E \ E9))))) by A8, A63, A81, A94, A93, SETFAM_1: 9

                      .= ((( meet ( rng (f | (E /\ E9)))) /\ ( meet ( rng (f | (E \ E9))))) /\ ( meet ( rng (f9 | (E /\ E9))))) by A17, A73, XBOOLE_1: 16;

                      hence thesis by A92, A99, A97, A100, A98, SETFAM_1: 9;

                    end;

                      suppose

                       A101: not (E9 \ E) = {} ;

                      (E9 \ E) c= E9 & E9 c= (E \/ E9) by XBOOLE_1: 7, XBOOLE_1: 36;

                      then (E9 \ E) c= ( dom g) by A8;

                      

                      then ( meet ( rng g)) = (( meet (( rng (g | (E /\ E9))) \/ ( rng (g | (E \ E9))))) /\ ( meet ( rng (g | (E9 \ E))))) by A8, A63, A81, A94, A101, SETFAM_1: 9

                      .= ((( meet ( rng (g | (E /\ E9)))) /\ ( meet ( rng (g | (E \ E9))))) /\ ( meet ( rng (g | (E9 \ E))))) by A8, A81, A94, A93, SETFAM_1: 9;

                      then

                       A102: ( meet ( rng g)) = (((( meet ( rng (f | (E /\ E9)))) /\ ( meet ( rng (f | (E \ E9))))) /\ ( meet ( rng (f9 | (E /\ E9))))) /\ ( meet ( rng (f9 | (E9 \ E))))) by A17, A73, A68, XBOOLE_1: 16;

                      (E /\ E9) c= E by XBOOLE_1: 17;

                      then

                       A103: (E /\ E9) c= ( dom f) by FUNCT_2:def 1;

                      (E \/ (E /\ E9)) = E by XBOOLE_1: 12, XBOOLE_1: 17;

                      then ( dom f) = (E \/ (E /\ E9)) by FUNCT_2:def 1;

                      then

                       A104: ( rng f) = ((( rng (f | (E /\ (E /\ E9)))) \/ ( rng (f | (E \ (E /\ E9))))) \/ ( rng (f | ((E /\ E9) \ E)))) by A49;

                      (E /\ E9) c= E by XBOOLE_1: 17;

                      then ((E /\ E9) \ E) = {} by XBOOLE_1: 37;

                      then

                       A105: ( rng (f | ((E /\ E9) \ E))) = {} ;

                      (E9 \ E) c= E9 by XBOOLE_1: 36;

                      then

                       A106: (E9 \ E) c= ( dom f9) by FUNCT_2:def 1;

                      (E /\ E9) c= E9 by XBOOLE_1: 17;

                      then

                       A107: (E /\ E9) c= ( dom f9) by FUNCT_2:def 1;

                      (E /\ E9) c= E9 by XBOOLE_1: 17;

                      then

                       A108: (E9 \ E) = (E9 \ (E /\ E9)) & ((E /\ E9) \ E9) = {} by XBOOLE_1: 37, XBOOLE_1: 47;

                      (E9 \/ (E /\ E9)) = E9 by XBOOLE_1: 12, XBOOLE_1: 17;

                      then

                       A109: ( dom f9) = (E9 \/ (E /\ E9)) by FUNCT_2:def 1;

                      (E9 /\ (E /\ E9)) = ((E9 /\ E9) /\ E) by XBOOLE_1: 16

                      .= (E /\ E9);

                      then ( rng f9) = ((( rng (f9 | (E /\ E9))) \/ ( rng (f9 | (E9 \ E)))) \/ ( rng (f9 | {} ))) by A49, A109, A108;

                      then

                       A110: ( meet ( rng f9)) = (( meet ( rng (f9 | (E /\ E9)))) /\ ( meet ( rng (f9 | (E9 \ E))))) by A81, A101, A107, A106, SETFAM_1: 9;

                      (E \ E9) c= E by XBOOLE_1: 36;

                      then

                       A111: (E \ E9) c= ( dom f) by FUNCT_2:def 1;

                      (E /\ (E /\ E9)) = ((E /\ E) /\ E9) by XBOOLE_1: 16

                      .= (E /\ E9);

                      then ( rng f) = (( rng (f | (E /\ E9))) \/ ( rng (f | (E \ E9)))) by A104, A105, XBOOLE_1: 47;

                      then ( meet ( rng f)) = (( meet ( rng (f | (E /\ E9)))) /\ ( meet ( rng (f | (E \ E9))))) by A81, A92, A103, A111, SETFAM_1: 9;

                      hence thesis by A110, A102, XBOOLE_1: 16;

                    end;

                  end;

                  hence thesis;

                end;

              end;

              hence thesis by A4, A6;

            end;

          end;

          for y be object holds y in (( meet ( rng f)) /\ ( meet ( rng f9))) implies y in Omega

          proof

            let y be object;

            consider S be object such that

             A112: S in ( rng f) by XBOOLE_0:def 1;

            consider S9 be object such that

             A113: S9 in ( rng f9) by XBOOLE_0:def 1;

            assume

             A114: y in (( meet ( rng f)) /\ ( meet ( rng f9)));

            reconsider S, S9 as set by TARSKI: 1;

            y in ( meet ( rng f9)) by XBOOLE_0:def 4, A114;

            then

             A115: y in S9 by A113, SETFAM_1:def 1;

            y in ( meet ( rng f)) by A114, XBOOLE_0:def 4;

            then y in S by A112, SETFAM_1:def 1;

            then

             A116: y in (S /\ S9) by A115, XBOOLE_0:def 4;

            (S /\ S9) is Event of Sigma by A112, A113, PROB_1: 19;

            hence thesis by A116;

          end;

          then

          reconsider xX = (x /\ X) as Subset of Omega by A4, A6, TARSKI:def 3;

          (E \/ E9) c= J by A3, A5, XBOOLE_1: 8;

          then xX in ( MeetSections (J,F)) by A16, Def9;

          hence thesis;

        end;

        hence thesis by FINSUB_1:def 2;

      end;

    end

    theorem :: KOLMOG01:14

    

     Th14: for F be ManySortedSigmaField of I, Sigma, J,K be non empty Subset of I st F is_independent_wrt P & J misses K holds for u, v st u in ( sigUn (F,J)) & v in ( sigUn (F,K)) holds (P . (u /\ v)) = ((P . u) * (P . v))

    proof

      let F be ManySortedSigmaField of I, Sigma, J,K be non empty Subset of I;

      

       A1: ( MeetSections (J,F)) is non empty Subset of Sigma & ( MeetSections (K,F)) is non empty Subset of Sigma by Th13;

      assume

       A2: F is_independent_wrt P & J misses K;

      

       A3: for p, q st p in ( MeetSections (J,F)) & q in ( MeetSections (K,F)) holds (p,q) are_independent_respect_to P

      proof

        let p, q;

        assume

         A4: p in ( MeetSections (J,F)) & q in ( MeetSections (K,F));

        reconsider p, q as Subset of Omega;

        (P . (p /\ q)) = ((P . p) * (P . q)) by A2, A4, Th12;

        hence thesis by PROB_2:def 4;

      end;

      let u, v;

      assume u in ( sigUn (F,J)) & v in ( sigUn (F,K));

      then u in ( sigma ( MeetSections (J,F))) & v in ( sigma ( MeetSections (K,F))) by Th11;

      then (u,v) are_independent_respect_to P by A1, A3, Th10;

      hence thesis by PROB_2:def 4;

    end;

    definition

      let I be set, Omega be non empty set, Sigma be SigmaField of Omega, F be ManySortedSigmaField of I, Sigma;

      :: KOLMOG01:def10

      func finSigmaFields (F,I) -> Subset-Family of Omega means

      : Def10: for S be Subset of Omega holds S in it iff ex E be finite Subset of I st S in ( sigUn (F,E));

      existence

      proof

        defpred P[ object] means ex E be finite Subset of I st $1 in ( sigUn (F,E));

        consider X such that

         A1: for x be object holds x in X iff x in ( bool Omega) & P[x] from XBOOLE_0:sch 1;

        for x be object holds x in X implies x in ( bool Omega) by A1;

        then

        reconsider X as Subset-Family of Omega by TARSKI:def 3;

        take X;

        let S be Subset of Omega;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let X1,X2 be Subset-Family of Omega;

        assume

         A2: for S be Subset of Omega holds S in X1 iff ex E be finite Subset of I st S in ( sigUn (F,E));

        assume

         A3: for S be Subset of Omega holds S in X2 iff ex E be finite Subset of I st S in ( sigUn (F,E));

        now

          let S be Subset of Omega;

          S in X1 iff ex E be finite Subset of I st S in ( sigUn (F,E)) by A2;

          hence S in X1 iff S in X2 by A3;

        end;

        hence thesis by SUBSET_1: 3;

      end;

    end

    theorem :: KOLMOG01:15

    

     Th15: for F be ManySortedSigmaField of I, Sigma holds ( tailSigmaField (F,I)) is SigmaField of Omega

    proof

      let F be ManySortedSigmaField of I, Sigma;

      

       A1: for A1 be SetSequence of Omega st ( rng A1) c= ( tailSigmaField (F,I)) holds ( Intersection A1) in ( tailSigmaField (F,I))

      proof

        let A1 be SetSequence of Omega;

        assume

         A2: ( rng A1) c= ( tailSigmaField (F,I));

        

         A3: for n holds for S holds S in ( futSigmaFields (F,I)) implies (A1 . n) in S

        proof

          let n, S;

          

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

          assume S in ( futSigmaFields (F,I));

          hence thesis by A2, A4, SETFAM_1:def 1;

        end;

        for S st S in ( futSigmaFields (F,I)) holds (( Union ( Complement A1)) ` ) in S

        proof

          let S;

          assume

           A5: S in ( futSigmaFields (F,I));

          then ex E be finite Subset of I st S = ( sigUn (F,(I \ E))) by Def7;

          then

          reconsider S as SigmaField of Omega;

          for n be Nat holds (( Complement A1) . n) in S

          proof

            let n be Nat;

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

            (A1 . n) in S by A3, A5;

            then ((A1 . n) ` ) is Event of S by PROB_1: 20;

            then ((A1 . n) ` ) in S;

            hence thesis by PROB_1:def 2;

          end;

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

          then

          reconsider CA1 = ( Complement A1) as SetSequence of S by RELAT_1:def 19;

          ( Union CA1) in S by PROB_1: 17;

          then (( Union ( Complement A1)) ` ) is Event of S by PROB_1: 20;

          hence thesis;

        end;

        hence thesis by SETFAM_1:def 1;

      end;

      for A be Subset of Omega st A in ( tailSigmaField (F,I)) holds (A ` ) in ( tailSigmaField (F,I))

      proof

        let A be Subset of Omega;

        assume

         A6: A in ( tailSigmaField (F,I));

        for S holds S in ( futSigmaFields (F,I)) implies (A ` ) in S

        proof

          let S;

          assume

           A7: S in ( futSigmaFields (F,I));

          then

          consider E be finite Subset of I such that

           A8: S = ( sigUn (F,(I \ E))) by Def7;

          A in S by A6, A7, SETFAM_1:def 1;

          then (A ` ) is Event of ( sigma ( Union (F | (I \ E)))) by A8, PROB_1: 20;

          hence thesis by A8;

        end;

        hence thesis by SETFAM_1:def 1;

      end;

      hence thesis by A1, PROB_1: 15;

    end;

    ::$Notion-Name

    theorem :: KOLMOG01:16

    for F be ManySortedSigmaField of I, Sigma st F is_independent_wrt P & a in ( tailSigmaField (F,I)) holds (P . a) = 0 or (P . a) = 1

    proof

      let F be ManySortedSigmaField of I, Sigma;

      reconsider T = ( tailSigmaField (F,I)) as SigmaField of Omega by Th15;

      set Ie = (I \ ( {} I));

      

       A1: a in ( tailSigmaField (F,I)) implies a in ( sigUn (F,Ie))

      proof

        assume

         A2: a in ( tailSigmaField (F,I));

        ( sigUn (F,Ie)) in ( futSigmaFields (F,I)) by Def7;

        hence thesis by A2, SETFAM_1:def 1;

      end;

      assume

       A3: F is_independent_wrt P;

      

       A4: for E be finite Subset of I holds for p, q st p in ( sigUn (F,E)) & q in ( tailSigmaField (F,I)) holds (p,q) are_independent_respect_to P

      proof

        let E be finite Subset of I;

        let p, q;

        assume that

         A5: p in ( sigUn (F,E)) and

         A6: q in ( tailSigmaField (F,I));

        for E be finite Subset of I holds q in ( sigUn (F,(I \ E)))

        proof

          let E be finite Subset of I;

          ( sigUn (F,(I \ E))) in ( futSigmaFields (F,I)) by Def7;

          hence thesis by A6, SETFAM_1:def 1;

        end;

        then

         A7: q in ( sigUn (F,(I \ E)));

        per cases ;

          suppose

           A8: E <> {} & (I \ E) <> {} ;

          then

          reconsider E as non empty Subset of I;

          reconsider IE = (I \ E) as non empty Subset of I by A8;

          E misses IE by XBOOLE_1: 79;

          then (P . (p /\ q)) = ((P . p) * (P . q)) by A3, A5, A7, Th14;

          hence thesis by PROB_2:def 4;

        end;

          suppose

           A9: not (E <> {} & (I \ E) <> {} );

          reconsider e = {} as Subset of I by XBOOLE_1: 2;

          

           A10: for u, v st u in { {} , Omega} holds (u,v) are_independent_respect_to P

          proof

            let u, v;

            assume

             A11: u in { {} , Omega};

            per cases ;

              suppose u = {} ;

              hence thesis by PROB_2: 19, PROB_2: 23;

            end;

              suppose u <> {} ;

              then u = ( [#] Sigma) by A11, TARSKI:def 2;

              hence thesis by PROB_2: 19, PROB_2: 24;

            end;

          end;

          ( Union (F | {} )) = {} by ZFMISC_1: 2;

          then

           A12: ( sigUn (F,e)) = { {} , Omega} by Th3;

          (p,q) are_independent_respect_to P

          proof

            per cases ;

              suppose E = {} ;

              hence thesis by A5, A12, A10;

            end;

              suppose E <> {} ;

              hence thesis by A7, A9, A12, A10, PROB_2: 19;

            end;

          end;

          hence thesis;

        end;

      end;

      

       A13: for p, q st p in ( finSigmaFields (F,I)) & q in ( tailSigmaField (F,I)) holds (p,q) are_independent_respect_to P

      proof

        let p, q;

        assume that

         A14: p in ( finSigmaFields (F,I)) and

         A15: q in ( tailSigmaField (F,I));

        ex E be finite Subset of I st p in ( sigUn (F,E)) by A14, Def10;

        hence thesis by A4, A15;

      end;

      ( Union (F | Ie)) c= ( sigma ( finSigmaFields (F,I)))

      proof

        let x be object;

        assume x in ( Union (F | Ie));

        then x in ( union ( rng F));

        then

        consider y such that

         A16: x in y and

         A17: y in ( rng F) by TARSKI:def 4;

        consider i be object such that

         A18: i in ( dom F) and

         A19: y = (F . i) by A17, FUNCT_1:def 3;

        

         A20: x in ( finSigmaFields (F,I))

        proof

          reconsider Fi = (F . i) as SigmaField of Omega by A18, Def2;

          

           A21: ( sigma Fi) c= Fi & Fi c= ( sigma Fi) by PROB_1:def 9;

          i in I by A18;

          then for z be object holds z in {i} implies z in I by TARSKI:def 1;

          then

          reconsider E = {i} as finite Subset of I by TARSKI:def 3;

          

           A22: ( dom (F | {i})) = (( dom F) /\ {i}) by RELAT_1: 61

          .= {i} by A18, ZFMISC_1: 46;

          then ( rng (F | {i})) = {((F | {i}) . i)} by FUNCT_1: 4;

          then

           A23: ( union ( rng (F | {i}))) = ((F | {i}) . i) by ZFMISC_1: 25;

          i in ( dom (F | {i})) by A22, TARSKI:def 1;

          then ( Union (F | {i})) = (F . i) by A23, FUNCT_1: 47;

          then ( sigUn (F,E)) = (F . i) by A21;

          hence thesis by A16, A19, Def10;

        end;

        ( finSigmaFields (F,I)) c= ( sigma ( finSigmaFields (F,I))) by PROB_1:def 9;

        hence thesis by A20;

      end;

      then

       A24: T c= ( sigma T) & ( sigUn (F,Ie)) c= ( sigma ( finSigmaFields (F,I))) by PROB_1:def 9;

      

       A25: for u, v st u in ( sigUn (F,Ie)) & v in ( tailSigmaField (F,I)) holds (u,v) are_independent_respect_to P

      proof

        for x, y st x in ( finSigmaFields (F,I)) & y in ( finSigmaFields (F,I)) holds (x /\ y) in ( finSigmaFields (F,I))

        proof

          let x, y;

          assume that

           A26: x in ( finSigmaFields (F,I)) and

           A27: y in ( finSigmaFields (F,I));

          consider E1 be finite Subset of I such that

           A28: x in ( sigUn (F,E1)) by A26, Def10;

          consider E2 be finite Subset of I such that

           A29: y in ( sigUn (F,E2)) by A27, Def10;

          

           A30: for E1,E2 be finite Subset of I holds z in ( sigUn (F,E1)) implies z in ( sigUn (F,(E1 \/ E2)))

          proof

            let E1,E2 be finite Subset of I;

            reconsider E3 = (E1 \/ E2) as finite Subset of I;

            

             A31: ( Union (F | E1)) c= ( Union (F | E3))

            proof

              let X be object;

              assume X in ( Union (F | E1));

              then

              consider S such that

               A32: X in S and

               A33: S in ( rng (F | E1)) by TARSKI:def 4;

              (F | E3) = ((F | E1) \/ (F | E2)) by RELAT_1: 78;

              then ( rng (F | E3)) = (( rng (F | E1)) \/ ( rng (F | E2))) by RELAT_1: 12;

              then S in ( rng (F | E3)) by A33, XBOOLE_0:def 3;

              hence thesis by A32, TARSKI:def 4;

            end;

            ( Union (F | E3)) c= ( sigma ( Union (F | E3))) by PROB_1:def 9;

            then ( Union (F | E1)) c= ( sigma ( Union (F | E3))) by A31;

            then

             A34: ( sigma ( Union (F | E1))) c= ( sigma ( Union (F | E3))) by PROB_1:def 9;

            assume z in ( sigUn (F,E1));

            hence thesis by A34;

          end;

          then

           A35: y in ( sigUn (F,(E2 \/ E1))) by A29;

          x in ( sigUn (F,(E1 \/ E2))) by A28, A30;

          then (x /\ y) in ( sigUn (F,(E1 \/ E2))) by A35, FINSUB_1:def 2;

          hence thesis by Def10;

        end;

        then

         A36: ( finSigmaFields (F,I)) is intersection_stable by FINSUB_1:def 2;

        let u, v;

        

         A37: ( finSigmaFields (F,I)) is non empty

        proof

          set E = the finite Subset of I;

           {} in ( sigUn (F,E)) by PROB_1: 4;

          hence thesis by Def10;

        end;

        

         A38: ( tailSigmaField (F,I)) c= Sigma

        proof

          set Ie = (I \ ( {} I));

          let x be object;

          assume

           A39: x in ( tailSigmaField (F,I));

          ( Union (F | Ie)) c= Sigma

          proof

            let y be object;

            assume y in ( Union (F | Ie));

            then ex S st y in S & S in ( rng (F | Ie)) by TARSKI:def 4;

            hence thesis;

          end;

          then

           A40: ( sigma ( Union (F | Ie))) c= Sigma by PROB_1:def 9;

          ( sigUn (F,Ie)) in ( futSigmaFields (F,I)) by Def7;

          then x in ( sigma ( Union (F | Ie))) by A39, SETFAM_1:def 1;

          hence thesis by A40;

        end;

        

         A41: ( finSigmaFields (F,I)) c= Sigma

        proof

          let x be object;

          assume x in ( finSigmaFields (F,I));

          then

          consider E be finite Subset of I such that

           A42: x in ( sigUn (F,E)) by Def10;

          ( Union (F | E)) c= Sigma

          proof

            let y be object;

            assume y in ( Union (F | E));

            then ex S st y in S & S in ( rng (F | E)) by TARSKI:def 4;

            hence thesis;

          end;

          then ( sigma ( Union (F | E))) c= Sigma by PROB_1:def 9;

          hence thesis by A42;

        end;

        assume u in ( sigUn (F,Ie)) & v in ( tailSigmaField (F,I));

        hence thesis by A13, A24, A37, A41, A36, A38, Th10;

      end;

      assume a in ( tailSigmaField (F,I));

      then (a,a) are_independent_respect_to P by A1, A25;

      then (P . (a /\ a)) = ((P . a) * (P . a)) by PROB_2:def 4;

      hence thesis by Th2;

    end;