:: PROB_4 semantic presentation

REAL is non empty V44() V50() V51() V52() V56() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() Element of bool REAL
bool REAL is non empty V79() set
ExtREAL is non empty V51() set
is non empty V13() V34() set
bool is non empty V79() set
bool ExtREAL is non empty V79() set
COMPLEX is non empty V44() V50() V56() set
RAT is non empty V44() V50() V51() V52() V53() V56() set
INT is non empty V44() V50() V51() V52() V53() V54() V56() set
is non empty V13() V33() V34() V35() set
bool is non empty V79() set
omega is non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() set
bool omega is non empty V79() set
bool () is non empty V79() set
{} is set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
{{},1} is V79() set
bool NAT is non empty V79() set
0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

+infty is non empty V12() ext-real positive non negative Element of ExtREAL
+infty is non empty V12() ext-real positive non negative set
-infty is non empty V12() ext-real non positive negative set
is V51() set
is V51() set
P is set
Sigma is set
Omega is set
Omega \ P is Element of bool Omega
bool Omega is non empty V79() set
Omega \ Sigma is Element of bool Omega
Sigma \ P is Element of bool Sigma
bool Sigma is non empty V79() set
Omega /\ (Sigma \ P) is Element of bool Sigma
(Omega \ Sigma) \/ (Omega /\ (Sigma \ P)) is set
A is set
A is set
Omega is set
bool Omega is non empty V79() set
bool (bool Omega) is non empty V79() set
Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
[:NAT,(bool Omega):] is non empty V13() set
bool [:NAT,(bool Omega):] is non empty V79() set
P is non empty V13() V16( NAT ) V17(Sigma) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
A is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
P . A is set
P . A is Event of Sigma
Omega is set
bool Omega is non empty V79() set
bool (bool Omega) is non empty V79() set
bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
[:NAT,(bool Omega):] is non empty V13() set
bool [:NAT,(bool Omega):] is non empty V79() set
Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
P is non empty V13() V16( NAT ) V17( bool Omega) V17(Sigma) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
rng P is non empty Element of bool (bool Omega)
A is set
B is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
(Omega,Sigma,P,B) is Element of Sigma
Omega is set
bool Omega is non empty V79() set
bool (bool Omega) is non empty V79() set
bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
[:NAT,(bool Omega):] is non empty V13() set
bool [:NAT,(bool Omega):] is non empty V79() set
Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
[:NAT,Sigma:] is non empty V13() set
bool [:NAT,Sigma:] is non empty V79() set
P is V13() Function-like set
A is non empty V13() V16( NAT ) V17( bool Omega) V17(Sigma) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
rng A is non empty Element of bool (bool Omega)
dom A is non empty V50() V51() V52() V53() V54() V55() Element of bool NAT
A is non empty V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
F1() is set
bool F1() is non empty V79() set
bool (bool F1()) is non empty V79() set
F2() is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool F1())
bool F1() is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool F1())
[:NAT,(bool F1()):] is non empty V13() set
bool [:NAT,(bool F1()):] is non empty V79() set
Omega is non empty V13() V16( NAT ) V17( bool F1()) Function-like V23( NAT ) V27( NAT , bool F1()) Element of bool [:NAT,(bool F1()):]
Omega is non empty V13() V16( NAT ) V17( bool F1()) Function-like V23( NAT ) V27( NAT , bool F1()) Element of bool [:NAT,(bool F1()):]

Omega . Sigma is set
F3(Sigma) is Element of F2()
rng Omega is non empty Element of bool (bool F1())
Sigma is non empty V13() V16( NAT ) V17(F2()) V17( bool F1()) Function-like V23( NAT ) V27( NAT , bool F1()) Element of bool [:NAT,(bool F1()):]
P is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
(F1(),F2(),Sigma,P) is Element of F2()
F3(P) is Element of F2()
Omega is set
bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
bool Omega is non empty V79() set
bool (bool Omega) is non empty V79() set
[:NAT,(bool Omega):] is non empty V13() set
bool [:NAT,(bool Omega):] is non empty V79() set
[:NAT,(bool Omega):] is non empty V13() set
bool [:NAT,(bool Omega):] is non empty V79() set
{} Omega is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() V13() non-empty empty-yielding V17( RAT ) ext-real non positive non negative V33() V34() V35() V36() V50() V51() V52() V53() V54() V55() V56() Element of bool Omega
NAT --> ({} Omega) is non empty T-Sequence-like V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) V33() V34() V35() V36() Element of bool [:NAT,(bool Omega):]
Sigma is non empty T-Sequence-like V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) V33() V34() V35() V36() Element of bool [:NAT,(bool Omega):]

Omega is set
bool Omega is non empty V79() set
bool (bool Omega) is non empty V79() set
Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
[:NAT,(bool Omega):] is non empty V13() set
bool [:NAT,(bool Omega):] is non empty V79() set
P is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
[:NAT,P:] is non empty V13() set
bool [:NAT,P:] is non empty V79() set
the non empty V13() V16( NAT ) V17(P) Function-like V23( NAT ) V27( NAT ,P) disjoint_valued Element of bool [:NAT,P:] is non empty V13() V16( NAT ) V17(P) Function-like V23( NAT ) V27( NAT ,P) disjoint_valued Element of bool [:NAT,P:]
B is non empty V13() V16( NAT ) V17(Sigma) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
Omega is set
bool Omega is non empty V79() set
Sigma is Element of bool Omega
P is Element of bool Omega
(Sigma,P) followed_by {} is V13() Function-like set
bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
bool (bool Omega) is non empty V79() set
[:NAT,(bool Omega):] is non empty V13() set
bool [:NAT,(bool Omega):] is non empty V79() set
{} Omega is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() V13() non-empty empty-yielding V17( RAT ) ext-real non positive non negative V33() V34() V35() V36() V50() V51() V52() V53() V54() V55() V56() Element of bool Omega
(Sigma,P) followed_by ({} Omega) is non empty V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
[:NAT,(bool Omega):] is non empty V13() set
bool [:NAT,(bool Omega):] is non empty V79() set
A is non empty V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
(Omega,(bool Omega),A,1) is Element of bool Omega

