:: KOLMOG01 semantic presentation

begin

theorem :: KOLMOG01:1
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function)
for X being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) c= dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) & X : ( ( ) ( ) set ) <> {} : ( ( ) ( ext-real empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined RAT : ( ( ) ( non empty non trivial non finite V79() V80() V81() V82() V85() ) set ) -valued Function-like one-to-one constant functional V33() V34() V35() V36() finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() V81() V82() V83() V84() V85() ) set ) holds
rng (f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) | X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) <> {} : ( ( ) ( ext-real empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined RAT : ( ( ) ( non empty non trivial non finite V79() V80() V81() V82() V85() ) set ) -valued Function-like one-to-one constant functional V33() V34() V35() V36() finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() V81() V82() V83() V84() V85() ) set ) ;

theorem :: KOLMOG01:2
for r being ( ( ) ( ext-real V14() real ) Real) holds
( not r : ( ( ) ( ext-real V14() real ) Real) * r : ( ( ) ( ext-real V14() real ) Real) : ( ( ) ( ext-real V14() real ) set ) = r : ( ( ) ( ext-real V14() real ) Real) or r : ( ( ) ( ext-real V14() real ) Real) = 0 : ( ( ) ( ext-real empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined RAT : ( ( ) ( non empty non trivial non finite V79() V80() V81() V82() V85() ) set ) -valued Function-like one-to-one constant functional V33() V34() V35() V36() finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V77() V78() V79() V80() V81() V82() V83() V84() V85() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) or r : ( ( ) ( ext-real V14() real ) Real) = 1 : ( ( ) ( ext-real non empty epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ;

theorem :: KOLMOG01:3
for Omega being ( ( non empty ) ( non empty ) set )
for X being ( ( ) ( ) Subset-Family of ) st X : ( ( ) ( ) Subset-Family of ) = {} : ( ( ) ( ext-real empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined RAT : ( ( ) ( non empty non trivial non finite V79() V80() V81() V82() V85() ) set ) -valued Function-like one-to-one constant functional V33() V34() V35() V36() finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() V81() V82() V83() V84() V85() ) set ) holds
sigma X : ( ( ) ( ) Subset-Family of ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) = {{} : ( ( ) ( ext-real empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined RAT : ( ( ) ( non empty non trivial non finite V79() V80() V81() V82() V85() ) set ) -valued Function-like one-to-one constant functional V33() V34() V35() V36() finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() V81() V82() V83() V84() V85() ) set ) ,Omega : ( ( non empty ) ( non empty ) set ) } : ( ( ) ( non empty finite intersection_stable ) set ) ;

definition
let Omega be ( ( non empty ) ( non empty ) set ) ;
let Sigma be ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ;
let B be ( ( ) ( ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ;
let P be ( ( ) ( non empty Relation-like Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) V30(Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) ;
func Indep (B,P) -> ( ( ) ( ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) means :: KOLMOG01:def 1
 for a being ( ( ) ( ) Element of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) holds
( a : ( ( ) ( ) Element of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) in it : ( ( ) ( ) set ) iff for b being ( ( ) ( ) Element of B : ( ( ) ( non empty Relation-like Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) V30(Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) holds P : ( ( ) ( ) Element of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) . (a : ( ( ) ( ) Element of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) /\ b : ( ( ) ( ) Element of B : ( ( ) ( ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( ) Element of bool Omega : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) = (P : ( ( ) ( ) Element of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) . a : ( ( ) ( ) Element of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) * (P : ( ( ) ( ) Element of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) . b : ( ( ) ( ) Element of B : ( ( ) ( ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) );
end;

theorem :: KOLMOG01:4
for Omega being ( ( non empty ) ( non empty ) set )
for Sigma being ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) )
for P being ( ( ) ( non empty Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) )
for B being ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) )
for b being ( ( ) ( ) Element of B : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) )
for f being ( ( b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -valued bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) SetSequence of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) st ( for n being ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) )
for b being ( ( ) ( ) Element of B : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) holds P : ( ( ) ( non empty Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) . ((f : ( ( b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -valued bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) SetSequence of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) . n : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( ) Event of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) /\ b : ( ( ) ( ) Element of b4 : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( ) Event of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) = (P : ( ( ) ( non empty Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) . (f : ( ( b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -valued bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) SetSequence of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) . n : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( ) Event of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) * (P : ( ( ) ( non empty Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) . b : ( ( ) ( ) Element of b4 : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) : ( ( ) ( ext-real V14() real ) set ) ) & f : ( ( b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -valued bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) SetSequence of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) is V65() holds
P : ( ( ) ( non empty Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) . (b : ( ( ) ( ) Element of b4 : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) /\ (Union f : ( ( b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -valued bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) SetSequence of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) : ( ( ) ( ) Element of bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) : ( ( ) ( ext-real V14() real ) set ) = (P : ( ( ) ( non empty Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) . b : ( ( ) ( ) Element of b4 : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) * (P : ( ( ) ( non empty Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) . (Union f : ( ( b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -valued bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) SetSequence of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) : ( ( ) ( ext-real V14() real ) set ) : ( ( ) ( ext-real V14() real ) set ) ;

theorem :: KOLMOG01:5
for Omega being ( ( non empty ) ( non empty ) set )
for Sigma being ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) )
for P being ( ( ) ( non empty Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) )
for B being ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) holds Indep (B : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ,P : ( ( ) ( non empty Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) is ( ( ) ( ) Dynkin_System of Omega : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: KOLMOG01:6
for Omega being ( ( non empty ) ( non empty ) set )
for Sigma being ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) )
for P being ( ( ) ( non empty Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) )
for B being ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) )
for A being ( ( ) ( ) Subset-Family of ) st A : ( ( ) ( ) Subset-Family of ) is intersection_stable & A : ( ( ) ( ) Subset-Family of ) c= Indep (B : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ,P : ( ( ) ( non empty Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) holds
sigma A : ( ( ) ( ) Subset-Family of ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) c= Indep (B : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ,P : ( ( ) ( non empty Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ;

theorem :: KOLMOG01:7
for Omega being ( ( non empty ) ( non empty ) set )
for Sigma being ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) )
for P being ( ( ) ( non empty Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) )
for A, B being ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) holds
( A : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) c= Indep (B : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ,P : ( ( ) ( non empty Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) iff for p, q being ( ( ) ( ) Event of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) st p : ( ( ) ( ) Event of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) in A : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) & q : ( ( ) ( ) Event of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) in B : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) holds
p : ( ( ) ( ) Event of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,q : ( ( ) ( ) Event of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) are_independent_respect_to P : ( ( ) ( non empty Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) ;

theorem :: KOLMOG01:8
for Omega being ( ( non empty ) ( non empty ) set )
for Sigma being ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) )
for P being ( ( ) ( non empty Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) )
for A, B being ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) st A : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) c= Indep (B : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ,P : ( ( ) ( non empty Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) holds
B : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) c= Indep (A : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ,P : ( ( ) ( non empty Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ;

theorem :: KOLMOG01:9
for Omega being ( ( non empty ) ( non empty ) set )
for Sigma being ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) )
for P being ( ( ) ( non empty Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) )
for A being ( ( ) ( ) Subset-Family of ) st A : ( ( ) ( ) Subset-Family of ) is ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) & A : ( ( ) ( ) Subset-Family of ) is intersection_stable holds
for B being ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) st B : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) is intersection_stable & A : ( ( ) ( ) Subset-Family of ) c= Indep (B : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ,P : ( ( ) ( non empty Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) holds
for D being ( ( ) ( ) Subset-Family of )
for sB being ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) st D : ( ( ) ( ) Subset-Family of ) = B : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) & sigma D : ( ( ) ( ) Subset-Family of ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) = sB : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) holds
sigma A : ( ( ) ( ) Subset-Family of ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) c= Indep (sB : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ,P : ( ( ) ( non empty Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ;

theorem :: KOLMOG01:10
for Omega being ( ( non empty ) ( non empty ) set )
for Sigma being ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) )
for P being ( ( ) ( non empty Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) )
for E, F being ( ( ) ( ) Subset-Family of ) st E : ( ( ) ( ) Subset-Family of ) is ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) & E : ( ( ) ( ) Subset-Family of ) is intersection_stable & F : ( ( ) ( ) Subset-Family of ) is ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) & F : ( ( ) ( ) Subset-Family of ) is intersection_stable & ( for p, q being ( ( ) ( ) Event of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) st p : ( ( ) ( ) Event of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) in E : ( ( ) ( ) Subset-Family of ) & q : ( ( ) ( ) Event of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) in F : ( ( ) ( ) Subset-Family of ) holds
p : ( ( ) ( ) Event of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,q : ( ( ) ( ) Event of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) are_independent_respect_to P : ( ( ) ( non empty Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) holds
for u, v being ( ( ) ( ) Event of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) st u : ( ( ) ( ) Event of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) in sigma E : ( ( ) ( ) Subset-Family of ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) & v : ( ( ) ( ) Event of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) in sigma F : ( ( ) ( ) Subset-Family of ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) holds
u : ( ( ) ( ) Event of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,v : ( ( ) ( ) Event of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) are_independent_respect_to P : ( ( ) ( non empty Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ;

definition
let I be ( ( ) ( ) set ) ;
let Omega be ( ( non empty ) ( non empty ) set ) ;
let Sigma be ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ;
mode ManySortedSigmaField of I,Sigma -> ( ( Function-like V30(I : ( ( non empty ) ( non empty ) set ) , bool Sigma : ( ( ) ( non empty Relation-like Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) V30(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( ) ( non empty Relation-like Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) V30(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined bool Sigma : ( ( ) ( non empty Relation-like Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) V30(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( ) ( non empty Relation-like Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) V30(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26(I : ( ( non empty ) ( non empty ) set ) ) V30(I : ( ( non empty ) ( non empty ) set ) , bool Sigma : ( ( ) ( non empty Relation-like Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) V30(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( ) ( non empty Relation-like Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) V30(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) Function of I : ( ( non empty ) ( non empty ) set ) , bool Sigma : ( ( ) ( non empty Relation-like Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) V30(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( ) ( non empty Relation-like Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) V30(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) means :: KOLMOG01:def 2
 for i being ( ( ) ( ) set ) st i : ( ( ) ( ) set ) in I : ( ( non empty ) ( non empty ) set ) holds
it : ( ( ) ( ) Element of Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) . i : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool (bool Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) is ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ;
end;

definition
let Omega be ( ( non empty ) ( non empty ) set ) ;
let Sigma be ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ;
let P be ( ( ) ( non empty Relation-like Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) V30(Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) ;
let I be ( ( ) ( ) set ) ;
let A be ( ( Function-like V30(I : ( ( ) ( ) set ) ,Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) ) ( Relation-like I : ( ( ) ( ) set ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) -valued Function-like V26(I : ( ( ) ( ) set ) ) V30(I : ( ( ) ( ) set ) ,Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) ) Function of I : ( ( ) ( ) set ) ,Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) ;
pred A is_independent_wrt P means :: KOLMOG01:def 3
 for e being ( ( one-to-one ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined I : ( ( ) ( ) Element of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like ) FinSequence of I : ( ( ) ( ) Element of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) st e : ( ( one-to-one ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined I : ( ( ) ( ) set ) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like ) FinSequence of I : ( ( ) ( ) set ) ) <> {} : ( ( ) ( ext-real empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined RAT : ( ( ) ( non empty non trivial non finite V79() V80() V81() V82() V85() ) set ) -valued Function-like one-to-one constant functional V33() V34() V35() V36() finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() V81() V82() V83() V84() V85() ) set ) holds
Product ((P : ( ( ) ( non empty Relation-like Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) V30(Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) * A : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like I : ( ( ) ( ) Element of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V33() V34() V35() ) Element of bool [:I : ( ( ) ( ) Element of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ,REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) :] : ( ( ) ( Relation-like V33() V34() V35() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) * e : ( ( one-to-one ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined I : ( ( ) ( ) set ) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like ) FinSequence of I : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V33() V34() V35() finite FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) = P : ( ( ) ( non empty Relation-like Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) V30(Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) . (meet (rng (A : ( ( ) ( ) set ) * e : ( ( one-to-one ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined I : ( ( ) ( ) set ) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like ) FinSequence of I : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( finite ) Element of bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) : ( ( ) ( ) set ) : ( ( ) ( ext-real V14() real ) set ) ;
end;

definition
let Omega be ( ( non empty ) ( non empty ) set ) ;
let Sigma be ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ;
let I be ( ( ) ( ) set ) ;
let J be ( ( ) ( ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ;
let F be ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26(I : ( ( ) ( ) set ) ) V30(I : ( ( ) ( ) set ) , bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ManySortedSigmaField of I : ( ( ) ( ) set ) ,Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) ;
mode SigmaSection of J,F -> ( ( Function-like V30(J : ( ( ) ( ) Element of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ,Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ( Relation-like J : ( ( ) ( ) Element of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26(J : ( ( ) ( ) Element of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) V30(J : ( ( ) ( ) Element of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ,Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) Function of J : ( ( ) ( ) Element of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ,Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) means :: KOLMOG01:def 4
 for i being ( ( ) ( ) set ) st i : ( ( ) ( ) set ) in J : ( ( ) ( ) Element of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) holds
it : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) . i : ( ( ) ( ) set ) : ( ( ) ( ) set ) in F : ( ( ) ( ) set ) . i : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ;
end;

definition
let Omega be ( ( non empty ) ( non empty ) set ) ;
let Sigma be ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ;
let P be ( ( ) ( non empty Relation-like Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) V30(Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) ;
let I be ( ( ) ( ) set ) ;
let F be ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26(I : ( ( ) ( ) set ) ) V30(I : ( ( ) ( ) set ) , bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ManySortedSigmaField of I : ( ( ) ( ) set ) ,Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) ;
pred F is_independent_wrt P means :: KOLMOG01:def 5
 for E being ( ( finite ) ( finite ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) )
for A being ( ( ) ( Relation-like b1 : ( ( finite ) ( finite ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26(b1 : ( ( finite ) ( finite ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) V30(b1 : ( ( finite ) ( finite ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ,Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) finite ) SigmaSection of E : ( ( finite ) ( finite ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ,F : ( ( ) ( ) set ) ) holds A : ( ( ) ( Relation-like b1 : ( ( finite ) ( finite ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) -valued Function-like V26(b1 : ( ( finite ) ( finite ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) V30(b1 : ( ( finite ) ( finite ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ,Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) finite ) SigmaSection of b1 : ( ( finite ) ( finite ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ,F : ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26(I : ( ( ) ( ) set ) ) V30(I : ( ( ) ( ) set ) , bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ManySortedSigmaField of I : ( ( ) ( ) set ) ,Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) ) is_independent_wrt P : ( ( ) ( non empty Relation-like Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) V30(Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ;
end;

definition
let I be ( ( ) ( ) set ) ;
let Omega be ( ( non empty ) ( non empty ) set ) ;
let Sigma be ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ;
let F be ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26(I : ( ( ) ( ) set ) ) V30(I : ( ( ) ( ) set ) , bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ManySortedSigmaField of I : ( ( ) ( ) set ) ,Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) ;
let J be ( ( ) ( ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ;
:: original: |
redefine func F | J -> ( ( Function-like V30(J : ( ( ) ( ) set ) , bool Sigma : ( ( ) ( non empty Relation-like Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) V30(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( ) ( non empty Relation-like Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) V30(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ( Relation-like J : ( ( ) ( ) set ) -defined bool Sigma : ( ( ) ( non empty Relation-like Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) V30(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( ) ( non empty Relation-like Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) V30(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26(J : ( ( ) ( ) set ) ) V30(J : ( ( ) ( ) set ) , bool Sigma : ( ( ) ( non empty Relation-like Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) V30(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( ) ( non empty Relation-like Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) V30(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) Function of J : ( ( ) ( ) set ) , bool Sigma : ( ( ) ( non empty Relation-like Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) V30(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( ) ( non empty Relation-like Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) V30(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ;
end;

definition
let I be ( ( ) ( ) set ) ;
let J be ( ( ) ( ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ;
let Omega be ( ( non empty ) ( non empty ) set ) ;
let Sigma be ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ;
let F be ( ( Function-like V30(J : ( ( ) ( ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) , bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ( Relation-like J : ( ( ) ( ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26(J : ( ( ) ( ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) V30(J : ( ( ) ( ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) , bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) Function of J : ( ( ) ( ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) , bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ;
:: original: Union
redefine func Union F -> ( ( ) ( ) Subset-Family of ) ;
end;

definition
let I be ( ( ) ( ) set ) ;
let Omega be ( ( non empty ) ( non empty ) set ) ;
let Sigma be ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ;
let F be ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26(I : ( ( ) ( ) set ) ) V30(I : ( ( ) ( ) set ) , bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ManySortedSigmaField of I : ( ( ) ( ) set ) ,Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) ;
let J be ( ( ) ( ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ;
func sigUn (F,J) -> ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) equals :: KOLMOG01:def 6
 sigma (Union (F : ( ( ) ( ) Element of Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) | J : ( ( ) ( ) set ) ) : ( ( Function-like V30(J : ( ( ) ( ) set ) , bool Sigma : ( ( ) ( non empty Relation-like Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) V30(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( ) ( non empty Relation-like Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) V30(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ( Relation-like J : ( ( ) ( ) set ) -defined bool Sigma : ( ( ) ( non empty Relation-like Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) V30(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( ) ( non empty Relation-like Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) V30(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26(J : ( ( ) ( ) set ) ) V30(J : ( ( ) ( ) set ) , bool Sigma : ( ( ) ( non empty Relation-like Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) V30(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( ) ( non empty Relation-like Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) V30(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) Function of J : ( ( ) ( ) set ) , bool Sigma : ( ( ) ( non empty Relation-like Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) V30(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( ) ( non empty Relation-like Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) V30(Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( ) Subset-Family of ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ;
end;

definition
let I be ( ( ) ( ) set ) ;
let Omega be ( ( non empty ) ( non empty ) set ) ;
let Sigma be ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ;
let F be ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26(I : ( ( ) ( ) set ) ) V30(I : ( ( ) ( ) set ) , bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ManySortedSigmaField of I : ( ( ) ( ) set ) ,Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) ;
func futSigmaFields (F,I) -> ( ( ) ( ) Subset-Family of ) means :: KOLMOG01:def 7
 for S being ( ( ) ( ) Subset-Family of ) holds
( S : ( ( ) ( ) Subset-Family of ) in it : ( ( ) ( ) set ) iff ex E being ( ( finite ) ( finite ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) st S : ( ( ) ( ) Subset-Family of ) = sigUn (F : ( ( ) ( ) Element of Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ,(I : ( ( non empty ) ( non empty ) set ) \ E : ( ( finite ) ( finite ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) : ( ( ) ( ) Element of bool I : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) );
end;

registration
let I be ( ( ) ( ) set ) ;
let Omega be ( ( non empty ) ( non empty ) set ) ;
let Sigma be ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ;
let F be ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26(I : ( ( ) ( ) set ) ) V30(I : ( ( ) ( ) set ) , bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ManySortedSigmaField of I : ( ( ) ( ) set ) ,Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) ;
cluster futSigmaFields (F : ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26(I : ( ( ) ( ) set ) ) V30(I : ( ( ) ( ) set ) , bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ManySortedSigmaField of I : ( ( ) ( ) set ) ,Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ,I : ( ( ) ( ) set ) ) : ( ( ) ( ) Subset-Family of ) -> non empty ;
end;

definition
let I be ( ( ) ( ) set ) ;
let Omega be ( ( non empty ) ( non empty ) set ) ;
let Sigma be ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ;
let F be ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26(I : ( ( ) ( ) set ) ) V30(I : ( ( ) ( ) set ) , bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ManySortedSigmaField of I : ( ( ) ( ) set ) ,Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) ;
func tailSigmaField (F,I) -> ( ( ) ( ) Subset-Family of ) equals :: KOLMOG01:def 8
 meet (futSigmaFields (F : ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26(I : ( ( ) ( ) set ) ) V30(I : ( ( ) ( ) set ) , bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ManySortedSigmaField of I : ( ( ) ( ) set ) ,Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ,I : ( ( ) ( ) set ) )) : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ;
end;

registration
let I be ( ( ) ( ) set ) ;
let Omega be ( ( non empty ) ( non empty ) set ) ;
let Sigma be ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ;
let F be ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26(I : ( ( ) ( ) set ) ) V30(I : ( ( ) ( ) set ) , bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ManySortedSigmaField of I : ( ( ) ( ) set ) ,Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) ;
cluster tailSigmaField (F : ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26(I : ( ( ) ( ) set ) ) V30(I : ( ( ) ( ) set ) , bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ManySortedSigmaField of I : ( ( ) ( ) set ) ,Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ,I : ( ( ) ( ) set ) ) : ( ( ) ( ) Subset-Family of ) -> non empty ;
end;

definition
let Omega be ( ( non empty ) ( non empty ) set ) ;
let Sigma be ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ;
let I be ( ( non empty ) ( non empty ) set ) ;
let J be ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ;
let F be ( ( ) ( non empty Relation-like I : ( ( non empty ) ( non empty ) set ) -defined bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26(I : ( ( non empty ) ( non empty ) set ) ) V30(I : ( ( non empty ) ( non empty ) set ) , bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ManySortedSigmaField of I : ( ( non empty ) ( non empty ) set ) ,Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) ;
func MeetSections (J,F) -> ( ( ) ( ) Subset-Family of ) means :: KOLMOG01:def 9
 for x being ( ( ) ( ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) holds
( x : ( ( ) ( ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) in it : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined Sigma : ( ( ) ( ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of Sigma : ( ( ) ( ) set ) ) iff ex E being ( ( non empty finite ) ( non empty finite ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ex f being ( ( ) ( non empty Relation-like b2 : ( ( non empty finite ) ( non empty finite ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined Sigma : ( ( ) ( ) set ) -valued Function-like V26(b2 : ( ( non empty finite ) ( non empty finite ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) V30(b2 : ( ( non empty finite ) ( non empty finite ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ,Sigma : ( ( ) ( ) set ) ) finite ) SigmaSection of E : ( ( non empty finite ) ( non empty finite ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ,F : ( ( ) ( ) set ) ) st
( E : ( ( non empty finite ) ( non empty finite ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) c= J : ( ( ) ( Relation-like Omega : ( ( ) ( ) set ) -defined bool I : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Sigma : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool I : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Sigma : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26(Omega : ( ( ) ( ) set ) ) V30(Omega : ( ( ) ( ) set ) , bool I : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Sigma : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool I : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Sigma : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ManySortedSigmaField of Omega : ( ( ) ( ) set ) ,I : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Sigma : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) & x : ( ( ) ( ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) = meet (rng f : ( ( ) ( non empty Relation-like b2 : ( ( non empty finite ) ( non empty finite ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) -valued Function-like V26(b2 : ( ( non empty finite ) ( non empty finite ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) V30(b2 : ( ( non empty finite ) ( non empty finite ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ,Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) finite ) SigmaSection of b2 : ( ( non empty finite ) ( non empty finite ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ,F : ( ( ) ( non empty Relation-like I : ( ( non empty ) ( non empty ) set ) -defined bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26(I : ( ( non empty ) ( non empty ) set ) ) V30(I : ( ( non empty ) ( non empty ) set ) , bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ManySortedSigmaField of I : ( ( non empty ) ( non empty ) set ) ,Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) ) ) : ( ( ) ( non empty finite ) Element of bool Sigma : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) : ( ( ) ( ) set ) ) );
end;

theorem :: KOLMOG01:11
for Omega, I being ( ( non empty ) ( non empty ) set )
for Sigma being ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) )
for F being ( ( ) ( non empty Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26(b2 : ( ( non empty ) ( non empty ) set ) ) V30(b2 : ( ( non empty ) ( non empty ) set ) , bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ManySortedSigmaField of I : ( ( non empty ) ( non empty ) set ) ,Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) )
for J being ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) holds sigma (MeetSections (J : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ,F : ( ( ) ( non empty Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26(b2 : ( ( non empty ) ( non empty ) set ) ) V30(b2 : ( ( non empty ) ( non empty ) set ) , bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ManySortedSigmaField of b2 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) )) : ( ( ) ( ) Subset-Family of ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) = sigUn (F : ( ( ) ( non empty Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26(b2 : ( ( non empty ) ( non empty ) set ) ) V30(b2 : ( ( non empty ) ( non empty ) set ) , bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ManySortedSigmaField of b2 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,J : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: KOLMOG01:12
for I, Omega being ( ( non empty ) ( non empty ) set )
for Sigma being ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) )
for P being ( ( ) ( non empty Relation-like b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) V30(b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) )
for F being ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26(b1 : ( ( non empty ) ( non empty ) set ) ) V30(b1 : ( ( non empty ) ( non empty ) set ) , bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ManySortedSigmaField of I : ( ( non empty ) ( non empty ) set ) ,Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) )
for J, K being ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) st F : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26(b1 : ( ( non empty ) ( non empty ) set ) ) V30(b1 : ( ( non empty ) ( non empty ) set ) , bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ManySortedSigmaField of b1 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) is_independent_wrt P : ( ( ) ( non empty Relation-like b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) V30(b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) & J : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) misses K : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) holds
for a, c being ( ( ) ( ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) st a : ( ( ) ( ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) in MeetSections (J : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ,F : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26(b1 : ( ( non empty ) ( non empty ) set ) ) V30(b1 : ( ( non empty ) ( non empty ) set ) , bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ManySortedSigmaField of b1 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset-Family of ) & c : ( ( ) ( ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) in MeetSections (K : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ,F : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26(b1 : ( ( non empty ) ( non empty ) set ) ) V30(b1 : ( ( non empty ) ( non empty ) set ) , bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ManySortedSigmaField of b1 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset-Family of ) holds
P : ( ( ) ( non empty Relation-like b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) V30(b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) . (a : ( ( ) ( ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) /\ c : ( ( ) ( ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) : ( ( ) ( ) Element of bool b2 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) : ( ( ) ( ext-real V14() real ) set ) = (P : ( ( ) ( non empty Relation-like b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) V30(b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) . a : ( ( ) ( ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) : ( ( ) ( ext-real V14() real ) set ) * (P : ( ( ) ( non empty Relation-like b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) V30(b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) . c : ( ( ) ( ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) : ( ( ) ( ext-real V14() real ) set ) : ( ( ) ( ext-real V14() real ) set ) ;

theorem :: KOLMOG01:13
for Omega, I being ( ( non empty ) ( non empty ) set )
for Sigma being ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) )
for F being ( ( ) ( non empty Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26(b2 : ( ( non empty ) ( non empty ) set ) ) V30(b2 : ( ( non empty ) ( non empty ) set ) , bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ManySortedSigmaField of I : ( ( non empty ) ( non empty ) set ) ,Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) )
for J being ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) holds MeetSections (J : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ,F : ( ( ) ( non empty Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26(b2 : ( ( non empty ) ( non empty ) set ) ) V30(b2 : ( ( non empty ) ( non empty ) set ) , bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ManySortedSigmaField of b2 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Subset-Family of ) is ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ;

registration
let I, Omega be ( ( non empty ) ( non empty ) set ) ;
let Sigma be ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ;
let F be ( ( ) ( non empty Relation-like I : ( ( non empty ) ( non empty ) set ) -defined bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26(I : ( ( non empty ) ( non empty ) set ) ) V30(I : ( ( non empty ) ( non empty ) set ) , bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ManySortedSigmaField of I : ( ( non empty ) ( non empty ) set ) ,Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) ;
let J be ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ;
cluster MeetSections (J : ( ( non empty ) ( non empty ) Element of bool I : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ,F : ( ( ) ( non empty Relation-like I : ( ( non empty ) ( non empty ) set ) -defined bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26(I : ( ( non empty ) ( non empty ) set ) ) V30(I : ( ( non empty ) ( non empty ) set ) , bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ManySortedSigmaField of I : ( ( non empty ) ( non empty ) set ) ,Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( ) Subset-Family of ) -> intersection_stable ;
end;

theorem :: KOLMOG01:14
for I, Omega being ( ( non empty ) ( non empty ) set )
for Sigma being ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) )
for P being ( ( ) ( non empty Relation-like b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) V30(b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) )
for F being ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26(b1 : ( ( non empty ) ( non empty ) set ) ) V30(b1 : ( ( non empty ) ( non empty ) set ) , bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ManySortedSigmaField of I : ( ( non empty ) ( non empty ) set ) ,Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) )
for J, K being ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) st F : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26(b1 : ( ( non empty ) ( non empty ) set ) ) V30(b1 : ( ( non empty ) ( non empty ) set ) , bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ManySortedSigmaField of b1 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) is_independent_wrt P : ( ( ) ( non empty Relation-like b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) V30(b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) & J : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) misses K : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) holds
for u, v being ( ( ) ( ) Event of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) st u : ( ( ) ( ) Event of b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) in sigUn (F : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26(b1 : ( ( non empty ) ( non empty ) set ) ) V30(b1 : ( ( non empty ) ( non empty ) set ) , bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ManySortedSigmaField of b1 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) ,J : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) & v : ( ( ) ( ) Event of b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) in sigUn (F : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26(b1 : ( ( non empty ) ( non empty ) set ) ) V30(b1 : ( ( non empty ) ( non empty ) set ) , bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ManySortedSigmaField of b1 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) ,K : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) holds
P : ( ( ) ( non empty Relation-like b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) V30(b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) . (u : ( ( ) ( ) Event of b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) /\ v : ( ( ) ( ) Event of b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Event of b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) = (P : ( ( ) ( non empty Relation-like b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) V30(b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) . u : ( ( ) ( ) Event of b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) * (P : ( ( ) ( non empty Relation-like b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) V30(b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) . v : ( ( ) ( ) Event of b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) : ( ( ) ( ext-real V14() real ) set ) ;

definition
let I be ( ( ) ( ) set ) ;
let Omega be ( ( non empty ) ( non empty ) set ) ;
let Sigma be ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ;
let F be ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26(I : ( ( ) ( ) set ) ) V30(I : ( ( ) ( ) set ) , bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ManySortedSigmaField of I : ( ( ) ( ) set ) ,Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) ;
func finSigmaFields (F,I) -> ( ( ) ( ) Subset-Family of ) means :: KOLMOG01:def 10
 for S being ( ( ) ( ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) holds
( S : ( ( ) ( ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) in it : ( ( non empty ) ( non empty ) Element of bool I : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) iff ex E being ( ( finite ) ( finite ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) st S : ( ( ) ( ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) in sigUn (F : ( ( ) ( non empty Relation-like I : ( ( ) ( ) set ) -defined bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26(I : ( ( ) ( ) set ) ) V30(I : ( ( ) ( ) set ) , bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ManySortedSigmaField of I : ( ( ) ( ) set ) ,Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ,E : ( ( finite ) ( finite ) Subset of ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( ) ( ) set ) ) );
end;

theorem :: KOLMOG01:15
for I, Omega being ( ( non empty ) ( non empty ) set )
for Sigma being ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) )
for F being ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26(b1 : ( ( non empty ) ( non empty ) set ) ) V30(b1 : ( ( non empty ) ( non empty ) set ) , bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ManySortedSigmaField of I : ( ( non empty ) ( non empty ) set ) ,Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) holds tailSigmaField (F : ( ( ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26(b1 : ( ( non empty ) ( non empty ) set ) ) V30(b1 : ( ( non empty ) ( non empty ) set ) , bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ManySortedSigmaField of b1 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b2 : ( ( non empty ) ( non empty ) set ) ) ) ,I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) Subset-Family of ) is ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: KOLMOG01:16
for Omega, I being ( ( non empty ) ( non empty ) set )
for Sigma being ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) )
for P being ( ( ) ( non empty Relation-like b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) V30(b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) )
for a being ( ( ) ( ) Element of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) )
for F being ( ( ) ( non empty Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26(b2 : ( ( non empty ) ( non empty ) set ) ) V30(b2 : ( ( non empty ) ( non empty ) set ) , bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ManySortedSigmaField of I : ( ( non empty ) ( non empty ) set ) ,Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) st F : ( ( ) ( non empty Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26(b2 : ( ( non empty ) ( non empty ) set ) ) V30(b2 : ( ( non empty ) ( non empty ) set ) , bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ManySortedSigmaField of b2 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) is_independent_wrt P : ( ( ) ( non empty Relation-like b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) V30(b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) & a : ( ( ) ( ) Element of b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) in tailSigmaField (F : ( ( ) ( non empty Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -valued Function-like V26(b2 : ( ( non empty ) ( non empty ) set ) ) V30(b2 : ( ( non empty ) ( non empty ) set ) , bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean ) Element of bool (bool b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ) ManySortedSigmaField of b2 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,I : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) Subset-Family of ) & not P : ( ( ) ( non empty Relation-like b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) V30(b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) . a : ( ( ) ( ) Element of b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) = 0 : ( ( ) ( ext-real empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) -defined RAT : ( ( ) ( non empty non trivial non finite V79() V80() V81() V82() V85() ) set ) -valued Function-like one-to-one constant functional V33() V34() V35() V36() finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V77() V78() V79() V80() V81() V82() V83() V84() V85() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) holds
P : ( ( ) ( non empty Relation-like b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) -valued Function-like V26(b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) V30(b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) V33() V34() V35() V42() ) Probability of b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) . a : ( ( ) ( ) Element of b3 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative intersection_stable ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) ) = 1 : ( ( ) ( ext-real non empty epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V79() V80() V81() V85() ) set ) : ( ( ) ( non empty cup-closed intersection_stable diff-closed preBoolean ) set ) ) ) ;