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

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

c

n is Event of P

n1 is Event of P

n /\ n1 is Event of P

c

c

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