A . B is set
A . C is set
(Omega,(bool Omega),A,0) is Element of bool Omega
C + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
C + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
B + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
Omega is set
bool Omega is non empty V79() set
bool (bool Omega) is non empty V79() set
bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
[:NAT,(bool Omega):] is non empty V13() set
bool [:NAT,(bool Omega):] is non empty V79() set
Sigma is non empty set
P is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
A is non empty V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
rng A is non empty Element of bool (bool Omega)
Union A is Element of bool Omega
B is non empty V13() V16( NAT ) V17( bool Omega) V17(P) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
Union B is Element of bool Omega
A is non empty V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
rng A is non empty Element of bool (bool Omega)
Union A is Element of bool Omega
B is Element of bool Omega
B ` is Element of bool Omega
Omega \ B is set
P is non empty V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
rng P is non empty Element of bool (bool Omega)
Intersection P is Element of bool Omega
Complement P is non empty V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

() . A is set
P . A is set
B is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
(Omega,(bool Omega),P,B) is Element of bool Omega
(Omega,(bool Omega),P,B) ` is Element of bool Omega
Omega \ (Omega,(bool Omega),P,B) is set
rng () is non empty Element of bool (bool Omega)
Union () is Element of bool Omega
(Union ()) ` is Element of bool Omega
Omega \ (Union ()) is set
Omega is non empty set
bool Omega is non empty V79() set
bool (bool Omega) is non empty V79() set
Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
P is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma
A is Event of Sigma
B is Event of Sigma
A \ B is Element of Sigma
P . (A \ B) is V11() V12() ext-real Element of REAL
A \/ B is Element of Sigma
P . (A \/ B) is V11() V12() ext-real Element of REAL
P . B is V11() V12() ext-real Element of REAL
(P . (A \/ B)) - (P . B) is V11() V12() ext-real Element of REAL
(P . B) + (P . (A \ B)) is V11() V12() ext-real Element of REAL
((P . B) + (P . (A \ B))) - (P . B) is V11() V12() ext-real Element of REAL
Omega is non empty set
bool Omega is non empty V79() set
bool (bool Omega) is non empty V79() set
Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
P is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma
A is Event of Sigma
B is Event of Sigma
P . B is V11() V12() ext-real Element of REAL
P . A is V11() V12() ext-real Element of REAL
Omega is non empty set
bool Omega is non empty V79() set
bool (bool Omega) is non empty V79() set
bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
[:NAT,(bool Omega):] is non empty V13() set
bool [:NAT,(bool Omega):] is non empty V79() set
Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
P is non empty V13() V16( NAT ) V17( bool Omega) V17(Sigma) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
Union P is Element of bool Omega
A is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma
A . () is V11() V12() ext-real set
A * P is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of bool
Partial_Sums (A * P) is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of bool
B is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
(Partial_Sums (A * P)) . B is V11() V12() ext-real Element of REAL
B + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
(Partial_Sums (A * P)) . (B + 1) is V11() V12() ext-real Element of REAL
(A * P) . (B + 1) is V11() V12() ext-real Element of REAL
((Partial_Sums (A * P)) . B) + ((A * P) . (B + 1)) is V11() V12() ext-real Element of REAL
(Omega,Sigma,P,(B + 1)) is Element of Sigma
A . (Omega,Sigma,P,(B + 1)) is V11() V12() ext-real Element of REAL
0 + (A . (Omega,Sigma,P,(B + 1))) is V11() V12() ext-real Element of REAL
(Partial_Sums (A * P)) . 0 is V11() V12() ext-real Element of REAL
(A * P) . 0 is V11() V12() ext-real Element of REAL
(Omega,Sigma,P,0) is Element of Sigma
A . (Omega,Sigma,P,0) is V11() V12() ext-real Element of REAL
B is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
(Partial_Sums (A * P)) . B is V11() V12() ext-real Element of REAL
lim (Partial_Sums (A * P)) is V11() V12() ext-real Element of REAL
Partial_Diff_Union P is non empty V13() V16( NAT ) V17( bool Omega) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) disjoint_valued Element of bool [:NAT,(bool Omega):]
B is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
(Omega,Sigma,,B) is Element of Sigma
(Omega,Sigma,P,B) is Element of Sigma
A * is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of bool
(A * ) . B is V11() V12() ext-real Element of REAL
(A * P) . B is V11() V12() ext-real Element of REAL
Partial_Sums (A * ) is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of bool
B is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
(Partial_Sums (A * )) . B is V11() V12() ext-real Element of REAL
(Partial_Sums (A * P)) . B is V11() V12() ext-real Element of REAL
Sum (A * ) is V11() V12() ext-real Element of REAL
lim (Partial_Sums (A * )) is V11() V12() ext-real Element of REAL
Union is Element of bool Omega
A . () is V11() V12() ext-real set
C is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
(Omega,Sigma,P,C) is Element of Sigma
rng P is non empty Element of bool (bool Omega)
union (rng P) is Element of bool Omega
B is Event of Sigma
B is Event of Sigma
A . (Omega,Sigma,P,C) is V11() V12() ext-real Element of REAL
Omega is non empty set
bool Omega is non empty V79() set
bool (bool Omega) is non empty V79() set
bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
[:NAT,(bool Omega):] is non empty V13() set
bool [:NAT,(bool Omega):] is non empty V79() set
Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
P is non empty V13() V16( NAT ) V17( bool Omega) V17(Sigma) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
rng P is non empty Element of bool (bool Omega)
union (rng P) is Element of bool Omega
A is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma
A . (union (rng P)) is V11() V12() ext-real set
B is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
(Omega,Sigma,P,B) is Element of Sigma
A . (Omega,Sigma,P,B) is V11() V12() ext-real Element of REAL
Union P is Element of bool Omega
A . () is V11() V12() ext-real set
B is set
A . B is V11() V12() ext-real set
C is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
(Omega,Sigma,P,C) is Element of Sigma
Omega is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of bool
Partial_Sums Omega is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of bool
Sigma is non empty V13() V16( NAT ) V17( ExtREAL ) Function-like V23( NAT ) V27( NAT , ExtREAL ) V34() Element of bool
Ser Sigma is non empty V13() V16( NAT ) V17( ExtREAL ) Function-like V23( NAT ) V27( NAT , ExtREAL ) V34() Element of bool
P is non empty V13() V16( NAT ) V17( ExtREAL ) Function-like V23( NAT ) V27( NAT , ExtREAL ) V34() Element of bool
A is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
P . A is ext-real Element of ExtREAL
(Ser Sigma) . A is ext-real Element of ExtREAL
A + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
P . (A + 1) is ext-real Element of ExtREAL
(Ser Sigma) . (A + 1) is ext-real Element of ExtREAL
(Partial_Sums Omega) . A is V11() V12() ext-real Element of REAL
B is V11() V12() ext-real Element of REAL
Omega . (A + 1) is V11() V12() ext-real Element of REAL
B + (Omega . (A + 1)) is V11() V12() ext-real Element of REAL
Sigma . (A + 1) is ext-real Element of ExtREAL
((Ser Sigma) . A) + (Sigma . (A + 1)) is ext-real Element of ExtREAL

Sigma . 0 is ext-real Element of ExtREAL
(Ser Sigma) . 0 is ext-real Element of ExtREAL
Omega is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of bool
upper_bound Omega is V11() V12() ext-real Element of REAL
Sigma is non empty V13() V16( NAT ) V17( ExtREAL ) Function-like V23( NAT ) V27( NAT , ExtREAL ) V34() Element of bool
rng Sigma is non empty V51() Element of bool ExtREAL
sup (rng Sigma) is ext-real set
dom Sigma is non empty V50() V51() V52() V53() V54() V55() Element of bool NAT
-infty is non empty V12() ext-real non positive negative Element of ExtREAL
is V51() set
A is ext-real Element of rng Sigma
B is set
Sigma . B is ext-real set
C is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
Omega . C is V11() V12() ext-real Element of REAL

A is ext-real set
B is set
Sigma . B is ext-real set
A is V11() V12() ext-real Element of REAL
B is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
Omega . B is V11() V12() ext-real Element of REAL
Omega is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of bool
lower_bound Omega is V11() V12() ext-real Element of REAL
Sigma is non empty V13() V16( NAT ) V17( ExtREAL ) Function-like V23( NAT ) V27( NAT , ExtREAL ) V34() Element of bool
rng Sigma is non empty V51() Element of bool ExtREAL
inf (rng Sigma) is ext-real set
dom Sigma is non empty V50() V51() V52() V53() V54() V55() Element of bool NAT
is V51() set
A is ext-real Element of rng Sigma
B is set
Sigma . B is ext-real set
C is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
Omega . C is V11() V12() ext-real Element of REAL

A is ext-real set
B is set
Sigma . B is ext-real set
A is V11() V12() ext-real Element of REAL
B is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
Omega . B is V11() V12() ext-real Element of REAL
Omega is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of bool
Sum Omega is V11() V12() ext-real Element of REAL
Partial_Sums Omega is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of bool
lim (Partial_Sums Omega) is V11() V12() ext-real Element of REAL
Sigma is non empty V13() V16( NAT ) V17( ExtREAL ) Function-like V23( NAT ) V27( NAT , ExtREAL ) V34() Element of bool
SUM Sigma is ext-real Element of ExtREAL
P is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
Omega . P is V11() V12() ext-real Element of REAL
upper_bound (Partial_Sums Omega) is V11() V12() ext-real Element of REAL
Ser Sigma is non empty V13() V16( NAT ) V17( ExtREAL ) Function-like V23( NAT ) V27( NAT , ExtREAL ) V34() Element of bool
rng (Ser Sigma) is non empty V51() Element of bool ExtREAL
sup (rng (Ser Sigma)) is ext-real set
Omega is non empty set
bool Omega is non empty V79() set
bool (bool Omega) is non empty V79() set
Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
[:Sigma,ExtREAL:] is non empty V13() V34() set
bool [:Sigma,ExtREAL:] is non empty V79() set
P is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma
B is non empty V13() V16(Sigma) V17( ExtREAL ) Function-like V23(Sigma) V27(Sigma, ExtREAL ) V34() Element of bool [:Sigma,ExtREAL:]
rng B is non empty V51() Element of bool ExtREAL

dom B is non empty Element of bool Sigma
bool Sigma is non empty V79() set
B is set
B . B is ext-real set
A is Event of Sigma
P . A is V11() V12() ext-real Element of REAL
[:NAT,Sigma:] is non empty V13() set
bool [:NAT,Sigma:] is non empty V79() set
C is non empty V13() V16( NAT ) V17(Sigma) Function-like V23( NAT ) V27( NAT ,Sigma) disjoint_valued Element of bool [:NAT,Sigma:]
B * C is non empty V13() V16( NAT ) V17( ExtREAL ) Function-like V23( NAT ) V27( NAT , ExtREAL ) V34() Element of bool
SUM (B * C) is ext-real Element of ExtREAL
rng C is non empty Element of bool (bool Omega)
union (rng C) is Element of bool Omega
B . (union (rng C)) is ext-real set
bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
[:NAT,(bool Omega):] is non empty V13() set
bool [:NAT,(bool Omega):] is non empty V79() set
B is non empty V13() V16( NAT ) V17(Sigma) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) disjoint_valued Element of bool [:NAT,(bool Omega):]
P * B is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of bool
A is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
(P * B) . A is V11() V12() ext-real Element of REAL
Partial_Sums (P * B) is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of bool
Union B is Element of bool Omega
P . () is V11() V12() ext-real set
Sum (P * B) is V11() V12() ext-real Element of REAL
lim (Partial_Sums (P * B)) is V11() V12() ext-real Element of REAL
Omega is non empty set
bool Omega is non empty V79() set
bool (bool Omega) is non empty V79() set
Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
P is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma
[:Sigma,ExtREAL:] is non empty V13() V34() set
bool [:Sigma,ExtREAL:] is non empty V79() set

Omega is non empty set
bool Omega is non empty V79() set
bool (bool Omega) is non empty V79() set
Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
[:Sigma,ExtREAL:] is non empty V13() V34() set
bool [:Sigma,ExtREAL:] is non empty V79() set
P is non empty V13() V16(Sigma) V17( ExtREAL ) Function-like V23(Sigma) V27(Sigma, ExtREAL ) V34() V42() nonnegative sigma-additive Element of bool [:Sigma,ExtREAL:]
P . Omega is ext-real set
B is Element of Sigma
P . B is ext-real Element of ExtREAL
A is Element of Sigma
P . A is ext-real Element of ExtREAL
A is set
P . A is ext-real set
B is Element of Sigma
P . B is ext-real Element of ExtREAL
dom P is non empty Element of bool Sigma
bool Sigma is non empty V79() set
[:Sigma,REAL:] is non empty V13() V33() V34() V35() set
bool [:Sigma,REAL:] is non empty V79() set
A is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() Element of bool [:Sigma,REAL:]
bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
[:NAT,(bool Omega):] is non empty V13() set
bool [:NAT,(bool Omega):] is non empty V79() set
B is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() Element of bool [:Sigma,REAL:]
C is non empty V13() V16( NAT ) V17(Sigma) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
B * C is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of bool
lim (B * C) is V11() V12() ext-real Element of REAL
Intersection C is Element of bool Omega
B . () is V11() V12() ext-real set
B is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
(B * C) . B is V11() V12() ext-real Element of REAL
(Omega,Sigma,C,B) is Element of Sigma
A is Event of Sigma
B . A is V11() V12() ext-real Element of REAL
dom (B * C) is non empty V50() V51() V52() V53() V54() V55() Element of bool NAT
[:NAT,Sigma:] is non empty V13() set
bool [:NAT,Sigma:] is non empty V79() set
B is non empty V13() V16( NAT ) V17(Sigma) Function-like V23( NAT ) V27( NAT ,Sigma) Element of bool [:NAT,Sigma:]
A is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
A + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
B . (A + 1) is Element of Sigma
B . A is Element of Sigma
B . 0 is Element of Sigma
P . (B . 0) is ext-real Element of ExtREAL
P * B is non empty V13() V16( NAT ) V17( ExtREAL ) Function-like V23( NAT ) V27( NAT , ExtREAL ) V34() Element of bool
dom (P * B) is non empty V50() V51() V52() V53() V54() V55() Element of bool NAT
A is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
(P * B) . A is ext-real Element of ExtREAL
B . A is Element of Sigma
P . (B . A) is ext-real Element of ExtREAL
A + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
(P * B) . (A + 1) is ext-real Element of ExtREAL
B . (A + 1) is Element of Sigma
P . (B . (A + 1)) is ext-real Element of ExtREAL
(B * C) . (A + 1) is V11() V12() ext-real Element of REAL
(B * C) . A is V11() V12() ext-real Element of REAL
lower_bound (B * C) is V11() V12() ext-real Element of REAL
rng (P * B) is non empty V51() Element of bool ExtREAL
inf (rng (P * B)) is ext-real set
rng B is non empty Element of bool (bool Omega)
meet (rng B) is Element of bool Omega
P . (meet (rng B)) is ext-real set
C is Event of Sigma
B is Event of Sigma
C \/ B is Element of Sigma
B . (C \/ B) is V11() V12() ext-real Element of REAL
B . C is V11() V12() ext-real Element of REAL
B . B is V11() V12() ext-real Element of REAL
(B . C) + (B . B) is V11() V12() ext-real Element of REAL
A is Element of Sigma
B is Element of Sigma
A \/ B is Element of Sigma
B . (A \/ B) is V11() V12() ext-real Element of REAL
O is Element of Sigma
P . O is ext-real Element of ExtREAL
B2 is Element of Sigma
P . B2 is ext-real Element of ExtREAL
(P . O) + (P . B2) is ext-real Element of ExtREAL
B . A is V11() V12() ext-real Element of REAL
B . B is V11() V12() ext-real Element of REAL
(B . A) + (B . B) is V11() V12() ext-real Element of REAL
B . Omega is V11() V12() ext-real set
C is Event of Sigma
B . C is V11() V12() ext-real Element of REAL
Omega is non empty set
bool Omega is non empty V79() set
bool (bool Omega) is non empty V79() set
Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
[:Sigma,ExtREAL:] is non empty V13() V34() set
bool [:Sigma,ExtREAL:] is non empty V79() set
P is non empty V13() V16(Sigma) V17( ExtREAL ) Function-like V23(Sigma) V27(Sigma, ExtREAL ) V34() V42() nonnegative sigma-additive Element of bool [:Sigma,ExtREAL:]
P . Omega is ext-real set
Omega is set
bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
bool Omega is non empty V79() set
bool (bool Omega) is non empty V79() set
[:NAT,(bool Omega):] is non empty V13() set
bool [:NAT,(bool Omega):] is non empty V79() set
Sigma is non empty V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
Partial_Union Sigma is non empty V13() V16( NAT ) V17( bool Omega) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
P is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
(Omega,(bool Omega),(Partial_Union Sigma),P) is Element of bool Omega
(Omega,(bool Omega),Sigma,P) is Element of bool Omega
P + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
(Omega,(bool Omega),(Partial_Union Sigma),(P + 1)) is Element of bool Omega
(Omega,(bool Omega),Sigma,(P + 1)) is Element of bool Omega
(Omega,(bool Omega),Sigma,P) \/ (Omega,(bool Omega),Sigma,(P + 1)) is Element of bool Omega
(Omega,(bool Omega),(Partial_Union Sigma),0) is Element of bool Omega
(Omega,(bool Omega),Sigma,0) is Element of bool Omega
Omega is set
bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
bool Omega is non empty V79() set
bool (bool Omega) is non empty V79() set
[:NAT,(bool Omega):] is non empty V13() set
bool [:NAT,(bool Omega):] is non empty V79() set
Sigma is non empty V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
Partial_Union Sigma is non empty V13() V16( NAT ) V17( bool Omega) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
P is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
(Omega,(bool Omega),(Partial_Union Sigma),P) is Element of bool Omega
(Omega,(bool Omega),Sigma,P) is Element of bool Omega
Omega is set
bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
bool Omega is non empty V79() set
bool (bool Omega) is non empty V79() set
[:NAT,(bool Omega):] is non empty V13() set
bool [:NAT,(bool Omega):] is non empty V79() set
Sigma is non empty V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
Partial_Diff_Union Sigma is non empty V13() V16( NAT ) V17( bool Omega) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) disjoint_valued Element of bool [:NAT,(bool Omega):]
(Omega,(bool Omega),(Partial_Diff_Union Sigma),0) is Element of bool Omega
(Omega,(bool Omega),Sigma,0) is Element of bool Omega
P is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
P + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
(Omega,(bool Omega),(Partial_Diff_Union Sigma),(P + 1)) is Element of bool Omega
(Omega,(bool Omega),Sigma,(P + 1)) is Element of bool Omega
(Omega,(bool Omega),Sigma,P) is Element of bool Omega
(Omega,(bool Omega),Sigma,(P + 1)) \ (Omega,(bool Omega),Sigma,P) is Element of bool Omega
Partial_Union Sigma is non empty V13() V16( NAT ) V17( bool Omega) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
(Omega,(bool Omega),(Partial_Union Sigma),P) is Element of bool Omega
(Omega,(bool Omega),Sigma,(P + 1)) \ (Omega,(bool Omega),(Partial_Union Sigma),P) is Element of bool Omega
Omega is set
bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
bool Omega is non empty V79() set
bool (bool Omega) is non empty V79() set
[:NAT,(bool Omega):] is non empty V13() set
bool [:NAT,(bool Omega):] is non empty V79() set
Sigma is non empty V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
Partial_Diff_Union Sigma is non empty V13() V16( NAT ) V17( bool Omega) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) disjoint_valued Element of bool [:NAT,(bool Omega):]
P is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
P + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
(Omega,(bool Omega),Sigma,(P + 1)) is Element of bool Omega
(Omega,(bool Omega),(Partial_Diff_Union Sigma),(P + 1)) is Element of bool Omega
(Omega,(bool Omega),Sigma,P) is Element of bool Omega
(Omega,(bool Omega),(Partial_Diff_Union Sigma),(P + 1)) \/ (Omega,(bool Omega),Sigma,P) is Element of bool Omega
Partial_Union Sigma is non empty V13() V16( NAT ) V17( bool Omega) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
(Omega,(bool Omega),(Partial_Union Sigma),P) is Element of bool Omega
(Omega,(bool Omega),Sigma,(P + 1)) \ (Omega,(bool Omega),(Partial_Union Sigma),P) is Element of bool Omega
((Omega,(bool Omega),Sigma,(P + 1)) \ (Omega,(bool Omega),(Partial_Union Sigma),P)) \/ (Omega,(bool Omega),Sigma,P) is Element of bool Omega
(Omega,(bool Omega),Sigma,(P + 1)) \ (Omega,(bool Omega),Sigma,P) is Element of bool Omega
((Omega,(bool Omega),Sigma,(P + 1)) \ (Omega,(bool Omega),Sigma,P)) \/ (Omega,(bool Omega),Sigma,P) is Element of bool Omega
(Omega,(bool Omega),Sigma,(P + 1)) \/ (Omega,(bool Omega),Sigma,P) is Element of bool Omega
Omega is set
bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
bool Omega is non empty V79() set
bool (bool Omega) is non empty V79() set
[:NAT,(bool Omega):] is non empty V13() set
bool [:NAT,(bool Omega):] is non empty V79() set
Sigma is non empty V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
Partial_Diff_Union Sigma is non empty V13() V16( NAT ) V17( bool Omega) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) disjoint_valued Element of bool [:NAT,(bool Omega):]
P is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
P + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
(Omega,(bool Omega),(Partial_Diff_Union Sigma),(P + 1)) is Element of bool Omega
(Omega,(bool Omega),Sigma,P) is Element of bool Omega
(Omega,(bool Omega),Sigma,(P + 1)) is Element of bool Omega
(Omega,(bool Omega),Sigma,(P + 1)) \ (Omega,(bool Omega),Sigma,P) is Element of bool Omega
Omega is set
bool Omega is non empty V79() set
bool (bool Omega) is non empty V79() set
Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
[:NAT,(bool Omega):] is non empty V13() set
bool [:NAT,(bool Omega):] is non empty V79() set
P is non empty V13() V16( NAT ) V17(Sigma) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
Partial_Union P is non empty V13() V16( NAT ) V17(Sigma) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
Omega is set
bool Omega is non empty V79() set
bool (bool Omega) is non empty V79() set
Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
[:NAT,(bool Omega):] is non empty V13() set
bool [:NAT,(bool Omega):] is non empty V79() set
P is non empty V13() V16( NAT ) V17(Sigma) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
Partial_Diff_Union P is non empty V13() V16( NAT ) V17(Sigma) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) disjoint_valued Element of bool [:NAT,(bool Omega):]
(Omega,Sigma,,0) is Element of Sigma
(Omega,Sigma,P,0) is Element of Sigma
A is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
A + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
(Omega,Sigma,,(A + 1)) is Element of Sigma
(Omega,Sigma,P,(A + 1)) is Element of Sigma
(Omega,Sigma,P,A) is Element of Sigma
(Omega,Sigma,P,(A + 1)) \ (Omega,Sigma,P,A) is Element of Sigma
Omega is set
bool Omega is non empty V79() set
bool (bool Omega) is non empty V79() set
Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
[:NAT,(bool Omega):] is non empty V13() set
bool [:NAT,(bool Omega):] is non empty V79() set
P is non empty V13() V16( NAT ) V17(Sigma) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
Partial_Diff_Union P is non empty V13() V16( NAT ) V17(Sigma) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) disjoint_valued Element of bool [:NAT,(bool Omega):]
A is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
A + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
(Omega,Sigma,,(A + 1)) is Element of Sigma
(Omega,Sigma,P,A) is Element of Sigma
Omega is non empty set
bool Omega is non empty V79() set
bool (bool Omega) is non empty V79() set
Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
Omega is non empty set
bool Omega is non empty V79() set
bool (bool Omega) is non empty V79() set
Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
P is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma
(Omega,Sigma,P) is non empty V13() V16(Sigma) V17( ExtREAL ) Function-like V23(Sigma) V27(Sigma, ExtREAL ) V34() V42() nonnegative sigma-additive Element of bool [:Sigma,ExtREAL:]
[:Sigma,ExtREAL:] is non empty V13() V34() set
bool [:Sigma,ExtREAL:] is non empty V79() set
B is set
A is Element of bool Omega
(Omega,Sigma,P) . B is ext-real set
B is set
A is Element of bool Omega
P . B is V11() V12() ext-real set
Omega is non empty set
bool Omega is non empty V79() set
bool (bool Omega) is non empty V79() set
Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
P is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma
A is Element of bool Omega
B is set
P . B is V11() V12() ext-real set
Omega is non empty set
bool Omega is non empty V79() set
bool (bool Omega) is non empty V79() set
Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
P is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma
(Omega,Sigma,P) is non empty V13() V16(Sigma) V17( ExtREAL ) Function-like V23(Sigma) V27(Sigma, ExtREAL ) V34() V42() nonnegative sigma-additive Element of bool [:Sigma,ExtREAL:]
[:Sigma,ExtREAL:] is non empty V13() V34() set
bool [:Sigma,ExtREAL:] is non empty V79() set
A is Element of bool Omega
B is set
P . B is V11() V12() ext-real set
B is set
(Omega,Sigma,P) . B is ext-real set
Omega is non empty set
bool Omega is non empty V79() set
bool (bool Omega) is non empty V79() set
Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
P is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma
P . {} is V11() V12() ext-real set
Omega is non empty set
bool Omega is non empty V79() set
bool (bool Omega) is non empty V79() set
Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
P is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma
A is set
B is set
P . A is V11() V12() ext-real set
P . B is V11() V12() ext-real set
C is (Omega,Sigma,P)
A \/ C is set
B is (Omega,Sigma,P)
B \/ B is set
A is set
P . A is V11() V12() ext-real set
A \/ A is set
B is set
P . B is V11() V12() ext-real set
B \/ B is set
O is Event of Sigma
D2 is Event of Sigma
O \/ D2 is Element of Sigma
P . (O \/ D2) is V11() V12() ext-real Element of REAL
P . O is V11() V12() ext-real Element of REAL
P . D2 is V11() V12() ext-real Element of REAL
(P . O) + (P . D2) is V11() V12() ext-real Element of REAL
B2 is Event of Sigma
P . B2 is V11() V12() ext-real Element of REAL
c13 is Event of Sigma
B2 \/ c13 is Element of Sigma
P . (B2 \/ c13) is V11() V12() ext-real Element of REAL
P . c13 is V11() V12() ext-real Element of REAL
(P . B2) + (P . c13) is V11() V12() ext-real Element of REAL
Omega is non empty set
bool Omega is non empty V79() set
bool (bool Omega) is non empty V79() set
Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
P is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma
A is set
B is set
C is (Omega,Sigma,P)
B \/ C is set
A is set
B is set
C is set
C is set
B is (Omega,Sigma,P)
C \/ B is set
C is set
B is set
A is (Omega,Sigma,P)
B \/ A is set
C is set
B is (Omega,Sigma,P)
C \/ B is set
B is set
B is non empty Element of bool (bool Omega)
C is set
A is set
B is set
B is (Omega,Sigma,P)
A \/ B is set
A is non empty Element of bool (bool Omega)
B is non empty Element of bool (bool Omega)
C is set
B is set
A is (Omega,Sigma,P)
B \/ A is set
B is set
A is (Omega,Sigma,P)
B \/ A is set
Omega is non empty set
bool Omega is non empty V79() set
bool (bool Omega) is non empty V79() set
Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
P is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma
(Omega,Sigma,P) is non empty Element of bool (bool Omega)
A is (Omega,Sigma,P)
B is Element of Sigma
B \/ A is Element of bool Omega
Omega is non empty set
bool Omega is non empty V79() set
bool (bool Omega) is non empty V79() set
Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
P is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma
(Omega,Sigma,P) is non empty Element of bool (bool Omega)
(Omega,Sigma,P) is non empty V13() V16(Sigma) V17( ExtREAL ) Function-like V23(Sigma) V27(Sigma, ExtREAL ) V34() V42() nonnegative sigma-additive Element of bool [:Sigma,ExtREAL:]
[:Sigma,ExtREAL:] is non empty V13() V34() set
bool [:Sigma,ExtREAL:] is non empty V79() set
COM (Sigma,(Omega,Sigma,P)) is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
A is set
B is set
C is thin of (Omega,Sigma,P)
B \/ C is set
C is thin of (Omega,Sigma,P)
B \/ C is set
B is (Omega,Sigma,P)
B \/ B is set
A is set
B is set
C is (Omega,Sigma,P)
B \/ C is set
C is (Omega,Sigma,P)
B \/ C is set
B is thin of (Omega,Sigma,P)
B \/ B is set
Omega is non empty set
bool Omega is non empty V79() set
bool (bool Omega) is non empty V79() set
Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
P is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma
(Omega,Sigma,P) is non empty Element of bool (bool Omega)
A is Element of (Omega,Sigma,P)
(Omega,Sigma,P) is non empty V13() V16(Sigma) V17( ExtREAL ) Function-like V23(Sigma) V27(Sigma, ExtREAL ) V34() V42() nonnegative sigma-additive Element of bool [:Sigma,ExtREAL:]
[:Sigma,ExtREAL:] is non empty V13() V34() set
bool [:Sigma,ExtREAL:] is non empty V79() set
COM (Sigma,(Omega,Sigma,P)) is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
Omega is non empty set
bool Omega is non empty V79() set
bool (bool Omega) is non empty V79() set
Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
P is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma
(Omega,Sigma,P) is non empty Element of bool (bool Omega)
B is set
A is (Omega,Sigma,P)
B \/ A is set
Omega is non empty set
bool Omega is non empty V79() set
bool (bool Omega) is non empty V79() set
Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
P is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma
(Omega,Sigma,P) is non empty Element of bool (bool Omega)
A is Element of (Omega,Sigma,P)
B is set
C is set
A \ C is Element of bool Omega
B is set
A \ B is Element of bool Omega
C is set
C is set
B is (Omega,Sigma,P)
C \/ B is set
B is (Omega,Sigma,P)
C \/ B is set
A is set
P . A is V11() V12() ext-real set
A \ C is Element of bool Omega
B \ C is Element of bool Omega
C is non empty Element of bool (bool Omega)
B is set
A \ B is Element of bool Omega
A is set
A \ A is Element of bool Omega
B is non empty Element of bool (bool Omega)
C is non empty Element of bool (bool Omega)
B is set
A \ B is Element of bool Omega
A \ B is Element of bool Omega
Omega is non empty set
bool Omega is non empty V79() set
bool (bool Omega) is non empty V79() set
Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
P is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma
(Omega,Sigma,P) is non empty Element of bool (bool Omega)
(Omega,Sigma,P) is non empty V13() V16(Sigma) V17( ExtREAL ) Function-like V23(Sigma) V27(Sigma, ExtREAL ) V34() V42() nonnegative sigma-additive Element of bool [:Sigma,ExtREAL:]
[:Sigma,ExtREAL:] is non empty V13() V34() set
bool [:Sigma,ExtREAL:] is non empty V79() set
A is Element of (Omega,Sigma,P)
(Omega,Sigma,P,A) is non empty Element of bool (bool Omega)
(Omega,Sigma,P,A) is Element of COM (Sigma,(Omega,Sigma,P))
COM (Sigma,(Omega,Sigma,P)) is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
MeasPart (Omega,Sigma,P,A) is non empty Element of bool (bool Omega)
B is set
(Omega,Sigma,P,A) \ B is Element of bool Omega
A \ B is Element of bool Omega
B is set
A \ B is Element of bool Omega
(Omega,Sigma,P,A) \ B is Element of bool Omega
Omega is non empty set
bool Omega is non empty V79() set
bool (bool Omega) is non empty V79() set
Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
P is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma
(Omega,Sigma,P) is non empty Element of bool (bool Omega)
A is Element of (Omega,Sigma,P)
(Omega,Sigma,P,A) is non empty Element of bool (bool Omega)
B is set
C is set
P . B is V11() V12() ext-real set
P . C is V11() V12() ext-real set
A \ B is Element of bool Omega
A \ C is Element of bool Omega
B is (Omega,Sigma,P)
B \/ B is set
A is (Omega,Sigma,P)
C \/ A is set
Omega is non empty set
bool Omega is non empty V79() set
bool (bool Omega) is non empty V79() set
bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
[:NAT,(bool Omega):] is non empty V13() set
bool [:NAT,(bool Omega):] is non empty V79() set
Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
P is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma
(Omega,Sigma,P) is non empty Element of bool (bool Omega)
[:NAT,(Omega,Sigma,P):] is non empty V13() set
bool [:NAT,(Omega,Sigma,P):] is non empty V79() set
A is non empty V13() V16( NAT ) V17((Omega,Sigma,P)) Function-like V23( NAT ) V27( NAT ,(Omega,Sigma,P)) Element of bool [:NAT,(Omega,Sigma,P):]
B is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
A . B is Element of (Omega,Sigma,P)
(Omega,Sigma,P,(A . B)) is non empty Element of bool (bool Omega)
the Element of (Omega,Sigma,P,(A . B)) is Element of (Omega,Sigma,P,(A . B))
B is Element of Sigma
A is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
B is set
A . A is Element of (Omega,Sigma,P)
(Omega,Sigma,P,(A . A)) is non empty Element of bool (bool Omega)
[:NAT,Sigma:] is non empty V13() set
bool [:NAT,Sigma:] is non empty V79() set
B is non empty V13() V16( NAT ) V17(Sigma) Function-like V23( NAT ) V27( NAT ,Sigma) Element of bool [:NAT,Sigma:]
B is non empty V13() V16( NAT ) V17(Sigma) Function-like V23( NAT ) V27( NAT ,Sigma) Element of bool [:NAT,Sigma:]
C is non empty V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
B is non empty V13() V16( NAT ) V17( bool Omega) V17(Sigma) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
A is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
(Omega,Sigma,B,A) is Element of Sigma
A . A is Element of (Omega,Sigma,P)
(Omega,Sigma,P,(A . A)) is non empty Element of bool (bool Omega)
Omega is non empty set
bool Omega is non empty V79() set
bool (bool Omega) is non empty V79() set
bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
[:NAT,(bool Omega):] is non empty V13() set
bool [:NAT,(bool Omega):] is non empty V79() set
Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
P is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma
(Omega,Sigma,P) is non empty Element of bool (bool Omega)
[:NAT,(Omega,Sigma,P):] is non empty V13() set
bool [:NAT,(Omega,Sigma,P):] is non empty V79() set
A is non empty V13() V16( NAT ) V17((Omega,Sigma,P)) Function-like V23( NAT ) V27( NAT ,(Omega,Sigma,P)) Element of bool [:NAT,(Omega,Sigma,P):]
B is non empty V13() V16( NAT ) V17( bool Omega) V17(Sigma) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
C is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
A . C is Element of (Omega,Sigma,P)
(Omega,Sigma,B,C) is Element of Sigma
(A . C) \ (Omega,Sigma,B,C) is Element of bool (A . C)
bool (A . C) is non empty V79() set
B is Element of bool Omega
A is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
B is set
A . A is Element of (Omega,Sigma,P)
(Omega,Sigma,B,A) is Element of Sigma
(A . A) \ (Omega,Sigma,B,A) is Element of bool (A . A)
bool (A . A) is non empty V79() set
[:NAT,(bool Omega):] is non empty V13() set
bool [:NAT,(bool Omega):] is non empty V79() set
C is non empty V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
C is non empty V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
B is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
(Omega,(bool Omega),C,B) is Element of bool Omega
A . B is Element of (Omega,Sigma,P)
(Omega,Sigma,B,B) is Element of Sigma
(A . B) \ (Omega,Sigma,B,B) is Element of bool (A . B)
bool (A . B) is non empty V79() set
Omega is non empty set
bool Omega is non empty V79() set
bool (bool Omega) is non empty V79() set
bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
[:NAT,(bool Omega):] is non empty V13() set
bool [:NAT,(bool Omega):] is non empty V79() set
Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
P is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma
A is non empty V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
B is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
(Omega,(bool Omega),A,B) is Element of bool Omega
C is set
P . C is V11() V12() ext-real set
B is Element of Sigma
A is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
B is set
(Omega,(bool Omega),A,A) is Element of bool Omega
P . B is V11() V12() ext-real set
[:NAT,Sigma:] is non empty V13() set
bool [:NAT,Sigma:] is non empty V79() set
B is non empty V13() V16( NAT ) V17(Sigma) Function-like V23( NAT ) V27( NAT ,Sigma) Element of bool [:NAT,Sigma:]
B is non empty V13() V16( NAT ) V17(Sigma) Function-like V23( NAT ) V27( NAT ,Sigma) Element of bool [:NAT,Sigma:]
C is non empty V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
B is non empty V13() V16( NAT ) V17( bool Omega) V17(Sigma) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
A is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
(Omega,(bool Omega),A,A) is Element of bool Omega
(Omega,Sigma,B,A) is Element of Sigma
B is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
(Omega,Sigma,B,B) is Element of Sigma
P . (Omega,Sigma,B,B) is V11() V12() ext-real Element of REAL
Omega is non empty set
bool Omega is non empty V79() set
bool (bool Omega) is non empty V79() set
Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
P is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma
A is non empty Element of bool (bool Omega)
bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
[:NAT,(bool Omega):] is non empty V13() set
bool [:NAT,(bool Omega):] is non empty V79() set
B is non empty V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
rng B is non empty Element of bool (bool Omega)
Union B is Element of bool Omega
[:NAT,(bool Omega):] is non empty V13() set
bool [:NAT,(bool Omega):] is non empty V79() set
C is non empty V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
dom C is non empty V50() V51() V52() V53() V54() V55() Element of bool NAT
B is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
C . B is Element of bool Omega
rng C is non empty Element of bool (bool Omega)
(Omega,Sigma,P) is non empty Element of bool (bool Omega)
B is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
C . B is Element of bool Omega
A is set
B is (Omega,Sigma,P)
A \/ B is set
B is set
C . B is set
[:NAT,(Omega,Sigma,P):] is non empty V13() set
bool [:NAT,(Omega,Sigma,P):] is non empty V79() set
B is non empty V13() V16( NAT ) V17((Omega,Sigma,P)) Function-like V23( NAT ) V27( NAT ,(Omega,Sigma,P)) Element of bool [:NAT,(Omega,Sigma,P):]
A is non empty V13() V16( NAT ) V17(Sigma) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
B is non empty V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
O is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
(Omega,Sigma,A,O) is Element of Sigma
B . O is Element of (Omega,Sigma,P)
(B . O) \ (Omega,Sigma,A,O) is Element of bool (B . O)
bool (B . O) is non empty V79() set
(Omega,Sigma,P,(B . O)) is non empty