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
[:NAT,REAL:] is non empty V35() V36() V37() set
bool [:NAT,REAL:] is non empty set
bool (bool REAL) is non empty set
{} is ext-real non positive non negative empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real V45() V46() V47() V48() V49() V50() V51() set
0 is ext-real non positive non negative empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() V51() Element of NAT
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
Sigma is Relation-like NAT -defined REAL -valued Function-like V30( NAT , REAL ) V35() V36() V37() Element of bool [:NAT,REAL:]
lim Sigma is ext-real V14() real Element of REAL
Omega - (lim Sigma) is ext-real V14() real Element of REAL
A is Relation-like NAT -defined REAL -valued Function-like V30( NAT , REAL ) V35() V36() V37() Element of bool [:NAT,REAL:]
lim A is ext-real V14() real Element of REAL
B is ext-real V14() real set
P is ext-real V14() real set
A3 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
P is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
n is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
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
n is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
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):]
B is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
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 (Complement A) is Element of bool Omega
(Union (Complement A)) ` is Element of bool Omega
Omega \ (Union (Complement A)) 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
P is Relation-like Function-like set
dom P is set
A3 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(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
P is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real set
n is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(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):]
n is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(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
A3 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
B . A3 is set
P is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
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 (Complement A) is Element of bool Omega
(Union (Complement A)) ` is Element of bool Omega
Omega \ (Union (Complement A)) 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 (Complement B) is Element of bool Omega
(Union (Complement B)) ` is Element of bool Omega
Omega \ (Union (Complement B)) is set
P is Event of Sigma
(Intersection B) /\ P is Element of bool Omega
A3 is set
P is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(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
P is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(Omega,Sigma,B,P) is Event of Sigma
(Omega,Sigma,B,P) /\ P is Event of Sigma
A3 is set
P is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(Omega,Sigma,B,P) is Event of Sigma
(Omega,Sigma,B,P) /\ P is Event of Sigma
P is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(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):]
B is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real set
P 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),(Complement A),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
(Complement A) . B is Element of K231(Omega)
rng (Complement A) 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 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
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 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
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 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
B 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)
P is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
A + P 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)) 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)
A + 0 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 + 0)) is Event of K231(Omega)
P is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real set
A + P 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,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 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
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)
A 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)
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)
A is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
B 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)
P is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
A + P 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)) 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)
A + 0 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 + 0)) is Event of K231(Omega)
P is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real set
A + P 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,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):]
A is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
B 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,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)
A is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
B 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),(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):]
A is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
B 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,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)
A is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
B 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),(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):]
B is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
P is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(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):]
A * B is Relation-like NAT -defined REAL -valued Function-like V30( NAT , REAL ) V35() V36() V37() Element of bool [:NAT,REAL:]
lim (A * B) is ext-real V14() real Element of REAL
Union B is Element of bool Omega
A . (Union B) 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 * (Complement B) is Relation-like NAT -defined REAL -valued Function-like V30( NAT , REAL ) V35() V36() V37() Element of bool [:NAT,REAL:]
A3 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(A * (Complement B)) . A3 is ext-real V14() real Element of REAL
(Omega,Sigma,(Complement B),A3) is Event of Sigma
A . (Omega,Sigma,(Complement B),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 * (Complement B)) . A3) is ext-real V14() real Element of REAL
Intersection (Complement B) is Element of bool Omega
Complement (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 (Complement (Complement B)) is Element of bool Omega
(Union (Complement (Complement B))) ` is Element of bool Omega
Omega \ (Union (Complement (Complement B))) is set
([#] Sigma) \ (Union B) is Element of bool Omega
A . (Intersection (Complement B)) 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 * (Complement B)) is ext-real V14() real Element of REAL
1 - (lim (A * (Complement B))) 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):]
A * P is Relation-like NAT -defined REAL -valued Function-like V30( NAT , REAL ) V35() V36() V37() Element of bool [:NAT,REAL:]
lim (A * P) is ext-real V14() real Element of REAL
Union P is Element of bool Omega
A . (Union P) 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):]
A * B is Relation-like NAT -defined REAL -valued Function-like V30( NAT , REAL ) V35() V36() V37() Element of bool [:NAT,REAL:]
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 (Complement B) is Element of bool Omega
(Union (Complement B)) ` is Element of bool Omega
Omega \ (Union (Complement B)) is set
A . (Intersection B) 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 * (Complement B) is Relation-like NAT -defined REAL -valued Function-like V30( NAT , REAL ) V35() V36() V37() Element of bool [:NAT,REAL:]
P is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(A * (Complement B)) . P is ext-real V14() real Element of REAL
(Omega,Sigma,(Complement B),P) is Event of Sigma
A . (Omega,Sigma,(Complement B),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 * (Complement B)) . P) is ext-real V14() real Element of REAL
(Intersection B) ` is Element of bool Omega
Omega \ (Intersection B) is set
A . (Union (Complement B)) 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 * (Complement B)) is ext-real V14() real Element of REAL
1 - (lim (A * (Complement B))) 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
{} Sigma is ext-real non positive non negative empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real V45() V46() V47() V48() V49() V50() V51() Element of bool 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
- 0 is ext-real non positive non negative empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real V45() V46() V47() V48() V49() V50() V51() 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):]
P * A3 is Relation-like NAT -defined REAL -valued Function-like V30( NAT , REAL ) V35() V36() V37() Element of bool [:NAT,REAL:]
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 (Complement A3) is Element of bool Omega
(Union (Complement A3)) ` is Element of bool Omega
Omega \ (Union (Complement A3)) is set
P . (Intersection A3) 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
n1 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
(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 is Relation-like NAT -defined REAL -valued Function-like V30( NAT , REAL ) V35() V36() V37() Element of bool [:NAT,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 [:NAT,REAL:]
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 (Complement P) is Element of bool Omega
(Union (Complement P)) ` is Element of bool Omega
Omega \ (Union (Complement P)) is set
A . (Intersection 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
((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 REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
(Omega,Sigma,A,P) . B is ext-real V14() real Element of REAL
((Omega,Sigma,A,P) . B) * (A . P) is ext-real V14() real Element of REAL
A3 is Event of Sigma
A . A3 is ext-real V14() real Element of REAL
(Omega,Sigma,A,A3) is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
(Omega,Sigma,A,A3) . B is ext-real V14() real Element of REAL
((Omega,Sigma,A,A3) . B) * (A . A3) is ext-real V14() real Element of REAL
(((Omega,Sigma,A,P) . B) * (A . P)) + (((Omega,Sigma,A,A3) . B) * (A . A3)) 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
B /\ A3 is Event of Sigma
A . (B /\ A3) is ext-real V14() real Element of REAL
(A . (B /\ P)) + (A . (B /\ A3)) is ext-real V14() real Element of REAL
(((Omega,Sigma,A,P) . B) * (A . P)) + (A . (B /\ 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
A . P is ext-real V14() real Element of REAL
(Omega,Sigma,A,P) is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
(Omega,Sigma,A,P) . B is ext-real V14() real Element of REAL
((Omega,Sigma,A,P) . B) * (A . P) is ext-real V14() real Element of REAL
A3 is Event of Sigma
P \/ A3 is Event of Sigma
(P \/ A3) ` is Element of bool Omega
Omega \ (P \/ A3) is set
A . A3 is ext-real V14() real Element of REAL
(Omega,Sigma,A,A3) is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
(Omega,Sigma,A,A3) . B is ext-real V14() real Element of REAL
((Omega,Sigma,A,A3) . B) * (A . A3) is ext-real V14() real Element of REAL
(((Omega,Sigma,A,P) . B) * (A . P)) + (((Omega,Sigma,A,A3) . B) * (A . A3)) is ext-real V14() real Element of REAL
P is Event of Sigma
A . P is ext-real V14() real Element of REAL
(Omega,Sigma,A,P) is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
(Omega,Sigma,A,P) . B is ext-real V14() real Element of REAL
((Omega,Sigma,A,P) . B) * (A . P) is ext-real V14() real Element of REAL
((((Omega,Sigma,A,P) . B) * (A . P)) + (((Omega,Sigma,A,A3) . B) * (A . A3))) + (((Omega,Sigma,A,P) . B) * (A . P)) is ext-real V14() real Element of REAL
B /\ P is Event of Sigma
B /\ A3 is Event of Sigma
B /\ (P \/ A3) is Event of Sigma
B /\ P is Event of Sigma
(P \/ A3) \/ P is Event of Sigma
[#] Omega is non empty non proper Element of bool Omega
A . (B /\ P) is ext-real V14() real Element of REAL
(A . (B /\ P)) + (((Omega,Sigma,A,A3) . B) * (A . A3)) is ext-real V14() real Element of REAL
((A . (B /\ P)) + (((Omega,Sigma,A,A3) . B) * (A . A3))) + (((Omega,Sigma,A,P) . B) * (A . P)) is ext-real V14() real Element of REAL
A . (B /\ A3) is ext-real V14() real Element of REAL
(A . (B /\ P)) + (A . (B /\ A3)) is ext-real V14() real Element of REAL
((A . (B /\ P)) + (A . (B /\ A3))) + (((Omega,Sigma,A,P) . B) * (A . P)) is ext-real V14() real Element of REAL
A . (B /\ P) is ext-real V14() real Element of REAL
((A . (B /\ P)) + (A . (B /\ A3))) + (A . (B /\ P)) is ext-real V14() real Element of REAL
(B /\ P) \/ (B /\ A3) is Event of Sigma
A . ((B /\ P) \/ (B /\ A3)) is ext-real V14() real Element of REAL
(A . ((B /\ P) \/ (B /\ A3))) + (A . (B /\ P)) is ext-real V14() real Element of REAL
A . (B /\ (P \/ A3)) is ext-real V14() real Element of REAL
(A . (B /\ (P \/ A3))) + (A . (B /\ P)) is ext-real V14() real Element of REAL
(B /\ (P \/ A3)) \/ (B /\ P) is Event of Sigma
A . ((B /\ (P \/ A3)) \/ (B /\ P)) is ext-real V14() real Element of REAL
B /\ Omega is Element of bool Omega
A . (B /\ Omega) 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
A . P is ext-real V14() real Element of REAL
(Omega,Sigma,A,P) is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
(Omega,Sigma,A,P) . B 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
(A . (B /\ P)) / (A . P) is ext-real V14() real Element of REAL
((A . (B /\ P)) / (A . P)) * (A . P) is ext-real V14() real Element of REAL
(A . B) * (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
(A . P) " is ext-real V14() real Element of REAL
(A . (B /\ P)) * ((A . P) ") is ext-real V14() real Element of REAL
(A . B) * (A . P) is ext-real V14() real Element of REAL
((A . B) * (A . P)) * ((A . P) ") is ext-real V14() real Element of REAL
(A . P) * ((A . P) ") is ext-real V14() real Element of REAL
(A . B) * ((A . P) * ((A . P) ")) is ext-real V14() real Element of REAL
(A . B) * 1 is ext-real V14() real Element of REAL
(A . (B /\ P)) / (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)
[#] Sigma is Event of Sigma
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
P is Event of Sigma
A . P is ext-real V14() real Element of REAL
(Omega,Sigma,A,P) is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
(Omega,Sigma,A,P) . B is ext-real V14() real Element of REAL
([#] Sigma) \ P is Event of Sigma
(Omega,Sigma,A,(([#] Sigma) \ P)) is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
(Omega,Sigma,A,(([#] Sigma) \ P)) . B is ext-real V14() real Element of REAL
A . (([#] Sigma) \ 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
(A . (B /\ P)) / (A . P) is ext-real V14() real Element of REAL
B /\ (([#] Sigma) \ P) is Event of Sigma
A . (B /\ (([#] Sigma) \ P)) is ext-real V14() real Element of REAL
(A . (B /\ (([#] Sigma) \ P))) / (A . (([#] Sigma) \ P)) is ext-real V14() real Element of REAL
P ` is Element of bool Omega
Omega \ P is set
(A . (B /\ P)) * (A . (([#] Sigma) \ P)) is ext-real V14() real Element of REAL
(A . (B /\ (([#] Sigma) \ P))) * (A . P) is ext-real V14() real Element of REAL
1 - (A . P) is ext-real V14() real Element of REAL
(A . (B /\ P)) * (1 - (A . P)) is ext-real V14() real Element of REAL
(A . (B /\ (([#] Sigma) \ P))) + (A . (B /\ P)) is ext-real V14() real Element of REAL
((A . (B /\ (([#] Sigma) \ P))) + (A . (B /\ P))) * (A . P) is ext-real V14() real Element of REAL
A . B is ext-real V14() real Element of REAL
(A . B) * (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 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
(A . B) + (A . P) is ext-real V14() real Element of REAL
((A . B) + (A . P)) - 1 is ext-real V14() real Element of REAL
(((A . B) + (A . P)) - 1) / (A . P) is ext-real V14() real Element of REAL
(Omega,Sigma,A,P) is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
(Omega,Sigma,A,P) . B 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
(A . (B /\ P)) / (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
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
(Omega,Sigma,P,B) is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
(Omega,Sigma,P,B) . A is ext-real V14() real Element of REAL
(Omega,Sigma,P,A) is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
(Omega,Sigma,P,A) . B is ext-real V14() real Element of REAL
((Omega,Sigma,P,A) . B) * (P . A) is ext-real V14() real Element of REAL
(((Omega,Sigma,P,A) . B) * (P . A)) / (P . 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)) / (P . 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 Event of Sigma
B ` is Element of bool Omega
Omega \ B is set
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 is ext-real V14() real Element of REAL
A3 . B is ext-real V14() real Element of REAL
A3 . P is ext-real V14() real Element of REAL
(Omega,Sigma,A3,A) is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
(Omega,Sigma,A3,A) . B is ext-real V14() real Element of REAL
(Omega,Sigma,A3,B) is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
(Omega,Sigma,A3,B) . A is ext-real V14() real Element of REAL
((Omega,Sigma,A3,B) . A) * (A3 . B) is ext-real V14() real Element of REAL
(Omega,Sigma,A3,P) is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
(Omega,Sigma,A3,P) . A is ext-real V14() real Element of REAL
((Omega,Sigma,A3,P) . A) * (A3 . P) is ext-real V14() real Element of REAL
(((Omega,Sigma,A3,B) . A) * (A3 . B)) + (((Omega,Sigma,A3,P) . A) * (A3 . P)) is ext-real V14() real Element of REAL
(((Omega,Sigma,A3,B) . A) * (A3 . B)) / ((((Omega,Sigma,A3,B) . A) * (A3 . B)) + (((Omega,Sigma,A3,P) . A) * (A3 . P))) is ext-real V14() real Element of REAL
(Omega,Sigma,A3,A) . P is ext-real V14() real Element of REAL
(((Omega,Sigma,A3,P) . A) * (A3 . P)) / ((((Omega,Sigma,A3,B) . A) * (A3 . B)) + (((Omega,Sigma,A3,P) . A) * (A3 . P))) is ext-real V14() real Element of REAL
(((Omega,Sigma,A3,B) . A) * (A3 . B)) / (A3 . A) is ext-real V14() real Element of REAL
(((Omega,Sigma,A3,P) . A) * (A3 . P)) / (A3 . 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
P is Event of Sigma
B \/ P is Event of Sigma
(B \/ P) ` is Element of bool Omega
Omega \ (B \/ P) is set
A3 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 . P is ext-real V14() real Element of REAL
P . A3 is ext-real V14() real Element of REAL
(Omega,Sigma,P,A) is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
(Omega,Sigma,P,A) . B is ext-real V14() real Element of REAL
(Omega,Sigma,P,B) is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
(Omega,Sigma,P,B) . A is ext-real V14() real Element of REAL
((Omega,Sigma,P,B) . A) * (P . B) is ext-real V14() real Element of REAL
(Omega,Sigma,P,P) is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
(Omega,Sigma,P,P) . A is ext-real V14() real Element of REAL
((Omega,Sigma,P,P) . A) * (P . P) is ext-real V14() real Element of REAL
(((Omega,Sigma,P,B) . A) * (P . B)) + (((Omega,Sigma,P,P) . A) * (P . P)) is ext-real V14() real Element of REAL
(Omega,Sigma,P,A3) is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
(Omega,Sigma,P,A3) . A is ext-real V14() real Element of REAL
((Omega,Sigma,P,A3) . A) * (P . A3) is ext-real V14() real Element of REAL
((((Omega,Sigma,P,B) . A) * (P . B)) + (((Omega,Sigma,P,P) . A) * (P . P))) + (((Omega,Sigma,P,A3) . A) * (P . A3)) is ext-real V14() real Element of REAL
(((Omega,Sigma,P,B) . A) * (P . B)) / (((((Omega,Sigma,P,B) . A) * (P . B)) + (((Omega,Sigma,P,P) . A) * (P . P))) + (((Omega,Sigma,P,A3) . A) * (P . A3))) is ext-real V14() real Element of REAL
(Omega,Sigma,P,A) . P is ext-real V14() real Element of REAL
(((Omega,Sigma,P,P) . A) * (P . P)) / (((((Omega,Sigma,P,B) . A) * (P . B)) + (((Omega,Sigma,P,P) . A) * (P . P))) + (((Omega,Sigma,P,A3) . A) * (P . A3))) is ext-real V14() real Element of REAL
(Omega,Sigma,P,A) . A3 is ext-real V14() real Element of REAL
(((Omega,Sigma,P,A3) . A) * (P . A3)) / (((((Omega,Sigma,P,B) . A) * (P . B)) + (((Omega,Sigma,P,P) . A) * (P . P))) + (((Omega,Sigma,P,A3) . A) * (P . A3))) is ext-real V14() real Element of REAL
(((Omega,Sigma,P,B) . A) * (P . B)) / (P . A) is ext-real V14() real Element of REAL
(((Omega,Sigma,P,P) . A) * (P . P)) / (P . A) is ext-real V14() real Element of REAL
(((Omega,Sigma,P,A3) . A) * (P . A3)) / (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)
[#] Sigma is Event of Sigma
A is Event of Sigma
([#] Sigma) \ 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
P . B is ext-real V14() real Element of REAL
P . (([#] Sigma) \ A) is ext-real V14() real Element of REAL
(P . (([#] Sigma) \ A)) / (P . B) is ext-real V14() real Element of REAL
1 - ((P . (([#] Sigma) \ A)) / (P . B)) is ext-real V14() real Element of REAL
(Omega,Sigma,P,B) is Relation-like Sigma -defined REAL -valued Function-like V30(Sigma, REAL ) V35() V36() V37() V44() Probability of Sigma
(Omega,Sigma,P,B) . A 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
((P . B) + (P . A)) - 1 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
1 - (P . A) is ext-real V14() real Element of REAL
- (1 - (P . A)) is ext-real V14() real Element of REAL
(P . B) + (- (1 - (P . A))) is ext-real V14() real Element of REAL
- (P . (([#] Sigma) \ A)) is ext-real V14() real Element of REAL
(P . B) + (- (P . (([#] Sigma) \ A))) is ext-real V14() real Element of REAL
((P . B) + (- (P . (([#] Sigma) \ A)))) / (P . B) is ext-real V14() real Element of REAL
(P . (A /\ B)) / (P . B) is ext-real V14() real Element of REAL
(P . B) - (P . (([#] Sigma) \ A)) is ext-real V14() real Element of REAL
((P . B) - (P . (([#] Sigma) \ A))) / (P . B) is ext-real V14() real Element of REAL
(P . B) / (P . B) is ext-real V14() real Element of REAL
((P . B) / (P . B)) - ((P . (([#] Sigma) \ A)) / (P . B)) is ext-real V14() real Element of REAL