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