:: PROB_2 semantic presentation

REAL is non empty V45() V46() V47() V51() V52() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() Element of bool REAL
bool REAL is non empty set
COMPLEX is non empty V45() V51() V52() set
RAT is non empty V45() V46() V47() V48() V51() V52() set
INT is non empty V45() V46() V47() V48() V49() V51() V52() set
omega is non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() set
bool omega is non empty set
is non empty V35() V36() V37() set
bool is non empty set
bool () is non empty set

1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
Omega is ext-real V14() real Element of REAL
Sigma is ext-real V14() real Element of REAL
A is ext-real V14() real Element of REAL
A / Omega is ext-real V14() real Element of REAL
A * Sigma is ext-real V14() real Element of REAL
B is ext-real V14() real Element of REAL
B / Sigma is ext-real V14() real Element of REAL
B * Omega is ext-real V14() real Element of REAL
(B / Sigma) * Sigma is ext-real V14() real Element of REAL
((B / Sigma) * Sigma) * Omega is ext-real V14() real Element of REAL
(A / Omega) * Omega is ext-real V14() real Element of REAL
((A / Omega) * Omega) * Sigma is ext-real V14() real Element of REAL
B * 1 is ext-real V14() real Element of REAL
(B * 1) / Sigma is ext-real V14() real Element of REAL
Omega " is ext-real V14() real Element of REAL
Omega * (Omega ") is ext-real V14() real Element of REAL
B * (Omega * (Omega ")) is ext-real V14() real Element of REAL
(B * (Omega * (Omega "))) / Sigma is ext-real V14() real Element of REAL
(A * Sigma) * (Omega ") is ext-real V14() real Element of REAL
((A * Sigma) * (Omega ")) / Sigma is ext-real V14() real Element of REAL
A * (Omega ") is ext-real V14() real Element of REAL
(A * (Omega ")) * Sigma is ext-real V14() real Element of REAL
((A * (Omega ")) * Sigma) / Sigma is ext-real V14() real Element of REAL
(A / Omega) * Sigma is ext-real V14() real Element of REAL
((A / Omega) * Sigma) / Sigma is ext-real V14() real Element of REAL
Sigma " is ext-real V14() real Element of REAL
((A / Omega) * Sigma) * (Sigma ") is ext-real V14() real Element of REAL
Sigma * (Sigma ") is ext-real V14() real Element of REAL
(A / Omega) * (Sigma * (Sigma ")) is ext-real V14() real Element of REAL
(A / Omega) * 1 is ext-real V14() real Element of REAL
Omega is ext-real V14() real Element of REAL

lim Sigma is ext-real V14() real Element of REAL
Omega - (lim Sigma) is ext-real V14() real Element of REAL

B is ext-real V14() real set
P is ext-real V14() real set

Sigma . n is ext-real V14() real Element of REAL
(Sigma . n) - B is ext-real V14() real Element of REAL
abs ((Sigma . n) - B) is ext-real V14() real Element of REAL
- ((Sigma . n) - B) is ext-real V14() real Element of REAL
abs (- ((Sigma . n) - B)) is ext-real V14() real Element of REAL
B - Omega is ext-real V14() real Element of REAL
Omega - (Sigma . n) is ext-real V14() real Element of REAL
(B - Omega) + (Omega - (Sigma . n)) is ext-real V14() real Element of REAL
abs ((B - Omega) + (Omega - (Sigma . n))) is ext-real V14() real Element of REAL
A . n is ext-real V14() real Element of REAL
- (B - Omega) is ext-real V14() real Element of REAL
- (- (B - Omega)) is ext-real V14() real Element of REAL
(A . n) + (- (- (B - Omega))) is ext-real V14() real Element of REAL
abs ((A . n) + (- (- (B - Omega)))) is ext-real V14() real Element of REAL
Omega - B is ext-real V14() real Element of REAL
(A . n) - (Omega - B) is ext-real V14() real Element of REAL
abs ((A . n) - (Omega - B)) is ext-real V14() real Element of REAL

A . n is ext-real V14() real Element of REAL
(A . n) - (Omega - B) is ext-real V14() real Element of REAL
abs ((A . n) - (Omega - B)) is ext-real V14() real Element of REAL
Omega is set
bool Omega is non empty set
bool (bool Omega) is non empty set
Sigma is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
K231(Omega) is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
[:NAT,K231(Omega):] is non empty set
bool [:NAT,K231(Omega):] is non empty set
A is Relation-like NAT -defined Sigma -valued K231(Omega) -valued Function-like V30( NAT ,K231(Omega)) Element of bool [:NAT,K231(Omega):]

A . B is set
Omega is set
bool Omega is non empty set
bool (bool Omega) is non empty set
Sigma is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
K231(Omega) is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
[:NAT,K231(Omega):] is non empty set
bool [:NAT,K231(Omega):] is non empty set
A is Relation-like NAT -defined Sigma -valued K231(Omega) -valued Function-like V30( NAT ,K231(Omega)) Element of bool [:NAT,K231(Omega):]
Intersection A is Element of bool Omega
Complement A is Relation-like NAT -defined K231(Omega) -valued Function-like V30( NAT ,K231(Omega)) Element of bool [:NAT,K231(Omega):]
Union () is Element of bool Omega
(Union ()) ` is Element of bool Omega
Omega \ (Union ()) is set
rng A is set
Omega is set
bool Omega is non empty set
bool (bool Omega) is non empty set
K231(Omega) is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
[:NAT,K231(Omega):] is non empty set
bool [:NAT,K231(Omega):] is non empty set
Sigma is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
A is Relation-like NAT -defined K231(Omega) -valued Sigma -valued Function-like V30( NAT ,K231(Omega)) Element of bool [:NAT,K231(Omega):]
B is Event of Sigma

dom P is set

(Omega,Sigma,A,A3) is Event of Sigma
(Omega,Sigma,A,A3) /\ B is Event of Sigma
P . A3 is set
A3 is set
P . A3 is set

(Omega,Sigma,A,n) is Event of Sigma
(Omega,Sigma,A,n) /\ B is Event of Sigma
A3 is Relation-like NAT -defined K231(Omega) -valued Function-like V30( NAT ,K231(Omega)) Element of bool [:NAT,K231(Omega):]
A3 . P is Element of K231(Omega)
rng A3 is set
P is Relation-like NAT -defined K231(Omega) -valued Sigma -valued Function-like V30( NAT ,K231(Omega)) Element of bool [:NAT,K231(Omega):]

(Omega,Sigma,P,n) is Event of Sigma
(Omega,Sigma,A,n) is Event of Sigma
(Omega,Sigma,A,n) /\ B is Event of Sigma
Omega is set
bool Omega is non empty set
bool (bool Omega) is non empty set
K231(Omega) is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
[:NAT,K231(Omega):] is non empty set
bool [:NAT,K231(Omega):] is non empty set
Sigma is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
A is Relation-like NAT -defined K231(Omega) -valued Sigma -valued Function-like V30( NAT ,K231(Omega)) Element of bool [:NAT,K231(Omega):]
B is Relation-like NAT -defined K231(Omega) -valued Sigma -valued Function-like V30( NAT ,K231(Omega)) Element of bool [:NAT,K231(Omega):]
P is Event of Sigma

B . A3 is set

B . P is set
(Omega,Sigma,A,P) is Event of Sigma
(Omega,Sigma,A,A3) is Event of Sigma
(Omega,Sigma,A,P) /\ P is Event of Sigma
(Omega,Sigma,A,A3) /\ P is Event of Sigma
(Omega,Sigma,B,P) is Event of Sigma
(Omega,Sigma,B,A3) is Event of Sigma
Omega is set
bool Omega is non empty set
bool (bool Omega) is non empty set
K231(Omega) is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
[:NAT,K231(Omega):] is non empty set
bool [:NAT,K231(Omega):] is non empty set
Sigma is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
A is Relation-like NAT -defined K231(Omega) -valued Sigma -valued Function-like V30( NAT ,K231(Omega)) Element of bool [:NAT,K231(Omega):]
Intersection A is Element of bool Omega
Complement A is Relation-like NAT -defined K231(Omega) -valued Function-like V30( NAT ,K231(Omega)) Element of bool [:NAT,K231(Omega):]
Union () is Element of bool Omega
(Union ()) ` is Element of bool Omega
Omega \ (Union ()) is set
B is Relation-like NAT -defined K231(Omega) -valued Sigma -valued Function-like V30( NAT ,K231(Omega)) Element of bool [:NAT,K231(Omega):]
Intersection B is Element of bool Omega
Complement B is Relation-like NAT -defined K231(Omega) -valued Function-like V30( NAT ,K231(Omega)) Element of bool [:NAT,K231(Omega):]
Union () is Element of bool Omega
(Union ()) ` is Element of bool Omega
Omega \ (Union ()) is set
P is Event of Sigma
() /\ P is Element of bool Omega
A3 is set

(Omega,Sigma,B,P) is Event of Sigma
(Omega,Sigma,B,P) /\ P is Event of Sigma
(Omega,Sigma,A,P) is Event of Sigma

(Omega,Sigma,B,P) is Event of Sigma
(Omega,Sigma,B,P) /\ P is Event of Sigma
A3 is set

(Omega,Sigma,B,P) is Event of Sigma
(Omega,Sigma,B,P) /\ P is Event of Sigma

(Omega,Sigma,A,P) is Event of Sigma
(Omega,Sigma,B,P) is Event of Sigma
(Omega,Sigma,B,P) /\ P is Event of Sigma
Omega is set
bool Omega is non empty set
bool (bool Omega) is non empty set
Sigma is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
K231(Omega) is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
[:NAT,K231(Omega):] is non empty set
bool [:NAT,K231(Omega):] is non empty set
A is Relation-like NAT -defined Sigma -valued K231(Omega) -valued Function-like V30( NAT ,K231(Omega)) Element of bool [:NAT,K231(Omega):]
Complement A is Relation-like NAT -defined K231(Omega) -valued Function-like V30( NAT ,K231(Omega)) Element of bool [:NAT,K231(Omega):]

(Omega,K231(Omega),(),P) is Event of K231(Omega)
(Omega,Sigma,A,P) is Event of Sigma
(Omega,Sigma,A,P) ` is Element of bool Omega
Omega \ (Omega,Sigma,A,P) is set
() . B is Element of K231(Omega)
rng () is set
Omega is set
K231(Omega) is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
bool Omega is non empty set
bool (bool Omega) is non empty set
[:NAT,K231(Omega):] is non empty set
bool [:NAT,K231(Omega):] is non empty set
Sigma is Relation-like NAT -defined K231(Omega) -valued Function-like V30( NAT ,K231(Omega)) Element of bool [:NAT,K231(Omega):]

A + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(Omega,K231(Omega),Sigma,(A + 1)) is Event of K231(Omega)
(Omega,K231(Omega),Sigma,A) is Event of K231(Omega)

A + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(Omega,K231(Omega),Sigma,(A + 1)) is Event of K231(Omega)
(Omega,K231(Omega),Sigma,A) is Event of K231(Omega)

(Omega,K231(Omega),Sigma,A) is Event of K231(Omega)

(Omega,K231(Omega),Sigma,(A + P)) is Event of K231(Omega)
P + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
A + (P + 1) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(Omega,K231(Omega),Sigma,(A + (P + 1))) is Event of K231(Omega)
(A + P) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(Omega,K231(Omega),Sigma,((A + P) + 1)) is Event of K231(Omega)

(Omega,K231(Omega),Sigma,(A + 0)) is Event of K231(Omega)

(Omega,K231(Omega),Sigma,B) is Event of K231(Omega)
Omega is set
K231(Omega) is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
bool Omega is non empty set
bool (bool Omega) is non empty set
[:NAT,K231(Omega):] is non empty set
bool [:NAT,K231(Omega):] is non empty set
Sigma is Relation-like NAT -defined K231(Omega) -valued Function-like V30( NAT ,K231(Omega)) Element of bool [:NAT,K231(Omega):]

A + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(Omega,K231(Omega),Sigma,A) is Event of K231(Omega)
(Omega,K231(Omega),Sigma,(A + 1)) is Event of K231(Omega)

(Omega,K231(Omega),Sigma,A) is Event of K231(Omega)
A + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(Omega,K231(Omega),Sigma,(A + 1)) is Event of K231(Omega)

(Omega,K231(Omega),Sigma,A) is Event of K231(Omega)

(Omega,K231(Omega),Sigma,(A + P)) is Event of K231(Omega)
P + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
A + (P + 1) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(Omega,K231(Omega),Sigma,(A + (P + 1))) is Event of K231(Omega)
(A + P) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(Omega,K231(Omega),Sigma,((A + P) + 1)) is Event of K231(Omega)

(Omega,K231(Omega),Sigma,(A + 0)) is Event of K231(Omega)

(Omega,K231(Omega),Sigma,B) is Event of K231(Omega)
Omega is set
K231(Omega) is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
bool Omega is non empty set
bool (bool Omega) is non empty set
[:NAT,K231(Omega):] is non empty set
bool [:NAT,K231(Omega):] is non empty set
Sigma is Relation-like NAT -defined K231(Omega) -valued Function-like V30( NAT ,K231(Omega)) Element of bool [:NAT,K231(Omega):]
Complement Sigma is Relation-like NAT -defined K231(Omega) -valued K231(Omega) -valued Function-like V30( NAT ,K231(Omega)) Element of bool [:NAT,K231(Omega):]

(Omega,K231(Omega),Sigma,B) is Event of K231(Omega)
(Omega,K231(Omega),Sigma,A) is Event of K231(Omega)
(Omega,K231(Omega),Sigma,A) ` is Element of bool Omega
Omega \ (Omega,K231(Omega),Sigma,A) is set
(Omega,K231(Omega),Sigma,B) ` is Element of bool Omega
Omega \ (Omega,K231(Omega),Sigma,B) is set
(Omega,K231(Omega),(Complement Sigma),A) is Event of K231(Omega)
(Omega,K231(Omega),(Complement Sigma),B) is Event of K231(Omega)

(Omega,K231(Omega),(Complement Sigma),A) is Event of K231(Omega)
(Omega,K231(Omega),(Complement Sigma),B) is Event of K231(Omega)
(Omega,K231(Omega),Sigma,A) is Event of K231(Omega)
(Omega,K231(Omega),Sigma,A) ` is Element of bool Omega
Omega \ (Omega,K231(Omega),Sigma,A) is set
(Omega,K231(Omega),Sigma,B) is Event of K231(Omega)
(Omega,K231(Omega),Sigma,B) ` is Element of bool Omega
Omega \ (Omega,K231(Omega),Sigma,B) is set
Omega is set
K231(Omega) is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
bool Omega is non empty set
bool (bool Omega) is non empty set
[:NAT,K231(Omega):] is non empty set
bool [:NAT,K231(Omega):] is non empty set
Sigma is Relation-like NAT -defined K231(Omega) -valued Function-like V30( NAT ,K231(Omega)) Element of bool [:NAT,K231(Omega):]
Complement Sigma is Relation-like NAT -defined K231(Omega) -valued K231(Omega) -valued Function-like V30( NAT ,K231(Omega)) Element of bool [:NAT,K231(Omega):]

(Omega,K231(Omega),Sigma,A) is Event of K231(Omega)
(Omega,K231(Omega),Sigma,B) is Event of K231(Omega)
(Omega,K231(Omega),Sigma,B) ` is Element of bool Omega
Omega \ (Omega,K231(Omega),Sigma,B) is set
(Omega,K231(Omega),Sigma,A) ` is Element of bool Omega
Omega \ (Omega,K231(Omega),Sigma,A) is set
(Omega,K231(Omega),(Complement Sigma),B) is Event of K231(Omega)
(Omega,K231(Omega),(Complement Sigma),A) is Event of K231(Omega)

(Omega,K231(Omega),(Complement Sigma),B) is Event of K231(Omega)
(Omega,K231(Omega),(Complement Sigma),A) is Event of K231(Omega)
(Omega,K231(Omega),Sigma,B) is Event of K231(Omega)
(Omega,K231(Omega),Sigma,B) ` is Element of bool Omega
Omega \ (Omega,K231(Omega),Sigma,B) is set
(Omega,K231(Omega),Sigma,A) is Event of K231(Omega)
(Omega,K231(Omega),Sigma,A) ` is Element of bool Omega
Omega \ (Omega,K231(Omega),Sigma,A) is set
Omega is set
bool Omega is non empty set
bool (bool Omega) is non empty set
Sigma is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
K231(Omega) is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
[:NAT,K231(Omega):] is non empty set
bool [:NAT,K231(Omega):] is non empty set
A is Relation-like NAT -defined Sigma -valued K231(Omega) -valued Function-like V30( NAT ,K231(Omega)) Element of bool [:NAT,K231(Omega):]

(Omega,Sigma,A,B) is Event of Sigma
(Omega,Sigma,A,P) is Event of Sigma
dom A is set
B is set
A . B is set
P is set
A . P is set
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
K231(Omega) is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
[:NAT,K231(Omega):] is non empty set
bool [:NAT,K231(Omega):] is non empty set
Sigma is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
A is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
B is Relation-like NAT -defined K231(Omega) -valued Sigma -valued Function-like V30( NAT ,K231(Omega)) Element of bool [:NAT,K231(Omega):]

lim (A * B) is ext-real V14() real Element of REAL
Union B is Element of bool Omega
A . () is ext-real V14() real Element of REAL
Complement B is Relation-like NAT -defined K231(Omega) -valued K231(Omega) -valued Function-like V30( NAT ,K231(Omega)) Element of bool [:NAT,K231(Omega):]

(A * ()) . A3 is ext-real V14() real Element of REAL
(Omega,Sigma,(),A3) is Event of Sigma
A . (Omega,Sigma,(),A3) is ext-real V14() real Element of REAL
(Omega,Sigma,B,A3) is Event of Sigma
(Omega,Sigma,B,A3) ` is Element of bool Omega
Omega \ (Omega,Sigma,B,A3) is set
A . ((Omega,Sigma,B,A3) `) is ext-real V14() real Element of REAL
[#] Sigma is Event of Sigma
([#] Sigma) \ (Omega,Sigma,B,A3) is Event of Sigma
A . (([#] Sigma) \ (Omega,Sigma,B,A3)) is ext-real V14() real Element of REAL
A . (Omega,Sigma,B,A3) is ext-real V14() real Element of REAL
1 - (A . (Omega,Sigma,B,A3)) is ext-real V14() real Element of REAL
(A * B) . A3 is ext-real V14() real Element of REAL
1 - ((A * B) . A3) is ext-real V14() real Element of REAL
- ((A * B) . A3) is ext-real V14() real Element of REAL
1 + (- ((A * B) . A3)) is ext-real V14() real Element of REAL
1 - ((A * ()) . A3) is ext-real V14() real Element of REAL
Intersection () is Element of bool Omega
Complement () is Relation-like NAT -defined K231(Omega) -valued K231(Omega) -valued Function-like V30( NAT ,K231(Omega)) Element of bool [:NAT,K231(Omega):]
Union () is Element of bool Omega
(Union ()) ` is Element of bool Omega
Omega \ (Union ()) is set
([#] Sigma) \ () is Element of bool Omega
A . () is ext-real V14() real Element of REAL
A3 is Event of Sigma
A . A3 is ext-real V14() real Element of REAL
1 - (A . A3) is ext-real V14() real Element of REAL
lim (A * ()) is ext-real V14() real Element of REAL
1 - (lim (A * ())) is ext-real V14() real Element of REAL
1 - (1 - (A . A3)) is ext-real V14() real Element of REAL
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
Sigma is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
A is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
B is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
P is set
A . P is ext-real V14() real Element of REAL
B . P is ext-real V14() real Element of REAL
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
K231(Omega) is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
[:NAT,K231(Omega):] is non empty set
bool [:NAT,K231(Omega):] is non empty set
Sigma is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
[:Sigma,REAL:] is non empty V35() V36() V37() set
bool [:Sigma,REAL:] is non empty set
A is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() Element of bool [:Sigma,REAL:]
A . Omega is ext-real V14() real Element of REAL
B is Event of Sigma
A . B is ext-real V14() real Element of REAL
P is Event of Sigma
A3 is Event of Sigma
P \/ A3 is Event of Sigma
A . (P \/ A3) is ext-real V14() real Element of REAL
A . P is ext-real V14() real Element of REAL
A . A3 is ext-real V14() real Element of REAL
(A . P) + (A . A3) is ext-real V14() real Element of REAL
P is Relation-like NAT -defined K231(Omega) -valued Sigma -valued Function-like V30( NAT ,K231(Omega)) Element of bool [:NAT,K231(Omega):]

lim (A * P) is ext-real V14() real Element of REAL
Union P is Element of bool Omega
A . () is ext-real V14() real Element of REAL
B is Relation-like NAT -defined K231(Omega) -valued Sigma -valued Function-like V30( NAT ,K231(Omega)) Element of bool [:NAT,K231(Omega):]

lim (A * B) is ext-real V14() real Element of REAL
Intersection B is Element of bool Omega
Complement B is Relation-like NAT -defined K231(Omega) -valued K231(Omega) -valued Function-like V30( NAT ,K231(Omega)) Element of bool [:NAT,K231(Omega):]
Union () is Element of bool Omega
(Union ()) ` is Element of bool Omega
Omega \ (Union ()) is set
A . () is ext-real V14() real Element of REAL
(Omega,Sigma,B) is Event of Sigma
P is Event of Sigma
P ` is Element of bool Omega
Omega \ P is set
A . (P `) is ext-real V14() real Element of REAL
A . P is ext-real V14() real Element of REAL
1 - (A . P) is ext-real V14() real Element of REAL
n is Event of Sigma
[#] Omega is non empty non proper Element of bool Omega
A . ([#] Omega) is ext-real V14() real Element of REAL
P \/ n is Event of Sigma
A . (P \/ n) is ext-real V14() real Element of REAL
A . n is ext-real V14() real Element of REAL
(A . P) + (A . n) is ext-real V14() real Element of REAL

(A * ()) . P is ext-real V14() real Element of REAL
(Omega,Sigma,(),P) is Event of Sigma
A . (Omega,Sigma,(),P) is ext-real V14() real Element of REAL
(Omega,Sigma,B,P) is Event of Sigma
(Omega,Sigma,B,P) ` is Element of bool Omega
Omega \ (Omega,Sigma,B,P) is set
A . ((Omega,Sigma,B,P) `) is ext-real V14() real Element of REAL
A . (Omega,Sigma,B,P) is ext-real V14() real Element of REAL
1 - (A . (Omega,Sigma,B,P)) is ext-real V14() real Element of REAL
(A * B) . P is ext-real V14() real Element of REAL
1 - ((A * B) . P) is ext-real V14() real Element of REAL
- ((A * B) . P) is ext-real V14() real Element of REAL
1 + (- ((A * B) . P)) is ext-real V14() real Element of REAL
1 - ((A * ()) . P) is ext-real V14() real Element of REAL
() ` is Element of bool Omega
Omega \ () is set
A . (Union ()) is ext-real V14() real Element of REAL
P is Event of Sigma
A . P is ext-real V14() real Element of REAL
1 - (A . P) is ext-real V14() real Element of REAL
lim (A * ()) is ext-real V14() real Element of REAL
1 - (lim (A * ())) is ext-real V14() real Element of REAL
1 - (1 - (A . P)) is ext-real V14() real Element of REAL
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
Sigma is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
A is Event of Sigma
B is Event of Sigma
A \/ B is Event of Sigma
A /\ B is Event of Sigma
P is Event of Sigma
(A \/ B) \/ P is Event of Sigma
B /\ P is Event of Sigma
A /\ P is Event of Sigma
(A /\ B) /\ P is Event of Sigma
A3 is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
A3 . ((A \/ B) \/ P) is ext-real V14() real Element of REAL
A3 . A is ext-real V14() real Element of REAL
A3 . B is ext-real V14() real Element of REAL
(A3 . A) + (A3 . B) is ext-real V14() real Element of REAL
A3 . P is ext-real V14() real Element of REAL
((A3 . A) + (A3 . B)) + (A3 . P) is ext-real V14() real Element of REAL
A3 . (A /\ B) is ext-real V14() real Element of REAL
A3 . (B /\ P) is ext-real V14() real Element of REAL
(A3 . (A /\ B)) + (A3 . (B /\ P)) is ext-real V14() real Element of REAL
A3 . (A /\ P) is ext-real V14() real Element of REAL
((A3 . (A /\ B)) + (A3 . (B /\ P))) + (A3 . (A /\ P)) is ext-real V14() real Element of REAL
(((A3 . A) + (A3 . B)) + (A3 . P)) - (((A3 . (A /\ B)) + (A3 . (B /\ P))) + (A3 . (A /\ P))) is ext-real V14() real Element of REAL
A3 . ((A /\ B) /\ P) is ext-real V14() real Element of REAL
((((A3 . A) + (A3 . B)) + (A3 . P)) - (((A3 . (A /\ B)) + (A3 . (B /\ P))) + (A3 . (A /\ P)))) + (A3 . ((A /\ B) /\ P)) is ext-real V14() real Element of REAL
(A \/ B) /\ P is Event of Sigma
A3 . ((A \/ B) /\ P) is ext-real V14() real Element of REAL
(A /\ P) \/ (B /\ P) is Event of Sigma
A3 . ((A /\ P) \/ (B /\ P)) is ext-real V14() real Element of REAL
(A3 . (A /\ P)) + (A3 . (B /\ P)) is ext-real V14() real Element of REAL
(A /\ P) /\ (B /\ P) is Event of Sigma
A3 . ((A /\ P) /\ (B /\ P)) is ext-real V14() real Element of REAL
((A3 . (A /\ P)) + (A3 . (B /\ P))) - (A3 . ((A /\ P) /\ (B /\ P))) is ext-real V14() real Element of REAL
(B /\ P) /\ P is Event of Sigma
A /\ ((B /\ P) /\ P) is Event of Sigma
A3 . (A /\ ((B /\ P) /\ P)) is ext-real V14() real Element of REAL
((A3 . (A /\ P)) + (A3 . (B /\ P))) - (A3 . (A /\ ((B /\ P) /\ P))) is ext-real V14() real Element of REAL
P /\ P is Event of Sigma
B /\ (P /\ P) is Event of Sigma
A /\ (B /\ (P /\ P)) is Event of Sigma
A3 . (A /\ (B /\ (P /\ P))) is ext-real V14() real Element of REAL
((A3 . (A /\ P)) + (A3 . (B /\ P))) - (A3 . (A /\ (B /\ (P /\ P)))) is ext-real V14() real Element of REAL
(A3 . (B /\ P)) + (A3 . (A /\ P)) is ext-real V14() real Element of REAL
((A3 . (B /\ P)) + (A3 . (A /\ P))) - (A3 . ((A /\ B) /\ P)) is ext-real V14() real Element of REAL
A3 . (A \/ B) is ext-real V14() real Element of REAL
(A3 . (A \/ B)) + (A3 . P) is ext-real V14() real Element of REAL
((A3 . (A \/ B)) + (A3 . P)) - (A3 . ((A \/ B) /\ P)) is ext-real V14() real Element of REAL
((A3 . A) + (A3 . B)) - (A3 . (A /\ B)) is ext-real V14() real Element of REAL
(((A3 . A) + (A3 . B)) - (A3 . (A /\ B))) + (A3 . P) is ext-real V14() real Element of REAL
((((A3 . A) + (A3 . B)) - (A3 . (A /\ B))) + (A3 . P)) - (A3 . ((A \/ B) /\ P)) is ext-real V14() real Element of REAL
(A3 . (A /\ B)) + (A3 . ((A \/ B) /\ P)) is ext-real V14() real Element of REAL
(((A3 . A) + (A3 . B)) + (A3 . P)) - ((A3 . (A /\ B)) + (A3 . ((A \/ B) /\ P))) is ext-real V14() real Element of REAL
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
Sigma is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
P is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
A is Event of Sigma
B is Event of Sigma
A /\ B is Event of Sigma
A \ (A /\ B) is Event of Sigma
P . (A \ (A /\ B)) is ext-real V14() real Element of REAL
P . A is ext-real V14() real Element of REAL
P . (A /\ B) is ext-real V14() real Element of REAL
(P . A) - (P . (A /\ B)) is ext-real V14() real Element of REAL
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
Sigma is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
A3 is non empty set
bool A3 is non empty set
bool (bool A3) is non empty set
P is non empty compl-closed sigma-multiplicative Element of bool (bool A3)
P is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
A is Event of Sigma
B is Event of Sigma
A /\ B is Event of Sigma
P . (A /\ B) is ext-real V14() real Element of REAL
P . B is ext-real V14() real Element of REAL
c10 is Relation-like P -defined REAL -valued Function-like V30(P, REAL ) V35() V36() V37() V44() Probability of P
n is Event of P
n1 is Event of P
n /\ n1 is Event of P
c10 . (n /\ n1) is ext-real V14() real Element of REAL
c10 . n is ext-real V14() real Element of REAL
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
Sigma is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
A is Event of Sigma
B is Event of Sigma
B ` is Element of bool Omega
Omega \ B is set
P is Event of Sigma
P /\ B is Event of Sigma
P /\ A is Event of Sigma
A3 is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
A3 . P is ext-real V14() real Element of REAL
A3 . (P /\ B) is ext-real V14() real Element of REAL
A3 . (P /\ A) is ext-real V14() real Element of REAL
(A3 . (P /\ B)) + (A3 . (P /\ A)) is ext-real V14() real Element of REAL
[#] Omega is non empty non proper Element of bool Omega
P /\ ([#] Omega) is Element of bool Omega
A3 . (P /\ ([#] Omega)) is ext-real V14() real Element of REAL
B \/ A is Event of Sigma
P /\ (B \/ A) is Event of Sigma
A3 . (P /\ (B \/ A)) is ext-real V14() real Element of REAL
(P /\ B) \/ (P /\ A) is Event of Sigma
A3 . ((P /\ B) \/ (P /\ A)) is ext-real V14() real Element of REAL
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
Sigma is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
A is Event of Sigma
B is Event of Sigma
A /\ B is Event of Sigma
P is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
P . A is ext-real V14() real Element of REAL
P . B is ext-real V14() real Element of REAL
(P . A) + (P . B) is ext-real V14() real Element of REAL
((P . A) + (P . B)) - 1 is ext-real V14() real Element of REAL
P . (A /\ B) is ext-real V14() real Element of REAL
((P . A) + (P . B)) - (P . (A /\ B)) is ext-real V14() real Element of REAL
A \/ B is Event of Sigma
P . (A \/ B) is ext-real V14() real Element of REAL
(P . (A /\ B)) + 1 is ext-real V14() real Element of REAL
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
Sigma is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
[#] Sigma is Event of Sigma
A is Event of Sigma
([#] Sigma) \ A is Event of Sigma
B is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
B . A is ext-real V14() real Element of REAL
B . (([#] Sigma) \ A) is ext-real V14() real Element of REAL
1 - (B . (([#] Sigma) \ A)) is ext-real V14() real Element of REAL
(B . (([#] Sigma) \ A)) + (B . A) is ext-real V14() real Element of REAL
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
Sigma is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
[#] Sigma is Event of Sigma
A is Event of Sigma
([#] Sigma) \ A is Event of Sigma
B is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
B . A is ext-real V14() real Element of REAL
B . (([#] Sigma) \ A) is ext-real V14() real Element of REAL
1 - (B . (([#] Sigma) \ A)) is ext-real V14() real Element of REAL
- (B . (([#] Sigma) \ A)) is ext-real V14() real Element of REAL
1 + (- (B . (([#] Sigma) \ A))) is ext-real V14() real Element of REAL
1 - 1 is ext-real V14() real Element of REAL
1 - (B . A) is ext-real V14() real Element of REAL
(B . A) + 0 is ext-real V14() real Element of REAL
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
Sigma is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
[#] Sigma is Event of Sigma
A is Event of Sigma
([#] Sigma) \ A is Event of Sigma
B is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
B . (([#] Sigma) \ A) is ext-real V14() real Element of REAL
B . A is ext-real V14() real Element of REAL
1 - (B . A) is ext-real V14() real Element of REAL
- (B . A) is ext-real V14() real Element of REAL
1 + (- (B . A)) is ext-real V14() real Element of REAL
1 - 1 is ext-real V14() real Element of REAL
1 - (B . (([#] Sigma) \ A)) is ext-real V14() real Element of REAL
(B . (([#] Sigma) \ A)) + 0 is ext-real V14() real Element of REAL
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
Sigma is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
Sigma is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
A is Event of Sigma
B is Event of Sigma
P is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
B /\ A is Event of Sigma
P . (B /\ A) is ext-real V14() real Element of REAL
P . B is ext-real V14() real Element of REAL
P . A is ext-real V14() real Element of REAL
(P . B) * (P . A) is ext-real V14() real Element of REAL
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
Sigma is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
A is Event of Sigma
B is Event of Sigma
A /\ B is Event of Sigma
P is Event of Sigma
(A /\ B) /\ P is Event of Sigma
A3 is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
A3 . ((A /\ B) /\ P) is ext-real V14() real Element of REAL
A3 . A is ext-real V14() real Element of REAL
A3 . B is ext-real V14() real Element of REAL
(A3 . A) * (A3 . B) is ext-real V14() real Element of REAL
A3 . P is ext-real V14() real Element of REAL
((A3 . A) * (A3 . B)) * (A3 . P) is ext-real V14() real Element of REAL
B /\ P is Event of Sigma
A3 . (B /\ P) is ext-real V14() real Element of REAL
(A3 . B) * (A3 . P) is ext-real V14() real Element of REAL
A3 . (A /\ B) is ext-real V14() real Element of REAL
A /\ P is Event of Sigma
A3 . (A /\ P) is ext-real V14() real Element of REAL
(A3 . A) * (A3 . P) is ext-real V14() real Element of REAL
B /\ P is Event of Sigma
A3 . (B /\ P) is ext-real V14() real Element of REAL
(A3 . B) * (A3 . P) is ext-real V14() real Element of REAL
A3 . (A /\ B) is ext-real V14() real Element of REAL
A /\ P is Event of Sigma
A3 . (A /\ P) is ext-real V14() real Element of REAL
(A3 . A) * (A3 . P) is ext-real V14() real Element of REAL
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
Sigma is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
A is Event of Sigma
B is Event of Sigma
P is Event of Sigma
A3 is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
A /\ B is Event of Sigma
(A /\ B) /\ P is Event of Sigma
A3 . ((A /\ B) /\ P) is ext-real V14() real Element of REAL
A3 . A is ext-real V14() real Element of REAL
A3 . B is ext-real V14() real Element of REAL
(A3 . A) * (A3 . B) is ext-real V14() real Element of REAL
A3 . P is ext-real V14() real Element of REAL
((A3 . A) * (A3 . B)) * (A3 . P) is ext-real V14() real Element of REAL
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
Sigma is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
A is Event of Sigma
B is Event of Sigma
P is Event of Sigma
A3 is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
A /\ B is Event of Sigma
(A /\ B) /\ P is Event of Sigma
A3 . ((A /\ B) /\ P) is ext-real V14() real Element of REAL
A3 . A is ext-real V14() real Element of REAL
A3 . B is ext-real V14() real Element of REAL
(A3 . A) * (A3 . B) is ext-real V14() real Element of REAL
A3 . P is ext-real V14() real Element of REAL
((A3 . A) * (A3 . B)) * (A3 . P) is ext-real V14() real Element of REAL
A /\ P is Event of Sigma
(A /\ P) /\ B is Event of Sigma
A3 . ((A /\ P) /\ B) is ext-real V14() real Element of REAL
(A3 . A) * (A3 . P) is ext-real V14() real Element of REAL
((A3 . A) * (A3 . P)) * (A3 . B) is ext-real V14() real Element of REAL
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
Sigma is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
A is Event of Sigma
B is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
P is Event of Sigma

bool Sigma is non empty set
A /\ ({} Sigma) is V45() V46() V47() V48() V49() V50() Element of bool Sigma
B . (A /\ ({} Sigma)) is ext-real V14() real Element of REAL
B . A is ext-real V14() real Element of REAL
(B . A) * 0 is ext-real V14() real Element of REAL
B . ({} Sigma) is ext-real V14() real Element of REAL
(B . A) * (B . ({} Sigma)) is ext-real V14() real Element of REAL
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
Sigma is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
[#] Sigma is Event of Sigma
A is Event of Sigma
B is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
A /\ ([#] Sigma) is Event of Sigma
B . (A /\ ([#] Sigma)) is ext-real V14() real Element of REAL
B . A is ext-real V14() real Element of REAL
(B . A) * 1 is ext-real V14() real Element of REAL
B . ([#] Sigma) is ext-real V14() real Element of REAL
(B . A) * (B . ([#] Sigma)) is ext-real V14() real Element of REAL
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
Sigma is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
[#] Sigma is Event of Sigma
A is Event of Sigma
B is Event of Sigma
([#] Sigma) \ B is Event of Sigma
P is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
A /\ B is Event of Sigma
P . (A /\ B) is ext-real V14() real Element of REAL
P . A is ext-real V14() real Element of REAL
P . B is ext-real V14() real Element of REAL
(P . A) * (P . B) is ext-real V14() real Element of REAL
A /\ (([#] Sigma) \ B) is Event of Sigma
P . (A /\ (([#] Sigma) \ B)) is ext-real V14() real Element of REAL
B ` is Element of bool Omega
Omega \ B is set
A /\ (B `) is Element of bool Omega
P . (A /\ (B `)) is ext-real V14() real Element of REAL
A \ B is Event of Sigma
P . (A \ B) is ext-real V14() real Element of REAL
A \ (A /\ B) is Event of Sigma
P . (A \ (A /\ B)) is ext-real V14() real Element of REAL
(P . A) * 1 is ext-real V14() real Element of REAL
((P . A) * 1) - ((P . A) * (P . B)) is ext-real V14() real Element of REAL
1 - (P . B) is ext-real V14() real Element of REAL
(P . A) * (1 - (P . B)) is ext-real V14() real Element of REAL
P . (([#] Sigma) \ B) is ext-real V14() real Element of REAL
(P . A) * (P . (([#] Sigma) \ B)) is ext-real V14() real Element of REAL
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
Sigma is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
[#] Sigma is Event of Sigma
A is Event of Sigma
([#] Sigma) \ A is Event of Sigma
B is Event of Sigma
([#] Sigma) \ B is Event of Sigma
P is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
Sigma is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
A is Event of Sigma
B is Event of Sigma
P is Event of Sigma
B \/ P is Event of Sigma
A3 is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
A /\ B is Event of Sigma
A /\ P is Event of Sigma
A /\ (B \/ P) is Event of Sigma
A3 . (A /\ (B \/ P)) is ext-real V14() real Element of REAL
(A /\ B) \/ (A /\ P) is Event of Sigma
A3 . ((A /\ B) \/ (A /\ P)) is ext-real V14() real Element of REAL
A3 . (A /\ B) is ext-real V14() real Element of REAL
A3 . (A /\ P) is ext-real V14() real Element of REAL
(A3 . (A /\ B)) + (A3 . (A /\ P)) is ext-real V14() real Element of REAL
A3 . A is ext-real V14() real Element of REAL
A3 . B is ext-real V14() real Element of REAL
(A3 . A) * (A3 . B) is ext-real V14() real Element of REAL
((A3 . A) * (A3 . B)) + (A3 . (A /\ P)) is ext-real V14() real Element of REAL
A3 . P is ext-real V14() real Element of REAL
(A3 . A) * (A3 . P) is ext-real V14() real Element of REAL
((A3 . A) * (A3 . B)) + ((A3 . A) * (A3 . P)) is ext-real V14() real Element of REAL
(A3 . B) + (A3 . P) is ext-real V14() real Element of REAL
(A3 . A) * ((A3 . B) + (A3 . P)) is ext-real V14() real Element of REAL
A3 . (B \/ P) is ext-real V14() real Element of REAL
(A3 . A) * (A3 . (B \/ P)) is ext-real V14() real Element of REAL
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
Sigma is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
B is ext-real V14() real Element of REAL

- B is ext-real V14() real Element of REAL
A is ext-real V14() real Element of REAL
A + 0 is ext-real V14() real Element of REAL
A + (- B) is ext-real V14() real Element of REAL
A - B is ext-real V14() real Element of REAL
A is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
B is Event of Sigma
A . B is ext-real V14() real Element of REAL
P is Event of Sigma
A . P is ext-real V14() real Element of REAL
B \/ P is Event of Sigma
A . (B \/ P) is ext-real V14() real Element of REAL
[#] Sigma is Event of Sigma
([#] Sigma) \ B is Event of Sigma
([#] Sigma) \ P is Event of Sigma
A . (([#] Sigma) \ B) is ext-real V14() real Element of REAL
A . (([#] Sigma) \ P) is ext-real V14() real Element of REAL
([#] Sigma) \ (B \/ P) is Event of Sigma
A . (([#] Sigma) \ (B \/ P)) is ext-real V14() real Element of REAL
1 - (A . (([#] Sigma) \ (B \/ P))) is ext-real V14() real Element of REAL
(([#] Sigma) \ B) /\ (([#] Sigma) \ P) is Event of Sigma
A . ((([#] Sigma) \ B) /\ (([#] Sigma) \ P)) is ext-real V14() real Element of REAL
1 - (A . ((([#] Sigma) \ B) /\ (([#] Sigma) \ P))) is ext-real V14() real Element of REAL
(A . (([#] Sigma) \ B)) * (A . (([#] Sigma) \ P)) is ext-real V14() real Element of REAL
1 - ((A . (([#] Sigma) \ B)) * (A . (([#] Sigma) \ P))) is ext-real V14() real Element of REAL
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
Sigma is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
A is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
B is Event of Sigma
A . B is ext-real V14() real Element of REAL
P is set
A3 is Event of Sigma
A3 /\ B is Event of Sigma
A . (A3 /\ B) is ext-real V14() real Element of REAL
(A . (A3 /\ B)) / (A . B) is ext-real V14() real Element of REAL
P is set
[:Sigma,REAL:] is non empty V35() V36() V37() set
bool [:Sigma,REAL:] is non empty set
P is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() Element of bool [:Sigma,REAL:]
A3 is Event of Sigma
P . A3 is ext-real V14() real Element of REAL
A3 /\ B is Event of Sigma
A . (A3 /\ B) is ext-real V14() real Element of REAL
(A . (A3 /\ B)) / (A . B) is ext-real V14() real Element of REAL
P is Event of Sigma
n is ext-real V14() real Element of REAL
P /\ B is Event of Sigma
A . (P /\ B) is ext-real V14() real Element of REAL
(A . (P /\ B)) / (A . B) is ext-real V14() real Element of REAL
P . Omega is ext-real V14() real Element of REAL
[#] Sigma is Event of Sigma
([#] Sigma) /\ B is Event of Sigma
A . (([#] Sigma) /\ B) is ext-real V14() real Element of REAL
(A . (([#] Sigma) /\ B)) / (A . B) is ext-real V14() real Element of REAL
(A . B) / (A . B) is ext-real V14() real Element of REAL
A3 is Event of Sigma
P . A3 is ext-real V14() real Element of REAL
P is Event of Sigma
A3 \/ P is Event of Sigma
P . (A3 \/ P) is ext-real V14() real Element of REAL
P . P is ext-real V14() real Element of REAL
(P . A3) + (P . P) is ext-real V14() real Element of REAL
A3 /\ B is Event of Sigma
P /\ B is Event of Sigma
(A3 \/ P) /\ B is Event of Sigma
A . ((A3 \/ P) /\ B) is ext-real V14() real Element of REAL
(A . ((A3 \/ P) /\ B)) / (A . B) is ext-real V14() real Element of REAL
(A3 /\ B) \/ (P /\ B) is Event of Sigma
A . ((A3 /\ B) \/ (P /\ B)) is ext-real V14() real Element of REAL
(A . ((A3 /\ B) \/ (P /\ B))) / (A . B) is ext-real V14() real Element of REAL
A . (A3 /\ B) is ext-real V14() real Element of REAL
A . (P /\ B) is ext-real V14() real Element of REAL
(A . (A3 /\ B)) + (A . (P /\ B)) is ext-real V14() real Element of REAL
((A . (A3 /\ B)) + (A . (P /\ B))) / (A . B) is ext-real V14() real Element of REAL
(A . (A3 /\ B)) / (A . B) is ext-real V14() real Element of REAL
(A . (P /\ B)) / (A . B) is ext-real V14() real Element of REAL
((A . (A3 /\ B)) / (A . B)) + ((A . (P /\ B)) / (A . B)) is ext-real V14() real Element of REAL
((A . (A3 /\ B)) / (A . B)) + (P . P) is ext-real V14() real Element of REAL
A3 is Event of Sigma
P . A3 is ext-real V14() real Element of REAL
A3 /\ B is Event of Sigma
A . (A3 /\ B) is ext-real V14() real Element of REAL
(A . (A3 /\ B)) / (A . B) is ext-real V14() real Element of REAL
K231(Omega) is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
[:NAT,K231(Omega):] is non empty set
bool [:NAT,K231(Omega):] is non empty set
A3 is Relation-like NAT -defined Sigma -valued K231(Omega) -valued Function-like V30( NAT ,K231(Omega)) Element of bool [:NAT,K231(Omega):]

lim (P * A3) is ext-real V14() real Element of REAL
Intersection A3 is Element of bool Omega
Complement A3 is Relation-like NAT -defined Sigma -valued K231(Omega) -valued Function-like V30( NAT ,K231(Omega)) Element of bool [:NAT,K231(Omega):]
Union () is Element of bool Omega
(Union ()) ` is Element of bool Omega
Omega \ (Union ()) is set
P . () is ext-real V14() real Element of REAL
P is Relation-like NAT -defined Sigma -valued K231(Omega) -valued Function-like V30( NAT ,K231(Omega)) Element of bool [:NAT,K231(Omega):]
dom (P * A3) is set
n is set
(P * A3) . n is ext-real V14() real Element of REAL
A3 . n is set
P . (A3 . n) is ext-real V14() real Element of REAL

(Omega,Sigma,A3,n1) is Event of Sigma
(Omega,Sigma,A3,n1) /\ B is Event of Sigma
A . ((Omega,Sigma,A3,n1) /\ B) is ext-real V14() real Element of REAL
(A . ((Omega,Sigma,A3,n1) /\ B)) / (A . B) is ext-real V14() real Element of REAL
P . n is set
A . (P . n) is ext-real V14() real Element of REAL
(A . (P . n)) / (A . B) is ext-real V14() real Element of REAL

(A * P) . n is ext-real V14() real Element of REAL
((A * P) . n) / (A . B) is ext-real V14() real Element of REAL
(A . B) " is ext-real V14() real Element of REAL
((A . B) ") * ((A * P) . n) is ext-real V14() real Element of REAL
dom (A * P) is set
((A . B) ") (#) (A * P) is Relation-like NAT -defined REAL -valued Function-like V35() V36() V37() Element of bool
lim (A * P) is ext-real V14() real Element of REAL
Intersection P is Element of bool Omega
Complement P is Relation-like NAT -defined Sigma -valued K231(Omega) -valued Function-like V30( NAT ,K231(Omega)) Element of bool [:NAT,K231(Omega):]
Union () is Element of bool Omega
(Union ()) ` is Element of bool Omega
Omega \ (Union ()) is set
A . () is ext-real V14() real Element of REAL
(Omega,Sigma,P) is Event of Sigma
A . (Omega,Sigma,P) is ext-real V14() real Element of REAL
((A . B) ") * (A . (Omega,Sigma,P)) is ext-real V14() real Element of REAL
(A . (Omega,Sigma,P)) / (A . B) is ext-real V14() real Element of REAL
(Omega,Sigma,A3) is Event of Sigma
(Omega,Sigma,A3) /\ B is Event of Sigma
A . ((Omega,Sigma,A3) /\ B) is ext-real V14() real Element of REAL
(A . ((Omega,Sigma,A3) /\ B)) / (A . B) is ext-real V14() real Element of REAL
A3 is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
P is Event of Sigma
A3 . P is ext-real V14() real Element of REAL
P /\ B is Event of Sigma
A . (P /\ B) is ext-real V14() real Element of REAL
(A . (P /\ B)) / (A . B) is ext-real V14() real Element of REAL
P is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
A3 is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
P is Event of Sigma
P . P is ext-real V14() real Element of REAL
P /\ B is Event of Sigma
A . (P /\ B) is ext-real V14() real Element of REAL
(A . (P /\ B)) / (A . B) is ext-real V14() real Element of REAL
A3 . P is ext-real V14() real Element of REAL
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
Sigma is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
A is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
B is Event of Sigma
A . B is ext-real V14() real Element of REAL
(Omega,Sigma,A,B) is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
P is Event of Sigma
P /\ B is Event of Sigma
A . (P /\ B) is ext-real V14() real Element of REAL
(Omega,Sigma,A,B) . P is ext-real V14() real Element of REAL
((Omega,Sigma,A,B) . P) * (A . B) is ext-real V14() real Element of REAL
(A . (P /\ B)) / (A . B) is ext-real V14() real Element of REAL
((A . (P /\ B)) / (A . B)) * (A . B) is ext-real V14() real Element of REAL
(A . B) " is ext-real V14() real Element of REAL
(A . (P /\ B)) * ((A . B) ") is ext-real V14() real Element of REAL
((A . (P /\ B)) * ((A . B) ")) * (A . B) is ext-real V14() real Element of REAL
((A . B) ") * (A . B) is ext-real V14() real Element of REAL
(A . (P /\ B)) * (((A . B) ") * (A . B)) is ext-real V14() real Element of REAL
(A . (P /\ B)) * 1 is ext-real V14() real Element of REAL
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
Sigma is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
A is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
B is Event of Sigma
A . B is ext-real V14() real Element of REAL
(Omega,Sigma,A,B) is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
P is Event of Sigma
B /\ P is Event of Sigma
A . (B /\ P) is ext-real V14() real Element of REAL
(Omega,Sigma,A,B) . P is ext-real V14() real Element of REAL
(A . B) * ((Omega,Sigma,A,B) . P) is ext-real V14() real Element of REAL
(Omega,Sigma,A,(B /\ P)) is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
A3 is Event of Sigma
(B /\ P) /\ A3 is Event of Sigma
A . ((B /\ P) /\ A3) is ext-real V14() real Element of REAL
(Omega,Sigma,A,(B /\ P)) . A3 is ext-real V14() real Element of REAL
((A . B) * ((Omega,Sigma,A,B) . P)) * ((Omega,Sigma,A,(B /\ P)) . A3) is ext-real V14() real Element of REAL
P /\ B is Event of Sigma
A . (P /\ B) is ext-real V14() real Element of REAL
(A . (P /\ B)) * ((Omega,Sigma,A,(B /\ P)) . A3) is ext-real V14() real Element of REAL
Omega is non empty set
bool Omega is non empty set
bool (bool Omega) is non empty set
Sigma is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
A is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
B is Event of Sigma
A . B is ext-real V14() real Element of REAL
P is Event of Sigma
P ` is Element of bool Omega
Omega \ P is set
A . P is ext-real V14() real Element of REAL
(Omega,Sigma,A,P) is Relation-like Sigma -defined