:: KOLMOG01 semantic presentation

begin


theorem Th1: :: KOLMOG01:1
for f being Function
for X being set st X c= dom f & X <> {} holds
rng (f | X) <> {}
proof
let f be Function; ::_thesis: for X being set st X c= dom f & X <> {} holds
rng (f | X) <> {}
let X be set ; ::_thesis: ( X c= dom f & X <> {} implies rng (f | X) <> {} )
assume A1: X c= dom f ; ::_thesis: ( not X <> {} or rng (f | X) <> {} )
set x = the Element of X;
assume  X <> {} ; ::_thesis: rng (f | X) <> {}
then  the Element of X in X ;
hence  rng (f | X) <> {} by A1, FUNCT_1:50; ::_thesis: verum
end;

theorem Th2: :: KOLMOG01:2
for r being Real holds
( not r * r = r or r = 0 or r = 1 )
proof
let r be Real; ::_thesis: ( not r * r = r or r = 0 or r = 1 )
assume  r * r = r ; ::_thesis: ( r = 0 or r = 1 )
then  r * (r - 1) = 0 ;
then  ( r = 0 or r - 1 = 0 ) by XCMPLX_1:6;
hence  ( r = 0 or r = 1 ) ; ::_thesis: verum
end;

theorem Th3: :: KOLMOG01:3
for Omega being non empty set
for X being Subset-Family of Omega st X = {} holds
sigma X = {{},Omega}
proof
let Omega be non empty set ; ::_thesis: for X being Subset-Family of Omega st X = {} holds
sigma X = {{},Omega}
let X be Subset-Family of Omega; ::_thesis: ( X = {} implies sigma X = {{},Omega} )
A1: for A1 being SetSequence of Omega st rng A1 c= {{},Omega} holds
Union A1 in {{},Omega}
proof
let A1 be SetSequence of Omega; ::_thesis: ( rng A1 c= {{},Omega} implies Union A1 in {{},Omega} )
assume A2: rng A1 c= {{},Omega} ; ::_thesis: Union A1 in {{},Omega}
A3: for n being Element of NAT holds
( (Partial_Union A1) . n = {} or (Partial_Union A1) . n = Omega )
proof
defpred S1[ Nat] means ( (Partial_Union A1) . $1 = {} or (Partial_Union A1) . $1 = Omega );
let n be Element of NAT ; ::_thesis: ( (Partial_Union A1) . n = {} or (Partial_Union A1) . n = Omega )
A4: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A5: ( (Partial_Union A1) . k = {} or (Partial_Union A1) . k = Omega ) ; ::_thesis: S1[k + 1]
reconsider k = k as Element of NAT by ORDINAL1:def_12;
A6: A1 . (k + 1) in rng A1 by NAT_1:51;
percases ( (Partial_Union A1) . (k + 1) = {} \/ (A1 . (k + 1)) or (Partial_Union A1) . (k + 1) = Omega \/ (A1 . (k + 1)) ) by A5, PROB_3:def_2;
suppose (Partial_Union A1) . (k + 1) = {} \/ (A1 . (k + 1)) ; ::_thesis: S1[k + 1]
hence  S1[k + 1] by A2, A6, TARSKI:def_2; ::_thesis: verum
end;
supposeA7: (Partial_Union A1) . (k + 1) = Omega \/ (A1 . (k + 1)) ; ::_thesis: S1[k + 1]
 ( A1 . (k + 1) = {} or A1 . (k + 1) = Omega ) by A2, A6, TARSKI:def_2;
hence  S1[k + 1] by A7; ::_thesis: verum
end;
end;
end;
 ( (Partial_Union A1) . 0 = A1 . 0 & A1 . 0 in rng A1 ) by NAT_1:51, PROB_3:def_2;
then A8: S1[ 0 ] by A2, TARSKI:def_2;
 for k being Nat holds S1[k] from NAT_1:sch_2(A8, A4);
hence  ( (Partial_Union A1) . n = {} or (Partial_Union A1) . n = Omega ) ; ::_thesis: verum
end;
 ( Union (Partial_Union A1) = {} or Union (Partial_Union A1) = Omega )
proof
percases ( for n being Element of NAT holds (Partial_Union A1) . n = {} or ex n being Element of NAT st not (Partial_Union A1) . n = {} ) ;
supposeA9: for n being Element of NAT holds (Partial_Union A1) . n = {} ; ::_thesis: ( Union (Partial_Union A1) = {} or Union (Partial_Union A1) = Omega )
 for x being set holds not x in Union (Partial_Union A1)
proof
let x be set ; ::_thesis: not x in Union (Partial_Union A1)
assume  x in Union (Partial_Union A1) ; ::_thesis: contradiction
then  ex n being Element of NAT st x in (Partial_Union A1) . n by PROB_1:12;
hence  contradiction by A9; ::_thesis: verum
end;
hence  ( Union (Partial_Union A1) = {} or Union (Partial_Union A1) = Omega ) by XBOOLE_0:def_1; ::_thesis: verum
end;
suppose not for n being Element of NAT holds (Partial_Union A1) . n = {} ; ::_thesis: ( Union (Partial_Union A1) = {} or Union (Partial_Union A1) = Omega )
then consider n being Element of NAT  such that
A10: (Partial_Union A1) . n <> {} ;
 (Partial_Union A1) . n = Omega by A3, A10;
then  for x being set st x in Omega holds
x in Union (Partial_Union A1) by PROB_1:12;
then  Omega c= Union (Partial_Union A1) by TARSKI:def_3;
hence  ( Union (Partial_Union A1) = {} or Union (Partial_Union A1) = Omega ) by XBOOLE_0:def_10; ::_thesis: verum
end;
end;
end;
then  ( Union A1 = {} or Union A1 = Omega ) by PROB_3:15;
hence  Union A1 in {{},Omega} by TARSKI:def_2; ::_thesis: verum
end;
A11: for A being Subset of Omega st A in {{},Omega} holds
A ` in {{},Omega}
proof
let A be Subset of Omega; ::_thesis: ( A in {{},Omega} implies A ` in {{},Omega} )
assume  A in {{},Omega} ; ::_thesis: A ` in {{},Omega}
then  ( A = {} or A = Omega ) by TARSKI:def_2;
then  ( A ` = Omega or A ` = {} ) by XBOOLE_1:37;
hence  A ` in {{},Omega} by TARSKI:def_2; ::_thesis: verum
end;
 ( {} in sigma X & Omega in sigma X ) by PROB_1:4, PROB_1:5;
then  for x being set st x in {{},Omega} holds
x in sigma X by TARSKI:def_2;
then A12: {{},Omega} c= sigma X by TARSKI:def_3;
assume  X = {} ; ::_thesis: sigma X = {{},Omega}
then A13: X c= {{},Omega} by XBOOLE_1:2;
 for x being set st x in {{},Omega} holds
x in bool Omega
proof
let x be set ; ::_thesis: ( x in {{},Omega} implies x in bool Omega )
assume  x in {{},Omega} ; ::_thesis: x in bool Omega
then  ( x = {} or x = Omega ) by TARSKI:def_2;
then  x c= Omega by XBOOLE_1:2;
hence  x in bool Omega ; ::_thesis: verum
end;
then  {{},Omega} is SigmaField of Omega by A1, A11, PROB_4:4, TARSKI:def_3;
then  sigma X c= {{},Omega} by A13, PROB_1:def_9;
hence  sigma X = {{},Omega} by A12, XBOOLE_0:def_10; ::_thesis: verum
end;

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let B be Subset of Sigma;
let P be Probability of Sigma;
func Indep (B,P) ->  Subset of Sigma means :Def1: :: KOLMOG01:def 1
 for a being Element of Sigma holds
( a in it iff for b being Element of B holds P . (a /\ b) = (P . a) * (P . b) );
existence
 ex b1 being Subset of Sigma st
for a being Element of Sigma holds
( a in b1 iff for b being Element of B holds P . (a /\ b) = (P . a) * (P . b) )
proof
defpred S1[ set ] means  for b being Element of B holds P . ($1 /\ b) = (P . $1) * (P . b);
consider X being set  such that
A1: for x being set holds
( x in X iff ( x in Sigma & S1[x] ) ) from XBOOLE_0:sch_1();
 for x being set st x in X holds
