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
[:NAT,ExtREAL:] is non empty V13() V34() set
bool [:NAT,ExtREAL:] 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
[:NAT,REAL:] is non empty V13() V33() V34() V35() set
bool [:NAT,REAL:] 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 (bool REAL) is non empty V79() set
{} is set
the 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() set 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() 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
0. is ext-real Element of ExtREAL
+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
{-infty} is V51() set
{+infty} 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()):]
Sigma is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative set
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):]
P is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative set
A is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative set
Sigma . P is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative set
Sigma . A is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative 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 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
B is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative set
C is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative set
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 epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative set
(Complement P) . 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 (Complement P) is non empty Element of bool (bool Omega)
Union (Complement P) is Element of bool Omega
(Union (Complement P)) ` is Element of bool Omega
Omega \ (Union (Complement P)) 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 . (Union P) 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 [:NAT,REAL:]
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 [:NAT,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
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,(Partial_Diff_Union P),B) is Element of Sigma
(Omega,Sigma,P,B) is Element of Sigma
A * (Partial_Diff_Union P) is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(A * (Partial_Diff_Union P)) . B is V11() V12() ext-real Element of REAL
(A * P) . B is V11() V12() ext-real Element of REAL
Partial_Sums (A * (Partial_Diff_Union P)) is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,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 * (Partial_Diff_Union P))) . B is V11() V12() ext-real Element of REAL
(Partial_Sums (A * P)) . B is V11() V12() ext-real Element of REAL
Sum (A * (Partial_Diff_Union P)) is V11() V12() ext-real Element of REAL
lim (Partial_Sums (A * (Partial_Diff_Union P))) is V11() V12() ext-real Element of REAL
Union (Partial_Diff_Union P) is Element of bool Omega
A . (Union (Partial_Diff_Union P)) 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 . (Union P) 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 [:NAT,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 [:NAT,REAL:]
Sigma is non empty V13() V16( NAT ) V17( ExtREAL ) Function-like V23( NAT ) V27( NAT , ExtREAL ) V34() Element of bool [:NAT,ExtREAL:]
Ser Sigma is non empty V13() V16( NAT ) V17( ExtREAL ) Function-like V23( NAT ) V27( NAT , ExtREAL ) V34() Element of bool [:NAT,ExtREAL:]
P is non empty V13() V16( NAT ) V17( ExtREAL ) Function-like V23( NAT ) V27( NAT , ExtREAL ) V34() Element of bool [:NAT,ExtREAL:]
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
P . 0 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 [:NAT,REAL:]
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 [:NAT,ExtREAL:]
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
{-infty} 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
P is ext-real Element of ExtREAL
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 [:NAT,REAL:]
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 [:NAT,ExtREAL:]
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
{+infty} 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
P is ext-real Element of ExtREAL
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 [:NAT,REAL:]
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 [:NAT,REAL:]
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 [:NAT,ExtREAL:]
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 [:NAT,ExtREAL:]
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
C is ext-real Element of 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 [:NAT,ExtREAL:]
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 [:NAT,REAL:]
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 [:NAT,REAL:]
Union B is Element of bool Omega
P . (Union B) 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
R_EAL 1 is ext-real Element of ExtREAL
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 [:NAT,REAL:]
lim (B * C) is V11() V12() ext-real Element of REAL
Intersection C is Element of bool Omega
B . (Intersection C) 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 [:NAT,ExtREAL:]
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,(Partial_Diff_Union P),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,(Partial_Diff_Union P),(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,(Partial_Diff_Union P),(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 Element of bool (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,(bool Omega),B,O) is Element of bool Omega
B . O is Element of (Omega,Sigma,P)
(Omega,Sigma,A,O) is Element of Sigma
(B . O) \ (Omega,Sigma,A,O) is Element of bool (B . O)
bool (B . O) is non empty V79() set
O 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):]
union (rng B) is Element of bool Omega
rng A is non empty Element of bool (bool Omega)
union (rng A) is Element of bool Omega
rng B is non empty Element of bool (Omega,Sigma,P)
bool (Omega,Sigma,P) is non empty V79() set
union (rng B) is set
D2 is set
c13 is set
dom A is non empty V50() V51() V52() V53() V54() V55() Element of bool NAT
k is set
A . k is set
x 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 . x is Element of (Omega,Sigma,P)
(Omega,Sigma,A,x) is Element of Sigma
n is set
(Union B) \ (union (rng A)) is Element of bool Omega
Union O is Element of bool Omega
rng O is non empty Element of bool (bool Omega)
union (rng O) is Element of bool Omega
rng B is non empty Element of bool (bool Omega)
union (rng B) is Element of bool Omega
c13 is set
k is set
x is set
B . x is 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,A,C) is Element of Sigma
dom A is non empty V50() V51() V52() V53() V54() V55() Element of bool NAT
B . C is Element of (Omega,Sigma,P)
(B . C) \ (Omega,Sigma,A,C) is Element of bool (B . C)
bool (B . C) is non empty V79() set
(Omega,(bool Omega),B,C) is Element of bool Omega
dom B is non empty V50() V51() V52() V53() V54() V55() Element of bool NAT
n is set
c13 is set
P . c13 is V11() V12() ext-real set
dom O is non empty V50() V51() V52() V53() V54() V55() Element of bool NAT
k is set
O . k is set
P . (union (rng O)) is V11() V12() ext-real set
c13 is set
k is set
dom B is non empty V50() V51() V52() V53() V54() V55() Element of bool NAT
x is set
B . x is 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
dom O is non empty V50() V51() V52() V53() V54() V55() Element of bool NAT
(Omega,Sigma,O,C) is Element of Sigma
(Omega,(bool Omega),B,C) is Element of bool Omega
(union (rng B)) /\ (union (rng A)) is Element of bool Omega
((Union B) \ (union (rng A))) \/ ((union (rng B)) /\ (union (rng A))) is Element of bool Omega
(union (rng A)) \/ ((Union B) \ (union (rng A))) is Element of bool Omega
c13 is (Omega,Sigma,P)
(union (rng A)) \/ c13 is Element of bool Omega
Union A is Element of bool Omega
D2 is (Omega,Sigma,P)
(union (rng A)) \/ D2 is Element of bool Omega
B2 is set
D2 is (Omega,Sigma,P)
B2 \/ D2 is set
B is Element of bool Omega
B ` is Element of bool Omega
Omega \ B is set
Omega \ B is Element of bool Omega
C is set
B is (Omega,Sigma,P)
C \/ B is set
B is (Omega,Sigma,P)
C \/ B is set
A is Element of bool Omega
Omega \ A is Element of bool Omega
O is set
P . O is V11() V12() ext-real set
(Omega \ A) \ O is Element of bool Omega
(Omega \ A) \ B is Element of bool Omega
O \ B is Element of bool O
bool O is non empty V79() set
(Omega \ A) /\ (O \ B) is Element of bool O
c13 is Element of bool Omega
k is (Omega,Sigma,P)
((Omega \ A) \ O) \/ k is Element of bool Omega
A ` is Element of bool Omega
Omega \ A is set
D2 is (Omega,Sigma,P)
((Omega \ A) \ O) \/ D2 is Element of bool Omega
C is set
B is (Omega,Sigma,P)
C \/ 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 set
C is set
B is set
B is (Omega,Sigma,P)
C \/ 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 compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
A is (Omega,Sigma,P)
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 compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
A is set
B is set
C is (Omega,Sigma,P)
B \/ C is set
C is (Omega,Sigma,P)
B \/ C is set
A is set
P . A is V11() V12() ext-real set
B is Event of Sigma
B is Event of Sigma
B \/ B is Element of Sigma
P . (B \/ B) is V11() V12() ext-real Element of REAL
P . B is V11() V12() ext-real Element of REAL
P . B is V11() V12() ext-real Element of REAL
(P . B) + (P . B) is V11() V12() ext-real Element of REAL
O is Event of Sigma
O \ B is Element of Sigma
P . (O \ B) is V11() V12() ext-real Element of REAL
B \ B is Element of Sigma
P . (B \ B) is V11() V12() ext-real Element of REAL
(P . (B \/ B)) - (P . B) is V11() V12() ext-real Element of REAL
B2 is (Omega,Sigma,P)
B \/ B2 is set
B is set
C is set
C \ B is Element of bool C
bool C is non empty V79() set
P . (C \ B) is V11() V12() ext-real set
A is Element of Sigma
A \ A is Element of bool A
bool A is non empty V79() set
B is Element of Sigma
B \ A is Element of Sigma
O is Element of Sigma
B2 is set
A \/ (A \ 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 compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
A is non empty Element of bool (bool Omega)
B is set
C is set
B is set
B \ C is Element of bool B
bool B is non empty V79() set
P . (B \ C) is V11() V12() ext-real set
C is set
B is set
B \ C is Element of bool B
bool B is non empty V79() set
P . (B \ C) 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 compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
C is set
B is set
P . B is V11() V12() ext-real set
A is set
B is set
O is set
B2 is (Omega,Sigma,P)
O \/ B2 is set
P . O is V11() V12() ext-real set
D2 is (Omega,Sigma,P)
B \/ D2 is set
[:(Omega,Sigma,P),REAL:] is non empty V13() V33() V34() V35() set
bool [:(Omega,Sigma,P),REAL:] is non empty V79() set
C is non empty V13() V16((Omega,Sigma,P)) V17( REAL ) Function-like V23((Omega,Sigma,P)) V27((Omega,Sigma,P), REAL ) V33() V34() V35() Element of bool [:(Omega,Sigma,P),REAL:]
B is set
P . B is V11() V12() ext-real set
A is (Omega,Sigma,P)
B \/ A is set
C . (B \/ A) is V11() V12() 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((Omega,Sigma,P)) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
C * B is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Sum (C * B) is V11() V12() ext-real Element of REAL
Partial_Sums (C * B) is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
lim (Partial_Sums (C * B)) is V11() V12() ext-real Element of REAL
Union B is Element of bool Omega
C . (Union B) is V11() V12() ext-real set
[: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):]
rng A 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
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):]
O 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):]
rng O is non empty Element of bool (bool Omega)
union (rng O) is Element of bool Omega
B2 is set
Union O is Element of bool Omega
c13 is non empty V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
k 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,O,k) is Element of Sigma
B . k is Element of (Omega,Sigma,P)
(B . k) \ (Omega,Sigma,O,k) is Element of bool (B . k)
bool (B . k) is non empty V79() set
(Omega,Sigma,P,(B . k)) is non empty Element of bool (bool Omega)
k 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),c13,k) is Element of bool Omega
B . k is Element of (Omega,Sigma,P)
(Omega,Sigma,O,k) is Element of Sigma
(B . k) \ (Omega,Sigma,O,k) is Element of bool (B . k)
bool (B . k) is non empty V79() set
k 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):]
dom B is non empty V50() V51() V52() V53() V54() V55() Element of bool NAT
D2 is Element of Sigma
rng B is non empty Element of bool (bool Omega)
union (rng B) is Element of bool Omega
x is set
C is set
dom O is non empty V50() V51() V52() V53() V54() V55() Element of bool NAT
n is set
O . n is set
c18 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 . c18 is Element of (Omega,Sigma,P)
(Omega,Sigma,O,c18) is Element of Sigma
n is set
(union (rng B)) \ D2 is Element of bool Omega
(union (rng B)) /\ D2 is Element of bool Omega
((union (rng B)) \ D2) \/ ((union (rng B)) /\ D2) is Element of bool Omega
D2 \/ ((union (rng B)) \ D2) is Element of bool Omega
C is Element of bool Omega
rng c13 is non empty Element of bool (bool Omega)
union (rng c13) is Element of bool Omega
n is set
c18 is set
n is set
B . n is set
n 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,O,n) is Element of Sigma
dom O is non empty V50() V51() V52() V53() V54() V55() Element of bool NAT
B . n is Element of (Omega,Sigma,P)
(B . n) \ (Omega,Sigma,O,n) is Element of bool (B . n)
bool (B . n) is non empty V79() set
(Omega,(bool Omega),c13,n) is Element of bool Omega
dom c13 is non empty V50() V51() V52() V53() V54() V55() Element of bool NAT
c21 is set
rng k is non empty Element of bool (bool Omega)
n is set
P . n is V11() V12() ext-real set
dom k is non empty V50() V51() V52() V53() V54() V55() Element of bool NAT
c18 is set
k . c18 is set
union (rng k) is Element of bool Omega
P . (union (rng k)) is V11() V12() ext-real set
Union k is Element of bool Omega
n is set
c18 is set
dom c13 is non empty V50() V51() V52() V53() V54() V55() Element of bool NAT
n is set
c13 . n is set
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
dom k is non empty V50() V51() V52() V53() V54() V55() Element of bool NAT
(Omega,Sigma,k,n) is Element of Sigma
(Omega,(bool Omega),c13,n) is Element of bool Omega
n is (Omega,Sigma,P)
D2 \/ n is Element of bool Omega
x is set
C is set
O . x is set
O . C is set
dom B is non empty V50() V51() V52() V53() V54() V55() Element of bool NAT
dom O is non empty V50() V51() V52() V53() V54() V55() Element of bool NAT
n is set
O . n is set
B . n is set
B . x is set
B . C is set
(B . x) /\ (B . C) is set
(O . x) /\ (O . C) is set
C * B is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Sum (C * B) is V11() V12() ext-real Element of REAL
Partial_Sums (C * B) is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
lim (Partial_Sums (C * B)) is V11() V12() ext-real Element of REAL
Union B is set
C . (Union B) is V11() V12() ext-real set
x 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 . x is Element of (Omega,Sigma,P)
C . (B . x) is V11() V12() ext-real Element of REAL
(Omega,Sigma,O,x) is Element of Sigma
P . (Omega,Sigma,O,x) is V11() V12() ext-real Element of REAL
(B . x) \ (Omega,Sigma,O,x) is Element of bool (B . x)
bool (B . x) is non empty V79() set
C is (Omega,Sigma,P)
(B . x) /\ (Omega,Sigma,O,x) is Element of bool Omega
((B . x) /\ (Omega,Sigma,O,x)) \/ ((B . x) \ (Omega,Sigma,O,x)) is set
(Omega,Sigma,O,x) \/ C is Element of bool Omega
P * O is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
x 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) . x is V11() V12() ext-real Element of REAL
(P * O) . x is V11() V12() ext-real Element of REAL
B . x is Element of (Omega,Sigma,P)
C . (B . x) is V11() V12() ext-real Element of REAL
(Omega,Sigma,O,x) is Element of Sigma
P . (Omega,Sigma,O,x) is V11() V12() ext-real Element of REAL
Sum (P * O) is V11() V12() ext-real Element of REAL
Partial_Sums (P * O) is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
lim (Partial_Sums (P * O)) is V11() V12() ext-real Element of REAL
C . (union (rng B)) is V11() V12() ext-real set
P . (union (rng O)) is V11() V12() ext-real set
x is (Omega,Sigma,P)
D2 \/ x is Element of bool Omega
P . (Union O) is V11() V12() ext-real set
B is Element of (Omega,Sigma,P)
C . B is V11() V12() ext-real Element of REAL
A is set
B is Element of Sigma
P . B is V11() V12() ext-real Element of REAL
O is (Omega,Sigma,P)
A \/ O is set
A is (Omega,Sigma,P)
{} \/ A is set
C . {} is V11() V12() ext-real set
P . {} is V11() V12() ext-real set
B is Event of (Omega,Sigma,P)
A is Event of (Omega,Sigma,P)
B \/ A is Element of (Omega,Sigma,P)
C . (B \/ A) is V11() V12() ext-real Element of REAL
C . B is V11() V12() ext-real Element of REAL
C . A is V11() V12() ext-real Element of REAL
(C . B) + (C . A) is V11() V12() ext-real Element of REAL
B is Element of bool Omega
O is Element of bool Omega
{} Omega is empty proper 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
(B,O) 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
B2 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),B2,1) is Element of bool Omega
(Omega,(bool Omega),B2,0) is Element of bool Omega
D2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative set
B2 . D2 is set
D2 + 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
rng B2 is non empty Element of bool (bool Omega)
2 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
D2 is non empty V13() V16( NAT ) V17((Omega,Sigma,P)) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
C * D2 is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Partial_Sums (C * D2) is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(Partial_Sums (C * D2)) . 0 is V11() V12() ext-real Element of REAL
(C * D2) . 0 is V11() V12() ext-real Element of REAL
0 + 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 (C * D2)) . 1 is V11() V12() ext-real Element of REAL
(C * D2) . 1 is V11() V12() ext-real Element of REAL
((Partial_Sums (C * D2)) . 0) + ((C * D2) . 1) is V11() V12() ext-real Element of REAL
c13 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
2 + c13 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 (C * D2)) . (2 + c13) is V11() V12() ext-real Element of REAL
c13 + 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
2 + (c13 + 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 (C * D2)) . (2 + (c13 + 1)) is V11() V12() ext-real Element of REAL
(2 + c13) + 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 * D2) . ((2 + c13) + 1) is V11() V12() ext-real Element of REAL
((Partial_Sums (C * D2)) . (2 + c13)) + ((C * D2) . ((2 + c13) + 1)) is V11() V12() ext-real Element of REAL
(Omega,(Omega,Sigma,P),D2,((2 + c13) + 1)) is Element of (Omega,Sigma,P)
C . (Omega,(Omega,Sigma,P),D2,((2 + c13) + 1)) is V11() V12() ext-real Element of REAL
((C . B) + (C . A)) + (C . (Omega,(Omega,Sigma,P),D2,((2 + c13) + 1))) is V11() V12() ext-real Element of REAL
((C . B) + (C . A)) + (C . {}) is V11() V12() ext-real Element of REAL
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
2 + 0 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 (C * D2)) . (2 + 0) is V11() V12() ext-real Element of REAL
(C * D2) . 2 is V11() V12() ext-real Element of REAL
((Partial_Sums (C * D2)) . 1) + ((C * D2) . 2) is V11() V12() ext-real Element of REAL
(Omega,(Omega,Sigma,P),D2,2) is Element of (Omega,Sigma,P)
C . (Omega,(Omega,Sigma,P),D2,2) is V11() V12() ext-real Element of REAL
((C . B) + (C . A)) + (C . (Omega,(Omega,Sigma,P),D2,2)) is V11() V12() ext-real Element of REAL
((C . B) + (C . A)) + (C . {}) is V11() V12() ext-real Element of REAL
c13 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 (C * D2)) . c13 is V11() V12() ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative set
2 + k 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
Union D2 is Element of bool Omega
Sum (C * D2) is V11() V12() ext-real Element of REAL
lim (Partial_Sums (C * D2)) is V11() V12() ext-real Element of REAL
B is Event of (Omega,Sigma,P)
A is Event of (Omega,Sigma,P)
A \ B is Element of (Omega,Sigma,P)
C . (A \ B) is V11() V12() ext-real Element of REAL
C . A is V11() V12() ext-real Element of REAL
C . B is V11() V12() ext-real Element of REAL
(C . A) - (C . B) is V11() V12() ext-real Element of REAL
(C . B) + (C . (A \ B)) is V11() V12() ext-real Element of REAL
B \/ (A \ B) is Element of (Omega,Sigma,P)
C . (B \/ (A \ B)) is V11() V12() ext-real Element of REAL
B is Event of (Omega,Sigma,P)
A is Event of (Omega,Sigma,P)
C . B is V11() V12() ext-real Element of REAL
C . A is V11() V12() ext-real Element of REAL
A \ B is Element of (Omega,Sigma,P)
C . (A \ B) is V11() V12() ext-real Element of REAL
(C . A) - (C . B) is V11() V12() ext-real Element of REAL
0 + (C . B) is V11() V12() ext-real Element of REAL
B is non empty V13() V16( NAT ) V17((Omega,Sigma,P)) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
C * B is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
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
(C * B) . 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
(C * B) . B is V11() V12() ext-real Element of REAL
(Omega,(Omega,Sigma,P),B,A) is Element of (Omega,Sigma,P)
(Omega,(Omega,Sigma,P),B,B) is Element of (Omega,Sigma,P)
C . (Omega,(Omega,Sigma,P),B,A) is V11() V12() ext-real Element of REAL
C . (Omega,(Omega,Sigma,P),B,B) is V11() V12() ext-real Element of REAL
C . Omega is V11() V12() ext-real set
{} \/ Omega is set
C . ({} \/ Omega) is V11() V12() ext-real set
P . Omega is V11() V12() ext-real set
A is Event of (Omega,Sigma,P)
C . A is V11() V12() ext-real Element of REAL
B is Event of (Omega,Sigma,P)
C . B is V11() V12() ext-real Element of REAL
B is non empty V13() V16( NAT ) V17((Omega,Sigma,P)) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
C * B is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
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
(C * B) . A is V11() V12() ext-real Element of REAL
(Omega,(Omega,Sigma,P),B,A) is Element of (Omega,Sigma,P)
C . (Omega,(Omega,Sigma,P),B,A) is V11() V12() ext-real Element of REAL
B is non empty V13() V16( NAT ) V17((Omega,Sigma,P)) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
C * B is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
2 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
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
(C * B) . A is V11() V12() ext-real Element of REAL
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
((C * B) . A) + 0 is V11() V12() ext-real Element of REAL
B is non empty V13() V16( NAT ) V17((Omega,Sigma,P)) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
C * B is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
lim (C * B) is V11() V12() ext-real Element of REAL
Union B is Element of bool Omega
C . (Union B) is V11() V12() ext-real set
Partial_Diff_Union B is non empty V13() V16( NAT ) V17((Omega,Sigma,P)) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) disjoint_valued Element of bool [:NAT,(bool Omega):]
A is non empty V13() V16( NAT ) V17((Omega,Sigma,P)) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
C * A is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Partial_Sums (C * A) is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,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 (C * A)) . B is V11() V12() ext-real Element of REAL
(C * B) . 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 (C * A)) . (B + 1) is V11() V12() ext-real Element of REAL
(C * B) . (B + 1) is V11() V12() ext-real Element of REAL
(Omega,(Omega,Sigma,P),B,B) is Element of (Omega,Sigma,P)
(Omega,(Omega,Sigma,P),B,(B + 1)) is Element of (Omega,Sigma,P)
(C * A) . (B + 1) is V11() V12() ext-real Element of REAL
((C * B) . B) + ((C * A) . (B + 1)) is V11() V12() ext-real Element of REAL
C . (Omega,(Omega,Sigma,P),B,B) is V11() V12() ext-real Element of REAL
(C . (Omega,(Omega,Sigma,P),B,B)) + ((C * A) . (B + 1)) is V11() V12() ext-real Element of REAL
(Omega,(Omega,Sigma,P),A,(B + 1)) is Element of (Omega,Sigma,P)
C . (Omega,(Omega,Sigma,P),A,(B + 1)) is V11() V12() ext-real Element of REAL
(C . (Omega,(Omega,Sigma,P),B,B)) + (C . (Omega,(Omega,Sigma,P),A,(B + 1))) is V11() V12() ext-real Element of REAL
(Omega,(Omega,Sigma,P),B,B) \/ (Omega,(Omega,Sigma,P),A,(B + 1)) is Element of (Omega,Sigma,P)
C . ((Omega,(Omega,Sigma,P),B,B) \/ (Omega,(Omega,Sigma,P),A,(B + 1))) is V11() V12() ext-real Element of REAL
(Omega,(Omega,Sigma,P),B,(B + 1)) \ (Omega,(Omega,Sigma,P),B,B) is Element of (Omega,Sigma,P)
(Omega,(Omega,Sigma,P),B,B) \/ ((Omega,(Omega,Sigma,P),B,(B + 1)) \ (Omega,(Omega,Sigma,P),B,B)) is Element of (Omega,Sigma,P)
C . ((Omega,(Omega,Sigma,P),B,B) \/ ((Omega,(Omega,Sigma,P),B,(B + 1)) \ (Omega,(Omega,Sigma,P),B,B))) is V11() V12() ext-real Element of REAL
(Omega,(Omega,Sigma,P),B,B) \/ (Omega,(Omega,Sigma,P),B,(B + 1)) is Element of (Omega,Sigma,P)
C . ((Omega,(Omega,Sigma,P),B,B) \/ (Omega,(Omega,Sigma,P),B,(B + 1))) is V11() V12() ext-real Element of REAL
C . (Omega,(Omega,Sigma,P),B,(B + 1)) is V11() V12() ext-real Element of REAL
(Partial_Sums (C * A)) . 0 is V11() V12() ext-real Element of REAL
(C * A) . 0 is V11() V12() ext-real Element of REAL
(Omega,(Omega,Sigma,P),A,0) is Element of (Omega,Sigma,P)
C . (Omega,(Omega,Sigma,P),A,0) is V11() V12() ext-real Element of REAL
(Omega,(Omega,Sigma,P),B,0) is Element of (Omega,Sigma,P)
C . (Omega,(Omega,Sigma,P),B,0) is V11() V12() ext-real Element of REAL
(C * B) . 0 is V11() V12() ext-real Element of REAL
Union A is Element of bool Omega
C . (Union A) is V11() V12() ext-real set
Sum (C * A) is V11() V12() ext-real Element of REAL
lim (Partial_Sums (C * A)) is V11() V12() ext-real Element of REAL
B is non empty V13() V16((Omega,Sigma,P)) V17( REAL ) Function-like V23((Omega,Sigma,P)) V27((Omega,Sigma,P), REAL ) V33() V34() V35() V42() Probability of (Omega,Sigma,P)
A is set
B is (Omega,Sigma,P)
A \/ B is set
B . (A \/ B) is V11() V12() ext-real set
P . A is V11() V12() ext-real set
A is non empty V13() V16((Omega,Sigma,P)) V17( REAL ) Function-like V23((Omega,Sigma,P)) V27((Omega,Sigma,P), REAL ) V33() V34() V35() V42() Probability of (Omega,Sigma,P)
B is non empty V13() V16((Omega,Sigma,P)) V17( REAL ) Function-like V23((Omega,Sigma,P)) V27((Omega,Sigma,P), REAL ) V33() V34() V35() V42() Probability of (Omega,Sigma,P)
C is set
A . C is V11() V12() ext-real set
B . C is V11() V12() ext-real set
B is set
P . B is V11() V12() ext-real set
A is (Omega,Sigma,P)
B \/ A 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 compl-closed sigma-multiplicative V78() V79() V80() sigma-additive 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)
(Omega,Sigma,P) is non empty V13() V16((Omega,Sigma,P)) V17( REAL ) Function-like V23((Omega,Sigma,P)) V27((Omega,Sigma,P), REAL ) V33() V34() V35() V42() Probability of (Omega,Sigma,P)
COM (Omega,Sigma,P) is non empty V13() V16( COM (Sigma,(Omega,Sigma,P))) V17( ExtREAL ) Function-like V23( COM (Sigma,(Omega,Sigma,P))) V27( COM (Sigma,(Omega,Sigma,P)), ExtREAL ) V34() V42() nonnegative sigma-additive Element of bool [:(COM (Sigma,(Omega,Sigma,P))),ExtREAL:]
[:(COM (Sigma,(Omega,Sigma,P))),ExtREAL:] is non empty V13() V34() set
bool [:(COM (Sigma,(Omega,Sigma,P))),ExtREAL:] is non empty V79() set
(Omega,(Omega,Sigma,P),(Omega,Sigma,P)) is non empty V13() V16((Omega,Sigma,P)) V17( ExtREAL ) Function-like V23((Omega,Sigma,P)) V27((Omega,Sigma,P), ExtREAL ) V34() V42() nonnegative sigma-additive Element of bool [:(Omega,Sigma,P),ExtREAL:]
[:(Omega,Sigma,P),ExtREAL:] is non empty V13() V34() set
bool [:(Omega,Sigma,P),ExtREAL:] is non empty V79() set
B is non empty V13() V16( COM (Sigma,(Omega,Sigma,P))) V17( ExtREAL ) Function-like V23( COM (Sigma,(Omega,Sigma,P))) V27( COM (Sigma,(Omega,Sigma,P)), ExtREAL ) V34() V42() nonnegative sigma-additive Element of bool [:(COM (Sigma,(Omega,Sigma,P))),ExtREAL:]
C is set
(Omega,Sigma,P) . C is ext-real set
B is thin of (Omega,Sigma,P)
C \/ B is set
B . (C \/ B) is ext-real set
A is (Omega,Sigma,P)
C \/ A is set
(Omega,Sigma,P) . (C \/ A) is V11() V12() ext-real set
P . C 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 compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
(Omega,Sigma,P) is non empty V13() V16((Omega,Sigma,P)) V17( REAL ) Function-like V23((Omega,Sigma,P)) V27((Omega,Sigma,P), REAL ) V33() V34() V35() V42() Probability of (Omega,Sigma,P)
A is Element of bool Omega
B is set
(Omega,Sigma,P) . B is V11() V12() ext-real set
C is set
P . C is V11() V12() ext-real set
B is (Omega,Sigma,P)
C \/ B is set
B is (Omega,Sigma,P)
C \/ B is set
B is (Omega,Sigma,P)
C \/ B is set
A /\ C is Element of bool Omega
A /\ B is Element of bool Omega
(A /\ C) \/ (A /\ B) is Element of bool Omega
B is set
P . B is V11() V12() ext-real set
C \/ B is set
P . (C \/ B) is V11() V12() ext-real set
B2 is Element of Sigma
D2 is Element of Sigma
B2 \/ D2 is Element of Sigma
P . (B2 \/ D2) is V11() V12() ext-real Element of REAL
0 + 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
B2 is set
P . B2 is V11() V12() ext-real set
A /\ (C \/ B) is Element of bool Omega
{} \/ ((A /\ C) \/ (A /\ B)) is set
C is set
B is (Omega,Sigma,P)
C \/ 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 V13() V16((Omega,Sigma,P)) V17( REAL ) Function-like V23((Omega,Sigma,P)) V27((Omega,Sigma,P), REAL ) V33() V34() V35() V42() Probability of (Omega,Sigma,P)
(Omega,Sigma,P) is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
B is Event of Sigma
P . B is V11() V12() ext-real Element of REAL
(Omega,Sigma,P) . B is V11() V12() ext-real set
A is (Omega,Sigma,P)
B \/ A is Element of bool Omega
(Omega,Sigma,P) . (B \/ A) 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 compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
(Omega,Sigma,P) is non empty V13() V16((Omega,Sigma,P)) V17( REAL ) Function-like V23((Omega,Sigma,P)) V27((Omega,Sigma,P), REAL ) V33() V34() V35() V42() Probability of (Omega,Sigma,P)
A is (Omega,Sigma,P)
(Omega,Sigma,P) . A is V11() V12() ext-real Element of REAL
B is set
P . B is V11() V12() ext-real set
C is Event of Sigma
(Omega,Sigma,P) . C is V11() V12() ext-real set
B is Event of (Omega,Sigma,P)
(Omega,Sigma,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
(Omega,Sigma,P) is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)
(Omega,Sigma,P) is non empty V13() V16((Omega,Sigma,P)) V17( REAL ) Function-like V23((Omega,Sigma,P)) V27((Omega,Sigma,P), REAL ) V33() V34() V35() V42() Probability of (Omega,Sigma,P)
A is Element of (Omega,Sigma,P)
(Omega,Sigma,P,A) is non empty Element of bool (bool Omega)
(Omega,Sigma,P) . A is V11() V12() ext-real Element of REAL
B is set
P . B is V11() V12() ext-real set
A \ B is Element of bool Omega
C is (Omega,Sigma,P)
B \/ C is set
B is Event of (Omega,Sigma,P)
A is Event of (Omega,Sigma,P)
(Omega,Sigma,P) . A is V11() V12() ext-real Element of REAL
(Omega,Sigma,P) . B is V11() V12() ext-real Element of REAL
(Omega,Sigma,P) . C is V11() V12() ext-real Element of REAL
((Omega,Sigma,P) . B) + ((Omega,Sigma,P) . C) is V11() V12() ext-real Element of REAL
((Omega,Sigma,P) . B) + 0 is V11() V12() ext-real Element of REAL
B is Event of Sigma
P . B is V11() V12() ext-real Element of REAL