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