x in Sigma by A1;
then reconsider X = X as Subset of Sigma by TARSKI:def_3;
take  X ; ::_thesis: for a being Element of Sigma holds
( a in X iff for b being Element of B holds P . (a /\ b) = (P . a) * (P . b) )
let a be Element of Sigma; ::_thesis: ( a in X iff for b being Element of B holds P . (a /\ b) = (P . a) * (P . b) )
thus  ( a in X iff for b being Element of B holds P . (a /\ b) = (P . a) * (P . b) ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of Sigma st ( for a being Element of Sigma holds
( a in b1 iff for b being Element of B holds P . (a /\ b) = (P . a) * (P . b) ) ) & ( for a being Element of Sigma holds
( a in b2 iff for b being Element of B holds P . (a /\ b) = (P . a) * (P . b) ) ) holds
b1 = b2
proof
let X1, X2 be Subset of Sigma; ::_thesis: ( ( for a being Element of Sigma holds
( a in X1 iff for b being Element of B holds P . (a /\ b) = (P . a) * (P . b) ) ) & ( for a being Element of Sigma holds
( a in X2 iff for b being Element of B holds P . (a /\ b) = (P . a) * (P . b) ) ) implies X1 = X2 )
assume A2: for a being Element of Sigma holds
( a in X1 iff for b being Element of B holds P . (a /\ b) = (P . a) * (P . b) ) ; ::_thesis: ( ex a being Element of Sigma st
( ( a in X2 implies for b being Element of B holds P . (a /\ b) = (P . a) * (P . b) ) implies ( ( for b being Element of B holds P . (a /\ b) = (P . a) * (P . b) ) & not a in X2 ) ) or X1 = X2 )
assume A3: for a being Element of Sigma holds
( a in X2 iff for b being Element of B holds P . (a /\ b) = (P . a) * (P . b) ) ; ::_thesis: X1 = X2
now__::_thesis:_for_a_being_Element_of_Sigma_holds_
(_a_in_X1_iff_a_in_X2_)
let a be Element of Sigma; ::_thesis: ( a in X1 iff a in X2 )
 ( a in X1 iff for b being Element of B holds P . (a /\ b) = (P . a) * (P . b) ) by A2;
hence  ( a in X1 iff a in X2 ) by A3; ::_thesis: verum
end;
hence  X1 = X2 by SUBSET_1:3; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines Indep KOLMOG01:def_1_:_
 for Omega being non empty set
for Sigma being SigmaField of Omega
for B being Subset of Sigma
for P being Probability of Sigma
for b5 being Subset of Sigma holds
( b5 = Indep (B,P) iff for a being Element of Sigma holds
( a in b5 iff for b being Element of B holds P . (a /\ b) = (P . a) * (P . b) ) );

theorem Th4: :: KOLMOG01:4
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for B being non empty Subset of Sigma
for b being Element of B
for f being SetSequence of Sigma st ( for n being Element of NAT
for b being Element of B holds P . ((f . n) /\ b) = (P . (f . n)) * (P . b) ) & f is V65() holds
P . (b /\ (Union f)) = (P . b) * (P . (Union f))
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for B being non empty Subset of Sigma
for b being Element of B
for f being SetSequence of Sigma st ( for n being Element of NAT
for b being Element of B holds P . ((f . n) /\ b) = (P . (f . n)) * (P . b) ) & f is V65() holds
P . (b /\ (Union f)) = (P . b) * (P . (Union f))
let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma
for B being non empty Subset of Sigma
for b being Element of B
for f being SetSequence of Sigma st ( for n being Element of NAT
for b being Element of B holds P . ((f . n) /\ b) = (P . (f . n)) * (P . b) ) & f is V65() holds
P . (b /\ (Union f)) = (P . b) * (P . (Union f))
let P be Probability of Sigma; ::_thesis: for B being non empty Subset of Sigma
for b being Element of B
for f being SetSequence of Sigma st ( for n being Element of NAT
for b being Element of B holds P . ((f . n) /\ b) = (P . (f . n)) * (P . b) ) & f is V65() holds
P . (b /\ (Union f)) = (P . b) * (P . (Union f))
let B be non empty Subset of Sigma; ::_thesis: for b being Element of B
for f being SetSequence of Sigma st ( for n being Element of NAT
for b being Element of B holds P . ((f . n) /\ b) = (P . (f . n)) * (P . b) ) & f is V65() holds
P . (b /\ (Union f)) = (P . b) * (P . (Union f))
let b be Element of B; ::_thesis: for f being SetSequence of Sigma st ( for n being Element of NAT
for b being Element of B holds P . ((f . n) /\ b) = (P . (f . n)) * (P . b) ) & f is V65() holds
P . (b /\ (Union f)) = (P . b) * (P . (Union f))
let f be SetSequence of Sigma; ::_thesis: ( ( for n being Element of NAT
for b being Element of B holds P . ((f . n) /\ b) = (P . (f . n)) * (P . b) ) & f is V65() implies P . (b /\ (Union f)) = (P . b) * (P . (Union f)) )
reconsider b = b as Element of Sigma ;
reconsider r = P . b as real number ;
 for n being Element of NAT holds (seqIntersection (b,f)) . n is Event of Sigma
proof
let n be Element of NAT ; ::_thesis: (seqIntersection (b,f)) . n is Event of Sigma
 b /\ (f . n) is Event of Sigma ;
hence  (seqIntersection (b,f)) . n is Event of Sigma by DYNKIN:def_1; ::_thesis: verum
end;
then reconsider seqIntf = seqIntersection (b,f) as SetSequence of Sigma by PROB_1:25;
 for n being Element of NAT holds (seqIntersection (b,(Partial_Union f))) . n is Event of Sigma
proof
let n be Element of NAT ; ::_thesis: (seqIntersection (b,(Partial_Union f))) . n is Event of Sigma
 b /\ ((Partial_Union f) . n) is Event of Sigma ;
hence  (seqIntersection (b,(Partial_Union f))) . n is Event of Sigma by DYNKIN:def_1; ::_thesis: verum
end;
then reconsider seqIntPf = seqIntersection (b,(Partial_Union f)) as SetSequence of Sigma by PROB_1:25;
A1: b /\ (Union f) = b /\ (Union (Partial_Union f)) by PROB_3:15
.= Union seqIntPf by DYNKIN:10 ;
assume A2: for n being Element of NAT
for b being Element of B holds P . ((f . n) /\ b) = (P . (f . n)) * (P . b) ; ::_thesis: ( not f is V65() or P . (b /\ (Union f)) = (P . b) * (P . (Union f)) )
now__::_thesis:_for_n_being_Element_of_NAT_holds_(P_*_seqIntf)_._n_=_(r_(#)_(P_*_f))_._n
let n be Element of NAT ; ::_thesis: (P * seqIntf) . n = (r (#) (P * f)) . n
thus (P * seqIntf) . n = P . (seqIntf . n) by FUNCT_2:15
.= P . ((f . n) /\ b) by DYNKIN:def_1
.= (P . (f . n)) * (P . b) by A2
.= ((P * f) . n) * r by FUNCT_2:15
.= (r (#) (P * f)) . n by SEQ_1:9 ; ::_thesis: verum
end;
then A3: P * seqIntf = r (#) (P * f) by FUNCT_2:def_7;
A4: for x being set
for n, m being Element of NAT st n <= m & x in (Partial_Union f) . n holds
x in (Partial_Union f) . m
proof
let x be set ; ::_thesis: for n, m being Element of NAT st n <= m & x in (Partial_Union f) . n holds
x in (Partial_Union f) . m
reconsider Pf = Partial_Union f as SetSequence of Sigma ;
let n, m be Element of NAT ; ::_thesis: ( n <= m & x in (Partial_Union f) . n implies x in (Partial_Union f) . m )
assume A5: n <= m ; ::_thesis: ( not x in (Partial_Union f) . n or x in (Partial_Union f) . m )
assume A6: x in (Partial_Union f) . n ; ::_thesis: x in (Partial_Union f) . m
 Pf is non-descending by PROB_3:11;
then  Pf . n c= Pf . m by A5, PROB_1:def_5;
hence  x in (Partial_Union f) . m by A6; ::_thesis: verum
end;
 for n, m being Element of NAT st n <= m holds
(seqIntersection (b,(Partial_Union f))) . n c= (seqIntersection (b,(Partial_Union f))) . m
proof
let n, m be Element of NAT ; ::_thesis: ( n <= m implies (seqIntersection (b,(Partial_Union f))) . n c= (seqIntersection (b,(Partial_Union f))) . m )
assume A7: n <= m ; ::_thesis: (seqIntersection (b,(Partial_Union f))) . n c= (seqIntersection (b,(Partial_Union f))) . m
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (seqIntersection (b,(Partial_Union f))) . n or x in (seqIntersection (b,(Partial_Union f))) . m )
assume  x in (seqIntersection (b,(Partial_Union f))) . n ; ::_thesis: x in (seqIntersection (b,(Partial_Union f))) . m
then A8: x in b /\ ((Partial_Union f) . n) by DYNKIN:def_1;
then  x in (Partial_Union f) . n by XBOOLE_0:def_4;
then A9: x in (Partial_Union f) . m by A4, A7;
 x in b by A8, XBOOLE_0:def_4;
then  x in b /\ ((Partial_Union f) . m) by A9, XBOOLE_0:def_4;
hence  x in (seqIntersection (b,(Partial_Union f))) . m by DYNKIN:def_1; ::_thesis: verum
end;
then A10: seqIntersection (b,(Partial_Union f)) is non-descending by PROB_1:def_5;
assume A11: f is V65() ; ::_thesis: P . (b /\ (Union f)) = (P . b) * (P . (Union f))
then A12: seqIntersection (b,f) is V65() by DYNKIN:9;
 for n being Element of NAT holds (Partial_Union seqIntf) . n = (seqIntersection (b,(Partial_Union f))) . n
proof
defpred S1[ Nat] means (Partial_Union seqIntf) . $1 = (seqIntersection (b,(Partial_Union f))) . $1;
let n be Element of NAT ; ::_thesis: (Partial_Union seqIntf) . n = (seqIntersection (b,(Partial_Union f))) . n
A13: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A14: (Partial_Union seqIntf) . k = (seqIntersection (b,(Partial_Union f))) . k ; ::_thesis: S1[k + 1]
reconsider k = k as Element of NAT by ORDINAL1:def_12;
(Partial_Union seqIntf) . (k + 1) = ((Partial_Union seqIntf) . k) \/ (seqIntf . (k + 1)) by PROB_3:def_2
.= (b /\ ((Partial_Union f) . k)) \/ (seqIntf . (k + 1)) by A14, DYNKIN:def_1
.= (b /\ ((Partial_Union f) . k)) \/ (b /\ (f . (k + 1))) by DYNKIN:def_1
.= b /\ (((Partial_Union f) . k) \/ (f . (k + 1))) by XBOOLE_1:23
.= b /\ ((Partial_Union f) . (k + 1)) by PROB_3:def_2
.= (seqIntersection (b,(Partial_Union f))) . (k + 1) by DYNKIN:def_1 ;
hence  S1[k + 1] ; ::_thesis: verum
end;
(Partial_Union seqIntf) . 0 = seqIntf . 0 by PROB_3:def_2
.= b /\ (f . 0) by DYNKIN:def_1
.= b /\ ((Partial_Union f) . 0) by PROB_3:def_2
.= (seqIntersection (b,(Partial_Union f))) . 0 by DYNKIN:def_1 ;
then A15: S1[ 0 ] ;
 for k being Nat holds S1[k] from NAT_1:sch_2(A15, A13);
hence  (Partial_Union seqIntf) . n = (seqIntersection (b,(Partial_Union f))) . n ; ::_thesis: verum
end;
then P * (seqIntersection (b,(Partial_Union f))) = P * (Partial_Union seqIntf) by FUNCT_2:63
.= Partial_Sums (P * seqIntf) by A12, PROB_3:44
.= r (#) (Partial_Sums (P * f)) by A3, SERIES_1:9
.= r (#) (P * (Partial_Union f)) by A11, PROB_3:44 ;
then r * (lim (P * (Partial_Union f))) = lim (P * seqIntPf) by PROB_3:41, SEQ_2:8
.= P . (b /\ (Union f)) by A10, A1, PROB_2:10 ;
hence  P . (b /\ (Union f)) = (P . b) * (P . (Union f)) by PROB_3:41; ::_thesis: verum
end;

theorem Th5: :: KOLMOG01:5
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for B being non empty Subset of Sigma holds Indep (B,P) is Dynkin_System of Omega
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for B being non empty Subset of Sigma holds Indep (B,P) is Dynkin_System of Omega
let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma
for B being non empty Subset of Sigma holds Indep (B,P) is Dynkin_System of Omega
let P be Probability of Sigma; ::_thesis: for B being non empty Subset of Sigma holds Indep (B,P) is Dynkin_System of Omega
let B be non empty Subset of Sigma; ::_thesis: Indep (B,P) is Dynkin_System of Omega
A1: for b being Element of B holds P . ({} /\ b) = (P . {}) * (P . b)
proof
let b be Element of B; ::_thesis: P . ({} /\ b) = (P . {}) * (P . b)
reconsider b = b as Event of Sigma ;
 P . ({} /\ b) = 0 by VALUED_0:def_19;
hence  P . ({} /\ b) = (P . {}) * (P . b) ; ::_thesis: verum
end;
reconsider Indp = Indep (B,P) as Subset-Family of Omega by XBOOLE_1:1;
 {} is Element of Sigma by PROB_1:22;
then A2: {} in Indep (B,P) by A1, Def1;
A3: for g being SetSequence of Omega st rng g c= Indep (B,P) & g is V65() holds
Union g in Indep (B,P)
proof
let g be SetSequence of Omega; ::_thesis: ( rng g c= Indep (B,P) & g is V65() implies Union g in Indep (B,P) )
assume that
A4: rng g c= Indep (B,P) and
A5: g is V65() ; ::_thesis: Union g in Indep (B,P)
now__::_thesis:_for_n_being_Element_of_NAT_holds_g_._n_is_Event_of_Sigma
let n be Element of NAT ; ::_thesis: g . n is Event of Sigma
 g . n is Element of Sigma
proof
percases ( n in dom g or not n in dom g ) ;
suppose n in dom g ; ::_thesis: g . n is Element of Sigma
then  g . n in rng g by FUNCT_1:3;
hence  g . n is Element of Sigma by A4, TARSKI:def_3; ::_thesis: verum
end;
suppose not n in dom g ; ::_thesis: g . n is Element of Sigma
then  g . n = {} by FUNCT_1:def_2;
hence  g . n is Element of Sigma by PROB_1:4; ::_thesis: verum
end;
end;
end;
hence  g . n is Event of Sigma ; ::_thesis: verum
end;
then reconsider g = g as SetSequence of Sigma by PROB_1:25;
reconsider Ug = Union g as Element of Sigma by PROB_1:26;
 for n being Element of NAT
for b being Element of B holds P . ((g . n) /\ b) = (P . (g . n)) * (P . b)
proof
let n be Element of NAT ; ::_thesis: for b being Element of B holds P . ((g . n) /\ b) = (P . (g . n)) * (P . b)
let b be Element of B; ::_thesis: P . ((g . n) /\ b) = (P . (g . n)) * (P . b)
 g . n in Indep (B,P)
proof
percases ( n in dom g or not n in dom g ) ;
suppose n in dom g ; ::_thesis: g . n in Indep (B,P)
then  g . n in rng g by FUNCT_1:3;
hence  g . n in Indep (B,P) by A4; ::_thesis: verum
end;
suppose not n in dom g ; ::_thesis: g . n in Indep (B,P)
hence  g . n in Indep (B,P) by A2, FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
hence  P . ((g . n) /\ b) = (P . (g . n)) * (P . b) by Def1; ::_thesis: verum
end;
then  for b being Element of B holds P . (Ug /\ b) = (P . Ug) * (P . b) by A5, Th4;
hence  Union g in Indep (B,P) by Def1; ::_thesis: verum
end;
 for Z being Subset of Omega st Z in Indep (B,P) holds
Z ` in Indep (B,P)
proof
let Z be Subset of Omega; ::_thesis: ( Z in Indep (B,P) implies Z ` in Indep (B,P) )
assume A6: Z in Indep (B,P) ; ::_thesis: Z ` in Indep (B,P)
then reconsider Z = Z as Event of Sigma ;
reconsider Z9 = Z ` as Element of Sigma by PROB_1:20;
 for b being Element of B holds P . ((Z `) /\ b) = (P . (Z `)) * (P . b)
proof
let b be Element of B; ::_thesis: P . ((Z `) /\ b) = (P . (Z `)) * (P . b)
 P . (b /\ Z) = (P . b) * (P . Z) by A6, Def1;
then  b,Z are_independent_respect_to P by PROB_2:def_4;
then  b,([#] Sigma) \ Z are_independent_respect_to P by PROB_2:25;
hence  P . ((Z `) /\ b) = (P . (Z `)) * (P . b) by PROB_2:def_4; ::_thesis: verum
end;
then  Z9 in Indep (B,P) by Def1;
hence  Z ` in Indep (B,P) ; ::_thesis: verum
end;
then  Indp is Dynkin_System of Omega by A2, A3, DYNKIN:def_5;
hence  Indep (B,P) is Dynkin_System of Omega ; ::_thesis: verum
end;

theorem Th6: :: KOLMOG01:6
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for B being non empty Subset of Sigma
for A being Subset-Family of Omega st A is intersection_stable & A c= Indep (B,P) holds
sigma A c= Indep (B,P)
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for B being non empty Subset of Sigma
for A being Subset-Family of Omega st A is intersection_stable & A c= Indep (B,P) holds
sigma A c= Indep (B,P)
let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma
for B being non empty Subset of Sigma
for A being Subset-Family of Omega st A is intersection_stable & A c= Indep (B,P) holds
sigma A c= Indep (B,P)
let P be Probability of Sigma; ::_thesis: for B being non empty Subset of Sigma
for A being Subset-Family of Omega st A is intersection_stable & A c= Indep (B,P) holds
sigma A c= Indep (B,P)
let B be non empty Subset of Sigma; ::_thesis: for A being Subset-Family of Omega st A is intersection_stable & A c= Indep (B,P) holds
sigma A c= Indep (B,P)
reconsider Indp = Indep (B,P) as Dynkin_System of Omega by Th5;
let A be Subset-Family of Omega; ::_thesis: ( A is intersection_stable & A c= Indep (B,P) implies sigma A c= Indep (B,P) )
assume  ( A is intersection_stable & A c= Indep (B,P) ) ; ::_thesis: sigma A c= Indep (B,P)
then  sigma A c= Indp by DYNKIN:24;
hence  sigma A c= Indep (B,P) ; ::_thesis: verum
end;

theorem Th7: :: KOLMOG01:7
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A, B being non empty Subset of Sigma holds
( A c= Indep (B,P) iff for p, q being Event of Sigma st p in A & q in B holds
p,q are_independent_respect_to P )
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A, B being non empty Subset of Sigma holds
( A c= Indep (B,P) iff for p, q being Event of Sigma st p in A & q in B holds
p,q are_independent_respect_to P )
let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma
for A, B being non empty Subset of Sigma holds
( A c= Indep (B,P) iff for p, q being Event of Sigma st p in A & q in B holds
p,q are_independent_respect_to P )
let P be Probability of Sigma; ::_thesis: for A, B being non empty Subset of Sigma holds
( A c= Indep (B,P) iff for p, q being Event of Sigma st p in A & q in B holds
p,q are_independent_respect_to P )
let A, B be non empty Subset of Sigma; ::_thesis: ( A c= Indep (B,P) iff for p, q being Event of Sigma st p in A & q in B holds
p,q are_independent_respect_to P )
A1: now__::_thesis:_(_(_for_p,_q_being_Event_of_Sigma_st_p_in_A_&_q_in_B_holds_
p,q_are_independent_respect_to_P_)_implies_A_c=_Indep_(B,P)_)
assume A2: for p, q being Event of Sigma st p in A & q in B holds
p,q are_independent_respect_to P ; ::_thesis: A c= Indep (B,P)
thus  A c= Indep (B,P) ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in Indep (B,P) )
assume A3: x in A ; ::_thesis: x in Indep (B,P)
then reconsider x = x as Event of Sigma ;
 for b being Element of B holds P . (x /\ b) = (P . x) * (P . b)
proof
let b be Element of B; ::_thesis: P . (x /\ b) = (P . x) * (P . b)
reconsider b = b as Event of Sigma ;
 x,b are_independent_respect_to P by A2, A3;
hence  P . (x /\ b) = (P . x) * (P . b) by PROB_2:def_4; ::_thesis: verum
end;
hence  x in Indep (B,P) by Def1; ::_thesis: verum
end;
end;
now__::_thesis:_(_A_c=_Indep_(B,P)_implies_for_p,_q_being_Event_of_Sigma_st_p_in_A_&_q_in_B_holds_
p,q_are_independent_respect_to_P_)
assume A4: A c= Indep (B,P) ; ::_thesis: for p, q being Event of Sigma st p in A & q in B holds
p,q are_independent_respect_to P
thus  for p, q being Event of Sigma st p in A & q in B holds
p,q are_independent_respect_to P ::_thesis: verum
proof
let p, q be Event of Sigma; ::_thesis: ( p in A & q in B implies p,q are_independent_respect_to P )
assume that
A5: p in A and
A6: q in B ; ::_thesis: p,q are_independent_respect_to P
reconsider q = q as Element of B by A6;
reconsider p = p as Element of Sigma ;
 P . (p /\ q) = (P . p) * (P . q) by A4, A5, Def1;
hence  p,q are_independent_respect_to P by PROB_2:def_4; ::_thesis: verum
end;
end;
hence  ( A c= Indep (B,P) iff for p, q being Event of Sigma st p in A & q in B holds
p,q are_independent_respect_to P ) by A1; ::_thesis: verum
end;

theorem Th8: :: KOLMOG01:8
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A, B being non empty Subset of Sigma st A c= Indep (B,P) holds
B c= Indep (A,P)
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A, B being non empty Subset of Sigma st A c= Indep (B,P) holds
B c= Indep (A,P)
let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma
for A, B being non empty Subset of Sigma st A c= Indep (B,P) holds
B c= Indep (A,P)
let P be Probability of Sigma; ::_thesis: for A, B being non empty Subset of Sigma st A c= Indep (B,P) holds
B c= Indep (A,P)
let A, B be non empty Subset of Sigma; ::_thesis: ( A c= Indep (B,P) implies B c= Indep (A,P) )
assume A1: A c= Indep (B,P) ; ::_thesis: B c= Indep (A,P)
 for q, p being Event of Sigma st q in B & p in A holds
q,p are_independent_respect_to P
proof
let q, p be Event of Sigma; ::_thesis: ( q in B & p in A implies q,p are_independent_respect_to P )
assume A2: q in B ; ::_thesis: ( not p in A or q,p are_independent_respect_to P )
assume  p in A ; ::_thesis: q,p are_independent_respect_to P
then  p,q are_independent_respect_to P by A1, A2, Th7;
hence  q,p are_independent_respect_to P by PROB_2:19; ::_thesis: verum
end;
hence  B c= Indep (A,P) by Th7; ::_thesis: verum
end;

theorem Th9: :: KOLMOG01:9
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A being Subset-Family of Omega st A is non empty Subset of Sigma & A is intersection_stable holds
for B being non empty Subset of Sigma st B is intersection_stable & A c= Indep (B,P) holds
for D being Subset-Family of Omega
for sB being non empty Subset of Sigma st D = B & sigma D = sB holds
sigma A c= Indep (sB,P)
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A being Subset-Family of Omega st A is non empty Subset of Sigma & A is intersection_stable holds
for B being non empty Subset of Sigma st B is intersection_stable & A c= Indep (B,P) holds
for D being Subset-Family of Omega
for sB being non empty Subset of Sigma st D = B & sigma D = sB holds
sigma A c= Indep (sB,P)
let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma
for A being Subset-Family of Omega st A is non empty Subset of Sigma & A is intersection_stable holds
for B being non empty Subset of Sigma st B is intersection_stable & A c= Indep (B,P) holds
for D being Subset-Family of Omega
for sB being non empty Subset of Sigma st D = B & sigma D = sB holds
sigma A c= Indep (sB,P)
let P be Probability of Sigma; ::_thesis: for A being Subset-Family of Omega st A is non empty Subset of Sigma & A is intersection_stable holds
for B being non empty Subset of Sigma st B is intersection_stable & A c= Indep (B,P) holds
for D being Subset-Family of Omega
for sB being non empty Subset of Sigma st D = B & sigma D = sB holds
sigma A c= Indep (sB,P)
let A be Subset-Family of Omega; ::_thesis: ( A is non empty Subset of Sigma & A is intersection_stable implies for B being non empty Subset of Sigma st B is intersection_stable & A c= Indep (B,P) holds
for D being Subset-Family of Omega
for sB being non empty Subset of Sigma st D = B & sigma D = sB holds
sigma A c= Indep (sB,P) )
assume  A is non empty Subset of Sigma ; ::_thesis: ( not A is intersection_stable or for B being non empty Subset of Sigma st B is intersection_stable & A c= Indep (B,P) holds
for D being Subset-Family of Omega
for sB being non empty Subset of Sigma st D = B & sigma D = sB holds
sigma A c= Indep (sB,P) )
then reconsider sA = sigma A as non empty Subset of Sigma by PROB_1:def_9;
assume A1: A is intersection_stable ; ::_thesis: for B being non empty Subset of Sigma st B is intersection_stable & A c= Indep (B,P) holds
for D being Subset-Family of Omega
for sB being non empty Subset of Sigma st D = B & sigma D = sB holds
sigma A c= Indep (sB,P)
let B be non empty Subset of Sigma; ::_thesis: ( B is intersection_stable & A c= Indep (B,P) implies for D being Subset-Family of Omega
for sB being non empty Subset of Sigma st D = B & sigma D = sB holds
sigma A c= Indep (sB,P) )
assume A2: B is intersection_stable ; ::_thesis: ( not A c= Indep (B,P) or for D being Subset-Family of Omega
for sB being non empty Subset of Sigma st D = B & sigma D = sB holds
sigma A c= Indep (sB,P) )
assume  A c= Indep (B,P) ; ::_thesis: for D being Subset-Family of Omega
for sB being non empty Subset of Sigma st D = B & sigma D = sB holds
sigma A c= Indep (sB,P)
then A3: sigma A c= Indep (B,P) by A1, Th6;
let D be Subset-Family of Omega; ::_thesis: for sB being non empty Subset of Sigma st D = B & sigma D = sB holds
sigma A c= Indep (sB,P)
let sB be non empty Subset of Sigma; ::_thesis: ( D = B & sigma D = sB implies sigma A c= Indep (sB,P) )
assume A4: ( D = B & sigma D = sB ) ; ::_thesis: sigma A c= Indep (sB,P)
reconsider B = B as Subset-Family of Omega by XBOOLE_1:1;
 B c= Indep (sA,P) by A3, Th8;
then  sigma B c= Indep (sA,P) by A2, Th6;
hence  sigma A c= Indep (sB,P) by A4, Th8; ::_thesis: verum
end;

theorem Th10: :: KOLMOG01:10
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for E, F being Subset-Family of Omega st E is non empty Subset of Sigma & E is intersection_stable & F is non empty Subset of Sigma & F is intersection_stable & ( for p, q being Event of Sigma st p in E & q in F holds
p,q are_independent_respect_to P ) holds
for u, v being Event of Sigma st u in sigma E & v in sigma F holds
u,v are_independent_respect_to P
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for E, F being Subset-Family of Omega st E is non empty Subset of Sigma & E is intersection_stable & F is non empty Subset of Sigma & F is intersection_stable & ( for p, q being Event of Sigma st p in E & q in F holds
p,q are_independent_respect_to P ) holds
for u, v being Event of Sigma st u in sigma E & v in sigma F holds
u,v are_independent_respect_to P
let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma
for E, F being Subset-Family of Omega st E is non empty Subset of Sigma & E is intersection_stable & F is non empty Subset of Sigma & F is intersection_stable & ( for p, q being Event of Sigma st p in E & q in F holds
p,q are_independent_respect_to P ) holds
for u, v being Event of Sigma st u in sigma E & v in sigma F holds
u,v are_independent_respect_to P
let P be Probability of Sigma; ::_thesis: for E, F being Subset-Family of Omega st E is non empty Subset of Sigma & E is intersection_stable & F is non empty Subset of Sigma & F is intersection_stable & ( for p, q being Event of Sigma st p in E & q in F holds
p,q are_independent_respect_to P ) holds
for u, v being Event of Sigma st u in sigma E & v in sigma F holds
u,v are_independent_respect_to P
let E, F be Subset-Family of Omega; ::_thesis: ( E is non empty Subset of Sigma & E is intersection_stable & F is non empty Subset of Sigma & F is intersection_stable & ( for p, q being Event of Sigma st p in E & q in F holds
p,q are_independent_respect_to P ) implies for u, v being Event of Sigma st u in sigma E & v in sigma F holds
u,v are_independent_respect_to P )
assume A1: E is non empty Subset of Sigma ; ::_thesis: ( not E is intersection_stable or not F is non empty Subset of Sigma or not F is intersection_stable or ex p, q being Event of Sigma st
( p in E & q in F & not p,q are_independent_respect_to P ) or for u, v being Event of Sigma st u in sigma E & v in sigma F holds
u,v are_independent_respect_to P )
assume A2: E is intersection_stable ; ::_thesis: ( not F is non empty Subset of Sigma or not F is intersection_stable or ex p, q being Event of Sigma st
( p in E & q in F & not p,q are_independent_respect_to P ) or for u, v being Event of Sigma st u in sigma E & v in sigma F holds
u,v are_independent_respect_to P )
assume A3: F is non empty Subset of Sigma ; ::_thesis: ( not F is intersection_stable or ex p, q being Event of Sigma st
( p in E & q in F & not p,q are_independent_respect_to P ) or for u, v being Event of Sigma st u in sigma E & v in sigma F holds
u,v are_independent_respect_to P )
assume A4: F is intersection_stable ; ::_thesis: ( ex p, q being Event of Sigma st
( p in E & q in F & not p,q are_independent_respect_to P ) or for u, v being Event of Sigma st u in sigma E & v in sigma F holds
u,v are_independent_respect_to P )
assume A5: for p, q being Event of Sigma st p in E & q in F holds
p,q are_independent_respect_to P ; ::_thesis: for u, v being Event of Sigma st u in sigma E & v in sigma F holds
u,v are_independent_respect_to P
reconsider F = F as non empty Subset of Sigma by A3;
reconsider E = E as non empty Subset of Sigma by A1;
A6: E c= Indep (F,P) by A5, Th7;
reconsider E = E, F = F as Subset-Family of Omega ;
reconsider sF = sigma F as non empty Subset of Sigma by PROB_1:def_9;
 sigma E c= Indep (sF,P) by A2, A4, A6, Th9;
hence  for u, v being Event of Sigma st u in sigma E & v in sigma F holds
u,v are_independent_respect_to P by Th7; ::_thesis: verum
end;

definition
let I be set ;
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
mode ManySortedSigmaField of I,Sigma ->  Function of I,(bool Sigma) means :Def2: :: KOLMOG01:def 2
 for i being set st i in I holds
it . i is SigmaField of Omega;
existence
 ex b1 being Function of I,(bool Sigma) st
for i being set st i in I holds
b1 . i is SigmaField of Omega
proof
set F = I --> Sigma;
A1: rng (I --> Sigma) c= bool Sigma
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (I --> Sigma) or y in bool Sigma )
assume  y in rng (I --> Sigma) ; ::_thesis: y in bool Sigma
then  ex x being set st
( x in dom (I --> Sigma) & y = (I --> Sigma) . x ) by FUNCT_1:def_3;
then  y = Sigma by FUNCOP_1:7;
hence  y in bool Sigma by ZFMISC_1:def_1; ::_thesis: verum
end;
A2: for i being set st i in I holds
(I --> Sigma) . i is SigmaField of Omega by FUNCOP_1:7;
 dom (I --> Sigma) = I by FUNCOP_1:13;
then  I --> Sigma is Function of I,(bool Sigma) by A1, FUNCT_2:2;
hence  ex b1 being Function of I,(bool Sigma) st
for i being set st i in I holds
b1 . i is SigmaField of Omega by A2; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines ManySortedSigmaField KOLMOG01:def_2_:_
 for I being set
for Omega being non empty set
for Sigma being SigmaField of Omega
for b4 being Function of I,(bool Sigma) holds
( b4 is ManySortedSigmaField of I,Sigma iff for i being set st i in I holds
b4 . i is SigmaField of Omega );

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let P be Probability of Sigma;
let I be set ;
let A be Function of I,Sigma;
predA is_independent_wrt P means :Def3: :: KOLMOG01:def 3
 for e being one-to-one FinSequence of I st e <> {} holds
Product ((P * A) * e) = P . (meet (rng (A * e)));
end;

:: deftheorem Def3 defines is_independent_wrt KOLMOG01:def_3_:_
 for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for I being set
for A being Function of I,Sigma holds
( A is_independent_wrt P iff for e being one-to-one FinSequence of I st e <> {} holds
Product ((P * A) * e) = P . (meet (rng (A * e))) );

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let I be set ;
let J be Subset of I;
let F be ManySortedSigmaField of I,Sigma;
mode SigmaSection of J,F ->  Function of J,Sigma means :Def4: :: KOLMOG01:def 4
 for i being set st i in J holds
it . i in F . i;
existence
 ex b1 being Function of J,Sigma st
for i being set st i in J holds
b1 . i in F . i
proof
set f = J --> {};
A1: for i being set st i in J holds
(J --> {}) . i in F . i
proof
let i be set ; ::_thesis: ( i in J implies (J --> {}) . i in F . i )
assume A2: i in J ; ::_thesis: (J --> {}) . i in F . i
then  F . i is SigmaField of Omega by Def2;
then  {} in F . i by PROB_1:4;
hence  (J --> {}) . i in F . i by A2, FUNCOP_1:7; ::_thesis: verum
end;
A3: dom (J --> {}) = J by FUNCOP_1:13;
 rng (J --> {}) c= Sigma
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (J --> {}) or y in Sigma )
assume  y in rng (J --> {}) ; ::_thesis: y in Sigma
then consider i being set  such that
A4: ( i in J & y = (J --> {}) . i ) by A3, FUNCT_1:def_3;
 ( y in F . i & F . i in bool Sigma ) by A1, A4, FUNCT_2:5;
hence  y in Sigma ; ::_thesis: verum
end;
then  J --> {} is Function of J,Sigma by A3, FUNCT_2:2;
hence  ex b1 being Function of J,Sigma st
for i being set st i in J holds
b1 . i in F . i by A1; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines SigmaSection KOLMOG01:def_4_:_
 for Omega being non empty set
for Sigma being SigmaField of Omega
for I being set
for J being Subset of I
for F being ManySortedSigmaField of I,Sigma
for b6 being Function of J,Sigma holds
( b6 is SigmaSection of J,F iff for i being set st i in J holds
b6 . i in F . i );

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let P be Probability of Sigma;
let I be set ;
let F be ManySortedSigmaField of I,Sigma;
predF is_independent_wrt P means :Def5: :: KOLMOG01:def 5
 for E being finite Subset of I
for A being SigmaSection of E,F holds A is_independent_wrt P;
end;

:: deftheorem Def5 defines is_independent_wrt KOLMOG01:def_5_:_
 for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for I being set
for F being ManySortedSigmaField of I,Sigma holds
( F is_independent_wrt P iff for E being finite Subset of I
for A being SigmaSection of E,F holds A is_independent_wrt P );

definition
let I be set ;
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let F be ManySortedSigmaField of I,Sigma;
let J be Subset of I;
:: original: |
redefine funcF | J ->  Function of J,(bool Sigma);
coherence
 F | J is Function of J,(bool Sigma) by FUNCT_2:32;
end;

definition
let I be set ;
let J be Subset of I;
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let F be Function of J,(bool Sigma);
:: original: Union
redefine func Union F ->  Subset-Family of Omega;
coherence
 Union F is Subset-Family of Omega
proof
 for y being set st y in Union F holds
y in bool Omega
proof
let y be set ; ::_thesis: ( y in Union F implies y in bool Omega )
assume  y in Union F ; ::_thesis: y in bool Omega
then  ex i being set st
( i in dom F & y in F . i ) by CARD_5:2;
hence  y in bool Omega ; ::_thesis: verum
end;
hence  Union F is Subset-Family of Omega by TARSKI:def_3; ::_thesis: verum
end;
end;

definition
let I be set ;
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let F be ManySortedSigmaField of I,Sigma;
let J be Subset of I;
func sigUn (F,J) ->  SigmaField of Omega equals :: KOLMOG01:def 6
 sigma (Union (F | J));
coherence
 sigma (Union (F | J)) is SigmaField of Omega ;
end;

:: deftheorem  defines sigUn KOLMOG01:def_6_:_
 for I being set
for Omega being non empty set
for Sigma being SigmaField of Omega
for F being ManySortedSigmaField of I,Sigma
for J being Subset of I holds sigUn (F,J) = sigma (Union (F | J));

definition
let I be set ;
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let F be ManySortedSigmaField of I,Sigma;
func futSigmaFields (F,I) ->  Subset-Family of (bool Omega) means :Def7: :: KOLMOG01:def 7
 for S being Subset-Family of Omega holds
( S in it iff ex E being finite Subset of I st S = sigUn (F,(I \ E)) );
existence
 ex b1 being Subset-Family of (bool Omega) st
for S being Subset-Family of Omega holds
( S in b1 iff ex E being finite Subset of I st S = sigUn (F,(I \ E)) )
proof
defpred S1[ set ] means  ex E being finite Subset of I st $1 = sigUn (F,(I \ E));
consider X being set  such that
A1: for x being set holds
( x in X iff ( x in bool (bool Omega) & S1[x] ) ) from XBOOLE_0:sch_1();
A2: not X is empty
proof
set Ie = I \ ({} I);
 sigUn (F,(I \ ({} I))) in X by A1;
hence  not X is empty ; ::_thesis: verum
end;
 for x being set st x in X holds
x in bool (bool Omega) by A1;
then reconsider X = X as non empty Subset-Family of (bool Omega) by A2, TARSKI:def_3;
take  X ; ::_thesis: for S being Subset-Family of Omega holds
( S in X iff ex E being finite Subset of I st S = sigUn (F,(I \ E)) )
let S be Subset-Family of Omega; ::_thesis: ( S in X iff ex E being finite Subset of I st S = sigUn (F,(I \ E)) )
thus  ( S in X iff ex E being finite Subset of I st S = sigUn (F,(I \ E)) ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset-Family of (bool Omega) st ( for S being Subset-Family of Omega holds
( S in b1 iff ex E being finite Subset of I st S = sigUn (F,(I \ E)) ) ) & ( for S being Subset-Family of Omega holds
( S in b2 iff ex E being finite Subset of I st S = sigUn (F,(I \ E)) ) ) holds
b1 = b2
proof
let X1, X2 be Subset-Family of (bool Omega); ::_thesis: ( ( for S being Subset-Family of Omega holds
( S in X1 iff ex E being finite Subset of I st S = sigUn (F,(I \ E)) ) ) & ( for S being Subset-Family of Omega holds
( S in X2 iff ex E being finite Subset of I st S = sigUn (F,(I \ E)) ) ) implies X1 = X2 )
assume A3: for S being Subset-Family of Omega holds
( S in X1 iff ex E being finite Subset of I st S = sigUn (F,(I \ E)) ) ; ::_thesis: ( ex S being Subset-Family of Omega st
( ( S in X2 implies ex E being finite Subset of I st S = sigUn (F,(I \ E)) ) implies ( ex E being finite Subset of I st S = sigUn (F,(I \ E)) & not S in X2 ) ) or X1 = X2 )
assume A4: for S being Subset-Family of Omega holds
( S in X2 iff ex E being finite Subset of I st S = sigUn (F,(I \ E)) ) ; ::_thesis: X1 = X2
now__::_thesis:_for_S_being_Subset-Family_of_Omega_holds_
(_S_in_X1_iff_S_in_X2_)
let S be Subset-Family of Omega; ::_thesis: ( S in X1 iff S in X2 )
 ( S in X1 iff ex E being finite Subset of I st S = sigUn (F,(I \ E)) ) by A3;
hence  ( S in X1 iff S in X2 ) by A4; ::_thesis: verum
end;
hence  X1 = X2 by SUBSET_1:3; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines futSigmaFields KOLMOG01:def_7_:_
 for I being set
for Omega being non empty set
for Sigma being SigmaField of Omega
for F being ManySortedSigmaField of I,Sigma
for b5 being Subset-Family of (bool Omega) holds
( b5 = futSigmaFields (F,I) iff for S being Subset-Family of Omega holds
( S in b5 iff ex E being finite Subset of I st S = sigUn (F,(I \ E)) ) );

registration
let I be set ;
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let F be ManySortedSigmaField of I,Sigma;
cluster futSigmaFields (F,I) ->  non empty ;
coherence
 not futSigmaFields (F,I) is empty
proof
set Ie = I \ ({} I);
 sigUn (F,(I \ ({} I))) in futSigmaFields (F,I) by Def7;
hence  not futSigmaFields (F,I) is empty ; ::_thesis: verum
end;
end;

definition
let I be set ;
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let F be ManySortedSigmaField of I,Sigma;
func tailSigmaField (F,I) ->  Subset-Family of Omega equals :: KOLMOG01:def 8
 meet (futSigmaFields (F,I));
coherence
 meet (futSigmaFields (F,I)) is Subset-Family of Omega ;
end;

:: deftheorem  defines tailSigmaField KOLMOG01:def_8_:_
 for I being set
for Omega being non empty set
for Sigma being SigmaField of Omega
for F being ManySortedSigmaField of I,Sigma holds tailSigmaField (F,I) = meet (futSigmaFields (F,I));

registration
let I be set ;
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let F be ManySortedSigmaField of I,Sigma;
cluster tailSigmaField (F,I) ->  non empty ;
coherence
 not tailSigmaField (F,I) is empty
proof
 for X being set st X in futSigmaFields (F,I) holds
{} in X
proof
let X be set ; ::_thesis: ( X in futSigmaFields (F,I) implies {} in X )
assume  X in futSigmaFields (F,I) ; ::_thesis: {} in X
then  ex E being finite Subset of I st X = sigUn (F,(I \ E)) by Def7;
hence  {} in X by PROB_1:4; ::_thesis: verum
end;
hence  not tailSigmaField (F,I) is empty by SETFAM_1:def_1; ::_thesis: verum
end;
end;

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let I be non empty set ;
let J be non empty Subset of I;
let F be ManySortedSigmaField of I,Sigma;
func MeetSections (J,F) ->  Subset-Family of Omega means :Def9: :: KOLMOG01:def 9
 for x being Subset of Omega holds
( x in it iff ex E being non empty finite Subset of I ex f being SigmaSection of E,F st
( E c= J & x = meet (rng f) ) );
existence
 ex b1 being Subset-Family of Omega st
for x being Subset of Omega holds
( x in b1 iff ex E being non empty finite Subset of I ex f being SigmaSection of E,F st
( E c= J & x = meet (rng f) ) )
proof
defpred S1[ set ] means  ex E being non empty finite Subset of I ex f being SigmaSection of E,F st
( E c= J & $1 = meet (rng f) );
consider X being set  such that
A1: for x being set holds
( x in X iff ( x in bool Omega & S1[x] ) ) from XBOOLE_0:sch_1();
 for x being set st x in X holds
x in bool Omega by A1;
then reconsider X = X as Subset-Family of Omega by TARSKI:def_3;
take  X ; ::_thesis: for x being Subset of Omega holds
( x in X iff ex E being non empty finite Subset of I ex f being SigmaSection of E,F st
( E c= J & x = meet (rng f) ) )
let x be Subset of Omega; ::_thesis: ( x in X iff ex E being non empty finite Subset of I ex f being SigmaSection of E,F st
( E c= J & x = meet (rng f) ) )
thus  ( x in X iff ex E being non empty finite Subset of I ex f being SigmaSection of E,F st
( E c= J & x = meet (rng f) ) ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset-Family of Omega st ( for x being Subset of Omega holds
( x in b1 iff ex E being non empty finite Subset of I ex f being SigmaSection of E,F st
( E c= J & x = meet (rng f) ) ) ) & ( for x being Subset of Omega holds
( x in b2 iff ex E being non empty finite Subset of I ex f being SigmaSection of E,F st
( E c= J & x = meet (rng f) ) ) ) holds
b1 = b2
proof
let X1, X2 be Subset-Family of Omega; ::_thesis: ( ( for x being Subset of Omega holds
( x in X1 iff ex E being non empty finite Subset of I ex f being SigmaSection of E,F st
( E c= J & x = meet (rng f) ) ) ) & ( for x being Subset of Omega holds
( x in X2 iff ex E being non empty finite Subset of I ex f being SigmaSection of E,F st
( E c= J & x = meet (rng f) ) ) ) implies X1 = X2 )
assume A2: for x being Subset of Omega holds
( x in X1 iff ex E being non empty finite Subset of I ex f being SigmaSection of E,F st
( E c= J & x = meet (rng f) ) ) ; ::_thesis: ( ex x being Subset of Omega st
( ( x in X2 implies ex E being non empty finite Subset of I ex f being SigmaSection of E,F st
( E c= J & x = meet (rng f) ) ) implies ( ex E being non empty finite Subset of I ex f being SigmaSection of E,F st
( E c= J & x = meet (rng f) ) & not x in X2 ) ) or X1 = X2 )
assume A3: for x being Subset of Omega holds
( x in X2 iff ex E being non empty finite Subset of I ex f being SigmaSection of E,F st
( E c= J & x = meet (rng f) ) ) ; ::_thesis: X1 = X2
now__::_thesis:_for_x_being_Subset_of_Omega_holds_
(_x_in_X1_iff_x_in_X2_)
let x be Subset of Omega; ::_thesis: ( x in X1 iff x in X2 )
 ( x in X1 iff ex E being non empty finite Subset of I ex f being SigmaSection of E,F st
( E c= J & x = meet (rng f) ) ) by A2;
hence  ( x in X1 iff x in X2 ) by A3; ::_thesis: verum
end;
hence  X1 = X2 by SUBSET_1:3; ::_thesis: verum
end;
end;

:: deftheorem Def9 defines MeetSections KOLMOG01:def_9_:_
 for Omega being non empty set
for Sigma being SigmaField of Omega
for I being non empty set
for J being non empty Subset of I
for F being ManySortedSigmaField of I,Sigma
for b6 being Subset-Family of Omega holds
( b6 = MeetSections (J,F) iff for x being Subset of Omega holds
( x in b6 iff ex E being non empty finite Subset of I ex f being SigmaSection of E,F st
( E c= J & x = meet (rng f) ) ) );

theorem Th11: :: KOLMOG01:11
for Omega, I being non empty set
for Sigma being SigmaField of Omega
for F being ManySortedSigmaField of I,Sigma
for J being non empty Subset of I holds sigma (MeetSections (J,F)) = sigUn (F,J)
proof
let Omega, I be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for F being ManySortedSigmaField of I,Sigma
for J being non empty Subset of I holds sigma (MeetSections (J,F)) = sigUn (F,J)
let Sigma be SigmaField of Omega; ::_thesis: for F being ManySortedSigmaField of I,Sigma
for J being non empty Subset of I holds sigma (MeetSections (J,F)) = sigUn (F,J)
let F be ManySortedSigmaField of I,Sigma; ::_thesis: for J being non empty Subset of I holds sigma (MeetSections (J,F)) = sigUn (F,J)
let J be non empty Subset of I; ::_thesis: sigma (MeetSections (J,F)) = sigUn (F,J)
A1: Union (F | J) c= MeetSections (J,F)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Union (F | J) or x in MeetSections (J,F) )
assume  x in Union (F | J) ; ::_thesis: x in MeetSections (J,F)
then consider y being set  such that
A2: x in y and
A3: y in rng (F | J) by TARSKI:def_4;
consider i being set  such that
A4: i in dom (F | J) and
A5: y = (F | J) . i by A3, FUNCT_1:def_3;
reconsider x = x as Subset of Omega by A2, A5;
defpred S1[ set , set ] means ( $2 = x & $2 in F . $1 );
A6: {i} c= J by A4, ZFMISC_1:31;
then reconsider E = {i} as finite Subset of I by XBOOLE_1:1;
A7: for j being set st j in E holds
ex y being set st
( y in Sigma & S1[j,y] )
proof
let j be set ; ::_thesis: ( j in E implies ex y being set st
( y in Sigma & S1[j,y] ) )
assume A8: j in E ; ::_thesis: ex y being set st
( y in Sigma & S1[j,y] )
 i in I by A4, TARSKI:def_3;
then A9: F . i in bool Sigma by FUNCT_2:5;
take y = x; ::_thesis: ( y in Sigma & S1[j,y] )
 y in F . i by A2, A4, A5, FUNCT_1:49;
hence  ( y in Sigma & S1[j,y] ) by A8, A9, TARSKI:def_1; ::_thesis: verum
end;
consider g being Function of E,Sigma such that
A10: for j being set st j in E holds
S1[j,g . j] from FUNCT_2:sch_1(A7);
 for i being set st i in E holds
g . i in F . i by A10;
then reconsider g = g as SigmaSection of E,F by Def4;
 dom g = E by FUNCT_2:def_1;
then A11: rng g = {(g . i)} by FUNCT_1:4;
 i in E by TARSKI:def_1;
then x = g . i by A10
.= meet (rng g) by A11, SETFAM_1:10 ;
hence  x in MeetSections (J,F) by A6, Def9; ::_thesis: verum
end;
 MeetSections (J,F) c= sigma (Union (F | J))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in MeetSections (J,F) or x in sigma (Union (F | J)) )
assume  x in MeetSections (J,F) ; ::_thesis: x in sigma (Union (F | J))
then consider E being non empty finite Subset of I, f being SigmaSection of E,F such that
A12: E c= J and
A13: x = meet (rng f) by Def9;
reconsider Ee = E as Element of Fin E by FINSUB_1:def_5;
 for B being Element of Fin E holds meet (rng (f | B)) in sigma (Union (F | J))
proof
defpred S1[ set ] means  meet (rng (f | $1)) in sigma (Union (F | J));
let B be Element of Fin E; ::_thesis: meet (rng (f | B)) in sigma (Union (F | J))
A14: for B9 being Element of Fin E
for b being Element of E st S1[B9] & not b in B9 holds
S1[B9 \/ {b}]
proof
let B9 be Element of Fin E; ::_thesis: for b being Element of E st S1[B9] & not b in B9 holds
S1[B9 \/ {b}]
let b be Element of E; ::_thesis: ( S1[B9] & not b in B9 implies S1[B9 \/ {b}] )
assume that
A15: meet (rng (f | B9)) in sigma (Union (F | J)) and
 not b in B9 ; ::_thesis: S1[B9 \/ {b}]
reconsider rfb = rng (f | {b}) as set ;
reconsider rfB9 = rng (f | B9) as set ;
reconsider rfB9b = rng (f | (B9 \/ {b})) as set ;
 rng (f | (B9 \/ {b})) = rng ((f | B9) \/ (f | {b})) by RELAT_1:78;
then A16: rng (f | (B9 \/ {b})) = (rng (f | B9)) \/ (rng (f | {b})) by RELAT_1:12;
 dom (F | J) = J by FUNCT_2:def_1;
then A17: b in dom (F | J) by A12, TARSKI:def_3;
then  (F | J) . b in rng (F | J) by FUNCT_1:def_3;
then  F . b in rng (F | J) by A17, FUNCT_1:47;
then A18: F . b c= Union (F | J) by ZFMISC_1:74;
 Union (F | J) c= sigma (Union (F | J)) by PROB_1:def_9;
then A19: F . b c= sigma (Union (F | J)) by A18, XBOOLE_1:1;
 b is Element of dom f by FUNCT_2:def_1;
then A20: {b} = (dom f) /\ {b} by ZFMISC_1:46
.= dom (f | {b}) by RELAT_1:61 ;
then A21: b in dom (f | {b}) by TARSKI:def_1;
rng (f | {b}) = {((f | {b}) . b)} by A20, FUNCT_1:4
.= {(f . b)} by A21, FUNCT_1:47 ;
then  meet (rng (f | {b})) = f . b by SETFAM_1:10;
then A22: meet (rng (f | {b})) in F . b by Def4;
percases ( rng (f | B9) = {} or not rng (f | B9) = {} ) ;
suppose rng (f | B9) = {} ; ::_thesis: S1[B9 \/ {b}]
hence  S1[B9 \/ {b}] by A22, A19, A16; ::_thesis: verum
end;
supposeA23: not rng (f | B9) = {} ; ::_thesis: S1[B9 \/ {b}]
 ( dom f = E & b in {b} ) by FUNCT_2:def_1, TARSKI:def_1;
then  rfb <> {} by FUNCT_1:50;
then  meet rfB9b = (meet rfB9) /\ (meet rfb) by A16, A23, SETFAM_1:9;
then  meet (rng (f | (B9 \/ {b}))) is Event of sigma (Union (F | J)) by A15, A22, A19, PROB_1:19;
hence  S1[B9 \/ {b}] ; ::_thesis: verum
end;
end;
end;
 meet (rng (f | {})) = {} by SETFAM_1:def_1;
then A24: S1[ {}. E] by PROB_1:4;
 for B1 being Element of Fin E holds S1[B1] from SETWISEO:sch_2(A24, A14);
hence  meet (rng (f | B)) in sigma (Union (F | J)) ; ::_thesis: verum
end;
then  meet (rng (f | Ee)) in sigma (Union (F | J)) ;
hence  x in sigma (Union (F | J)) by A13, RELSET_1:19; ::_thesis: verum
end;
hence  sigma (MeetSections (J,F)) c= sigUn (F,J) by PROB_1:def_9; :: according to XBOOLE_0:def_10 ::_thesis: sigUn (F,J) c= sigma (MeetSections (J,F))
 MeetSections (J,F) c= sigma (MeetSections (J,F)) by PROB_1:def_9;
then  Union (F | J) c= sigma (MeetSections (J,F)) by A1, XBOOLE_1:1;
hence  sigUn (F,J) c= sigma (MeetSections (J,F)) by PROB_1:def_9; ::_thesis: verum
end;

theorem Th12: :: KOLMOG01:12
for I, Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for F being ManySortedSigmaField of I,Sigma
for J, K being non empty Subset of I st F is_independent_wrt P & J misses K holds
for a, c being Subset of Omega st a in MeetSections (J,F) & c in MeetSections (K,F) holds
P . (a /\ c) = (P . a) * (P . c)
proof
let I, Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for F being ManySortedSigmaField of I,Sigma
for J, K being non empty Subset of I st F is_independent_wrt P & J misses K holds
for a, c being Subset of Omega st a in MeetSections (J,F) & c in MeetSections (K,F) holds
P . (a /\ c) = (P . a) * (P . c)
let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma
for F being ManySortedSigmaField of I,Sigma
for J, K being non empty Subset of I st F is_independent_wrt P & J misses K holds
for a, c being Subset of Omega st a in MeetSections (J,F) & c in MeetSections (K,F) holds
P . (a /\ c) = (P . a) * (P . c)
let P be Probability of Sigma; ::_thesis: for F being ManySortedSigmaField of I,Sigma
for J, K being non empty Subset of I st F is_independent_wrt P & J misses K holds
for a, c being Subset of Omega st a in MeetSections (J,F) & c in MeetSections (K,F) holds
P . (a /\ c) = (P . a) * (P . c)
let F be ManySortedSigmaField of I,Sigma; ::_thesis: for J, K being non empty Subset of I st F is_independent_wrt P & J misses K holds
for a, c being Subset of Omega st a in MeetSections (J,F) & c in MeetSections (K,F) holds
P . (a /\ c) = (P . a) * (P . c)
let J, K be non empty Subset of I; ::_thesis: ( F is_independent_wrt P & J misses K implies for a, c being Subset of Omega st a in MeetSections (J,F) & c in MeetSections (K,F) holds
P . (a /\ c) = (P . a) * (P . c) )
assume A1: F is_independent_wrt P ; ::_thesis: ( not J misses K or for a, c being Subset of Omega st a in MeetSections (J,F) & c in MeetSections (K,F) holds
P . (a /\ c) = (P . a) * (P . c) )
reconsider Si = Sigma as set ;
assume A2: J misses K ; ::_thesis: for a, c being Subset of Omega st a in MeetSections (J,F) & c in MeetSections (K,F) holds
P . (a /\ c) = (P . a) * (P . c)
let a, c be Subset of Omega; ::_thesis: ( a in MeetSections (J,F) & c in MeetSections (K,F) implies P . (a /\ c) = (P . a) * (P . c) )
assume that
A3: a in MeetSections (J,F) and
A4: c in MeetSections (K,F) ; ::_thesis: P . (a /\ c) = (P . a) * (P . c)
consider E1 being non empty finite Subset of I, f1 being SigmaSection of E1,F such that
A5: E1 c= J and
A6: a = meet (rng f1) by A3, Def9;
A7: f1 is_independent_wrt P by A1, Def5;
consider E2 being non empty finite Subset of I, f2 being SigmaSection of E2,F such that
A8: E2 c= K and
A9: c = meet (rng f2) by A4, Def9;
A10: f2 is_independent_wrt P by A1, Def5;
reconsider rngf1 = rng f1, rngf2 = rng f2 as set ;
reconsider f1 = f1 as Function of E1,rngf1 by FUNCT_2:6;
reconsider f2 = f2 as Function of E2,rngf2 by FUNCT_2:6;
consider m being Nat such that
A11: E2, Seg m are_equipotent by FINSEQ_1:56;
consider e2 being Function such that
A12: e2 is one-to-one and
A13: dom e2 = Seg m and
A14: rng e2 = E2 by A11, WELLORD2:def_4;
A15: e2 <> {} by A14;
reconsider e2 = e2 as Function of (Seg m),E2 by A13, A14, FUNCT_2:1;
A16: e2 is FinSequence by A13, FINSEQ_1:def_2;
A17: rng (f2 * e2) = rng f2 by A14, FUNCT_2:14;
reconsider e2 = e2 as one-to-one FinSequence of E2 by A12, A14, A16, FINSEQ_1:def_4;
reconsider f2 = f2 as Function of E2,Si ;
deffunc H1( set ) ->  set = f2 . $1;
reconsider fe2 = f2 * e2 as FinSequence of Si ;
 rng e2 = dom f2 by A14, FUNCT_2:def_1;
then A18: len fe2 = len e2 by FINSEQ_2:29;
 E2 c= E1 \/ E2 by XBOOLE_1:7;
then A19: rng e2 c= E1 \/ E2 by XBOOLE_1:1;
defpred S1[ set ] means $1 in E1;
consider n being Nat such that
A20: E1, Seg n are_equipotent by FINSEQ_1:56;
consider e1 being Function such that
A21: e1 is one-to-one and
A22: dom e1 = Seg n and
A23: rng e1 = E1 by A20, WELLORD2:def_4;
A24: e1 <> {} by A23;
reconsider e1 = e1 as Function of (Seg n),E1 by A22, A23, FUNCT_2:1;
A25: e1 is FinSequence by A22, FINSEQ_1:def_2;
A26: rng (f1 * e1) = rng f1 by A23, FUNCT_2:14;
reconsider e1 = e1 as one-to-one FinSequence of E1 by A21, A23, A25, FINSEQ_1:def_4;
reconsider f1 = f1 as Function of E1,Si ;
deffunc H2( set ) ->  set = f1 . $1;
reconsider fe1 = f1 * e1 as FinSequence of Si ;
 rng e1 = dom f1 by A23, FUNCT_2:def_1;
then A27: len fe1 = len e1 by FINSEQ_2:29;
consider h being Function such that
A28: ( dom h = E1 \/ E2 & ( for i being set st i in E1 \/ E2 holds
( ( S1[i] implies h . i = H2(i) ) & ( not S1[i] implies h . i = H1(i) ) ) ) ) from PARTFUN1:sch_1();
 for x being set st x in dom (e1 ^ e2) holds
x in dom (h * (e1 ^ e2))
proof
let x be set ; ::_thesis: ( x in dom (e1 ^ e2) implies x in dom (h * (e1 ^ e2)) )
assume A29: x in dom (e1 ^ e2) ; ::_thesis: x in dom (h * (e1 ^ e2))
 rng (e1 ^ e2) = dom h by A23, A14, A28, FINSEQ_1:31;
then  (e1 ^ e2) . x in dom h by A29, FUNCT_1:3;
hence  x in dom (h * (e1 ^ e2)) by A29, FUNCT_1:11; ::_thesis: verum
end;
then A30: dom (e1 ^ e2) c= dom (h * (e1 ^ e2)) by TARSKI:def_3;
 for x being set st x in dom (h * (e1 ^ e2)) holds
x in dom (e1 ^ e2) by FUNCT_1:11;
then A31: dom (h * (e1 ^ e2)) c= dom (e1 ^ e2) by TARSKI:def_3;
A32: dom (fe1 ^ fe2) = Seg ((len fe1) + (len fe2)) by FINSEQ_1:def_7
.= dom (e1 ^ e2) by A27, A18, FINSEQ_1:def_7
.= dom (h * (e1 ^ e2)) by A31, A30, XBOOLE_0:def_10 ;
 for x being set st x in dom (fe1 ^ fe2) holds
(fe1 ^ fe2) . x = (h * (e1 ^ e2)) . x
proof
let x be set ; ::_thesis: ( x in dom (fe1 ^ fe2) implies (fe1 ^ fe2) . x = (h * (e1 ^ e2)) . x )
assume A33: x in dom (fe1 ^ fe2) ; ::_thesis: (fe1 ^ fe2) . x = (h * (e1 ^ e2)) . x
then reconsider x = x as Element of NAT ;
percases ( x in dom fe1 or not x in dom fe1 ) ;
supposeA34: x in dom fe1 ; ::_thesis: (fe1 ^ fe2) . x = (h * (e1 ^ e2)) . x
then A35: (fe1 ^ fe2) . x = fe1 . x by FINSEQ_1:def_7;
A36: E1 c= E1 \/ E2 by XBOOLE_1:7;
A37: x in dom e1 by A34, FUNCT_1:11;
then  e1 . x in E1 by A23, FUNCT_1:3;
then  h . (e1 . x) = f1 . (e1 . x) by A28, A36;
then A38: (fe1 ^ fe2) . x = h . (e1 . x) by A34, A35, FUNCT_1:12;
 (e1 ^ e2) . x = e1 . x by A37, FINSEQ_1:def_7;
hence  (fe1 ^ fe2) . x = (h * (e1 ^ e2)) . x by A32, A33, A38, FUNCT_1:12; ::_thesis: verum
end;
suppose not x in dom fe1 ; ::_thesis: (fe1 ^ fe2) . x = (h * (e1 ^ e2)) . x
then consider n being Nat such that
A39: n in dom fe2 and
A40: x = (len fe1) + n by A33, FINSEQ_1:25;
A41: n in dom e2 by A39, FUNCT_1:11;
then A42: e2 . n in E2 by A14, FUNCT_1:3;
 E1 /\ E2 c= J /\ K by A5, A8, XBOOLE_1:27;
then  E1 /\ E2 c= {} by A2, XBOOLE_0:def_7;
then  E1 /\ E2 = {} ;
then  E2 = (E2 \ E1) \/ {} by XBOOLE_1:51;
then A43: not e2 . n in E1 by A42, XBOOLE_0:def_5;
A44: E2 c= E1 \/ E2 by XBOOLE_1:7;
(fe1 ^ fe2) . x = fe2 . n by A39, A40, FINSEQ_1:def_7
.= f2 . (e2 . n) by A39, FUNCT_1:12
.= h . (e2 . n) by A28, A42, A43, A44
.= h . ((e1 ^ e2) . x) by A27, A40, A41, FINSEQ_1:def_7 ;
hence  (fe1 ^ fe2) . x = (h * (e1 ^ e2)) . x by A32, A33, FUNCT_1:12; ::_thesis: verum
end;
end;
end;
then A45: fe1 ^ fe2 = h * (e1 ^ e2) by A32, FUNCT_1:def_11;
 for i being set st i in E1 \/ E2 holds
h . i in Sigma
proof
let i be set ; ::_thesis: ( i in E1 \/ E2 implies h . i in Sigma )
assume A46: i in E1 \/ E2 ; ::_thesis: h . i in Sigma
percases ( i in E1 or not i in E1 ) ;
supposeA47: i in E1 ; ::_thesis: h . i in Sigma
then  h . i = f1 . i by A28, A46;
hence  h . i in Sigma by A47, FUNCT_2:5; ::_thesis: verum
end;
suppose not i in E1 ; ::_thesis: h . i in Sigma
then  ( h . i = f2 . i & i in E2 ) by A28, A46, XBOOLE_0:def_3;
hence  h . i in Sigma by FUNCT_2:5; ::_thesis: verum
end;
end;
end;
then reconsider h = h as Function of (E1 \/ E2),Sigma by A28, FUNCT_2:3;
 for i being set st i in E1 \/ E2 holds
h . i in F . i
proof
let i be set ; ::_thesis: ( i in E1 \/ E2 implies h . i in F . i )
assume A48: i in E1 \/ E2 ; ::_thesis: h . i in F . i
percases ( i in E1 or not i in E1 ) ;
supposeA49: i in E1 ; ::_thesis: h . i in F . i
then  f1 . i in F . i by Def4;
hence  h . i in F . i by A28, A48, A49; ::_thesis: verum
end;
supposeA50: not i in E1 ; ::_thesis: h . i in F . i
then  i in E2 by A48, XBOOLE_0:def_3;
then  f2 . i in F . i by Def4;
hence  h . i in F . i by A28, A48, A50; ::_thesis: verum
end;
end;
end;
then reconsider h = h as SigmaSection of E1 \/ E2,F by Def4;
A51: h is_independent_wrt P by A1, Def5;
 E1 c= E1 \/ E2 by XBOOLE_1:7;
then A52: rng e1 c= E1 \/ E2 by XBOOLE_1:1;
reconsider Pfe1 = (P * f1) * e1, Pfe2 = (P * f2) * e2 as FinSequence of REAL by FINSEQ_2:32;
reconsider e2 = e2 as FinSequence of E1 \/ E2 by A19, FINSEQ_1:def_4;
reconsider e1 = e1 as FinSequence of E1 \/ E2 by A52, FINSEQ_1:def_4;
 E1 /\ E2 c= J /\ K by A5, A8, XBOOLE_1:27;
then  E1 /\ E2 c= {} by A2, XBOOLE_0:def_7;
then  E1 /\ E2 = {} ;
then  rng e1 misses rng e2 by A23, A14, XBOOLE_0:def_7;
then reconsider e12 = e1 ^ e2 as one-to-one FinSequence of E1 \/ E2 by FINSEQ_3:91;
reconsider e1 = e1 as one-to-one FinSequence of E1 ;
reconsider fe1 = fe1 as FinSequence of Si ;
reconsider e2 = e2 as FinSequence of E2 ;
reconsider fe2 = fe2 as FinSequence of Si ;
reconsider f1 = f1 as Function of E1,Sigma ;
reconsider f2 = f2 as Function of E2,Sigma ;
reconsider P = P as Function of Si,REAL ;
A53: (P * h) * e12 = P * (h * (e1 ^ e2)) by RELAT_1:36
.= (P * fe1) ^ (P * fe2) by A45, FINSEQOP:9 ;
A54: ( P * fe1 = Pfe1 & P * fe2 = Pfe2 ) by RELAT_1:36;
reconsider P = P as Function of Sigma,REAL ;
A55: Product ((P * f1) * e1) = P . (meet (rng (f1 * e1))) by A24, A7, Def3;
P . (a /\ c) = P . (meet ((rng f1) \/ (rng f2))) by A6, A9, SETFAM_1:9
.= P . (meet (rng (fe1 ^ fe2))) by A26, A17, FINSEQ_1:31
.= Product (Pfe1 ^ Pfe2) by A24, A45, A51, A53, A54, Def3
.= (Product Pfe1) * (Product Pfe2) by RVSUM_1:97
.= (P . a) * (P . c) by A6, A9, A15, A10, A26, A17, A55, Def3 ;
hence  P . (a /\ c) = (P . a) * (P . c) ; ::_thesis: verum
end;

theorem Th13: :: KOLMOG01:13
for Omega, I being non empty set
for Sigma being SigmaField of Omega
for F being ManySortedSigmaField of I,Sigma
for J being non empty Subset of I holds MeetSections (J,F) is non empty Subset of Sigma
proof
let Omega, I be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for F being ManySortedSigmaField of I,Sigma
for J being non empty Subset of I holds MeetSections (J,F) is non empty Subset of Sigma
let Sigma be SigmaField of Omega; ::_thesis: for F being ManySortedSigmaField of I,Sigma
for J being non empty Subset of I holds MeetSections (J,F) is non empty Subset of Sigma
let F be ManySortedSigmaField of I,Sigma; ::_thesis: for J being non empty Subset of I holds MeetSections (J,F) is non empty Subset of Sigma
let J be non empty Subset of I; ::_thesis: MeetSections (J,F) is non empty Subset of Sigma
A1: MeetSections (J,F) c= Sigma
proof
let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in MeetSections (J,F) or X in Sigma )
assume  X in MeetSections (J,F) ; ::_thesis: X in Sigma
then consider E being non empty finite Subset of I, f being SigmaSection of E,F such that
 E c= J and
A2: X = meet (rng f) by Def9;
reconsider Ee = E as Element of Fin E by FINSUB_1:def_5;
 for B being Element of Fin E holds meet (rng (f | B)) in Sigma
proof
defpred S1[ set ] means  meet (rng (f | $1)) in Sigma;
let B be Element of Fin E; ::_thesis: meet (rng (f | B)) in Sigma
A3: for B9 being Element of Fin E
for b being Element of E st S1[B9] & not b in B9 holds
S1[B9 \/ {b}]
proof
let B9 be Element of Fin E; ::_thesis: for b being Element of E st S1[B9] & not b in B9 holds
S1[B9 \/ {b}]
let b be Element of E; ::_thesis: ( S1[B9] & not b in B9 implies S1[B9 \/ {b}] )
assume that
A4: meet (rng (f | B9)) in Sigma and
 not b in B9 ; ::_thesis: S1[B9 \/ {b}]
A5: rng (f | (B9 \/ {b})) = rng ((f | B9) \/ (f | {b})) by RELAT_1:78
.= (rng (f | B9)) \/ (rng (f | {b})) by RELAT_1:12 ;
 ( dom f = E & b in {b} ) by FUNCT_2:def_1, TARSKI:def_1;
then A6: f . b in rng (f | {b}) by FUNCT_1:50;
A7: b is Element of dom f by FUNCT_2:def_1;
then  (dom f) /\ {b} = {b} by ZFMISC_1:46;
then  dom (f | {b}) = {b} by RELAT_1:61;
then A8: rng (f | {b}) = {((f | {b}) . b)} by FUNCT_1:4;
 b in {b} by TARSKI:def_1;
then  b in dom (f | {b}) by A7, RELAT_1:57;
then  rng (f | {b}) = {(f . b)} by A8, FUNCT_1:47;
then A9: meet (rng (f | {b})) is Event of Sigma by SETFAM_1:10;
percases ( rng (f | B9) = {} or not rng (f | B9) = {} ) ;
suppose rng (f | B9) = {} ; ::_thesis: S1[B9 \/ {b}]
hence  S1[B9 \/ {b}] by A9, A5; ::_thesis: verum
end;
suppose not rng (f | B9) = {} ; ::_thesis: S1[B9 \/ {b}]
then  meet (rng (f | (B9 \/ {b}))) = (meet (rng (f | B9))) /\ (meet (rng (f | {b}))) by A5, A6, SETFAM_1:9;
then  meet (rng (f | (B9 \/ {b}))) is Event of Sigma by A4, A9, PROB_1:19;
hence  S1[B9 \/ {b}] ; ::_thesis: verum
end;
end;
end;
 meet (rng (f | {})) = {} by SETFAM_1:def_1;
then A10: S1[ {}. E] by PROB_1:4;
 for B1 being Element of Fin E holds S1[B1] from SETWISEO:sch_2(A10, A3);
hence  meet (rng (f | B)) in Sigma ; ::_thesis: verum
end;
then  meet (rng (f | Ee)) in Sigma ;
hence  X in Sigma by A2, RELSET_1:19; ::_thesis: verum
end;
 MeetSections (J,F) is non empty set
proof
set E = the non empty finite Subset of J;
consider f being Function such that
A11: dom f = the non empty finite Subset of J and
A12: rng f = {{}} by FUNCT_1:5;
reconsider E = the non empty finite Subset of J as non empty finite Subset of I by XBOOLE_1:1;
A13: meet (rng f) = {} by A12, SETFAM_1:10;
 rng f c= Sigma
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in Sigma )
assume  y in rng f ; ::_thesis: y in Sigma
then  y = {} by A12, TARSKI:def_1;
hence  y in Sigma by PROB_1:4; ::_thesis: verum
end;
then reconsider f = f as Function of E,Sigma by A11, FUNCT_2:2;
 for i being set st i in E holds
f . i in F . i
proof
let i be set ; ::_thesis: ( i in E implies f . i in F . i )
assume A14: i in E ; ::_thesis: f . i in F . i
then reconsider Fi = F . i as SigmaField of Omega by Def2;
 f . i in rng f by A11, A14, FUNCT_1:def_3;
then  f . i = {} by A12, TARSKI:def_1;
then  f . i in Fi by PROB_1:4;
hence  f . i in F . i ; ::_thesis: verum
end;
then reconsider f = f as SigmaSection of E,F by Def4;
reconsider mrf = meet (rng f) as Subset of Omega by A13, XBOOLE_1:2;
 mrf in MeetSections (J,F) by Def9;
hence  MeetSections (J,F) is non empty set ; ::_thesis: verum
end;
hence  MeetSections (J,F) is non empty Subset of Sigma by A1; ::_thesis: verum
end;

registration
let I, Omega be non empty set ;
let Sigma be SigmaField of Omega;
let F be ManySortedSigmaField of I,Sigma;
let J be non empty Subset of I;
cluster MeetSections (J,F) ->  intersection_stable ;
coherence
 MeetSections (J,F) is intersection_stable
proof
 for x, X being set st x in MeetSections (J,F) & X in MeetSections (J,F) holds
x /\ X in MeetSections (J,F)
proof
let x, X be set ; ::_thesis: ( x in MeetSections (J,F) & X in MeetSections (J,F) implies x /\ X in MeetSections (J,F) )
assume that
A1: x in MeetSections (J,F) and
A2: X in MeetSections (J,F) ; ::_thesis: x /\ X in MeetSections (J,F)
consider E being non empty finite Subset of I, f being SigmaSection of E,F such that
A3: E c= J and
A4: x = meet (rng f) by A1, Def9;
defpred S1[ set ] means I in E;
deffunc H1( set ) ->  set = f . I;
consider E9 being non empty finite Subset of I, f9 being SigmaSection of E9,F such that
A5: E9 c= J and
A6: X = meet (rng f9) by A2, Def9;
deffunc H2( set ) ->  set = f9 . I;
defpred S2[ set ] means I in (E \ E9) \/ (E9 \ E);
deffunc H3( set ) ->  set = (f . I) /\ (f9 . I);
consider h being Function such that
A7: ( dom h = E \/ E9 & ( for i being set st i in E \/ E9 holds
( ( S1[i] implies h . i = H1(i) ) & ( not S1[i] implies h . i = H2(i) ) ) ) ) from PARTFUN1:sch_1();
deffunc H4( set ) ->  set = h . I;
consider g being Function such that
A8: ( dom g = E \/ E9 & ( for i being set st i in E \/ E9 holds
( ( S2[i] implies g . i = H4(i) ) & ( not S2[i] implies g . i = H3(i) ) ) ) ) from PARTFUN1:sch_1();
A9: for i being set st i in E \/ E9 holds
g . i in F . i
proof
let i be set ; ::_thesis: ( i in E \/ E9 implies g . i in F . i )
assume A10: i in E \/ E9 ; ::_thesis: g . i in F . i
percases ( i in (E \ E9) \/ (E9 \ E) or not i in (E \ E9) \/ (E9 \ E) ) ;
supposeA11: i in (E \ E9) \/ (E9 \ E) ; ::_thesis: g . i in F . i
 h . i in F . i
proof
percases ( i in E or not i in E ) ;
supposeA12: i in E ; ::_thesis: h . i in F . i
then  h . i = f . i by A7, A10;
hence  h . i in F . i by A12, Def4; ::_thesis: verum
end;
suppose not i in E ; ::_thesis: h . i in F . i
then  ( i in E9 & h . i = f9 . i ) by A7, A10, XBOOLE_0:def_3;
hence  h . i in F . i by Def4; ::_thesis: verum
end;
end;
end;
hence  g . i in F . i by A8, A10, A11; ::_thesis: verum
end;
supposeA13: not i in (E \ E9) \/ (E9 \ E) ; ::_thesis: g . i in F . i
reconsider Fi = F . i as SigmaField of Omega by A10, Def2;
 not i in E \+\ E9 by A13;
then  ( i in E iff i in E9 ) by XBOOLE_0:1;
then  ( f . i in F . i & f9 . i in F . i ) by A10, Def4, XBOOLE_0:def_3;
then A14: (f . i) /\ (f9 . i) is Event of Fi by PROB_1:19;
 g . i = (f . i) /\ (f9 . i) by A8, A10, A13;
hence  g . i in F . i by A14; ::_thesis: verum
end;
end;
end;
 rng g c= Sigma
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng g or y in Sigma )
assume  y in rng g ; ::_thesis: y in Sigma
then consider i being set  such that
A15: ( i in dom g & y = g . i ) by FUNCT_1:def_3;
 ( y in F . i & F . i in bool Sigma ) by A8, A9, A15, FUNCT_2:5;
hence  y in Sigma ; ::_thesis: verum
end;
then  g is Function of (E \/ E9),Sigma by A8, FUNCT_2:2;
then reconsider g = g as SigmaSection of E \/ E9,F by A9, Def4;
A16: x /\ X = meet (rng g)
proof
A17: meet (rng (g | (E /\ E9))) = (meet (rng (f | (E /\ E9)))) /\ (meet (rng (f9 | (E /\ E9))))
proof
percases ( E /\ E9 = {} or not E /\ E9 = {} ) ;
supposeA18: E /\ E9 = {} ; ::_thesis: meet (rng (g | (E /\ E9))) = (meet (rng (f | (E /\ E9)))) /\ (meet (rng (f9 | (E /\ E9))))
then A19: ( meet (rng (f | (E /\ E9))) = meet (rng {}) & meet (rng (f9 | (E /\ E9))) = meet (rng {}) ) ;
meet (rng (g | (E /\ E9))) = meet (rng {}) by A18
.= {} by SETFAM_1:def_1 ;
hence  meet (rng (g | (E /\ E9))) = (meet (rng (f | (E /\ E9)))) /\ (meet (rng (f9 | (E /\ E9)))) by A19, SETFAM_1:def_1; ::_thesis: verum
end;
suppose not E /\ E9 = {} ; ::_thesis: meet (rng (g | (E /\ E9))) = (meet (rng (f | (E /\ E9)))) /\ (meet (rng (f9 | (E /\ E9))))
then reconsider EnE9 = E /\ E9 as non empty set ;
reconsider EE9 = EnE9 as Element of Fin EnE9 by FINSUB_1:def_5;
 for B being Element of Fin EnE9 holds meet (rng (g | B)) = (meet (rng (f | B))) /\ (meet (rng (f9 | B)))
proof
defpred S3[ set ] means  meet (rng (g | I)) = (meet (rng (f | I))) /\ (meet (rng (f9 | I)));
let B be Element of Fin EnE9; ::_thesis: meet (rng (g | B)) = (meet (rng (f | B))) /\ (meet (rng (f9 | B)))
A20: for B9 being Element of Fin EnE9
for b being Element of EnE9 st S3[B9] & not b in B9 holds
S3[B9 \/ {b}]
proof
let B9 be Element of Fin EnE9; ::_thesis: for b being Element of EnE9 st S3[B9] & not b in B9 holds
S3[B9 \/ {b}]
let b be Element of EnE9; ::_thesis: ( S3[B9] & not b in B9 implies S3[B9 \/ {b}] )
assume that
A21: meet (rng (g | B9)) = (meet (rng (f | B9))) /\ (meet (rng (f9 | B9))) and
 not b in B9 ; ::_thesis: S3[B9 \/ {b}]
A22: dom (f | {b}) = (dom f) /\ {b} by RELAT_1:61;
 dom f = E by FUNCT_2:def_1;
then A23: E /\ E9 c= dom f by XBOOLE_1:17;
then  b in dom f by TARSKI:def_3;
then A24: rng (f | {b}) = {((f | {b}) . b)} by A22, FUNCT_1:4, ZFMISC_1:46;
 b in (E \ (E \/ E9)) \/ ((E /\ E) /\ E9) by XBOOLE_0:def_3;
then  b in E \ (E \+\ E9) by XBOOLE_1:102;
then A25: not b in E \+\ E9 by XBOOLE_0:def_5;
A26: b in {b} by TARSKI:def_1;
 b in dom f by A23, TARSKI:def_3;
then  b in dom (f | {b}) by A26, RELAT_1:57;
then A27: rng (f | {b}) = {(f . b)} by A24, FUNCT_1:47;
then A28: meet (rng (f | {b})) = f . b by SETFAM_1:10;
A29: E /\ E9 c= E by XBOOLE_1:17;
A30: dom (f9 | {b}) = (dom f9) /\ {b} by RELAT_1:61;
 dom f9 = E9 by FUNCT_2:def_1;
then A31: E /\ E9 c= dom f9 by XBOOLE_1:17;
then  b in dom f9 by TARSKI:def_3;
then A32: rng (f9 | {b}) = {((f9 | {b}) . b)} by A30, FUNCT_1:4, ZFMISC_1:46;
 b in dom f9 by A31, TARSKI:def_3;
then  b in dom (f9 | {b}) by A26, RELAT_1:57;
then A33: rng (f9 | {b}) = {(f9 . b)} by A32, FUNCT_1:47;
then A34: meet (rng (f9 | {b})) = f9 . b by SETFAM_1:10;
A35: for g being Function
for B9, b being set holds meet (rng (g | (B9 \/ {b}))) = meet ((rng (g | B9)) \/ (rng (g | {b})))
proof
let g be Function; ::_thesis: for B9, b being set holds meet (rng (g | (B9 \/ {b}))) = meet ((rng (g | B9)) \/ (rng (g | {b})))
let B9, b be set ; ::_thesis: meet (rng (g | (B9 \/ {b}))) = meet ((rng (g | B9)) \/ (rng (g | {b})))
 rng (g | (B9 \/ {b})) = rng ((g | B9) \/ (g | {b})) by RELAT_1:78;
hence  meet (rng (g | (B9 \/ {b}))) = meet ((rng (g | B9)) \/ (rng (g | {b}))) by RELAT_1:12; ::_thesis: verum
end;
 E c= dom g by A8, XBOOLE_1:7;
then A36: E /\ E9 c= dom g by A29, XBOOLE_1:1;
then  b is Element of dom g by TARSKI:def_3;
then  (dom g) /\ {b} = {b} by ZFMISC_1:46;
then  dom (g | {b}) = {b} by RELAT_1:61;
then A37: rng (g | {b}) = {((g | {b}) . b)} by FUNCT_1:4;
 ( b in {b} & b in dom g ) by A36, TARSKI:def_1, TARSKI:def_3;
then  b in dom (g | {b}) by RELAT_1:57;
then A38: rng (g | {b}) = {(g . b)} by A37, FUNCT_1:47;
then A39: meet (rng (g | {b})) = g . b by SETFAM_1:10;
 E c= E \/ E9 by XBOOLE_1:7;
then A40: E /\ E9 c= E \/ E9 by A29, XBOOLE_1:1;
then  b in E \/ E9 by TARSKI:def_3;
then A41: g . b = (f . b) /\ (f9 . b) by A8, A25;
percases ( B9 = {} or B9 <> {} ) ;
suppose B9 = {} ; ::_thesis: S3[B9 \/ {b}]
hence  S3[B9 \/ {b}] by A28, A34, A41, A38, SETFAM_1:10; ::_thesis: verum
end;
supposeA42: B9 <> {} ; ::_thesis: S3[B9 \/ {b}]
set z = the Element of B9;
 B9 c= E /\ E9 by FINSUB_1:def_5;
then A43: B9 c= E \/ E9 by A40, XBOOLE_1:1;
 the Element of B9 in B9 by A42;
then  dom (g | B9) <> {} by A8, A43;
then  rng (g | B9) <> {} by RELAT_1:42;
then  meet ((rng (g | B9)) \/ (rng (g | {b}))) = (meet (rng (g | B9))) /\ (meet (rng (g | {b}))) by A37, SETFAM_1:9;
then A44: meet (rng (g | (B9 \/ {b}))) = ((meet (rng (f | B9))) /\ (meet (rng (f9 | B9)))) /\ (g . b) by A21, A35, A39
.= (meet (rng (f | B9))) /\ ((meet (rng (f9 | B9))) /\ ((f . b) /\ (f9 . b))) by A41, XBOOLE_1:16
.= (meet (rng (f | B9))) /\ ((f . b) /\ ((meet (rng (f9 | B9))) /\ (f9 . b))) by XBOOLE_1:16
.= ((meet (rng (f | B9))) /\ (f . b)) /\ ((meet (rng (f9 | B9))) /\ (f9 . b)) by XBOOLE_1:16 ;
 ( B9 c= E /\ E9 & E /\ E9 c= E9 ) by FINSUB_1:def_5, XBOOLE_1:17;
then  B9 c= E9 by XBOOLE_1:1;
then A45: B9 c= dom f9 by FUNCT_2:def_1;
 ( B9 c= E /\ E9 & E /\ E9 c= E ) by FINSUB_1:def_5, XBOOLE_1:17;
then  B9 c= E by XBOOLE_1:1;
then A46: B9 c= dom f by FUNCT_2:def_1;
meet (rng (f | (B9 \/ {b}))) = meet ((rng (f | B9)) \/ (rng (f | {b}))) by A35
.= (meet (rng (f | B9))) /\ (meet (rng (f | {b}))) by A24, A42, A46, SETFAM_1:9 ;
then A47: (meet (rng (f | B9))) /\ (f . b) = meet (rng (f | (B9 \/ {b}))) by A27, SETFAM_1:10;
meet (rng (f9 | (B9 \/ {b}))) = meet ((rng (f9 | B9)) \/ (rng (f9 | {b}))) by A35
.= (meet (rng (f9 | B9))) /\ (meet (rng (f9 | {b}))) by A32, A42, A45, SETFAM_1:9 ;
hence  S3[B9 \/ {b}] by A33, A44, A47, SETFAM_1:10; ::_thesis: verum
end;
end;
end;
A48: S3[ {}. EnE9] ;
 for B1 being Element of Fin EnE9 holds S3[B1] from SETWISEO:sch_2(A48, A20);
hence  meet (rng (g | B)) = (meet (rng (f | B))) /\ (meet (rng (f9 | B))) ; ::_thesis: verum
end;
then  meet (rng (g | EE9)) = (meet (rng (f | EE9))) /\ (meet (rng (f9 | EE9))) ;
hence  meet (rng (g | (E /\ E9))) = (meet (rng (f | (E /\ E9)))) /\ (meet (rng (f9 | (E /\ E9)))) ; ::_thesis: verum
end;
end;
end;
A49: for E, E9 being set
for g being Function st dom g = E \/ E9 holds
rng g = ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E)))
proof
let E, E9 be set ; ::_thesis: for g being Function st dom g = E \/ E9 holds
rng g = ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E)))
let g be Function; ::_thesis: ( dom g = E \/ E9 implies rng g = ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E))) )
 ( rng (g | (E /\ E9)) c= rng g & rng (g | (E \ E9)) c= rng g ) by RELAT_1:70;
then A50: (rng (g | (E /\ E9))) \/ (rng (g | (E \ E9))) c= rng g by XBOOLE_1:8;
assume A51: dom g = E \/ E9 ; ::_thesis: rng g = ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E)))
thus  rng g c= ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E))) :: according to XBOOLE_0:def_10 ::_thesis: ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E))) c= rng g
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng g or y in ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E))) )
assume  y in rng g ; ::_thesis: y in ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E)))
then consider i being set  such that
A52: i in dom g and
A53: y = g . i by FUNCT_1:def_3;
percases ( i in (E \ E9) \/ (E9 \ E) or not i in (E \ E9) \/ (E9 \ E) ) ;
supposeA54: i in (E \ E9) \/ (E9 \ E) ; ::_thesis: y in ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E)))
 y in ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E)))
proof
percases ( i in E or not i in E ) ;
supposeA55: i in E ; ::_thesis: y in ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E)))
A56: E /\ E9 c= E by XBOOLE_1:17;
E /\ ((E \ E9) \/ (E9 \ E)) = (E /\ (E \ E9)) \/ (E /\ (E9 \ E)) by XBOOLE_1:23
.= (E \ E9) \/ (E /\ (E9 \ E)) by XBOOLE_1:28
.= (E \ E9) \/ ((E /\ E9) \ E) by XBOOLE_1:49
.= (E \ E9) \/ {} by A56, XBOOLE_1:37 ;
then  i in E \ E9 by A54, A55, XBOOLE_0:def_4;
then  i in (dom g) /\ (E \ E9) by A52, XBOOLE_0:def_4;
then A57: i in dom (g | (E \ E9)) by RELAT_1:61;
then  (g | (E \ E9)) . i = y by A53, FUNCT_1:47;
then  y in rng (g | (E \ E9)) by A57, FUNCT_1:def_3;
then  y in (rng (g | (E /\ E9))) \/ (rng (g | (E \ E9))) by XBOOLE_0:def_3;
hence  y in ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E))) by XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA58: not i in E ; ::_thesis: y in ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E)))
((E \ E9) \/ (E9 \ E)) \ E = ((E \ E9) \ E) \/ ((E9 \ E) \ E) by XBOOLE_1:42
.= {} \/ ((E9 \ E) \ E) by XBOOLE_1:37
.= E9 \ (E \/ E) by XBOOLE_1:41 ;
then  i in E9 \ (E \/ E) by A54, A58, XBOOLE_0:def_5;
then  i in (dom g) /\ (E9 \ E) by A52, XBOOLE_0:def_4;
then A59: i in dom (g | (E9 \ E)) by RELAT_1:61;
then  (g | (E9 \ E)) . i = y by A53, FUNCT_1:47;
then  y in rng (g | (E9 \ E)) by A59, FUNCT_1:def_3;
then  y in (rng (g | (E \ E9))) \/ (rng (g | (E9 \ E))) by XBOOLE_0:def_3;
then  y in (rng (g | (E /\ E9))) \/ ((rng (g | (E \ E9))) \/ (rng (g | (E9 \ E)))) by XBOOLE_0:def_3;
hence  y in ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E))) by XBOOLE_1:4; ::_thesis: verum
end;
end;
end;
hence  y in ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E))) ; ::_thesis: verum
end;
supposeA60: not i in (E \ E9) \/ (E9 \ E) ; ::_thesis: y in ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E)))
A61: (E \/ E9) \ (E \+\ E9) = ((E \/ E9) \ (E \/ E9)) \/ (((E \/ E9) /\ E) /\ E9) by XBOOLE_1:102
.= {} \/ (((E \/ E9) /\ E) /\ E9) by XBOOLE_1:37
.= (E \/ E9) /\ (E /\ E9) by XBOOLE_1:16 ;
 i in (E \/ E9) \ (E \+\ E9) by A51, A52, A60, XBOOLE_0:def_5;
then A62: i in dom (g | (E /\ E9)) by A51, A61, RELAT_1:61;
then  (g | (E /\ E9)) . i = y by A53, FUNCT_1:47;
then  y in rng (g | (E /\ E9)) by A62, FUNCT_1:def_3;
then  y in (rng (g | (E /\ E9))) \/ (rng (g | (E \ E9))) by XBOOLE_0:def_3;
hence  y in ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E))) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
 rng (g | (E9 \ E)) c= rng g by RELAT_1:70;
hence  ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E))) c= rng g by A50, XBOOLE_1:8; ::_thesis: verum
end;
then A63: rng g = ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E))) by A8;
A64: dom (g | (E9 \ E)) = (dom g) /\ (E9 \ E) by RELAT_1:61
.= (E \/ E9) /\ (E9 \ E) by FUNCT_2:def_1
.= ((E \/ E9) /\ E9) \ E by XBOOLE_1:49
.= E9 \ E by XBOOLE_1:21 ;
A65: for i being set st i in dom (g | (E9 \ E)) holds
(g | (E9 \ E)) . i = f9 . i
proof
let i be set ; ::_thesis: ( i in dom (g | (E9 \ E)) implies (g | (E9 \ E)) . i = f9 . i )
assume A66: i in dom (g | (E9 \ E)) ; ::_thesis: (g | (E9 \ E)) . i = f9 . i
then A67: i in (E \ E9) \/ (E9 \ E) by A64, XBOOLE_0:def_3;
 not i in E by A64, A66, XBOOLE_0:def_5;
then f9 . i = h . i by A7, A66
.= g . i by A8, A66, A67 ;
hence  (g | (E9 \ E)) . i = f9 . i by A66, FUNCT_1:47; ::_thesis: verum
end;
dom (g | (E9 \ E)) = (E9 /\ E9) \ E by A64
.= E9 /\ (E9 \ E) by XBOOLE_1:49
.= (dom f9) /\ (E9 \ E) by FUNCT_2:def_1 ;
then A68: meet (rng (g | (E9 \ E))) = meet (rng (f9 | (E9 \ E))) by A65, FUNCT_1:46;
A69: dom (g | (E \ E9)) = (dom g) /\ (E \ E9) by RELAT_1:61
.= (E \/ E9) /\ (E \ E9) by FUNCT_2:def_1
.= ((E \/ E9) /\ E) \ E9 by XBOOLE_1:49
.= E \ E9 by XBOOLE_1:21 ;
A70: for i being set st i in dom (g | (E \ E9)) holds
(g | (E \ E9)) . i = f . i
proof
let i be set ; ::_thesis: ( i in dom (g | (E \ E9)) implies (g | (E \ E9)) . i = f . i )
A71: E \ E9 c= E by XBOOLE_1:36;
assume A72: i in dom (g | (E \ E9)) ; ::_thesis: (g | (E \ E9)) . i = f . i
then  i in (E \ E9) \/ (E9 \ E) by A69, XBOOLE_0:def_3;
then g . i = h . i by A8, A72
.= f . i by A7, A69, A72, A71 ;
hence  (g | (E \ E9)) . i = f . i by A72, FUNCT_1:47; ::_thesis: verum
end;
dom (g | (E \ E9)) = (E /\ E) \ E9 by A69
.= E /\ (E \ E9) by XBOOLE_1:49
.= (dom f) /\ (E \ E9) by FUNCT_2:def_1 ;
then A73: meet (rng (g | (E \ E9))) = meet (rng (f | (E \ E9))) by A70, FUNCT_1:46;
percases ( E /\ E9 = {} or not E /\ E9 = {} ) ;
supposeA74: E /\ E9 = {} ; ::_thesis: x /\ X = meet (rng g)
A75: E \ E9 c= E by XBOOLE_1:36;
A76: ( E9 c= dom g & E c= dom g ) by A8, XBOOLE_1:7;
A77: E9 \ E c= E9 by XBOOLE_1:36;
A78: E misses E9 by A74, XBOOLE_0:def_7;
then A79: ( f | (E \ E9) = f & f9 | (E9 \ E) = f9 ) by RELSET_1:19, XBOOLE_1:86;
 E c= E \ E9 by A78, XBOOLE_1:86;
then A80: E = E \ E9 by A75, XBOOLE_0:def_10;
 E9 c= E9 \ E by A78, XBOOLE_1:86;
then A81: E9 = E9 \ E by A77, XBOOLE_0:def_10;
 rng (g | (E /\ E9)) = {} by A74;
hence  x /\ X = meet (rng g) by A4, A6, A73, A68, A63, A79, A81, A80, A76, SETFAM_1:9; ::_thesis: verum
end;
supposeA82: not E /\ E9 = {} ; ::_thesis: x /\ X = meet (rng g)
 meet (rng g) = (meet (rng f)) /\ (meet (rng f9))
proof
percases ( E \ E9 = {} or not E \ E9 = {} ) ;
supposeA83: E \ E9 = {} ; ::_thesis: meet (rng g) = (meet (rng f)) /\ (meet (rng f9))
then A84: rng (g | (E \ E9)) = {} ;
A85: E c= E9 by A83, XBOOLE_1:37;
A86: E /\ E9 c= dom g by A8, XBOOLE_1:29;
 meet (rng g) = (meet (rng f)) /\ (meet (rng f9))
proof
percases ( E9 \ E = {} or E9 \ E <> {} ) ;
suppose E9 \ E = {} ; ::_thesis: meet (rng g) = (meet (rng f)) /\ (meet (rng f9))
then  E9 c= E by XBOOLE_1:37;
then A87: E = E9 by A85, XBOOLE_0:def_10;
 f | E = f ;
hence  meet (rng g) = (meet (rng f)) /\ (meet (rng f9)) by A17, A63, A84, A87, RELSET_1:19; ::_thesis: verum
end;
supposeA88: E9 \ E <> {} ; ::_thesis: meet (rng g) = (meet (rng f)) /\ (meet (rng f9))
 ( E9 \ E c= E9 & E9 c= E9 \/ E ) by XBOOLE_1:7, XBOOLE_1:36;
then  E9 \ E c= dom g by A8, XBOOLE_1:1;
then  meet (rng g) = (meet (rng (g | (E /\ E9)))) /\ (meet (rng (g | (E9 \ E)))) by A63, A82, A84, A86, A88, SETFAM_1:9;
then A89: meet (rng g) = ((meet (rng f)) /\ (meet (rng (f9 | (E /\ E9))))) /\ (meet (rng (f9 | (E9 \ E)))) by A17, A68, A85, RELSET_1:19, XBOOLE_1:19;
A90: rng (f9 | (E \ E9)) = {} by A83;
 E9 \ E c= E9 by XBOOLE_1:36;
then A91: E9 \ E c= dom f9 by FUNCT_2:def_1;
 E /\ E9 c= E9 by XBOOLE_1:17;
then A92: E /\ E9 c= dom f9 by FUNCT_2:def_1;
 ( E9 \/ E = E9 & dom f9 = E9 ) by A85, FUNCT_2:def_1, XBOOLE_1:12;
then  rng f9 = ((rng (f9 | (E /\ E9))) \/ (rng (f9 | (E \ E9)))) \/ (rng (f9 | (E9 \ E))) by A49
.= (rng (f9 | (E /\ E9))) \/ (rng (f9 | (E9 \ E))) by A90 ;
then  meet (rng f9) = (meet (rng (f9 | (E /\ E9)))) /\ (meet (rng (f9 | (E9 \ E)))) by A82, A88, A92, A91, SETFAM_1:9;
hence  meet (rng g) = (meet (rng f)) /\ (meet (rng f9)) by A89, XBOOLE_1:16; ::_thesis: verum
end;
end;
end;
hence  meet (rng g) = (meet (rng f)) /\ (meet (rng f9)) ; ::_thesis: verum
end;
supposeA93: not E \ E9 = {} ; ::_thesis: meet (rng g) = (meet (rng f)) /\ (meet (rng f9))
 meet (rng g) = (meet (rng f)) /\ (meet (rng f9))
proof
 ( E \ E9 c= E & E c= dom g ) by A8, XBOOLE_1:7, XBOOLE_1:36;
then A94: rng (g | (E \ E9)) <> {} by A93, Th1, XBOOLE_1:1;
A95: E /\ E9 c= E \/ E9 by XBOOLE_1:29;
percases ( E9 \ E = {} or not E9 \ E = {} ) ;
supposeA96: E9 \ E = {} ; ::_thesis: meet (rng g) = (meet (rng f)) /\ (meet (rng f9))
then A97: rng (f | (E9 \ E)) = {} ;
 E9 c= E by A96, XBOOLE_1:37;
then  E = E \/ E9 by XBOOLE_1:12;
then  dom f = E \/ E9 by FUNCT_2:def_1;
then A98: rng f = ((rng (f | (E /\ E9))) \/ (rng (f | (E \ E9)))) \/ (rng (f | (E9 \ E))) by A49
.= (rng (f | (E /\ E9))) \/ (rng (f | (E \ E9))) by A97 ;
 E \ E9 c= E by XBOOLE_1:36;
then A99: E \ E9 c= dom f by FUNCT_2:def_1;
 E9 c= E by A96, XBOOLE_1:37;
then A100: f9 | (E /\ E9) = f9 by RELSET_1:19, XBOOLE_1:19;
 dom f = E by FUNCT_2:def_1;
then A101: rng (f | (E /\ E9)) <> {} by A82, Th1, XBOOLE_1:17;
 rng (g | (E9 \ E)) = {} by A96;
then  meet (rng g) = (meet (rng (g | (E /\ E9)))) /\ (meet (rng (g | (E \ E9)))) by A8, A63, A82, A95, A94, SETFAM_1:9
.= ((meet (rng (f | (E /\ E9)))) /\ (meet (rng (f | (E \ E9))))) /\ (meet (rng (f9 | (E /\ E9)))) by A17, A73, XBOOLE_1:16 ;
hence  meet (rng g) = (meet (rng f)) /\ (meet (rng f9)) by A93, A100, A98, A101, A99, SETFAM_1:9; ::_thesis: verum
end;
supposeA102: not E9 \ E = {} ; ::_thesis: meet (rng g) = (meet (rng f)) /\ (meet (rng f9))
 ( E9 \ E c= E9 & E9 c= E \/ E9 ) by XBOOLE_1:7, XBOOLE_1:36;
then  E9 \ E c= dom g by A8, XBOOLE_1:1;
then  meet (rng g) = (meet ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9))))) /\ (meet (rng (g | (E9 \ E)))) by A8, A63, A82, A95, A102, SETFAM_1:9
.= ((meet (rng (g | (E /\ E9)))) /\ (meet (rng (g | (E \ E9))))) /\ (meet (rng (g | (E9 \ E)))) by A8, A82, A95, A94, SETFAM_1:9 ;
then A103: meet (rng g) = (((meet (rng (f | (E /\ E9)))) /\ (meet (rng (f | (E \ E9))))) /\ (meet (rng (f9 | (E /\ E9))))) /\ (meet (rng (f9 | (E9 \ E)))) by A17, A73, A68, XBOOLE_1:16;
 E /\ E9 c= E by XBOOLE_1:17;
then A104: E /\ E9 c= dom f by FUNCT_2:def_1;
 E \/ (E /\ E9) = E by XBOOLE_1:12, XBOOLE_1:17;
then  dom f = E \/ (E /\ E9) by FUNCT_2:def_1;
then A105: rng f = ((rng (f | (E /\ (E /\ E9)))) \/ (rng (f | (E \ (E /\ E9))))) \/ (rng (f | ((E /\ E9) \ E))) by A49;
 E /\ E9 c= E by XBOOLE_1:17;
then  (E /\ E9) \ E = {} by XBOOLE_1:37;
then A106: rng (f | ((E /\ E9) \ E)) = {} ;
 E9 \ E c= E9 by XBOOLE_1:36;
then A107: E9 \ E c= dom f9 by FUNCT_2:def_1;
 E /\ E9 c= E9 by XBOOLE_1:17;
then A108: E /\ E9 c= dom f9 by FUNCT_2:def_1;
 E /\ E9 c= E9 by XBOOLE_1:17;
then A109: ( E9 \ E = E9 \ (E /\ E9) & (E /\ E9) \ E9 = {} ) by XBOOLE_1:37, XBOOLE_1:47;
 E9 \/ (E /\ E9) = E9 by XBOOLE_1:12, XBOOLE_1:17;
then A110: dom f9 = E9 \/ (E /\ E9) by FUNCT_2:def_1;
E9 /\ (E /\ E9) = (E9 /\ E9) /\ E by XBOOLE_1:16
.= E /\ E9 ;
then  rng f9 = ((rng (f9 | (E /\ E9))) \/ (rng (f9 | (E9 \ E)))) \/ (rng (f9 | {})) by A49, A110, A109;
then A111: meet (rng f9) = (meet (rng (f9 | (E /\ E9)))) /\ (meet (rng (f9 | (E9 \ E)))) by A82, A102, A108, A107, SETFAM_1:9;
 E \ E9 c= E by XBOOLE_1:36;
then A112: E \ E9 c= dom f by FUNCT_2:def_1;
E /\ (E /\ E9) = (E /\ E) /\ E9 by XBOOLE_1:16
.= E /\ E9 ;
then  rng f = (rng (f | (E /\ E9))) \/ (rng (f | (E \ E9))) by A105, A106, XBOOLE_1:47;
then  meet (rng f) = (meet (rng (f | (E /\ E9)))) /\ (meet (rng (f | (E \ E9)))) by A82, A93, A104, A112, SETFAM_1:9;
hence  meet (rng g) = (meet (rng f)) /\ (meet (rng f9)) by A111, A103, XBOOLE_1:16; ::_thesis: verum
end;
end;
end;
hence  meet (rng g) = (meet (rng f)) /\ (meet (rng f9)) ; ::_thesis: verum
end;
end;
end;
hence  x /\ X = meet (rng g) by A4, A6; ::_thesis: verum
end;
end;
end;
 for y being set st y in (meet (rng f)) /\ (meet (rng f9)) holds
y in Omega
proof
let y be set ; ::_thesis: ( y in (meet (rng f)) /\ (meet (rng f9)) implies y in Omega )
consider S being set  such that
A113: S in rng f by XBOOLE_0:def_1;
consider S9 being set  such that
A114: S9 in rng f9 by XBOOLE_0:def_1;
assume A115: y in (meet (rng f)) /\ (meet (rng f9)) ; ::_thesis: y in Omega
then  y in meet (rng f9) by XBOOLE_0:def_4;
then A116: y in S9 by A114, SETFAM_1:def_1;
 y in meet (rng f) by A115, XBOOLE_0:def_4;
then  y in S by A113, SETFAM_1:def_1;
then A117: y in S /\ S9 by A116, XBOOLE_0:def_4;
 S /\ S9 is Event of Sigma by A113, A114, PROB_1:19;
hence  y in Omega by A117; ::_thesis: verum
end;
then reconsider xX = x /\ X as Subset of Omega by A4, A6, TARSKI:def_3;
 E \/ E9 c= J by A3, A5, XBOOLE_1:8;
then  xX in MeetSections (J,F) by A16, Def9;
hence  x /\ X in MeetSections (J,F) ; ::_thesis: verum
end;
hence  MeetSections (J,F) is intersection_stable by FINSUB_1:def_2; ::_thesis: verum
end;
end;

theorem Th14: :: KOLMOG01:14
for I, Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for F being ManySortedSigmaField of I,Sigma
for J, K being non empty Subset of I st F is_independent_wrt P & J misses K holds
for u, v being Event of Sigma st u in sigUn (F,J) & v in sigUn (F,K) holds
P . (u /\ v) = (P . u) * (P . v)
proof
let I, Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for F being ManySortedSigmaField of I,Sigma
for J, K being non empty Subset of I st F is_independent_wrt P & J misses K holds
for u, v being Event of Sigma st u in sigUn (F,J) & v in sigUn (F,K) holds
P . (u /\ v) = (P . u) * (P . v)
let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma
for F being ManySortedSigmaField of I,Sigma
for J, K being non empty Subset of I st F is_independent_wrt P & J misses K holds
for u, v being Event of Sigma st u in sigUn (F,J) & v in sigUn (F,K) holds
P . (u /\ v) = (P . u) * (P . v)
let P be Probability of Sigma; ::_thesis: for F being ManySortedSigmaField of I,Sigma
for J, K being non empty Subset of I st F is_independent_wrt P & J misses K holds
for u, v being Event of Sigma st u in sigUn (F,J) & v in sigUn (F,K) holds
P . (u /\ v) = (P . u) * (P . v)
let F be ManySortedSigmaField of I,Sigma; ::_thesis: for J, K being non empty Subset of I st F is_independent_wrt P & J misses K holds
for u, v being Event of Sigma st u in sigUn (F,J) & v in sigUn (F,K) holds
P . (u /\ v) = (P . u) * (P . v)
let J, K be non empty Subset of I; ::_thesis: ( F is_independent_wrt P & J misses K implies for u, v being Event of Sigma st u in sigUn (F,J) & v in sigUn (F,K) holds
P . (u /\ v) = (P . u) * (P . v) )
A1: ( MeetSections (J,F) is non empty Subset of Sigma & MeetSections (K,F) is non empty Subset of Sigma ) by Th13;
assume A2: ( F is_independent_wrt P & J misses K ) ; ::_thesis: for u, v being Event of Sigma st u in sigUn (F,J) & v in sigUn (F,K) holds
P . (u /\ v) = (P . u) * (P . v)
A3: for p, q being Event of Sigma st p in MeetSections (J,F) & q in MeetSections (K,F) holds
p,q are_independent_respect_to P
proof
let p, q be Event of Sigma; ::_thesis: ( p in MeetSections (J,F) & q in MeetSections (K,F) implies p,q are_independent_respect_to P )
assume A4: ( p in MeetSections (J,F) & q in MeetSections (K,F) ) ; ::_thesis: p,q are_independent_respect_to P
reconsider p = p, q = q as Subset of Omega ;
 P . (p /\ q) = (P . p) * (P . q) by A2, A4, Th12;
hence  p,q are_independent_respect_to P by PROB_2:def_4; ::_thesis: verum
end;
let u, v be Event of Sigma; ::_thesis: ( u in sigUn (F,J) & v in sigUn (F,K) implies P . (u /\ v) = (P . u) * (P . v) )
assume  ( u in sigUn (F,J) & v in sigUn (F,K) ) ; ::_thesis: P . (u /\ v) = (P . u) * (P . v)
then  ( u in sigma (MeetSections (J,F)) & v in sigma (MeetSections (K,F)) ) by Th11;
then  u,v are_independent_respect_to P by A1, A3, Th10;
hence  P . (u /\ v) = (P . u) * (P . v) by PROB_2:def_4; ::_thesis: verum
end;

definition
let I be set ;
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let F be ManySortedSigmaField of I,Sigma;
func finSigmaFields (F,I) ->  Subset-Family of Omega means :Def10: :: KOLMOG01:def 10
 for S being Subset of Omega holds
( S in it iff ex E being finite Subset of I st S in sigUn (F,E) );
existence
 ex b1 being Subset-Family of Omega st
for S being Subset of Omega holds
( S in b1 iff ex E being finite Subset of I st S in sigUn (F,E) )
proof
defpred S1[ set ] means  ex E being finite Subset of I st $1 in sigUn (F,E);
consider X being set  such that
A1: for x being set holds
( x in X iff ( x in bool Omega & S1[x] ) ) from XBOOLE_0:sch_1();
 for x being set st x in X holds
x in bool Omega by A1;
then reconsider X = X as Subset-Family of Omega by TARSKI:def_3;
take  X ; ::_thesis: for S being Subset of Omega holds
( S in X iff ex E being finite Subset of I st S in sigUn (F,E) )
let S be Subset of Omega; ::_thesis: ( S in X iff ex E being finite Subset of I st S in sigUn (F,E) )
thus  ( S in X iff ex E being finite Subset of I st S in sigUn (F,E) ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset-Family of Omega st ( for S being Subset of Omega holds
( S in b1 iff ex E being finite Subset of I st S in sigUn (F,E) ) ) & ( for S being Subset of Omega holds
( S in b2 iff ex E being finite Subset of I st S in sigUn (F,E) ) ) holds
b1 = b2
proof
let X1, X2 be Subset-Family of Omega; ::_thesis: ( ( for S being Subset of Omega holds
( S in X1 iff ex E being finite Subset of I st S in sigUn (F,E) ) ) & ( for S being Subset of Omega holds
( S in X2 iff ex E being finite Subset of I st S in sigUn (F,E) ) ) implies X1 = X2 )
assume A2: for S being Subset of Omega holds
( S in X1 iff ex E being finite Subset of I st S in sigUn (F,E) ) ; ::_thesis: ( ex S being Subset of Omega st
( ( S in X2 implies ex E being finite Subset of I st S in sigUn (F,E) ) implies ( ex E being finite Subset of I st S in sigUn (F,E) & not S in X2 ) ) or X1 = X2 )
assume A3: for S being Subset of Omega holds
( S in X2 iff ex E being finite Subset of I st S in sigUn (F,E) ) ; ::_thesis: X1 = X2
now__::_thesis:_for_S_being_Subset_of_Omega_holds_
(_S_in_X1_iff_S_in_X2_)
let S be Subset of Omega; ::_thesis: ( S in X1 iff S in X2 )
 ( S in X1 iff ex E being finite Subset of I st S in sigUn (F,E) ) by A2;
hence  ( S in X1 iff S in X2 ) by A3; ::_thesis: verum
end;
hence  X1 = X2 by SUBSET_1:3; ::_thesis: verum
end;
end;

:: deftheorem Def10 defines finSigmaFields KOLMOG01:def_10_:_
 for I being set
for Omega being non empty set
for Sigma being SigmaField of Omega
for F being ManySortedSigmaField of I,Sigma
for b5 being Subset-Family of Omega holds
( b5 = finSigmaFields (F,I) iff for S being Subset of Omega holds
( S in b5 iff ex E being finite Subset of I st S in sigUn (F,E) ) );

theorem Th15: :: KOLMOG01:15
for I, Omega being non empty set
for Sigma being SigmaField of Omega
for F being ManySortedSigmaField of I,Sigma holds tailSigmaField (F,I) is SigmaField of Omega
proof
let I, Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for F being ManySortedSigmaField of I,Sigma holds tailSigmaField (F,I) is SigmaField of Omega
let Sigma be SigmaField of Omega; ::_thesis: for F being ManySortedSigmaField of I,Sigma holds tailSigmaField (F,I) is SigmaField of Omega
let F be ManySortedSigmaField of I,Sigma; ::_thesis: tailSigmaField (F,I) is SigmaField of Omega
A1: for A1 being SetSequence of Omega st rng A1 c= tailSigmaField (F,I) holds
Intersection A1 in tailSigmaField (F,I)
proof
let A1 be SetSequence of Omega; ::_thesis: ( rng A1 c= tailSigmaField (F,I) implies Intersection A1 in tailSigmaField (F,I) )
assume A2: rng A1 c= tailSigmaField (F,I) ; ::_thesis: Intersection A1 in tailSigmaField (F,I)
A3: for n being Element of NAT
for S being set st S in futSigmaFields (F,I) holds
A1 . n in S
proof
let n be Element of NAT ; ::_thesis: for S being set st S in futSigmaFields (F,I) holds
A1 . n in S
let S be set ; ::_thesis: ( S in futSigmaFields (F,I) implies A1 . n in S )
A4: A1 . n in rng A1 by NAT_1:51;
assume  S in futSigmaFields (F,I) ; ::_thesis: A1 . n in S
hence  A1 . n in S by A2, A4, SETFAM_1:def_1; ::_thesis: verum
end;
 for S being set st S in futSigmaFields (F,I) holds
(Union (Complement A1)) ` in S
proof
let S be set ; ::_thesis: ( S in futSigmaFields (F,I) implies (Union (Complement A1)) ` in S )
assume A5: S in futSigmaFields (F,I) ; ::_thesis: (Union (Complement A1)) ` in S
then  ex E being finite Subset of I st S = sigUn (F,(I \ E)) by Def7;
then reconsider S = S as SigmaField of Omega ;
 for n being Nat holds (Complement A1) . n in S
proof
let n be Nat; ::_thesis: (Complement A1) . n in S
reconsider n = n as Element of NAT by ORDINAL1:def_12;
 A1 . n in S by A3, A5;
then  (A1 . n) ` is Event of S by PROB_1:20;
then  (A1 . n) ` in S ;
hence  (Complement A1) . n in S by PROB_1:def_2; ::_thesis: verum
end;
then  rng (Complement A1) c= S by NAT_1:52;
then reconsider CA1 = Complement A1 as SetSequence of S by RELAT_1:def_19;
 Union CA1 in S by PROB_1:17;
then  (Union (Complement A1)) ` is Event of S by PROB_1:20;
hence  (Union (Complement A1)) ` in S ; ::_thesis: verum
end;
hence  Intersection A1 in tailSigmaField (F,I) by SETFAM_1:def_1; ::_thesis: verum
end;
 for A being Subset of Omega st A in tailSigmaField (F,I) holds
A ` in tailSigmaField (F,I)
proof
let A be Subset of Omega; ::_thesis: ( A in tailSigmaField (F,I) implies A ` in tailSigmaField (F,I) )
assume A6: A in tailSigmaField (F,I) ; ::_thesis: A ` in tailSigmaField (F,I)
 for S being set st S in futSigmaFields (F,I) holds
A ` in S
proof
let S be set ; ::_thesis: ( S in futSigmaFields (F,I) implies A ` in S )
assume A7: S in futSigmaFields (F,I) ; ::_thesis: A ` in S
then consider E being finite Subset of I such that
A8: S = sigUn (F,(I \ E)) by Def7;
 A in S by A6, A7, SETFAM_1:def_1;
then  A ` is Event of sigma (Union (F | (I \ E))) by A8, PROB_1:20;
hence  A ` in S by A8; ::_thesis: verum
end;
hence  A ` in tailSigmaField (F,I) by SETFAM_1:def_1; ::_thesis: verum
end;
hence  tailSigmaField (F,I) is SigmaField of Omega by A1, PROB_1:15; ::_thesis: verum
end;

theorem :: KOLMOG01:16
for Omega, I being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for a being Element of Sigma
for F being ManySortedSigmaField of I,Sigma st F is_independent_wrt P & a in tailSigmaField (F,I) & not P . a = 0 holds
P . a = 1
proof
let Omega, I be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for a being Element of Sigma
for F being ManySortedSigmaField of I,Sigma st F is_independent_wrt P & a in tailSigmaField (F,I) & not P . a = 0 holds
P . a = 1
let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma
for a being Element of Sigma
for F being ManySortedSigmaField of I,Sigma st F is_independent_wrt P & a in tailSigmaField (F,I) & not P . a = 0 holds
P . a = 1
let P be Probability of Sigma; ::_thesis: for a being Element of Sigma
for F being ManySortedSigmaField of I,Sigma st F is_independent_wrt P & a in tailSigmaField (F,I) & not P . a = 0 holds
P . a = 1
let a be Element of Sigma; ::_thesis: for F being ManySortedSigmaField of I,Sigma st F is_independent_wrt P & a in tailSigmaField (F,I) & not P . a = 0 holds
P . a = 1
let F be ManySortedSigmaField of I,Sigma; ::_thesis: ( F is_independent_wrt P & a in tailSigmaField (F,I) & not P . a = 0 implies P . a = 1 )
reconsider T = tailSigmaField (F,I) as SigmaField of Omega by Th15;
set Ie = I \ ({} I);
A1: ( a in tailSigmaField (F,I) implies a in sigUn (F,(I \ ({} I))) )
proof
assume A2: a in tailSigmaField (F,I) ; ::_thesis: a in sigUn (F,(I \ ({} I)))
 sigUn (F,(I \ ({} I))) in futSigmaFields (F,I) by Def7;
hence  a in sigUn (F,(I \ ({} I))) by A2, SETFAM_1:def_1; ::_thesis: verum
end;
assume A3: F is_independent_wrt P ; ::_thesis: ( not a in tailSigmaField (F,I) or P . a = 0 or P . a = 1 )
A4: for E being finite Subset of I
for p, q being Event of Sigma st p in sigUn (F,E) & q in tailSigmaField (F,I) holds
p,q are_independent_respect_to P
proof
let E be finite Subset of I; ::_thesis: for p, q being Event of Sigma st p in sigUn (F,E) & q in tailSigmaField (F,I) holds
p,q are_independent_respect_to P
let p, q be Event of Sigma; ::_thesis: ( p in sigUn (F,E) & q in tailSigmaField (F,I) implies p,q are_independent_respect_to P )
assume that
A5: p in sigUn (F,E) and
A6: q in tailSigmaField (F,I) ; ::_thesis: p,q are_independent_respect_to P
 for E being finite Subset of I holds q in sigUn (F,(I \ E))
proof
let E be finite Subset of I; ::_thesis: q in sigUn (F,(I \ E))
 sigUn (F,(I \ E)) in futSigmaFields (F,I) by Def7;
hence  q in sigUn (F,(I \ E)) by A6, SETFAM_1:def_1; ::_thesis: verum
end;
then A7: q in sigUn (F,(I \ E)) ;
percases ( ( E <> {} & I \ E <> {} ) or not E <> {} or not I \ E <> {} ) ;
supposeA8: ( E <> {} & I \ E <> {} ) ; ::_thesis: p,q are_independent_respect_to P
then reconsider E = E as non empty Subset of I ;
reconsider IE = I \ E as non empty Subset of I by A8;
 E misses IE by XBOOLE_1:79;
then  P . (p /\ q) = (P . p) * (P . q) by A3, A5, A7, Th14;
hence  p,q are_independent_respect_to P by PROB_2:def_4; ::_thesis: verum
end;
supposeA9: ( not E <> {} or not I \ E <> {} ) ; ::_thesis: p,q are_independent_respect_to P
reconsider e = {} as Subset of I by XBOOLE_1:2;
A10: for u, v being Event of Sigma st u in {{},Omega} holds
u,v are_independent_respect_to P
proof
let u, v be Event of Sigma; ::_thesis: ( u in {{},Omega} implies u,v are_independent_respect_to P )
assume A11: u in {{},Omega} ; ::_thesis: u,v are_independent_respect_to P
percases ( u = {} or u <> {} ) ;
suppose u = {} ; ::_thesis: u,v are_independent_respect_to P
hence  u,v are_independent_respect_to P by PROB_2:19, PROB_2:23; ::_thesis: verum
end;
suppose u <> {} ; ::_thesis: u,v are_independent_respect_to P
then  u = [#] Sigma by A11, TARSKI:def_2;
hence  u,v are_independent_respect_to P by PROB_2:19, PROB_2:24; ::_thesis: verum
end;
end;
end;
 Union (F | {}) = {} by ZFMISC_1:2;
then A12: sigUn (F,e) = {{},Omega} by Th3;
 p,q are_independent_respect_to P
proof
percases ( E = {} or E <> {} ) ;
suppose E = {} ; ::_thesis: p,q are_independent_respect_to P
hence  p,q are_independent_respect_to P by A5, A12, A10; ::_thesis: verum
end;
suppose E <> {} ; ::_thesis: p,q are_independent_respect_to P
hence  p,q are_independent_respect_to P by A7, A9, A12, A10, PROB_2:19; ::_thesis: verum
end;
end;
end;
hence  p,q are_independent_respect_to P ; ::_thesis: verum
end;
end;
end;
A13: for p, q being Event of Sigma st p in finSigmaFields (F,I) & q in tailSigmaField (F,I) holds
p,q are_independent_respect_to P
proof
let p, q be Event of Sigma; ::_thesis: ( p in finSigmaFields (F,I) & q in tailSigmaField (F,I) implies p,q are_independent_respect_to P )
assume that
A14: p in finSigmaFields (F,I) and
A15: q in tailSigmaField (F,I) ; ::_thesis: p,q are_independent_respect_to P
 ex E being finite Subset of I st p in sigUn (F,E) by A14, Def10;
hence  p,q are_independent_respect_to P by A4, A15; ::_thesis: verum
end;
 Union (F | (I \ ({} I))) c= sigma (finSigmaFields (F,I))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Union (F | (I \ ({} I))) or x in sigma (finSigmaFields (F,I)) )
A16: dom F c= I \ ({} I) ;
assume  x in Union (F | (I \ ({} I))) ; ::_thesis: x in sigma (finSigmaFields (F,I))
then  x in union (rng F) by A16, RELAT_1:68;
then consider y being set  such that
A17: x in y and
A18: y in rng F by TARSKI:def_4;
consider i being set  such that
A19: i in dom F and
A20: y = F . i by A18, FUNCT_1:def_3;
A21: x in finSigmaFields (F,I)
proof
reconsider Fi = F . i as SigmaField of Omega by A19, Def2;
A22: ( sigma Fi c= Fi & Fi c= sigma Fi ) by PROB_1:def_9;
 i in I by A19;
then  for z being set st z in {i} holds
z in I by TARSKI:def_1;
then reconsider E = {i} as finite Subset of I by TARSKI:def_3;
A23: dom (F | {i}) = (dom F) /\ {i} by RELAT_1:61
.= {i} by A19, ZFMISC_1:46 ;
then  rng (F | {i}) = {((F | {i}) . i)} by FUNCT_1:4;
then A24: union (rng (F | {i})) = (F | {i}) . i by ZFMISC_1:25;
 i in dom (F | {i}) by A23, TARSKI:def_1;
then  Union (F | {i}) = F . i by A24, FUNCT_1:47;
then  sigUn (F,E) = F . i by A22, XBOOLE_0:def_10;
hence  x in finSigmaFields (F,I) by A17, A20, Def10; ::_thesis: verum
end;
 finSigmaFields (F,I) c= sigma (finSigmaFields (F,I)) by PROB_1:def_9;
hence  x in sigma (finSigmaFields (F,I)) by A21; ::_thesis: verum
end;
then A25: ( T c= sigma T & sigUn (F,(I \ ({} I))) c= sigma (finSigmaFields (F,I)) ) by PROB_1:def_9;
A26: for u, v being Event of Sigma st u in sigUn (F,(I \ ({} I))) & v in tailSigmaField (F,I) holds
u,v are_independent_respect_to P
proof
 for x, y being set st x in finSigmaFields (F,I) & y in finSigmaFields (F,I) holds
x /\ y in finSigmaFields (F,I)
proof
let x, y be set ; ::_thesis: ( x in finSigmaFields (F,I) & y in finSigmaFields (F,I) implies x /\ y in finSigmaFields (F,I) )
assume that
A27: x in finSigmaFields (F,I) and
A28: y in finSigmaFields (F,I) ; ::_thesis: x /\ y in finSigmaFields (F,I)
consider E1 being finite Subset of I such that
A29: x in sigUn (F,E1) by A27, Def10;
consider E2 being finite Subset of I such that
A30: y in sigUn (F,E2) by A28, Def10;
A31: for z being set
for E1, E2 being finite Subset of I st z in sigUn (F,E1) holds
z in sigUn (F,(E1 \/ E2))
proof
let z be set ; ::_thesis: for E1, E2 being finite Subset of I st z in sigUn (F,E1) holds
z in sigUn (F,(E1 \/ E2))
let E1, E2 be finite Subset of I; ::_thesis: ( z in sigUn (F,E1) implies z in sigUn (F,(E1 \/ E2)) )
reconsider E3 = E1 \/ E2 as finite Subset of I ;
A32: Union (F | E1) c= Union (F | E3)
proof
let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in Union (F | E1) or X in Union (F | E3) )
assume  X in Union (F | E1) ; ::_thesis: X in Union (F | E3)
then consider S being set  such that
A33: X in S and
A34: S in rng (F | E1) by TARSKI:def_4;
 F | E3 = (F | E1) \/ (F | E2) by RELAT_1:78;
then  rng (F | E3) = (rng (F | E1)) \/ (rng (F | E2)) by RELAT_1:12;
then  S in rng (F | E3) by A34, XBOOLE_0:def_3;
hence  X in Union (F | E3) by A33, TARSKI:def_4; ::_thesis: verum
end;
 Union (F | E3) c= sigma (Union (F | E3)) by PROB_1:def_9;
then  Union (F | E1) c= sigma (Union (F | E3)) by A32, XBOOLE_1:1;
then A35: sigma (Union (F | E1)) c= sigma (Union (F | E3)) by PROB_1:def_9;
assume  z in sigUn (F,E1) ; ::_thesis: z in sigUn (F,(E1 \/ E2))
hence  z in sigUn (F,(E1 \/ E2)) by A35; ::_thesis: verum
end;
then A36: y in sigUn (F,(E2 \/ E1)) by A30;
 x in sigUn (F,(E1 \/ E2)) by A29, A31;
then  x /\ y in sigUn (F,(E1 \/ E2)) by A36, FINSUB_1:def_2;
hence  x /\ y in finSigmaFields (F,I) by Def10; ::_thesis: verum
end;
then A37: finSigmaFields (F,I) is intersection_stable by FINSUB_1:def_2;
let u, v be Event of Sigma; ::_thesis: ( u in sigUn (F,(I \ ({} I))) & v in tailSigmaField (F,I) implies u,v are_independent_respect_to P )
A38: not finSigmaFields (F,I) is empty
proof
set E = the finite Subset of I;
 {} in sigUn (F, the finite Subset of I) by PROB_1:4;
hence  not finSigmaFields (F,I) is empty by Def10; ::_thesis: verum
end;
A39: tailSigmaField (F,I) c= Sigma
proof
set Ie = I \ ({} I);
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in tailSigmaField (F,I) or x in Sigma )
assume A40: x in tailSigmaField (F,I) ; ::_thesis: x in Sigma
 Union (F | (I \ ({} I))) c= Sigma
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Union (F | (I \ ({} I))) or y in Sigma )
assume  y in Union (F | (I \ ({} I))) ; ::_thesis: y in Sigma
then  ex S being set st
( y in S & S in rng (F | (I \ ({} I))) ) by TARSKI:def_4;
hence  y in Sigma ; ::_thesis: verum
end;
then A41: sigma (Union (F | (I \ ({} I)))) c= Sigma by PROB_1:def_9;
 sigUn (F,(I \ ({} I))) in futSigmaFields (F,I) by Def7;
then  x in sigma (Union (F | (I \ ({} I)))) by A40, SETFAM_1:def_1;
hence  x in Sigma by A41; ::_thesis: verum
end;
A42: finSigmaFields (F,I) c= Sigma
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in finSigmaFields (F,I) or x in Sigma )
assume  x in finSigmaFields (F,I) ; ::_thesis: x in Sigma
then consider E being finite Subset of I such that
A43: x in sigUn (F,E) by Def10;
 Union (F | E) c= Sigma
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Union (F | E) or y in Sigma )
assume  y in Union (F | E) ; ::_thesis: y in Sigma
then  ex S being set st
( y in S & S in rng (F | E) ) by TARSKI:def_4;
hence  y in Sigma ; ::_thesis: verum
end;
then  sigma (Union (F | E)) c= Sigma by PROB_1:def_9;
hence  x in Sigma by A43; ::_thesis: verum
end;
assume  ( u in sigUn (F,(I \ ({} I))) & v in tailSigmaField (F,I) ) ; ::_thesis: u,v are_independent_respect_to P
hence  u,v are_independent_respect_to P by A13, A25, A38, A42, A37, A39, Th10; ::_thesis: verum
end;
assume  a in tailSigmaField (F,I) ; ::_thesis: ( P . a = 0 or P . a = 1 )
then  a,a are_independent_respect_to P by A1, A26;
then  P . (a /\ a) = (P . a) * (P . a) by PROB_2:def_4;
hence  ( P . a = 0 or P . a = 1 ) by Th2; ::_thesis: verum
end;