:: PROB_2 semantic presentation begin theorem Th1: :: PROB_2:1 for r, r1, r2, r3 being Real st r <> 0 & r1 <> 0 holds ( r3 / r1 = r2 / r iff r3 * r = r2 * r1 ) proof let r, r1, r2, r3 be Real; ::_thesis: ( r <> 0 & r1 <> 0 implies ( r3 / r1 = r2 / r iff r3 * r = r2 * r1 ) ) assume that A1: r <> 0 and A2: r1 <> 0 ; ::_thesis: ( r3 / r1 = r2 / r iff r3 * r = r2 * r1 ) thus ( r3 / r1 = r2 / r implies r3 * r = r2 * r1 ) ::_thesis: ( r3 * r = r2 * r1 implies r3 / r1 = r2 / r ) proof assume A3: r3 / r1 = r2 / r ; ::_thesis: r3 * r = r2 * r1 r3 * r = ((r3 / r1) * r1) * r by A2, XCMPLX_1:87 .= ((r2 / r) * r) * r1 by A3 .= r2 * r1 by A1, XCMPLX_1:87 ; hence r3 * r = r2 * r1 ; ::_thesis: verum end; assume A4: r3 * r = r2 * r1 ; ::_thesis: r3 / r1 = r2 / r r3 / r1 = (r3 * 1) / r1 .= (r3 * (r * (r "))) / r1 by A1, XCMPLX_0:def_7 .= ((r2 * r1) * (r ")) / r1 by A4, XCMPLX_1:4 .= ((r2 * (r ")) * r1) / r1 .= ((r2 / r) * r1) / r1 by XCMPLX_0:def_9 .= ((r2 / r) * r1) * (r1 ") by XCMPLX_0:def_9 .= (r2 / r) * (r1 * (r1 ")) .= (r2 / r) * 1 by A2, XCMPLX_0:def_7 .= r2 / r ; hence r3 / r1 = r2 / r ; ::_thesis: verum end; theorem Th2: :: PROB_2:2 for r being Real for seq, seq1 being Real_Sequence st seq is convergent & ( for n being Element of NAT holds seq1 . n = r - (seq . n) ) holds ( seq1 is convergent & lim seq1 = r - (lim seq) ) proof let r be Real; ::_thesis: for seq, seq1 being Real_Sequence st seq is convergent & ( for n being Element of NAT holds seq1 . n = r - (seq . n) ) holds ( seq1 is convergent & lim seq1 = r - (lim seq) ) let seq, seq1 be Real_Sequence; ::_thesis: ( seq is convergent & ( for n being Element of NAT holds seq1 . n = r - (seq . n) ) implies ( seq1 is convergent & lim seq1 = r - (lim seq) ) ) assume that A1: seq is convergent and A2: for n being Element of NAT holds seq1 . n = r - (seq . n) ; ::_thesis: ( seq1 is convergent & lim seq1 = r - (lim seq) ) consider r1 being real number such that A3: for r2 being real number st 0 < r2 holds ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((seq . m) - r1) < r2 by A1, SEQ_2:def_6; A4: now__::_thesis:_for_r2_being_real_number_st_0_<_r2_holds_ ex_n_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_n_<=_m_holds_ abs_((seq1_._m)_-_(r_-_r1))_<_r2 let r2 be real number ; ::_thesis: ( 0 < r2 implies ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((seq1 . m) - (r - r1)) < r2 ) assume 0 < r2 ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((seq1 . m) - (r - r1)) < r2 then consider n being Element of NAT such that A5: for m being Element of NAT st n <= m holds abs ((seq . m) - r1) < r2 by A3; take n = n; ::_thesis: for m being Element of NAT st n <= m holds abs ((seq1 . m) - (r - r1)) < r2 now__::_thesis:_for_m_being_Element_of_NAT_st_n_<=_m_holds_ abs_((seq1_._m)_-_(r_-_r1))_<_r2 let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((seq1 . m) - (r - r1)) < r2 ) assume A6: n <= m ; ::_thesis: abs ((seq1 . m) - (r - r1)) < r2 abs ((seq . m) - r1) = abs (- ((seq . m) - r1)) by COMPLEX1:52 .= abs ((r1 - r) + (r - (seq . m))) .= abs ((seq1 . m) + (- (- (r1 - r)))) by A2 .= abs ((seq1 . m) - (r - r1)) ; hence abs ((seq1 . m) - (r - r1)) < r2 by A5, A6; ::_thesis: verum end; hence for m being Element of NAT st n <= m holds abs ((seq1 . m) - (r - r1)) < r2 ; ::_thesis: verum end; hence A7: seq1 is convergent by SEQ_2:def_6; ::_thesis: lim seq1 = r - (lim seq) lim seq = r1 by A1, A3, SEQ_2:def_7; hence lim seq1 = r - (lim seq) by A4, A7, SEQ_2:def_7; ::_thesis: verum end; definition let Omega be set ; let Sigma be SigmaField of Omega; let ASeq be SetSequence of Sigma; let n be Element of NAT ; :: original: . redefine funcASeq . n -> Event of Sigma; coherence ASeq . n is Event of Sigma by PROB_1:25; end; definition let Omega be set ; let Sigma be SigmaField of Omega; let ASeq be SetSequence of Sigma; func @Intersection ASeq -> Event of Sigma equals :: PROB_2:def 1 Intersection ASeq; coherence Intersection ASeq is Event of Sigma proof rng ASeq c= Sigma by RELAT_1:def_19; hence Intersection ASeq is Event of Sigma by PROB_1:def_6; ::_thesis: verum end; end; :: deftheorem defines @Intersection PROB_2:def_1_:_ for Omega being set for Sigma being SigmaField of Omega for ASeq being SetSequence of Sigma holds @Intersection ASeq = Intersection ASeq; theorem Th3: :: PROB_2:3 for Omega being set for Sigma being SigmaField of Omega for ASeq being SetSequence of Sigma for B being Event of Sigma ex BSeq being SetSequence of Sigma st for n being Element of NAT holds BSeq . n = (ASeq . n) /\ B proof let Omega be set ; ::_thesis: for Sigma being SigmaField of Omega for ASeq being SetSequence of Sigma for B being Event of Sigma ex BSeq being SetSequence of Sigma st for n being Element of NAT holds BSeq . n = (ASeq . n) /\ B let Sigma be SigmaField of Omega; ::_thesis: for ASeq being SetSequence of Sigma for B being Event of Sigma ex BSeq being SetSequence of Sigma st for n being Element of NAT holds BSeq . n = (ASeq . n) /\ B let ASeq be SetSequence of Sigma; ::_thesis: for B being Event of Sigma ex BSeq being SetSequence of Sigma st for n being Element of NAT holds BSeq . n = (ASeq . n) /\ B let B be Event of Sigma; ::_thesis: ex BSeq being SetSequence of Sigma st for n being Element of NAT holds BSeq . n = (ASeq . n) /\ B deffunc H1( Element of NAT ) -> Event of Sigma = (ASeq . \$1) /\ B; consider f being Function such that A1: ( dom f = NAT & ( for n being Element of NAT holds f . n = H1(n) ) ) from FUNCT_1:sch_4(); now__::_thesis:_for_m_being_Element_of_NAT_holds_f_._m_in_bool_Omega let m be Element of NAT ; ::_thesis: f . m in bool Omega (ASeq . m) /\ B in bool Omega ; hence f . m in bool Omega by A1; ::_thesis: verum end; then for x being set st x in NAT holds f . x in bool Omega ; then reconsider f = f as SetSequence of Omega by A1, FUNCT_2:3; now__::_thesis:_for_m_being_Nat_holds_f_._m_in_Sigma let m be Nat; ::_thesis: f . m in Sigma reconsider m1 = m as Element of NAT by ORDINAL1:def_12; (ASeq . m1) /\ B in Sigma ; hence f . m in Sigma by A1; ::_thesis: verum end; then rng f c= Sigma by NAT_1:52; then reconsider f = f as SetSequence of Sigma by RELAT_1:def_19; take f ; ::_thesis: for n being Element of NAT holds f . n = (ASeq . n) /\ B thus for n being Element of NAT holds f . n = (ASeq . n) /\ B by A1; ::_thesis: verum end; theorem Th4: :: PROB_2:4 for Omega being set for Sigma being SigmaField of Omega for ASeq, BSeq being SetSequence of Sigma for B being Event of Sigma st ASeq is non-ascending & ( for n being Element of NAT holds BSeq . n = (ASeq . n) /\ B ) holds BSeq is non-ascending proof let Omega be set ; ::_thesis: for Sigma being SigmaField of Omega for ASeq, BSeq being SetSequence of Sigma for B being Event of Sigma st ASeq is non-ascending & ( for n being Element of NAT holds BSeq . n = (ASeq . n) /\ B ) holds BSeq is non-ascending let Sigma be SigmaField of Omega; ::_thesis: for ASeq, BSeq being SetSequence of Sigma for B being Event of Sigma st ASeq is non-ascending & ( for n being Element of NAT holds BSeq . n = (ASeq . n) /\ B ) holds BSeq is non-ascending let ASeq, BSeq be SetSequence of Sigma; ::_thesis: for B being Event of Sigma st ASeq is non-ascending & ( for n being Element of NAT holds BSeq . n = (ASeq . n) /\ B ) holds BSeq is non-ascending let B be Event of Sigma; ::_thesis: ( ASeq is non-ascending & ( for n being Element of NAT holds BSeq . n = (ASeq . n) /\ B ) implies BSeq is non-ascending ) assume that A1: ASeq is non-ascending and A2: for n being Element of NAT holds BSeq . n = (ASeq . n) /\ B ; ::_thesis: BSeq is non-ascending thus BSeq is non-ascending ::_thesis: verum proof let m be Element of NAT ; :: according to PROB_1:def_4 ::_thesis: for b1 being Element of NAT holds ( not m <= b1 or BSeq . b1 c= BSeq . m ) let n be Element of NAT ; ::_thesis: ( not m <= n or BSeq . n c= BSeq . m ) assume m <= n ; ::_thesis: BSeq . n c= BSeq . m then ASeq . n c= ASeq . m by A1, PROB_1:def_4; then (ASeq . n) /\ B c= (ASeq . m) /\ B by XBOOLE_1:26; then BSeq . n c= (ASeq . m) /\ B by A2; hence BSeq . n c= BSeq . m by A2; ::_thesis: verum end; end; theorem Th5: :: PROB_2:5 for Omega being set for Sigma being SigmaField of Omega for BSeq, ASeq being SetSequence of Sigma for B being Event of Sigma st ( for n being Element of NAT holds BSeq . n = (ASeq . n) /\ B ) holds (Intersection ASeq) /\ B = Intersection BSeq proof let Omega be set ; ::_thesis: for Sigma being SigmaField of Omega for BSeq, ASeq being SetSequence of Sigma for B being Event of Sigma st ( for n being Element of NAT holds BSeq . n = (ASeq . n) /\ B ) holds (Intersection ASeq) /\ B = Intersection BSeq let Sigma be SigmaField of Omega; ::_thesis: for BSeq, ASeq being SetSequence of Sigma for B being Event of Sigma st ( for n being Element of NAT holds BSeq . n = (ASeq . n) /\ B ) holds (Intersection ASeq) /\ B = Intersection BSeq let BSeq, ASeq be SetSequence of Sigma; ::_thesis: for B being Event of Sigma st ( for n being Element of NAT holds BSeq . n = (ASeq . n) /\ B ) holds (Intersection ASeq) /\ B = Intersection BSeq let B be Event of Sigma; ::_thesis: ( ( for n being Element of NAT holds BSeq . n = (ASeq . n) /\ B ) implies (Intersection ASeq) /\ B = Intersection BSeq ) assume A1: for n being Element of NAT holds BSeq . n = (ASeq . n) /\ B ; ::_thesis: (Intersection ASeq) /\ B = Intersection BSeq A2: now__::_thesis:_for_x_being_set_st_x_in_Intersection_BSeq_holds_ x_in_(Intersection_ASeq)_/\_B let x be set ; ::_thesis: ( x in Intersection BSeq implies x in (Intersection ASeq) /\ B ) assume A3: x in Intersection BSeq ; ::_thesis: x in (Intersection ASeq) /\ B A4: for n being Element of NAT holds x in (ASeq . n) /\ B proof let n be Element of NAT ; ::_thesis: x in (ASeq . n) /\ B x in BSeq . n by A3, PROB_1:13; hence x in (ASeq . n) /\ B by A1; ::_thesis: verum end; A5: for n being Element of NAT holds ( x in ASeq . n & x in B ) proof let n be Element of NAT ; ::_thesis: ( x in ASeq . n & x in B ) x in (ASeq . n) /\ B by A4; hence ( x in ASeq . n & x in B ) by XBOOLE_0:def_4; ::_thesis: verum end; then x in Intersection ASeq by PROB_1:13; hence x in (Intersection ASeq) /\ B by A5, XBOOLE_0:def_4; ::_thesis: verum end; now__::_thesis:_for_x_being_set_st_x_in_(Intersection_ASeq)_/\_B_holds_ x_in_Intersection_BSeq let x be set ; ::_thesis: ( x in (Intersection ASeq) /\ B implies x in Intersection BSeq ) assume A6: x in (Intersection ASeq) /\ B ; ::_thesis: x in Intersection BSeq then A7: x in Intersection ASeq by XBOOLE_0:def_4; A8: for n being Element of NAT holds x in (ASeq . n) /\ B proof let n be Element of NAT ; ::_thesis: x in (ASeq . n) /\ B ( x in ASeq . n & x in B ) by A6, A7, PROB_1:13, XBOOLE_0:def_4; hence x in (ASeq . n) /\ B by XBOOLE_0:def_4; ::_thesis: verum end; for n being Element of NAT holds x in BSeq . n proof let n be Element of NAT ; ::_thesis: x in BSeq . n x in (ASeq . n) /\ B by A8; hence x in BSeq . n by A1; ::_thesis: verum end; hence x in Intersection BSeq by PROB_1:13; ::_thesis: verum end; hence (Intersection ASeq) /\ B = Intersection BSeq by A2, TARSKI:1; ::_thesis: verum end; registration let Omega be set ; let Sigma be SigmaField of Omega; let ASeq be SetSequence of Sigma; cluster Complement ASeq -> Sigma -valued ; coherence Complement ASeq is Sigma -valued proof now__::_thesis:_for_n_being_Nat_holds_(Complement_ASeq)_._n_in_Sigma let n be Nat; ::_thesis: (Complement ASeq) . n in Sigma reconsider n1 = n as Element of NAT by ORDINAL1:def_12; (Complement ASeq) . n1 = (ASeq . n1) ` by PROB_1:def_2; then (Complement ASeq) . n1 is Event of Sigma by PROB_1:20; hence (Complement ASeq) . n in Sigma ; ::_thesis: verum end; then rng (Complement ASeq) c= Sigma by NAT_1:52; hence Complement ASeq is Sigma -valued by RELAT_1:def_19; ::_thesis: verum end; end; theorem :: PROB_2:6 for X being set for S being SetSequence of X holds ( S is non-ascending iff for n being Element of NAT holds S . (n + 1) c= S . n ) proof let X be set ; ::_thesis: for S being SetSequence of X holds ( S is non-ascending iff for n being Element of NAT holds S . (n + 1) c= S . n ) let S be SetSequence of X; ::_thesis: ( S is non-ascending iff for n being Element of NAT holds S . (n + 1) c= S . n ) thus ( S is non-ascending implies for n being Element of NAT holds S . (n + 1) c= S . n ) ::_thesis: ( ( for n being Element of NAT holds S . (n + 1) c= S . n ) implies S is non-ascending ) proof assume A1: S is non-ascending ; ::_thesis: for n being Element of NAT holds S . (n + 1) c= S . n now__::_thesis:_for_n_being_Element_of_NAT_holds_S_._(n_+_1)_c=_S_._n let n be Element of NAT ; ::_thesis: S . (n + 1) c= S . n n <= n + 1 by NAT_1:11; hence S . (n + 1) c= S . n by A1, PROB_1:def_4; ::_thesis: verum end; hence for n being Element of NAT holds S . (n + 1) c= S . n ; ::_thesis: verum end; assume A2: for n being Element of NAT holds S . (n + 1) c= S . n ; ::_thesis: S is non-ascending now__::_thesis:_for_n,_m_being_Element_of_NAT_st_n_<=_m_holds_ S_._m_c=_S_._n let n, m be Element of NAT ; ::_thesis: ( n <= m implies S . m c= S . n ) assume A3: n <= m ; ::_thesis: S . m c= S . n A4: now__::_thesis:_for_k_being_Element_of_NAT_holds_S1[k] defpred S1[ Element of NAT ] means S . (n + \$1) c= S . n; A5: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A6: S . (n + k) c= S . n ; ::_thesis: S1[k + 1] S . ((n + k) + 1) c= S . (n + k) by A2; hence S1[k + 1] by A6, XBOOLE_1:1; ::_thesis: verum end; A7: S1[ 0 ] ; thus for k being Element of NAT holds S1[k] from NAT_1:sch_1(A7, A5); ::_thesis: verum end; consider k being Nat such that A8: m = n + k by A3, NAT_1:10; k in NAT by ORDINAL1:def_12; hence S . m c= S . n by A4, A8; ::_thesis: verum end; hence S is non-ascending by PROB_1:def_4; ::_thesis: verum end; theorem :: PROB_2:7 for X being set for S being SetSequence of X holds ( S is non-descending iff for n being Element of NAT holds S . n c= S . (n + 1) ) proof let X be set ; ::_thesis: for S being SetSequence of X holds ( S is non-descending iff for n being Element of NAT holds S . n c= S . (n + 1) ) let S be SetSequence of X; ::_thesis: ( S is non-descending iff for n being Element of NAT holds S . n c= S . (n + 1) ) thus ( S is non-descending implies for n being Element of NAT holds S . n c= S . (n + 1) ) ::_thesis: ( ( for n being Element of NAT holds S . n c= S . (n + 1) ) implies S is non-descending ) proof assume A1: S is non-descending ; ::_thesis: for n being Element of NAT holds S . n c= S . (n + 1) now__::_thesis:_for_n_being_Element_of_NAT_holds_S_._n_c=_S_._(n_+_1) let n be Element of NAT ; ::_thesis: S . n c= S . (n + 1) n <= n + 1 by NAT_1:11; hence S . n c= S . (n + 1) by A1, PROB_1:def_5; ::_thesis: verum end; hence for n being Element of NAT holds S . n c= S . (n + 1) ; ::_thesis: verum end; assume A2: for n being Element of NAT holds S . n c= S . (n + 1) ; ::_thesis: S is non-descending now__::_thesis:_for_n,_m_being_Element_of_NAT_st_n_<=_m_holds_ S_._n_c=_S_._m let n, m be Element of NAT ; ::_thesis: ( n <= m implies S . n c= S . m ) assume A3: n <= m ; ::_thesis: S . n c= S . m A4: now__::_thesis:_for_k_being_Element_of_NAT_holds_S1[k] defpred S1[ Element of NAT ] means S . n c= S . (n + \$1); A5: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A6: S . n c= S . (n + k) ; ::_thesis: S1[k + 1] S . (n + k) c= S . ((n + k) + 1) by A2; hence S1[k + 1] by A6, XBOOLE_1:1; ::_thesis: verum end; A7: S1[ 0 ] ; thus for k being Element of NAT holds S1[k] from NAT_1:sch_1(A7, A5); ::_thesis: verum end; consider k being Nat such that A8: m = n + k by A3, NAT_1:10; k in NAT by ORDINAL1:def_12; hence S . n c= S . m by A4, A8; ::_thesis: verum end; hence S is non-descending by PROB_1:def_5; ::_thesis: verum end; theorem Th8: :: PROB_2:8 for Omega being set for ASeq being SetSequence of Omega holds ( ASeq is non-ascending iff Complement ASeq is non-descending ) proof let Omega be set ; ::_thesis: for ASeq being SetSequence of Omega holds ( ASeq is non-ascending iff Complement ASeq is non-descending ) let ASeq be SetSequence of Omega; ::_thesis: ( ASeq is non-ascending iff Complement ASeq is non-descending ) thus ( ASeq is non-ascending implies Complement ASeq is non-descending ) ::_thesis: ( Complement ASeq is non-descending implies ASeq is non-ascending ) proof assume A1: ASeq is non-ascending ; ::_thesis: Complement ASeq is non-descending now__::_thesis:_for_n,_m_being_Element_of_NAT_st_n_<=_m_holds_ (Complement_ASeq)_._n_c=_(Complement_ASeq)_._m let n, m be Element of NAT ; ::_thesis: ( n <= m implies (Complement ASeq) . n c= (Complement ASeq) . m ) assume n <= m ; ::_thesis: (Complement ASeq) . n c= (Complement ASeq) . m then ASeq . m c= ASeq . n by A1, PROB_1:def_4; then (ASeq . n) ` c= (ASeq . m) ` by SUBSET_1:12; then (Complement ASeq) . n c= (ASeq . m) ` by PROB_1:def_2; hence (Complement ASeq) . n c= (Complement ASeq) . m by PROB_1:def_2; ::_thesis: verum end; hence Complement ASeq is non-descending by PROB_1:def_5; ::_thesis: verum end; assume A2: Complement ASeq is non-descending ; ::_thesis: ASeq is non-ascending now__::_thesis:_for_n,_m_being_Element_of_NAT_st_n_<=_m_holds_ ASeq_._m_c=_ASeq_._n let n, m be Element of NAT ; ::_thesis: ( n <= m implies ASeq . m c= ASeq . n ) assume n <= m ; ::_thesis: ASeq . m c= ASeq . n then (Complement ASeq) . n c= (Complement ASeq) . m by A2, PROB_1:def_5; then (ASeq . n) ` c= (Complement ASeq) . m by PROB_1:def_2; then (ASeq . n) ` c= (ASeq . m) ` by PROB_1:def_2; hence ASeq . m c= ASeq . n by SUBSET_1:12; ::_thesis: verum end; hence ASeq is non-ascending by PROB_1:def_4; ::_thesis: verum end; Lm1: for Omega being set for ASeq being SetSequence of Omega holds ( ASeq is non-descending iff Complement ASeq is non-ascending ) proof let Omega be set ; ::_thesis: for ASeq being SetSequence of Omega holds ( ASeq is non-descending iff Complement ASeq is non-ascending ) let ASeq be SetSequence of Omega; ::_thesis: ( ASeq is non-descending iff Complement ASeq is non-ascending ) thus ( ASeq is non-descending implies Complement ASeq is non-ascending ) ::_thesis: ( Complement ASeq is non-ascending implies ASeq is non-descending ) proof assume A1: ASeq is non-descending ; ::_thesis: Complement ASeq is non-ascending now__::_thesis:_for_n,_m_being_Element_of_NAT_st_n_<=_m_holds_ (Complement_ASeq)_._m_c=_(Complement_ASeq)_._n let n, m be Element of NAT ; ::_thesis: ( n <= m implies (Complement ASeq) . m c= (Complement ASeq) . n ) assume n <= m ; ::_thesis: (Complement ASeq) . m c= (Complement ASeq) . n then ASeq . n c= ASeq . m by A1, PROB_1:def_5; then (ASeq . m) ` c= (ASeq . n) ` by SUBSET_1:12; then (Complement ASeq) . m c= (ASeq . n) ` by PROB_1:def_2; hence (Complement ASeq) . m c= (Complement ASeq) . n by PROB_1:def_2; ::_thesis: verum end; hence Complement ASeq is non-ascending by PROB_1:def_4; ::_thesis: verum end; assume A2: Complement ASeq is non-ascending ; ::_thesis: ASeq is non-descending now__::_thesis:_for_n,_m_being_Element_of_NAT_st_n_<=_m_holds_ ASeq_._n_c=_ASeq_._m let n, m be Element of NAT ; ::_thesis: ( n <= m implies ASeq . n c= ASeq . m ) assume n <= m ; ::_thesis: ASeq . n c= ASeq . m then (Complement ASeq) . m c= (Complement ASeq) . n by A2, PROB_1:def_4; then (ASeq . m) ` c= (Complement ASeq) . n by PROB_1:def_2; then (ASeq . m) ` c= (ASeq . n) ` by PROB_1:def_2; hence ASeq . n c= ASeq . m by SUBSET_1:12; ::_thesis: verum end; hence ASeq is non-descending by PROB_1:def_5; ::_thesis: verum end; definition let F be Function; attrF is disjoint_valued means :Def2: :: PROB_2:def 2 for x, y being set st x <> y holds F . x misses F . y; end; :: deftheorem Def2 defines disjoint_valued PROB_2:def_2_:_ for F being Function holds ( F is disjoint_valued iff for x, y being set st x <> y holds F . x misses F . y ); definition let Omega be set ; let Sigma be SigmaField of Omega; let ASeq be SetSequence of Sigma; :: original: disjoint_valued redefine attrASeq is disjoint_valued means :: PROB_2:def 3 for m, n being Element of NAT st m <> n holds ASeq . m misses ASeq . n; compatibility ( ASeq is disjoint_valued iff for m, n being Element of NAT st m <> n holds ASeq . m misses ASeq . n ) proof thus ( ASeq is disjoint_valued implies for m, n being Element of NAT st m <> n holds ASeq . m misses ASeq . n ) by Def2; ::_thesis: ( ( for m, n being Element of NAT st m <> n holds ASeq . m misses ASeq . n ) implies ASeq is disjoint_valued ) A1: dom ASeq = NAT by FUNCT_2:def_1; assume A2: for m, n being Element of NAT st m <> n holds ASeq . m misses ASeq . n ; ::_thesis: ASeq is disjoint_valued let x be set ; :: according to PROB_2:def_2 ::_thesis: for y being set st x <> y holds ASeq . x misses ASeq . y let y be set ; ::_thesis: ( x <> y implies ASeq . x misses ASeq . y ) assume A3: x <> y ; ::_thesis: ASeq . x misses ASeq . y percases ( ( x in dom ASeq & y in dom ASeq ) or not x in dom ASeq or not y in dom ASeq ) ; suppose ( x in dom ASeq & y in dom ASeq ) ; ::_thesis: ASeq . x misses ASeq . y hence ASeq . x misses ASeq . y by A1, A2, A3; ::_thesis: verum end; suppose ( not x in dom ASeq or not y in dom ASeq ) ; ::_thesis: ASeq . x misses ASeq . y then ( ASeq . x = {} or ASeq . y = {} ) by FUNCT_1:def_2; hence ASeq . x misses ASeq . y by XBOOLE_1:65; ::_thesis: verum end; end; end; end; :: deftheorem defines disjoint_valued PROB_2:def_3_:_ for Omega being set for Sigma being SigmaField of Omega for ASeq being SetSequence of Sigma holds ( ASeq is disjoint_valued iff for m, n being Element of NAT st m <> n holds ASeq . m misses ASeq . n ); Lm2: for Omega being non empty set for Sigma being SigmaField of Omega for P being Probability of Sigma for ASeq being SetSequence of Sigma st ASeq is non-descending holds ( P * ASeq is convergent & lim (P * ASeq) = P . (Union ASeq) ) proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for P being Probability of Sigma for ASeq being SetSequence of Sigma st ASeq is non-descending holds ( P * ASeq is convergent & lim (P * ASeq) = P . (Union ASeq) ) let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma for ASeq being SetSequence of Sigma st ASeq is non-descending holds ( P * ASeq is convergent & lim (P * ASeq) = P . (Union ASeq) ) let P be Probability of Sigma; ::_thesis: for ASeq being SetSequence of Sigma st ASeq is non-descending holds ( P * ASeq is convergent & lim (P * ASeq) = P . (Union ASeq) ) let ASeq be SetSequence of Sigma; ::_thesis: ( ASeq is non-descending implies ( P * ASeq is convergent & lim (P * ASeq) = P . (Union ASeq) ) ) assume A1: ASeq is non-descending ; ::_thesis: ( P * ASeq is convergent & lim (P * ASeq) = P . (Union ASeq) ) set BSeq = Complement ASeq; A2: Complement ASeq is non-ascending by A1, Lm1; then A3: P * (Complement ASeq) is convergent by PROB_1:def_8; A4: now__::_thesis:_for_n_being_Element_of_NAT_holds_(P_*_ASeq)_._n_=_1_-_((P_*_(Complement_ASeq))_._n) let n be Element of NAT ; ::_thesis: (P * ASeq) . n = 1 - ((P * (Complement ASeq)) . n) (P * (Complement ASeq)) . n = P . ((Complement ASeq) . n) by FUNCT_2:15 .= P . ((ASeq . n) `) by PROB_1:def_2 .= P . (([#] Sigma) \ (ASeq . n)) .= 1 - (P . (ASeq . n)) by PROB_1:32 .= 1 - ((P * ASeq) . n) by FUNCT_2:15 .= 1 + (- ((P * ASeq) . n)) ; hence (P * ASeq) . n = 1 - ((P * (Complement ASeq)) . n) ; ::_thesis: verum end; hence P * ASeq is convergent by A3, Th2; ::_thesis: lim (P * ASeq) = P . (Union ASeq) reconsider V = Union ASeq as Event of Sigma by PROB_1:26; Intersection (Complement ASeq) = ([#] Sigma) \ (Union ASeq) ; then A5: P . (Intersection (Complement ASeq)) = 1 - (P . V) by PROB_1:32; thus lim (P * ASeq) = 1 - (lim (P * (Complement ASeq))) by A3, A4, Th2 .= 1 - (1 - (P . V)) by A2, A5, PROB_1:def_8 .= P . (Union ASeq) ; ::_thesis: verum end; theorem Th9: :: PROB_2:9 for Omega being non empty set for Sigma being SigmaField of Omega for P, P1 being Probability of Sigma st ( for A being Event of Sigma holds P . A = P1 . A ) holds P = P1 proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for P, P1 being Probability of Sigma st ( for A being Event of Sigma holds P . A = P1 . A ) holds P = P1 let Sigma be SigmaField of Omega; ::_thesis: for P, P1 being Probability of Sigma st ( for A being Event of Sigma holds P . A = P1 . A ) holds P = P1 let P, P1 be Probability of Sigma; ::_thesis: ( ( for A being Event of Sigma holds P . A = P1 . A ) implies P = P1 ) assume for A being Event of Sigma holds P . A = P1 . A ; ::_thesis: P = P1 then for x being set st x in Sigma holds P . x = P1 . x ; hence P = P1 by FUNCT_2:12; ::_thesis: verum end; theorem :: PROB_2:10 for Omega being non empty set for Sigma being SigmaField of Omega for P being Function of Sigma,REAL holds ( P is Probability of Sigma iff ( ( for A being Event of Sigma holds 0 <= P . A ) & P . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds P . (A \/ B) = (P . A) + (P . B) ) & ( for ASeq being SetSequence of Sigma st ASeq is non-descending holds ( P * ASeq is convergent & lim (P * ASeq) = P . (Union ASeq) ) ) ) ) proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for P being Function of Sigma,REAL holds ( P is Probability of Sigma iff ( ( for A being Event of Sigma holds 0 <= P . A ) & P . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds P . (A \/ B) = (P . A) + (P . B) ) & ( for ASeq being SetSequence of Sigma st ASeq is non-descending holds ( P * ASeq is convergent & lim (P * ASeq) = P . (Union ASeq) ) ) ) ) let Sigma be SigmaField of Omega; ::_thesis: for P being Function of Sigma,REAL holds ( P is Probability of Sigma iff ( ( for A being Event of Sigma holds 0 <= P . A ) & P . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds P . (A \/ B) = (P . A) + (P . B) ) & ( for ASeq being SetSequence of Sigma st ASeq is non-descending holds ( P * ASeq is convergent & lim (P * ASeq) = P . (Union ASeq) ) ) ) ) let P be Function of Sigma,REAL; ::_thesis: ( P is Probability of Sigma iff ( ( for A being Event of Sigma holds 0 <= P . A ) & P . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds P . (A \/ B) = (P . A) + (P . B) ) & ( for ASeq being SetSequence of Sigma st ASeq is non-descending holds ( P * ASeq is convergent & lim (P * ASeq) = P . (Union ASeq) ) ) ) ) thus ( P is Probability of Sigma implies ( ( for A being Event of Sigma holds 0 <= P . A ) & P . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds P . (A \/ B) = (P . A) + (P . B) ) & ( for ASeq being SetSequence of Sigma st ASeq is non-descending holds ( P * ASeq is convergent & lim (P * ASeq) = P . (Union ASeq) ) ) ) ) by Lm2, PROB_1:def_8; ::_thesis: ( ( for A being Event of Sigma holds 0 <= P . A ) & P . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds P . (A \/ B) = (P . A) + (P . B) ) & ( for ASeq being SetSequence of Sigma st ASeq is non-descending holds ( P * ASeq is convergent & lim (P * ASeq) = P . (Union ASeq) ) ) implies P is Probability of Sigma ) assume that A1: for A being Event of Sigma holds 0 <= P . A and A2: P . Omega = 1 and A3: for A, B being Event of Sigma st A misses B holds P . (A \/ B) = (P . A) + (P . B) and A4: for ASeq being SetSequence of Sigma st ASeq is non-descending holds ( P * ASeq is convergent & lim (P * ASeq) = P . (Union ASeq) ) ; ::_thesis: P is Probability of Sigma for ASeq being SetSequence of Sigma st ASeq is non-ascending holds ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) proof let ASeq be SetSequence of Sigma; ::_thesis: ( ASeq is non-ascending implies ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) ) assume A5: ASeq is non-ascending ; ::_thesis: ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) Intersection ASeq = @Intersection ASeq ; then reconsider V = Intersection ASeq as Event of Sigma ; set BSeq = Complement ASeq; A6: for A being Event of Sigma holds P . (A `) = 1 - (P . A) proof let A be Event of Sigma; ::_thesis: P . (A `) = 1 - (P . A) reconsider B = A ` as Event of Sigma by PROB_1:20; A7: A misses B by SUBSET_1:24; 1 = P . ([#] Omega) by A2 .= P . (A \/ B) by SUBSET_1:10 .= (P . A) + (P . B) by A3, A7 ; hence P . (A `) = 1 - (P . A) ; ::_thesis: verum end; A8: now__::_thesis:_for_n_being_Element_of_NAT_holds_(P_*_ASeq)_._n_=_1_-_((P_*_(Complement_ASeq))_._n) let n be Element of NAT ; ::_thesis: (P * ASeq) . n = 1 - ((P * (Complement ASeq)) . n) (P * (Complement ASeq)) . n = P . ((Complement ASeq) . n) by FUNCT_2:15 .= P . ((ASeq . n) `) by PROB_1:def_2 .= 1 - (P . (ASeq . n)) by A6 .= 1 - ((P * ASeq) . n) by FUNCT_2:15 .= 1 + (- ((P * ASeq) . n)) ; hence (P * ASeq) . n = 1 - ((P * (Complement ASeq)) . n) ; ::_thesis: verum end; Union (Complement ASeq) = (Intersection ASeq) ` ; then A9: P . (Union (Complement ASeq)) = 1 - (P . V) by A6; A10: Complement ASeq is non-descending by A5, Th8; then A11: P * (Complement ASeq) is convergent by A4; hence P * ASeq is convergent by A8, Th2; ::_thesis: lim (P * ASeq) = P . (Intersection ASeq) thus lim (P * ASeq) = 1 - (lim (P * (Complement ASeq))) by A11, A8, Th2 .= 1 - (1 - (P . V)) by A4, A10, A9 .= P . (Intersection ASeq) ; ::_thesis: verum end; hence P is Probability of Sigma by A1, A2, A3, PROB_1:def_8; ::_thesis: verum end; theorem :: PROB_2:11 for Omega being non empty set for Sigma being SigmaField of Omega for A, B, C being Event of Sigma for P being Probability of Sigma holds P . ((A \/ B) \/ C) = ((((P . A) + (P . B)) + (P . C)) - (((P . (A /\ B)) + (P . (B /\ C))) + (P . (A /\ C)))) + (P . ((A /\ B) /\ C)) proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for A, B, C being Event of Sigma for P being Probability of Sigma holds P . ((A \/ B) \/ C) = ((((P . A) + (P . B)) + (P . C)) - (((P . (A /\ B)) + (P . (B /\ C))) + (P . (A /\ C)))) + (P . ((A /\ B) /\ C)) let Sigma be SigmaField of Omega; ::_thesis: for A, B, C being Event of Sigma for P being Probability of Sigma holds P . ((A \/ B) \/ C) = ((((P . A) + (P . B)) + (P . C)) - (((P . (A /\ B)) + (P . (B /\ C))) + (P . (A /\ C)))) + (P . ((A /\ B) /\ C)) let A, B, C be Event of Sigma; ::_thesis: for P being Probability of Sigma holds P . ((A \/ B) \/ C) = ((((P . A) + (P . B)) + (P . C)) - (((P . (A /\ B)) + (P . (B /\ C))) + (P . (A /\ C)))) + (P . ((A /\ B) /\ C)) let P be Probability of Sigma; ::_thesis: P . ((A \/ B) \/ C) = ((((P . A) + (P . B)) + (P . C)) - (((P . (A /\ B)) + (P . (B /\ C))) + (P . (A /\ C)))) + (P . ((A /\ B) /\ C)) A1: P . ((A \/ B) /\ C) = P . ((A /\ C) \/ (B /\ C)) by XBOOLE_1:23 .= ((P . (A /\ C)) + (P . (B /\ C))) - (P . ((A /\ C) /\ (B /\ C))) by PROB_1:38 .= ((P . (A /\ C)) + (P . (B /\ C))) - (P . (A /\ ((B /\ C) /\ C))) by XBOOLE_1:16 .= ((P . (A /\ C)) + (P . (B /\ C))) - (P . (A /\ (B /\ (C /\ C)))) by XBOOLE_1:16 .= ((P . (B /\ C)) + (P . (A /\ C))) - (P . ((A /\ B) /\ C)) by XBOOLE_1:16 ; P . ((A \/ B) \/ C) = ((P . (A \/ B)) + (P . C)) - (P . ((A \/ B) /\ C)) by PROB_1:38 .= ((((P . A) + (P . B)) - (P . (A /\ B))) + (P . C)) - (P . ((A \/ B) /\ C)) by PROB_1:38 .= (((P . A) + (P . B)) + (P . C)) - ((P . (A /\ B)) + (P . ((A \/ B) /\ C))) ; hence P . ((A \/ B) \/ C) = ((((P . A) + (P . B)) + (P . C)) - (((P . (A /\ B)) + (P . (B /\ C))) + (P . (A /\ C)))) + (P . ((A /\ B) /\ C)) by A1; ::_thesis: verum end; theorem :: PROB_2:12 for Omega being non empty set for Sigma being SigmaField of Omega for A, B being Event of Sigma for P being Probability of Sigma holds P . (A \ (A /\ B)) = (P . A) - (P . (A /\ B)) by PROB_1:33, XBOOLE_1:17; theorem :: PROB_2:13 for Omega being non empty set for Sigma being SigmaField of Omega for A, B being Event of Sigma for P being Probability of Sigma holds ( P . (A /\ B) <= P . B & P . (A /\ B) <= P . A ) by PROB_1:34, XBOOLE_1:17; theorem Th14: :: PROB_2:14 for Omega being non empty set for Sigma being SigmaField of Omega for C, B, A being Event of Sigma for P being Probability of Sigma st C = B ` holds P . A = (P . (A /\ B)) + (P . (A /\ C)) proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for C, B, A being Event of Sigma for P being Probability of Sigma st C = B ` holds P . A = (P . (A /\ B)) + (P . (A /\ C)) let Sigma be SigmaField of Omega; ::_thesis: for C, B, A being Event of Sigma for P being Probability of Sigma st C = B ` holds P . A = (P . (A /\ B)) + (P . (A /\ C)) let C, B, A be Event of Sigma; ::_thesis: for P being Probability of Sigma st C = B ` holds P . A = (P . (A /\ B)) + (P . (A /\ C)) let P be Probability of Sigma; ::_thesis: ( C = B ` implies P . A = (P . (A /\ B)) + (P . (A /\ C)) ) assume A1: C = B ` ; ::_thesis: P . A = (P . (A /\ B)) + (P . (A /\ C)) then B misses C by SUBSET_1:24; then A /\ C misses B by XBOOLE_1:74; then A2: A /\ B misses A /\ C by XBOOLE_1:74; P . A = P . (A /\ ([#] Omega)) by XBOOLE_1:28 .= P . (A /\ (B \/ C)) by A1, SUBSET_1:10 .= P . ((A /\ B) \/ (A /\ C)) by XBOOLE_1:23 .= (P . (A /\ B)) + (P . (A /\ C)) by A2, PROB_1:def_8 ; hence P . A = (P . (A /\ B)) + (P . (A /\ C)) ; ::_thesis: verum end; theorem Th15: :: PROB_2:15 for Omega being non empty set for Sigma being SigmaField of Omega for A, B being Event of Sigma for P being Probability of Sigma holds ((P . A) + (P . B)) - 1 <= P . (A /\ B) proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for A, B being Event of Sigma for P being Probability of Sigma holds ((P . A) + (P . B)) - 1 <= P . (A /\ B) let Sigma be SigmaField of Omega; ::_thesis: for A, B being Event of Sigma for P being Probability of Sigma holds ((P . A) + (P . B)) - 1 <= P . (A /\ B) let A, B be Event of Sigma; ::_thesis: for P being Probability of Sigma holds ((P . A) + (P . B)) - 1 <= P . (A /\ B) let P be Probability of Sigma; ::_thesis: ((P . A) + (P . B)) - 1 <= P . (A /\ B) ((P . A) + (P . B)) - (P . (A /\ B)) = P . (A \/ B) by PROB_1:38; then ((P . A) + (P . B)) - (P . (A /\ B)) <= 1 by PROB_1:35; then (P . A) + (P . B) <= (P . (A /\ B)) + 1 by XREAL_1:20; hence ((P . A) + (P . B)) - 1 <= P . (A /\ B) by XREAL_1:20; ::_thesis: verum end; theorem Th16: :: PROB_2:16 for Omega being non empty set for Sigma being SigmaField of Omega for A being Event of Sigma for P being Probability of Sigma holds P . A = 1 - (P . (([#] Sigma) \ A)) proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for A being Event of Sigma for P being Probability of Sigma holds P . A = 1 - (P . (([#] Sigma) \ A)) let Sigma be SigmaField of Omega; ::_thesis: for A being Event of Sigma for P being Probability of Sigma holds P . A = 1 - (P . (([#] Sigma) \ A)) let A be Event of Sigma; ::_thesis: for P being Probability of Sigma holds P . A = 1 - (P . (([#] Sigma) \ A)) let P be Probability of Sigma; ::_thesis: P . A = 1 - (P . (([#] Sigma) \ A)) (P . (([#] Sigma) \ A)) + (P . A) = 1 by PROB_1:31; hence P . A = 1 - (P . (([#] Sigma) \ A)) ; ::_thesis: verum end; theorem Th17: :: PROB_2:17 for Omega being non empty set for Sigma being SigmaField of Omega for A being Event of Sigma for P being Probability of Sigma holds ( P . A < 1 iff 0 < P . (([#] Sigma) \ A) ) proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for A being Event of Sigma for P being Probability of Sigma holds ( P . A < 1 iff 0 < P . (([#] Sigma) \ A) ) let Sigma be SigmaField of Omega; ::_thesis: for A being Event of Sigma for P being Probability of Sigma holds ( P . A < 1 iff 0 < P . (([#] Sigma) \ A) ) let A be Event of Sigma; ::_thesis: for P being Probability of Sigma holds ( P . A < 1 iff 0 < P . (([#] Sigma) \ A) ) let P be Probability of Sigma; ::_thesis: ( P . A < 1 iff 0 < P . (([#] Sigma) \ A) ) thus ( P . A < 1 implies 0 < P . (([#] Sigma) \ A) ) ::_thesis: ( 0 < P . (([#] Sigma) \ A) implies P . A < 1 ) proof assume P . A < 1 ; ::_thesis: 0 < P . (([#] Sigma) \ A) then 1 - (P . (([#] Sigma) \ A)) < 1 by Th16; then 1 + (- (P . (([#] Sigma) \ A))) < 1 ; then - (P . (([#] Sigma) \ A)) < 1 - 1 by XREAL_1:20; hence 0 < P . (([#] Sigma) \ A) ; ::_thesis: verum end; assume 0 < P . (([#] Sigma) \ A) ; ::_thesis: P . A < 1 then 0 < 1 - (P . A) by PROB_1:32; then (P . A) + 0 < 1 by XREAL_1:20; hence P . A < 1 ; ::_thesis: verum end; theorem :: PROB_2:18 for Omega being non empty set for Sigma being SigmaField of Omega for A being Event of Sigma for P being Probability of Sigma holds ( P . (([#] Sigma) \ A) < 1 iff 0 < P . A ) proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for A being Event of Sigma for P being Probability of Sigma holds ( P . (([#] Sigma) \ A) < 1 iff 0 < P . A ) let Sigma be SigmaField of Omega; ::_thesis: for A being Event of Sigma for P being Probability of Sigma holds ( P . (([#] Sigma) \ A) < 1 iff 0 < P . A ) let A be Event of Sigma; ::_thesis: for P being Probability of Sigma holds ( P . (([#] Sigma) \ A) < 1 iff 0 < P . A ) let P be Probability of Sigma; ::_thesis: ( P . (([#] Sigma) \ A) < 1 iff 0 < P . A ) thus ( P . (([#] Sigma) \ A) < 1 implies 0 < P . A ) ::_thesis: ( 0 < P . A implies P . (([#] Sigma) \ A) < 1 ) proof assume P . (([#] Sigma) \ A) < 1 ; ::_thesis: 0 < P . A then 1 - (P . A) < 1 by PROB_1:32; then 1 + (- (P . A)) < 1 ; then - (P . A) < 1 - 1 by XREAL_1:20; hence 0 < P . A ; ::_thesis: verum end; assume 0 < P . A ; ::_thesis: P . (([#] Sigma) \ A) < 1 then 0 < 1 - (P . (([#] Sigma) \ A)) by Th16; then (P . (([#] Sigma) \ A)) + 0 < 1 by XREAL_1:20; hence P . (([#] Sigma) \ A) < 1 ; ::_thesis: verum end; definition let Omega be non empty set ; let Sigma be SigmaField of Omega; let P be Probability of Sigma; let A, B be Event of Sigma; predA,B are_independent_respect_to P means :Def4: :: PROB_2:def 4 P . (A /\ B) = (P . A) * (P . B); let C be Event of Sigma; predA,B,C are_independent_respect_to P means :Def5: :: PROB_2:def 5 ( P . ((A /\ B) /\ C) = ((P . A) * (P . B)) * (P . C) & P . (A /\ B) = (P . A) * (P . B) & P . (A /\ C) = (P . A) * (P . C) & P . (B /\ C) = (P . B) * (P . C) ); end; :: deftheorem Def4 defines are_independent_respect_to PROB_2:def_4_:_ for Omega being non empty set for Sigma being SigmaField of Omega for P being Probability of Sigma for A, B being Event of Sigma holds ( A,B are_independent_respect_to P iff P . (A /\ B) = (P . A) * (P . B) ); :: deftheorem Def5 defines are_independent_respect_to PROB_2:def_5_:_ for Omega being non empty set for Sigma being SigmaField of Omega for P being Probability of Sigma for A, B, C being Event of Sigma holds ( A,B,C are_independent_respect_to P iff ( P . ((A /\ B) /\ C) = ((P . A) * (P . B)) * (P . C) & P . (A /\ B) = (P . A) * (P . B) & P . (A /\ C) = (P . A) * (P . C) & P . (B /\ C) = (P . B) * (P . C) ) ); theorem Th19: :: PROB_2:19 for Omega being non empty set for Sigma being SigmaField of Omega for A, B being Event of Sigma for P being Probability of Sigma st A,B are_independent_respect_to P holds B,A are_independent_respect_to P proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for A, B being Event of Sigma for P being Probability of Sigma st A,B are_independent_respect_to P holds B,A are_independent_respect_to P let Sigma be SigmaField of Omega; ::_thesis: for A, B being Event of Sigma for P being Probability of Sigma st A,B are_independent_respect_to P holds B,A are_independent_respect_to P let A, B be Event of Sigma; ::_thesis: for P being Probability of Sigma st A,B are_independent_respect_to P holds B,A are_independent_respect_to P let P be Probability of Sigma; ::_thesis: ( A,B are_independent_respect_to P implies B,A are_independent_respect_to P ) assume A,B are_independent_respect_to P ; ::_thesis: B,A are_independent_respect_to P then P . (B /\ A) = (P . B) * (P . A) by Def4; hence B,A are_independent_respect_to P by Def4; ::_thesis: verum end; theorem Th20: :: PROB_2:20 for Omega being non empty set for Sigma being SigmaField of Omega for A, B, C being Event of Sigma for P being Probability of Sigma holds ( A,B,C are_independent_respect_to P iff ( P . ((A /\ B) /\ C) = ((P . A) * (P . B)) * (P . C) & A,B are_independent_respect_to P & B,C are_independent_respect_to P & A,C are_independent_respect_to P ) ) proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for A, B, C being Event of Sigma for P being Probability of Sigma holds ( A,B,C are_independent_respect_to P iff ( P . ((A /\ B) /\ C) = ((P . A) * (P . B)) * (P . C) & A,B are_independent_respect_to P & B,C are_independent_respect_to P & A,C are_independent_respect_to P ) ) let Sigma be SigmaField of Omega; ::_thesis: for A, B, C being Event of Sigma for P being Probability of Sigma holds ( A,B,C are_independent_respect_to P iff ( P . ((A /\ B) /\ C) = ((P . A) * (P . B)) * (P . C) & A,B are_independent_respect_to P & B,C are_independent_respect_to P & A,C are_independent_respect_to P ) ) let A, B, C be Event of Sigma; ::_thesis: for P being Probability of Sigma holds ( A,B,C are_independent_respect_to P iff ( P . ((A /\ B) /\ C) = ((P . A) * (P . B)) * (P . C) & A,B are_independent_respect_to P & B,C are_independent_respect_to P & A,C are_independent_respect_to P ) ) let P be Probability of Sigma; ::_thesis: ( A,B,C are_independent_respect_to P iff ( P . ((A /\ B) /\ C) = ((P . A) * (P . B)) * (P . C) & A,B are_independent_respect_to P & B,C are_independent_respect_to P & A,C are_independent_respect_to P ) ) thus ( A,B,C are_independent_respect_to P implies ( P . ((A /\ B) /\ C) = ((P . A) * (P . B)) * (P . C) & A,B are_independent_respect_to P & B,C are_independent_respect_to P & A,C are_independent_respect_to P ) ) ::_thesis: ( P . ((A /\ B) /\ C) = ((P . A) * (P . B)) * (P . C) & A,B are_independent_respect_to P & B,C are_independent_respect_to P & A,C are_independent_respect_to P implies A,B,C are_independent_respect_to P ) proof assume A1: A,B,C are_independent_respect_to P ; ::_thesis: ( P . ((A /\ B) /\ C) = ((P . A) * (P . B)) * (P . C) & A,B are_independent_respect_to P & B,C are_independent_respect_to P & A,C are_independent_respect_to P ) then A2: P . (B /\ C) = (P . B) * (P . C) by Def5; ( P . (A /\ B) = (P . A) * (P . B) & P . (A /\ C) = (P . A) * (P . C) ) by A1, Def5; hence ( P . ((A /\ B) /\ C) = ((P . A) * (P . B)) * (P . C) & A,B are_independent_respect_to P & B,C are_independent_respect_to P & A,C are_independent_respect_to P ) by A1, A2, Def4, Def5; ::_thesis: verum end; assume that A3: P . ((A /\ B) /\ C) = ((P . A) * (P . B)) * (P . C) and A4: A,B are_independent_respect_to P and A5: B,C are_independent_respect_to P and A6: A,C are_independent_respect_to P ; ::_thesis: A,B,C are_independent_respect_to P A7: P . (B /\ C) = (P . B) * (P . C) by A5, Def4; ( P . (A /\ B) = (P . A) * (P . B) & P . (A /\ C) = (P . A) * (P . C) ) by A4, A6, Def4; hence A,B,C are_independent_respect_to P by A3, A7, Def5; ::_thesis: verum end; theorem :: PROB_2:21 for Omega being non empty set for Sigma being SigmaField of Omega for A, B, C being Event of Sigma for P being Probability of Sigma st A,B,C are_independent_respect_to P holds B,A,C are_independent_respect_to P proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for A, B, C being Event of Sigma for P being Probability of Sigma st A,B,C are_independent_respect_to P holds B,A,C are_independent_respect_to P let Sigma be SigmaField of Omega; ::_thesis: for A, B, C being Event of Sigma for P being Probability of Sigma st A,B,C are_independent_respect_to P holds B,A,C are_independent_respect_to P let A, B, C be Event of Sigma; ::_thesis: for P being Probability of Sigma st A,B,C are_independent_respect_to P holds B,A,C are_independent_respect_to P let P be Probability of Sigma; ::_thesis: ( A,B,C are_independent_respect_to P implies B,A,C are_independent_respect_to P ) assume A1: A,B,C are_independent_respect_to P ; ::_thesis: B,A,C are_independent_respect_to P then A2: A,C are_independent_respect_to P by Th20; A,B are_independent_respect_to P by A1, Th20; then A3: B,A are_independent_respect_to P by Th19; ( P . ((A /\ B) /\ C) = ((P . A) * (P . B)) * (P . C) & B,C are_independent_respect_to P ) by A1, Th20; hence B,A,C are_independent_respect_to P by A2, A3, Th20; ::_thesis: verum end; theorem :: PROB_2:22 for Omega being non empty set for Sigma being SigmaField of Omega for A, B, C being Event of Sigma for P being Probability of Sigma st A,B,C are_independent_respect_to P holds A,C,B are_independent_respect_to P proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for A, B, C being Event of Sigma for P being Probability of Sigma st A,B,C are_independent_respect_to P holds A,C,B are_independent_respect_to P let Sigma be SigmaField of Omega; ::_thesis: for A, B, C being Event of Sigma for P being Probability of Sigma st A,B,C are_independent_respect_to P holds A,C,B are_independent_respect_to P let A, B, C be Event of Sigma; ::_thesis: for P being Probability of Sigma st A,B,C are_independent_respect_to P holds A,C,B are_independent_respect_to P let P be Probability of Sigma; ::_thesis: ( A,B,C are_independent_respect_to P implies A,C,B are_independent_respect_to P ) assume A1: A,B,C are_independent_respect_to P ; ::_thesis: A,C,B are_independent_respect_to P then P . ((A /\ B) /\ C) = ((P . A) * (P . B)) * (P . C) by Th20; then A2: P . ((A /\ C) /\ B) = ((P . A) * (P . C)) * (P . B) by XBOOLE_1:16; B,C are_independent_respect_to P by A1, Th20; then A3: C,B are_independent_respect_to P by Th19; ( A,B are_independent_respect_to P & A,C are_independent_respect_to P ) by A1, Th20; hence A,C,B are_independent_respect_to P by A2, A3, Th20; ::_thesis: verum end; theorem :: PROB_2:23 for Omega being non empty set for Sigma being SigmaField of Omega for A being Event of Sigma for P being Probability of Sigma for E being Event of Sigma st E = {} holds A,E are_independent_respect_to P proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for A being Event of Sigma for P being Probability of Sigma for E being Event of Sigma st E = {} holds A,E are_independent_respect_to P let Sigma be SigmaField of Omega; ::_thesis: for A being Event of Sigma for P being Probability of Sigma for E being Event of Sigma st E = {} holds A,E are_independent_respect_to P let A be Event of Sigma; ::_thesis: for P being Probability of Sigma for E being Event of Sigma st E = {} holds A,E are_independent_respect_to P let P be Probability of Sigma; ::_thesis: for E being Event of Sigma st E = {} holds A,E are_independent_respect_to P let E be Event of Sigma; ::_thesis: ( E = {} implies A,E are_independent_respect_to P ) A1: P . (A /\ ({} Sigma)) = (P . A) * 0 by VALUED_0:def_19 .= (P . A) * (P . ({} Sigma)) by VALUED_0:def_19 ; assume E = {} ; ::_thesis: A,E are_independent_respect_to P hence A,E are_independent_respect_to P by A1, Def4; ::_thesis: verum end; theorem :: PROB_2:24 for Omega being non empty set for Sigma being SigmaField of Omega for A being Event of Sigma for P being Probability of Sigma holds A, [#] Sigma are_independent_respect_to P proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for A being Event of Sigma for P being Probability of Sigma holds A, [#] Sigma are_independent_respect_to P let Sigma be SigmaField of Omega; ::_thesis: for A being Event of Sigma for P being Probability of Sigma holds A, [#] Sigma are_independent_respect_to P let A be Event of Sigma; ::_thesis: for P being Probability of Sigma holds A, [#] Sigma are_independent_respect_to P let P be Probability of Sigma; ::_thesis: A, [#] Sigma are_independent_respect_to P P . (A /\ ([#] Sigma)) = (P . A) * 1 by XBOOLE_1:28 .= (P . A) * (P . ([#] Sigma)) by PROB_1:30 ; hence A, [#] Sigma are_independent_respect_to P by Def4; ::_thesis: verum end; theorem Th25: :: PROB_2:25 for Omega being non empty set for Sigma being SigmaField of Omega for A, B being Event of Sigma for P being Probability of Sigma st A,B are_independent_respect_to P holds A,([#] Sigma) \ B are_independent_respect_to P proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for A, B being Event of Sigma for P being Probability of Sigma st A,B are_independent_respect_to P holds A,([#] Sigma) \ B are_independent_respect_to P let Sigma be SigmaField of Omega; ::_thesis: for A, B being Event of Sigma for P being Probability of Sigma st A,B are_independent_respect_to P holds A,([#] Sigma) \ B are_independent_respect_to P let A, B be Event of Sigma; ::_thesis: for P being Probability of Sigma st A,B are_independent_respect_to P holds A,([#] Sigma) \ B are_independent_respect_to P let P be Probability of Sigma; ::_thesis: ( A,B are_independent_respect_to P implies A,([#] Sigma) \ B are_independent_respect_to P ) assume A,B are_independent_respect_to P ; ::_thesis: A,([#] Sigma) \ B are_independent_respect_to P then A1: P . (A /\ B) = (P . A) * (P . B) by Def4; P . (A /\ (([#] Sigma) \ B)) = P . (A /\ (B `)) .= P . (A \ B) by SUBSET_1:13 .= P . (A \ (A /\ B)) by XBOOLE_1:47 .= ((P . A) * 1) - ((P . A) * (P . B)) by A1, PROB_1:33, XBOOLE_1:17 .= (P . A) * (1 - (P . B)) .= (P . A) * (P . (([#] Sigma) \ B)) by PROB_1:32 ; hence A,([#] Sigma) \ B are_independent_respect_to P by Def4; ::_thesis: verum end; theorem Th26: :: PROB_2:26 for Omega being non empty set for Sigma being SigmaField of Omega for A, B being Event of Sigma for P being Probability of Sigma st A,B are_independent_respect_to P holds ([#] Sigma) \ A,([#] Sigma) \ B are_independent_respect_to P proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for A, B being Event of Sigma for P being Probability of Sigma st A,B are_independent_respect_to P holds ([#] Sigma) \ A,([#] Sigma) \ B are_independent_respect_to P let Sigma be SigmaField of Omega; ::_thesis: for A, B being Event of Sigma for P being Probability of Sigma st A,B are_independent_respect_to P holds ([#] Sigma) \ A,([#] Sigma) \ B are_independent_respect_to P let A, B be Event of Sigma; ::_thesis: for P being Probability of Sigma st A,B are_independent_respect_to P holds ([#] Sigma) \ A,([#] Sigma) \ B are_independent_respect_to P let P be Probability of Sigma; ::_thesis: ( A,B are_independent_respect_to P implies ([#] Sigma) \ A,([#] Sigma) \ B are_independent_respect_to P ) assume A,B are_independent_respect_to P ; ::_thesis: ([#] Sigma) \ A,([#] Sigma) \ B are_independent_respect_to P then A,([#] Sigma) \ B are_independent_respect_to P by Th25; then ([#] Sigma) \ B,A are_independent_respect_to P by Th19; then ([#] Sigma) \ B,([#] Sigma) \ A are_independent_respect_to P by Th25; hence ([#] Sigma) \ A,([#] Sigma) \ B are_independent_respect_to P by Th19; ::_thesis: verum end; theorem :: PROB_2:27 for Omega being non empty set for Sigma being SigmaField of Omega for A, B, C being Event of Sigma for P being Probability of Sigma st A,B are_independent_respect_to P & A,C are_independent_respect_to P & B misses C holds A,B \/ C are_independent_respect_to P proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for A, B, C being Event of Sigma for P being Probability of Sigma st A,B are_independent_respect_to P & A,C are_independent_respect_to P & B misses C holds A,B \/ C are_independent_respect_to P let Sigma be SigmaField of Omega; ::_thesis: for A, B, C being Event of Sigma for P being Probability of Sigma st A,B are_independent_respect_to P & A,C are_independent_respect_to P & B misses C holds A,B \/ C are_independent_respect_to P let A, B, C be Event of Sigma; ::_thesis: for P being Probability of Sigma st A,B are_independent_respect_to P & A,C are_independent_respect_to P & B misses C holds A,B \/ C are_independent_respect_to P let P be Probability of Sigma; ::_thesis: ( A,B are_independent_respect_to P & A,C are_independent_respect_to P & B misses C implies A,B \/ C are_independent_respect_to P ) assume that A1: A,B are_independent_respect_to P and A2: A,C are_independent_respect_to P and A3: B misses C ; ::_thesis: A,B \/ C are_independent_respect_to P A4: A /\ B misses A /\ C by A3, XBOOLE_1:76; P . (A /\ (B \/ C)) = P . ((A /\ B) \/ (A /\ C)) by XBOOLE_1:23 .= (P . (A /\ B)) + (P . (A /\ C)) by A4, PROB_1:def_8 .= ((P . A) * (P . B)) + (P . (A /\ C)) by A1, Def4 .= ((P . A) * (P . B)) + ((P . A) * (P . C)) by A2, Def4 .= (P . A) * ((P . B) + (P . C)) .= (P . A) * (P . (B \/ C)) by A3, PROB_1:def_8 ; hence A,B \/ C are_independent_respect_to P by Def4; ::_thesis: verum end; theorem :: PROB_2:28 for Omega being non empty set for Sigma being SigmaField of Omega for P being Probability of Sigma for A, B being Event of Sigma st A,B are_independent_respect_to P & P . A < 1 & P . B < 1 holds P . (A \/ B) < 1 proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for P being Probability of Sigma for A, B being Event of Sigma st A,B are_independent_respect_to P & P . A < 1 & P . B < 1 holds P . (A \/ B) < 1 let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma for A, B being Event of Sigma st A,B are_independent_respect_to P & P . A < 1 & P . B < 1 holds P . (A \/ B) < 1 A1: now__::_thesis:_for_r,_r1_being_Real_st_0_<_r1_holds_ r_-_r1_<_r let r, r1 be Real; ::_thesis: ( 0 < r1 implies r - r1 < r ) assume 0 < r1 ; ::_thesis: r - r1 < r then - r1 < - 0 by XREAL_1:24; then r + (- r1) < r + 0 by XREAL_1:6; hence r - r1 < r ; ::_thesis: verum end; let P be Probability of Sigma; ::_thesis: for A, B being Event of Sigma st A,B are_independent_respect_to P & P . A < 1 & P . B < 1 holds P . (A \/ B) < 1 let A, B be Event of Sigma; ::_thesis: ( A,B are_independent_respect_to P & P . A < 1 & P . B < 1 implies P . (A \/ B) < 1 ) assume that A2: A,B are_independent_respect_to P and A3: ( P . A < 1 & P . B < 1 ) ; ::_thesis: P . (A \/ B) < 1 A4: ([#] Sigma) \ A,([#] Sigma) \ B are_independent_respect_to P by A2, Th26; A5: ( 0 < P . (([#] Sigma) \ A) & 0 < P . (([#] Sigma) \ B) ) by A3, Th17; P . (A \/ B) = 1 - (P . (([#] Sigma) \ (A \/ B))) by Th16 .= 1 - (P . ((([#] Sigma) \ A) /\ (([#] Sigma) \ B))) by XBOOLE_1:53 .= 1 - ((P . (([#] Sigma) \ A)) * (P . (([#] Sigma) \ B))) by A4, Def4 ; hence P . (A \/ B) < 1 by A5, A1, XREAL_1:129; ::_thesis: verum end; definition let Omega be non empty set ; let Sigma be SigmaField of Omega; let P be Probability of Sigma; let B be Event of Sigma; assume A1: 0 < P . B ; funcP .|. B -> Probability of Sigma means :Def6: :: PROB_2:def 6 for A being Event of Sigma holds it . A = (P . (A /\ B)) / (P . B); existence ex b1 being Probability of Sigma st for A being Event of Sigma holds b1 . A = (P . (A /\ B)) / (P . B) proof defpred S1[ set , set ] means ex A being Event of Sigma ex r being Real st ( A = \$1 & r = \$2 & r = (P . (A /\ B)) / (P . B) ); A2: for x being set st x in Sigma holds ex y being set st ( y in REAL & S1[x,y] ) proof let x be set ; ::_thesis: ( x in Sigma implies ex y being set st ( y in REAL & S1[x,y] ) ) assume x in Sigma ; ::_thesis: ex y being set st ( y in REAL & S1[x,y] ) then reconsider x = x as Event of Sigma ; consider y being set such that A3: y = (P . (x /\ B)) / (P . B) ; take y ; ::_thesis: ( y in REAL & S1[x,y] ) thus ( y in REAL & S1[x,y] ) by A3; ::_thesis: verum end; consider f being Function of Sigma,REAL such that A4: for x being set st x in Sigma holds S1[x,f . x] from FUNCT_2:sch_1(A2); A5: for A being Event of Sigma holds f . A = (P . (A /\ B)) / (P . B) proof let A be Event of Sigma; ::_thesis: f . A = (P . (A /\ B)) / (P . B) ex C being Event of Sigma ex r1 being Real st ( C = A & r1 = f . A & r1 = (P . (C /\ B)) / (P . B) ) by A4; hence f . A = (P . (A /\ B)) / (P . B) ; ::_thesis: verum end; then A6: f . Omega = (P . (([#] Sigma) /\ B)) / (P . B) .= (P . B) / (P . B) by XBOOLE_1:28 .= 1 by A1, XCMPLX_1:60 ; A7: for A, C being Event of Sigma st A misses C holds f . (A \/ C) = (f . A) + (f . C) proof let A, C be Event of Sigma; ::_thesis: ( A misses C implies f . (A \/ C) = (f . A) + (f . C) ) assume A misses C ; ::_thesis: f . (A \/ C) = (f . A) + (f . C) then A8: A /\ B misses C /\ B by XBOOLE_1:76; thus f . (A \/ C) = (P . ((A \/ C) /\ B)) / (P . B) by A5 .= (P . ((A /\ B) \/ (C /\ B))) / (P . B) by XBOOLE_1:23 .= ((P . (A /\ B)) + (P . (C /\ B))) / (P . B) by A8, PROB_1:def_8 .= ((P . (A /\ B)) / (P . B)) + ((P . (C /\ B)) / (P . B)) by XCMPLX_1:62 .= ((P . (A /\ B)) / (P . B)) + (f . C) by A5 .= (f . A) + (f . C) by A5 ; ::_thesis: verum end; A9: for A being Event of Sigma holds 0 <= f . A proof let A be Event of Sigma; ::_thesis: 0 <= f . A 0 <= P . (A /\ B) by PROB_1:def_8; then 0 <= (P . (A /\ B)) / (P . B) by A1; hence 0 <= f . A by A5; ::_thesis: verum end; for ASeq being SetSequence of Sigma st ASeq is non-ascending holds ( f * ASeq is convergent & lim (f * ASeq) = f . (Intersection ASeq) ) proof let ASeq be SetSequence of Sigma; ::_thesis: ( ASeq is non-ascending implies ( f * ASeq is convergent & lim (f * ASeq) = f . (Intersection ASeq) ) ) assume A10: ASeq is non-ascending ; ::_thesis: ( f * ASeq is convergent & lim (f * ASeq) = f . (Intersection ASeq) ) consider BSeq being SetSequence of Sigma such that A11: for n being Element of NAT holds BSeq . n = (ASeq . n) /\ B by Th3; A12: dom (f * ASeq) = NAT by FUNCT_2:def_1; A13: now__::_thesis:_for_n_being_set_st_n_in_dom_(f_*_ASeq)_holds_ (f_*_ASeq)_._n_=_((P_._B)_")_*_((P_*_BSeq)_._n) let n be set ; ::_thesis: ( n in dom (f * ASeq) implies (f * ASeq) . n = ((P . B) ") * ((P * BSeq) . n) ) assume A14: n in dom (f * ASeq) ; ::_thesis: (f * ASeq) . n = ((P . B) ") * ((P * BSeq) . n) then reconsider n1 = n as Element of NAT by FUNCT_2:def_1; thus (f * ASeq) . n = f . (ASeq . n) by A12, A14, FUNCT_2:15 .= (P . ((ASeq . n1) /\ B)) / (P . B) by A5 .= (P . (BSeq . n)) / (P . B) by A11 .= ((P * BSeq) . n) / (P . B) by A12, A14, FUNCT_2:15 .= ((P . B) ") * ((P * BSeq) . n) by XCMPLX_0:def_9 ; ::_thesis: verum end; A15: BSeq is non-ascending by A10, A11, Th4; then A16: P * BSeq is convergent by PROB_1:def_8; dom (P * BSeq) = NAT by FUNCT_2:def_1; then A17: f * ASeq = ((P . B) ") (#) (P * BSeq) by A12, A13, VALUED_1:def_5; hence f * ASeq is convergent by A16, SEQ_2:7; ::_thesis: lim (f * ASeq) = f . (Intersection ASeq) lim (P * BSeq) = P . (Intersection BSeq) by A15, PROB_1:def_8; hence lim (f * ASeq) = ((P . B) ") * (P . (@Intersection BSeq)) by A17, A16, SEQ_2:8 .= (P . (@Intersection BSeq)) / (P . B) by XCMPLX_0:def_9 .= (P . ((@Intersection ASeq) /\ B)) / (P . B) by A11, Th5 .= f . (Intersection ASeq) by A5 ; ::_thesis: verum end; then reconsider f = f as Probability of Sigma by A9, A6, A7, PROB_1:def_8; take f ; ::_thesis: for A being Event of Sigma holds f . A = (P . (A /\ B)) / (P . B) thus for A being Event of Sigma holds f . A = (P . (A /\ B)) / (P . B) by A5; ::_thesis: verum end; uniqueness for b1, b2 being Probability of Sigma st ( for A being Event of Sigma holds b1 . A = (P . (A /\ B)) / (P . B) ) & ( for A being Event of Sigma holds b2 . A = (P . (A /\ B)) / (P . B) ) holds b1 = b2 proof let P1, P2 be Probability of Sigma; ::_thesis: ( ( for A being Event of Sigma holds P1 . A = (P . (A /\ B)) / (P . B) ) & ( for A being Event of Sigma holds P2 . A = (P . (A /\ B)) / (P . B) ) implies P1 = P2 ) assume that A18: for A being Event of Sigma holds P1 . A = (P . (A /\ B)) / (P . B) and A19: for A being Event of Sigma holds P2 . A = (P . (A /\ B)) / (P . B) ; ::_thesis: P1 = P2 now__::_thesis:_for_A_being_Event_of_Sigma_holds_P1_._A_=_P2_._A let A be Event of Sigma; ::_thesis: P1 . A = P2 . A thus P1 . A = (P . (A /\ B)) / (P . B) by A18 .= P2 . A by A19 ; ::_thesis: verum end; hence P1 = P2 by Th9; ::_thesis: verum end; end; :: deftheorem Def6 defines .|. PROB_2:def_6_:_ for Omega being non empty set for Sigma being SigmaField of Omega for P being Probability of Sigma for B being Event of Sigma st 0 < P . B holds for b5 being Probability of Sigma holds ( b5 = P .|. B iff for A being Event of Sigma holds b5 . A = (P . (A /\ B)) / (P . B) ); theorem Th29: :: PROB_2:29 for Omega being non empty set for Sigma being SigmaField of Omega for P being Probability of Sigma for B, A being Event of Sigma st 0 < P . B holds P . (A /\ B) = ((P .|. B) . A) * (P . B) proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for P being Probability of Sigma for B, A being Event of Sigma st 0 < P . B holds P . (A /\ B) = ((P .|. B) . A) * (P . B) let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma for B, A being Event of Sigma st 0 < P . B holds P . (A /\ B) = ((P .|. B) . A) * (P . B) let P be Probability of Sigma; ::_thesis: for B, A being Event of Sigma st 0 < P . B holds P . (A /\ B) = ((P .|. B) . A) * (P . B) let B, A be Event of Sigma; ::_thesis: ( 0 < P . B implies P . (A /\ B) = ((P .|. B) . A) * (P . B) ) assume A1: 0 < P . B ; ::_thesis: P . (A /\ B) = ((P .|. B) . A) * (P . B) then ((P .|. B) . A) * (P . B) = ((P . (A /\ B)) / (P . B)) * (P . B) by Def6 .= ((P . (A /\ B)) * ((P . B) ")) * (P . B) by XCMPLX_0:def_9 .= (P . (A /\ B)) * (((P . B) ") * (P . B)) .= (P . (A /\ B)) * 1 by A1, XCMPLX_0:def_7 .= P . (A /\ B) ; hence P . (A /\ B) = ((P .|. B) . A) * (P . B) ; ::_thesis: verum end; theorem :: PROB_2:30 for Omega being non empty set for Sigma being SigmaField of Omega for P being Probability of Sigma for A, B, C being Event of Sigma st 0 < P . (A /\ B) holds P . ((A /\ B) /\ C) = ((P . A) * ((P .|. A) . B)) * ((P .|. (A /\ B)) . C) proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for P being Probability of Sigma for A, B, C being Event of Sigma st 0 < P . (A /\ B) holds P . ((A /\ B) /\ C) = ((P . A) * ((P .|. A) . B)) * ((P .|. (A /\ B)) . C) let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma for A, B, C being Event of Sigma st 0 < P . (A /\ B) holds P . ((A /\ B) /\ C) = ((P . A) * ((P .|. A) . B)) * ((P .|. (A /\ B)) . C) let P be Probability of Sigma; ::_thesis: for A, B, C being Event of Sigma st 0 < P . (A /\ B) holds P . ((A /\ B) /\ C) = ((P . A) * ((P .|. A) . B)) * ((P .|. (A /\ B)) . C) let A, B, C be Event of Sigma; ::_thesis: ( 0 < P . (A /\ B) implies P . ((A /\ B) /\ C) = ((P . A) * ((P .|. A) . B)) * ((P .|. (A /\ B)) . C) ) assume A1: 0 < P . (A /\ B) ; ::_thesis: P . ((A /\ B) /\ C) = ((P . A) * ((P .|. A) . B)) * ((P .|. (A /\ B)) . C) then A2: 0 < P . A by PROB_1:34, XBOOLE_1:17; P . ((A /\ B) /\ C) = (P . (B /\ A)) * ((P .|. (A /\ B)) . C) by A1, Th29 .= ((P . A) * ((P .|. A) . B)) * ((P .|. (A /\ B)) . C) by A2, Th29 ; hence P . ((A /\ B) /\ C) = ((P . A) * ((P .|. A) . B)) * ((P .|. (A /\ B)) . C) ; ::_thesis: verum end; theorem Th31: :: PROB_2:31 for Omega being non empty set for Sigma being SigmaField of Omega for P being Probability of Sigma for A, B, C being Event of Sigma st C = B ` & 0 < P . B & 0 < P . C holds P . A = (((P .|. B) . A) * (P . B)) + (((P .|. C) . A) * (P . C)) proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for P being Probability of Sigma for A, B, C being Event of Sigma st C = B ` & 0 < P . B & 0 < P . C holds P . A = (((P .|. B) . A) * (P . B)) + (((P .|. C) . A) * (P . C)) let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma for A, B, C being Event of Sigma st C = B ` & 0 < P . B & 0 < P . C holds P . A = (((P .|. B) . A) * (P . B)) + (((P .|. C) . A) * (P . C)) let P be Probability of Sigma; ::_thesis: for A, B, C being Event of Sigma st C = B ` & 0 < P . B & 0 < P . C holds P . A = (((P .|. B) . A) * (P . B)) + (((P .|. C) . A) * (P . C)) let A, B, C be Event of Sigma; ::_thesis: ( C = B ` & 0 < P . B & 0 < P . C implies P . A = (((P .|. B) . A) * (P . B)) + (((P .|. C) . A) * (P . C)) ) assume that A1: C = B ` and A2: 0 < P . B and A3: 0 < P . C ; ::_thesis: P . A = (((P .|. B) . A) * (P . B)) + (((P .|. C) . A) * (P . C)) P . A = (P . (A /\ B)) + (P . (A /\ C)) by A1, Th14 .= (((P .|. B) . A) * (P . B)) + (P . (A /\ C)) by A2, Th29 .= (((P .|. B) . A) * (P . B)) + (((P .|. C) . A) * (P . C)) by A3, Th29 ; hence P . A = (((P .|. B) . A) * (P . B)) + (((P .|. C) . A) * (P . C)) ; ::_thesis: verum end; theorem Th32: :: PROB_2:32 for Omega being non empty set for Sigma being SigmaField of Omega for P being Probability of Sigma for A, A1, A2, A3 being Event of Sigma st A1 misses A2 & A3 = (A1 \/ A2) ` & 0 < P . A1 & 0 < P . A2 & 0 < P . A3 holds P . A = ((((P .|. A1) . A) * (P . A1)) + (((P .|. A2) . A) * (P . A2))) + (((P .|. A3) . A) * (P . A3)) proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for P being Probability of Sigma for A, A1, A2, A3 being Event of Sigma st A1 misses A2 & A3 = (A1 \/ A2) ` & 0 < P . A1 & 0 < P . A2 & 0 < P . A3 holds P . A = ((((P .|. A1) . A) * (P . A1)) + (((P .|. A2) . A) * (P . A2))) + (((P .|. A3) . A) * (P . A3)) let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma for A, A1, A2, A3 being Event of Sigma st A1 misses A2 & A3 = (A1 \/ A2) ` & 0 < P . A1 & 0 < P . A2 & 0 < P . A3 holds P . A = ((((P .|. A1) . A) * (P . A1)) + (((P .|. A2) . A) * (P . A2))) + (((P .|. A3) . A) * (P . A3)) let P be Probability of Sigma; ::_thesis: for A, A1, A2, A3 being Event of Sigma st A1 misses A2 & A3 = (A1 \/ A2) ` & 0 < P . A1 & 0 < P . A2 & 0 < P . A3 holds P . A = ((((P .|. A1) . A) * (P . A1)) + (((P .|. A2) . A) * (P . A2))) + (((P .|. A3) . A) * (P . A3)) let A, A1, A2, A3 be Event of Sigma; ::_thesis: ( A1 misses A2 & A3 = (A1 \/ A2) ` & 0 < P . A1 & 0 < P . A2 & 0 < P . A3 implies P . A = ((((P .|. A1) . A) * (P . A1)) + (((P .|. A2) . A) * (P . A2))) + (((P .|. A3) . A) * (P . A3)) ) assume that A1: A1 misses A2 and A2: A3 = (A1 \/ A2) ` and A3: 0 < P . A1 and A4: 0 < P . A2 and A5: 0 < P . A3 ; ::_thesis: P . A = ((((P .|. A1) . A) * (P . A1)) + (((P .|. A2) . A) * (P . A2))) + (((P .|. A3) . A) * (P . A3)) A6: A /\ A1 misses A /\ A2 by A1, XBOOLE_1:76; A1 \/ A2 misses A3 by A2, SUBSET_1:24; then A7: A /\ (A1 \/ A2) misses A /\ A3 by XBOOLE_1:76; A8: (A1 \/ A2) \/ A3 = [#] Omega by A2, SUBSET_1:10 .= Omega ; ((((P .|. A1) . A) * (P . A1)) + (((P .|. A2) . A) * (P . A2))) + (((P .|. A3) . A) * (P . A3)) = ((P . (A /\ A1)) + (((P .|. A2) . A) * (P . A2))) + (((P .|. A3) . A) * (P . A3)) by A3, Th29 .= ((P . (A /\ A1)) + (P . (A /\ A2))) + (((P .|. A3) . A) * (P . A3)) by A4, Th29 .= ((P . (A /\ A1)) + (P . (A /\ A2))) + (P . (A /\ A3)) by A5, Th29 .= (P . ((A /\ A1) \/ (A /\ A2))) + (P . (A /\ A3)) by A6, PROB_1:def_8 .= (P . (A /\ (A1 \/ A2))) + (P . (A /\ A3)) by XBOOLE_1:23 .= P . ((A /\ (A1 \/ A2)) \/ (A /\ A3)) by A7, PROB_1:def_8 .= P . (A /\ Omega) by A8, XBOOLE_1:23 .= P . A by XBOOLE_1:28 ; hence P . A = ((((P .|. A1) . A) * (P . A1)) + (((P .|. A2) . A) * (P . A2))) + (((P .|. A3) . A) * (P . A3)) ; ::_thesis: verum end; theorem :: PROB_2:33 for Omega being non empty set for Sigma being SigmaField of Omega for P being Probability of Sigma for A, B being Event of Sigma st 0 < P . B holds ( (P .|. B) . A = P . A iff A,B 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 Event of Sigma st 0 < P . B holds ( (P .|. B) . A = P . A iff A,B are_independent_respect_to P ) let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma for A, B being Event of Sigma st 0 < P . B holds ( (P .|. B) . A = P . A iff A,B are_independent_respect_to P ) let P be Probability of Sigma; ::_thesis: for A, B being Event of Sigma st 0 < P . B holds ( (P .|. B) . A = P . A iff A,B are_independent_respect_to P ) let A, B be Event of Sigma; ::_thesis: ( 0 < P . B implies ( (P .|. B) . A = P . A iff A,B are_independent_respect_to P ) ) assume A1: 0 < P . B ; ::_thesis: ( (P .|. B) . A = P . A iff A,B are_independent_respect_to P ) thus ( (P .|. B) . A = P . A implies A,B are_independent_respect_to P ) ::_thesis: ( A,B are_independent_respect_to P implies (P .|. B) . A = P . A ) proof assume (P .|. B) . A = P . A ; ::_thesis: A,B are_independent_respect_to P then ((P . (A /\ B)) / (P . B)) * (P . B) = (P . A) * (P . B) by A1, Def6; then P . (A /\ B) = (P . A) * (P . B) by A1, XCMPLX_1:87; hence A,B are_independent_respect_to P by Def4; ::_thesis: verum end; assume A,B are_independent_respect_to P ; ::_thesis: (P .|. B) . A = P . A then (P . (A /\ B)) * ((P . B) ") = ((P . A) * (P . B)) * ((P . B) ") by Def4; then (P . (A /\ B)) * ((P . B) ") = (P . A) * ((P . B) * ((P . B) ")) ; then (P . (A /\ B)) * ((P . B) ") = (P . A) * 1 by A1, XCMPLX_0:def_7; then (P . (A /\ B)) / (P . B) = P . A by XCMPLX_0:def_9; hence (P .|. B) . A = P . A by A1, Def6; ::_thesis: verum end; theorem :: PROB_2:34 for Omega being non empty set for Sigma being SigmaField of Omega for P being Probability of Sigma for A, B being Event of Sigma st 0 < P . B & P . B < 1 & (P .|. B) . A = (P .|. (([#] Sigma) \ B)) . A holds A,B 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 Event of Sigma st 0 < P . B & P . B < 1 & (P .|. B) . A = (P .|. (([#] Sigma) \ B)) . A holds A,B are_independent_respect_to P let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma for A, B being Event of Sigma st 0 < P . B & P . B < 1 & (P .|. B) . A = (P .|. (([#] Sigma) \ B)) . A holds A,B are_independent_respect_to P let P be Probability of Sigma; ::_thesis: for A, B being Event of Sigma st 0 < P . B & P . B < 1 & (P .|. B) . A = (P .|. (([#] Sigma) \ B)) . A holds A,B are_independent_respect_to P let A, B be Event of Sigma; ::_thesis: ( 0 < P . B & P . B < 1 & (P .|. B) . A = (P .|. (([#] Sigma) \ B)) . A implies A,B are_independent_respect_to P ) assume that A1: 0 < P . B and A2: P . B < 1 and A3: (P .|. B) . A = (P .|. (([#] Sigma) \ B)) . A ; ::_thesis: A,B are_independent_respect_to P ( 0 < P . (([#] Sigma) \ B) & (P . (A /\ B)) / (P . B) = (P .|. (([#] Sigma) \ B)) . A ) by A1, A2, A3, Def6, Th17; then A4: (P . (A /\ B)) / (P . B) = (P . (A /\ (([#] Sigma) \ B))) / (P . (([#] Sigma) \ B)) by Def6; A5: B ` = ([#] Sigma) \ B ; P . (([#] Sigma) \ B) <> 0 by A2, Th17; then (P . (A /\ B)) * (P . (([#] Sigma) \ B)) = (P . (A /\ (([#] Sigma) \ B))) * (P . B) by A1, A4, Th1; then (P . (A /\ B)) * (1 - (P . B)) = (P . (A /\ (([#] Sigma) \ B))) * (P . B) by PROB_1:32; then P . (A /\ B) = ((P . (A /\ (([#] Sigma) \ B))) + (P . (A /\ B))) * (P . B) .= (P . A) * (P . B) by A5, Th14 ; hence A,B are_independent_respect_to P by Def4; ::_thesis: verum end; theorem :: PROB_2:35 for Omega being non empty set for Sigma being SigmaField of Omega for P being Probability of Sigma for A, B being Event of Sigma st 0 < P . B holds (((P . A) + (P . B)) - 1) / (P . B) <= (P .|. B) . A proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for P being Probability of Sigma for A, B being Event of Sigma st 0 < P . B holds (((P . A) + (P . B)) - 1) / (P . B) <= (P .|. B) . A let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma for A, B being Event of Sigma st 0 < P . B holds (((P . A) + (P . B)) - 1) / (P . B) <= (P .|. B) . A let P be Probability of Sigma; ::_thesis: for A, B being Event of Sigma st 0 < P . B holds (((P . A) + (P . B)) - 1) / (P . B) <= (P .|. B) . A let A, B be Event of Sigma; ::_thesis: ( 0 < P . B implies (((P . A) + (P . B)) - 1) / (P . B) <= (P .|. B) . A ) assume A1: 0 < P . B ; ::_thesis: (((P . A) + (P . B)) - 1) / (P . B) <= (P .|. B) . A (((P . A) + (P . B)) - 1) / (P . B) <= (P . (A /\ B)) / (P . B) by A1, Th15, XREAL_1:72; hence (((P . A) + (P . B)) - 1) / (P . B) <= (P .|. B) . A by A1, Def6; ::_thesis: verum end; theorem Th36: :: PROB_2:36 for Omega being non empty set for Sigma being SigmaField of Omega for A, B being Event of Sigma for P being Probability of Sigma st 0 < P . A & 0 < P . B holds (P .|. B) . A = (((P .|. A) . B) * (P . A)) / (P . B) proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for A, B being Event of Sigma for P being Probability of Sigma st 0 < P . A & 0 < P . B holds (P .|. B) . A = (((P .|. A) . B) * (P . A)) / (P . B) let Sigma be SigmaField of Omega; ::_thesis: for A, B being Event of Sigma for P being Probability of Sigma st 0 < P . A & 0 < P . B holds (P .|. B) . A = (((P .|. A) . B) * (P . A)) / (P . B) let A, B be Event of Sigma; ::_thesis: for P being Probability of Sigma st 0 < P . A & 0 < P . B holds (P .|. B) . A = (((P .|. A) . B) * (P . A)) / (P . B) let P be Probability of Sigma; ::_thesis: ( 0 < P . A & 0 < P . B implies (P .|. B) . A = (((P .|. A) . B) * (P . A)) / (P . B) ) assume that A1: 0 < P . A and A2: 0 < P . B ; ::_thesis: (P .|. B) . A = (((P .|. A) . B) * (P . A)) / (P . B) thus (((P .|. A) . B) * (P . A)) / (P . B) = (P . (A /\ B)) / (P . B) by A1, Th29 .= (P .|. B) . A by A2, Def6 ; ::_thesis: verum end; theorem :: PROB_2:37 for Omega being non empty set for Sigma being SigmaField of Omega for B, A1, A2 being Event of Sigma for P being Probability of Sigma st 0 < P . B & A2 = A1 ` & 0 < P . A1 & 0 < P . A2 holds ( (P .|. B) . A1 = (((P .|. A1) . B) * (P . A1)) / ((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) & (P .|. B) . A2 = (((P .|. A2) . B) * (P . A2)) / ((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) ) proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for B, A1, A2 being Event of Sigma for P being Probability of Sigma st 0 < P . B & A2 = A1 ` & 0 < P . A1 & 0 < P . A2 holds ( (P .|. B) . A1 = (((P .|. A1) . B) * (P . A1)) / ((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) & (P .|. B) . A2 = (((P .|. A2) . B) * (P . A2)) / ((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) ) let Sigma be SigmaField of Omega; ::_thesis: for B, A1, A2 being Event of Sigma for P being Probability of Sigma st 0 < P . B & A2 = A1 ` & 0 < P . A1 & 0 < P . A2 holds ( (P .|. B) . A1 = (((P .|. A1) . B) * (P . A1)) / ((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) & (P .|. B) . A2 = (((P .|. A2) . B) * (P . A2)) / ((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) ) let B, A1, A2 be Event of Sigma; ::_thesis: for P being Probability of Sigma st 0 < P . B & A2 = A1 ` & 0 < P . A1 & 0 < P . A2 holds ( (P .|. B) . A1 = (((P .|. A1) . B) * (P . A1)) / ((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) & (P .|. B) . A2 = (((P .|. A2) . B) * (P . A2)) / ((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) ) let P be Probability of Sigma; ::_thesis: ( 0 < P . B & A2 = A1 ` & 0 < P . A1 & 0 < P . A2 implies ( (P .|. B) . A1 = (((P .|. A1) . B) * (P . A1)) / ((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) & (P .|. B) . A2 = (((P .|. A2) . B) * (P . A2)) / ((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) ) ) assume that A1: 0 < P . B and A2: A2 = A1 ` and A3: 0 < P . A1 and A4: 0 < P . A2 ; ::_thesis: ( (P .|. B) . A1 = (((P .|. A1) . B) * (P . A1)) / ((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) & (P .|. B) . A2 = (((P .|. A2) . B) * (P . A2)) / ((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) ) thus (((P .|. A1) . B) * (P . A1)) / ((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) = (((P .|. A1) . B) * (P . A1)) / (P . B) by A2, A3, A4, Th31 .= (P .|. B) . A1 by A1, A3, Th36 ; ::_thesis: (P .|. B) . A2 = (((P .|. A2) . B) * (P . A2)) / ((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) thus (((P .|. A2) . B) * (P . A2)) / ((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) = (((P .|. A2) . B) * (P . A2)) / (P . B) by A2, A3, A4, Th31 .= (P .|. B) . A2 by A1, A4, Th36 ; ::_thesis: verum end; theorem :: PROB_2:38 for Omega being non empty set for Sigma being SigmaField of Omega for B, A1, A2, A3 being Event of Sigma for P being Probability of Sigma st 0 < P . B & 0 < P . A1 & 0 < P . A2 & 0 < P . A3 & A1 misses A2 & A3 = (A1 \/ A2) ` holds ( (P .|. B) . A1 = (((P .|. A1) . B) * (P . A1)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) & (P .|. B) . A2 = (((P .|. A2) . B) * (P . A2)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) & (P .|. B) . A3 = (((P .|. A3) . B) * (P . A3)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) ) proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for B, A1, A2, A3 being Event of Sigma for P being Probability of Sigma st 0 < P . B & 0 < P . A1 & 0 < P . A2 & 0 < P . A3 & A1 misses A2 & A3 = (A1 \/ A2) ` holds ( (P .|. B) . A1 = (((P .|. A1) . B) * (P . A1)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) & (P .|. B) . A2 = (((P .|. A2) . B) * (P . A2)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) & (P .|. B) . A3 = (((P .|. A3) . B) * (P . A3)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) ) let Sigma be SigmaField of Omega; ::_thesis: for B, A1, A2, A3 being Event of Sigma for P being Probability of Sigma st 0 < P . B & 0 < P . A1 & 0 < P . A2 & 0 < P . A3 & A1 misses A2 & A3 = (A1 \/ A2) ` holds ( (P .|. B) . A1 = (((P .|. A1) . B) * (P . A1)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) & (P .|. B) . A2 = (((P .|. A2) . B) * (P . A2)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) & (P .|. B) . A3 = (((P .|. A3) . B) * (P . A3)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) ) let B, A1, A2, A3 be Event of Sigma; ::_thesis: for P being Probability of Sigma st 0 < P . B & 0 < P . A1 & 0 < P . A2 & 0 < P . A3 & A1 misses A2 & A3 = (A1 \/ A2) ` holds ( (P .|. B) . A1 = (((P .|. A1) . B) * (P . A1)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) & (P .|. B) . A2 = (((P .|. A2) . B) * (P . A2)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) & (P .|. B) . A3 = (((P .|. A3) . B) * (P . A3)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) ) let P be Probability of Sigma; ::_thesis: ( 0 < P . B & 0 < P . A1 & 0 < P . A2 & 0 < P . A3 & A1 misses A2 & A3 = (A1 \/ A2) ` implies ( (P .|. B) . A1 = (((P .|. A1) . B) * (P . A1)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) & (P .|. B) . A2 = (((P .|. A2) . B) * (P . A2)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) & (P .|. B) . A3 = (((P .|. A3) . B) * (P . A3)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) ) ) assume that A1: 0 < P . B and A2: 0 < P . A1 and A3: 0 < P . A2 and A4: 0 < P . A3 and A5: ( A1 misses A2 & A3 = (A1 \/ A2) ` ) ; ::_thesis: ( (P .|. B) . A1 = (((P .|. A1) . B) * (P . A1)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) & (P .|. B) . A2 = (((P .|. A2) . B) * (P . A2)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) & (P .|. B) . A3 = (((P .|. A3) . B) * (P . A3)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) ) thus (((P .|. A1) . B) * (P . A1)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) = (((P .|. A1) . B) * (P . A1)) / (P . B) by A2, A3, A4, A5, Th32 .= (P .|. B) . A1 by A1, A2, Th36 ; ::_thesis: ( (P .|. B) . A2 = (((P .|. A2) . B) * (P . A2)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) & (P .|. B) . A3 = (((P .|. A3) . B) * (P . A3)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) ) thus (((P .|. A2) . B) * (P . A2)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) = (((P .|. A2) . B) * (P . A2)) / (P . B) by A2, A3, A4, A5, Th32 .= (P .|. B) . A2 by A1, A3, Th36 ; ::_thesis: (P .|. B) . A3 = (((P .|. A3) . B) * (P . A3)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) thus (((P .|. A3) . B) * (P . A3)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) = (((P .|. A3) . B) * (P . A3)) / (P . B) by A2, A3, A4, A5, Th32 .= (P .|. B) . A3 by A1, A4, Th36 ; ::_thesis: verum end; theorem :: PROB_2:39 for Omega being non empty set for Sigma being SigmaField of Omega for A, B being Event of Sigma for P being Probability of Sigma st 0 < P . B holds 1 - ((P . (([#] Sigma) \ A)) / (P . B)) <= (P .|. B) . A proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for A, B being Event of Sigma for P being Probability of Sigma st 0 < P . B holds 1 - ((P . (([#] Sigma) \ A)) / (P . B)) <= (P .|. B) . A let Sigma be SigmaField of Omega; ::_thesis: for A, B being Event of Sigma for P being Probability of Sigma st 0 < P . B holds 1 - ((P . (([#] Sigma) \ A)) / (P . B)) <= (P .|. B) . A let A, B be Event of Sigma; ::_thesis: for P being Probability of Sigma st 0 < P . B holds 1 - ((P . (([#] Sigma) \ A)) / (P . B)) <= (P .|. B) . A let P be Probability of Sigma; ::_thesis: ( 0 < P . B implies 1 - ((P . (([#] Sigma) \ A)) / (P . B)) <= (P .|. B) . A ) assume A1: 0 < P . B ; ::_thesis: 1 - ((P . (([#] Sigma) \ A)) / (P . B)) <= (P .|. B) . A ((P . B) + (P . A)) - 1 <= P . (A /\ B) by Th15; then (P . B) + (- (1 - (P . A))) <= P . (A /\ B) ; then (P . B) + (- (P . (([#] Sigma) \ A))) <= P . (A /\ B) by PROB_1:32; then ((P . B) + (- (P . (([#] Sigma) \ A)))) / (P . B) <= (P . (A /\ B)) / (P . B) by A1, XREAL_1:72; then ((P . B) - (P . (([#] Sigma) \ A))) / (P . B) <= (P .|. B) . A by A1, Def6; then ((P . B) / (P . B)) - ((P . (([#] Sigma) \ A)) / (P . B)) <= (P .|. B) . A by XCMPLX_1:120; hence 1 - ((P . (([#] Sigma) \ A)) / (P . B)) <= (P .|. B) . A by A1, XCMPLX_1:60; ::_thesis: verum end;