:: KOLMOG01 semantic presentation

REAL is non empty non trivial non finite V79() V80() V81() V85() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() Element of bool REAL

ExtREAL is non empty V80() set
is non empty Relation-like V34() set

omega is non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() set

is non empty Relation-like V33() V34() V35() set

COMPLEX is non empty non trivial non finite V79() V85() set
RAT is non empty non trivial non finite V79() V80() V81() V82() V85() set
INT is non empty non trivial non finite V79() V80() V81() V82() V83() V85() set
is non empty Relation-like V33() set

is non empty Relation-like V33() V34() V35() set

is non empty Relation-like V33() V34() V35() set

is non empty Relation-like RAT -valued V33() V34() V35() set

is non empty Relation-like RAT -valued V33() V34() V35() set

is non empty Relation-like RAT -valued INT -valued V33() V34() V35() set

is non empty Relation-like RAT -valued INT -valued V33() V34() V35() V36() set
is non empty Relation-like RAT -valued INT -valued V33() V34() V35() V36() set

1 is ext-real non empty epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
2 is ext-real non empty epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
3 is ext-real non empty epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT

dom Omega is set
I is set
Omega | I is Relation-like Function-like set
rng (Omega | I) is set
the Element of I is Element of I
Omega is ext-real V14() real Element of REAL
Omega * Omega is ext-real V14() real set
Omega - 1 is ext-real V14() real set
Omega * (Omega - 1) is ext-real V14() real set
Omega is non empty set

{{},Omega} is non empty finite intersection_stable set
I is Element of bool (bool Omega)
sigma I is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)

[:NAT,(bool Omega):] is non empty Relation-like set

Sigma is non empty Relation-like NAT -defined bool Omega -valued Function-like V26( NAT ) V30( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
rng Sigma is non empty Element of bool (bool Omega)

Union Sigma is Element of bool Omega
rng Sigma is non empty set
union (rng Sigma) is set
Partial_Union Sigma is non empty Relation-like NAT -defined bool Omega -valued bool Omega -valued Function-like V26( NAT ) V30( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

(Partial_Union Sigma) . P is Event of bool Omega

(Partial_Union Sigma) . a is set
a + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
(Partial_Union Sigma) . (a + 1) is set

F + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
Sigma . (F + 1) is Event of bool Omega
(Partial_Union Sigma) . (F + 1) is Event of bool Omega
{} \/ (Sigma . (F + 1)) is set
(Partial_Union Sigma) . (F + 1) is Event of bool Omega
Omega \/ (Sigma . (F + 1)) is non empty set
(Partial_Union Sigma) . (F + 1) is Event of bool Omega
{} \/ (Sigma . (F + 1)) is set
Omega \/ (Sigma . (F + 1)) is non empty set
(Partial_Union Sigma) . 0 is Event of bool Omega
Sigma . 0 is Event of bool Omega
(Partial_Union Sigma) . 0 is set
Union (Partial_Union Sigma) is Element of bool Omega
rng (Partial_Union Sigma) is non empty set
union (rng (Partial_Union Sigma)) is set
P is set

(Partial_Union Sigma) . a is Event of bool Omega

(Partial_Union Sigma) . P is Event of bool Omega

(Partial_Union Sigma) . P is Event of bool Omega
a is set

(Partial_Union Sigma) . P is Event of bool Omega
Sigma is Element of bool Omega
Sigma ` is Element of bool Omega
Omega \ Sigma is set
Sigma is set
Sigma is set
Omega is non empty set

I is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)

Sigma is Element of bool I
P is non empty Relation-like I -defined REAL -valued Function-like V26(I) V30(I, REAL ) V33() V34() V35() V42() Probability of I
a is set
F is set
F is Element of bool I
T is Element of I
P . T is ext-real V14() real Element of REAL
Ie is Element of Sigma
T /\ Ie is Element of bool Omega
P . (T /\ Ie) is ext-real V14() real set
P . Ie is ext-real V14() real set
(P . T) * (P . Ie) is ext-real V14() real set
a is Element of bool I
F is Element of bool I
T is Element of I
P . T is ext-real V14() real Element of REAL
Ie is Element of Sigma
T /\ Ie is Element of bool Omega
P . (T /\ Ie) is ext-real V14() real set
P . Ie is ext-real V14() real set
(P . T) * (P . Ie) is ext-real V14() real set
Ie is Element of Sigma
T /\ Ie is Element of bool Omega
P . (T /\ Ie) is ext-real V14() real set
P . Ie is ext-real V14() real set
(P . T) * (P . Ie) is ext-real V14() real set
Omega is non empty set

[:NAT,(bool Omega):] is non empty Relation-like set

I is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)

Sigma is non empty Relation-like I -defined REAL -valued Function-like V26(I) V30(I, REAL ) V33() V34() V35() V42() Probability of I
P is non empty Element of bool I
a is Element of P
Sigma . a is ext-real V14() real Element of REAL
F is non empty Relation-like NAT -defined bool Omega -valued I -valued Function-like V26( NAT ) V30( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
Union F is Element of bool Omega
rng F is non empty set
union (rng F) is set
a /\ () is Element of bool Omega
Sigma . (a /\ ()) is ext-real V14() real set
Sigma . () is ext-real V14() real set
(Sigma . a) * (Sigma . ()) is ext-real V14() real set
T is Element of I
Sigma . T is ext-real V14() real Element of REAL
seqIntersection (T,F) is non empty Relation-like NAT -defined bool Omega -valued Function-like V26( NAT ) V30( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

(seqIntersection (T,F)) . u is Event of bool Omega
F . u is Event of I
T /\ (F . u) is Event of I
Partial_Union F is non empty Relation-like NAT -defined bool Omega -valued bool Omega -valued Function-like V26( NAT ) V30( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
seqIntersection (T,()) is non empty Relation-like NAT -defined bool Omega -valued Function-like V26( NAT ) V30( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

(seqIntersection (T,())) . v is Event of bool Omega
() . v is Event of I
T /\ (() . v) is Event of I
T /\ () is Element of bool Omega
Union () is Element of bool Omega
rng () is non empty set
union (rng ()) is set
T /\ () is Element of bool Omega
v is non empty Relation-like NAT -defined bool Omega -valued I -valued Function-like V26( NAT ) V30( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
Union v is Element of bool Omega
rng v is non empty set
union (rng v) is set
u is non empty Relation-like NAT -defined bool Omega -valued I -valued Function-like V26( NAT ) V30( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
Sigma * u is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool

(Sigma * u) . x is ext-real V14() real Element of REAL
u . x is Event of I
Sigma . (u . x) is ext-real V14() real Element of REAL
F . x is Event of I
(F . x) /\ T is Event of I
Sigma . ((F . x) /\ T) is ext-real V14() real Element of REAL
Sigma . (F . x) is ext-real V14() real Element of REAL
(Sigma . (F . x)) * (Sigma . T) is ext-real V14() real set
Sigma * F is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool
(Sigma * F) . x is ext-real V14() real Element of REAL
Ie is ext-real V14() real set
((Sigma * F) . x) * Ie is ext-real V14() real set
Ie (#) (Sigma * F) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool
(Ie (#) (Sigma * F)) . x is ext-real V14() real Element of REAL
x is set

() . y is Event of I

() . E1 is Event of I
E is non empty Relation-like NAT -defined bool Omega -valued I -valued Function-like V26( NAT ) V30( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
E . y is Event of I
E . E1 is Event of I

(seqIntersection (T,())) . x is Event of bool Omega

(seqIntersection (T,())) . E is Event of bool Omega
y is set
() . x is Event of I
T /\ (() . x) is Event of I
() . E is Event of I
T /\ (() . E) is Event of I
Partial_Union u is non empty Relation-like NAT -defined bool Omega -valued bool Omega -valued Function-like V26( NAT ) V30( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

() . x is Event of I
(seqIntersection (T,())) . x is Event of bool Omega

() . E is set
(seqIntersection (T,())) . E is set
E + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
() . (E + 1) is set
(seqIntersection (T,())) . (E + 1) is set

y + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
() . (y + 1) is Event of I
() . y is Event of I
u . (y + 1) is Event of I
(() . y) \/ (u . (y + 1)) is Event of I
() . y is Event of I
T /\ (() . y) is Event of I
(T /\ (() . y)) \/ (u . (y + 1)) is Event of I
F . (y + 1) is Event of I
T /\ (F . (y + 1)) is Event of I
(T /\ (() . y)) \/ (T /\ (F . (y + 1))) is Event of I
(() . y) \/ (F . (y + 1)) is Event of I
T /\ ((() . y) \/ (F . (y + 1))) is Event of I
() . (y + 1) is Event of I
T /\ (() . (y + 1)) is Event of I
(seqIntersection (T,())) . (y + 1) is Event of bool Omega
() . 0 is Event of I
u . 0 is Event of I
F . 0 is Event of I
T /\ (F . 0) is Event of I
() . 0 is Event of I
T /\ (() . 0) is Event of I
(seqIntersection (T,())) . 0 is Event of bool Omega
() . 0 is set
(seqIntersection (T,())) . 0 is set
Sigma * (seqIntersection (T,())) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() Element of bool
Sigma * () is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool
Partial_Sums (Sigma * u) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool
Partial_Sums (Sigma * F) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool
Ie (#) (Partial_Sums (Sigma * F)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool
Sigma * () is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool
Ie (#) (Sigma * ()) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool
lim (Sigma * ()) is ext-real V14() real Element of REAL
Ie * (lim (Sigma * ())) is ext-real V14() real set
Sigma * v is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool
lim (Sigma * v) is ext-real V14() real Element of REAL
Sigma . (T /\ ()) is ext-real V14() real set
Omega is non empty set

I is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)

Sigma is non empty Relation-like I -defined REAL -valued Function-like V26(I) V30(I, REAL ) V33() V34() V35() V42() Probability of I
P is non empty Element of bool I
(Omega,I,P,Sigma) is Element of bool I
Sigma . {} is ext-real V14() real set
a is Element of P
{} /\ a is Relation-like finite V79() V80() V81() V82() V83() V84() set
Sigma . ({} /\ a) is ext-real V14() real set
Sigma . a is ext-real V14() real Element of REAL
(Sigma . {}) * (Sigma . a) is ext-real V14() real set
F is Event of I
{} /\ F is Relation-like finite V79() V80() V81() V82() V83() V84() Element of bool Omega
Sigma . ({} /\ F) is ext-real V14() real set

[:NAT,(bool Omega):] is non empty Relation-like set

F is non empty Relation-like NAT -defined bool Omega -valued Function-like V26( NAT ) V30( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
rng F is non empty Element of bool (bool Omega)

Union F is Element of bool Omega
rng F is non empty set
union (rng F) is set

F . T is Event of bool Omega
dom F is non empty V79() V80() V81() V82() V83() V84() Element of bool NAT
dom F is non empty V79() V80() V81() V82() V83() V84() Element of bool NAT
dom F is non empty V79() V80() V81() V82() V83() V84() Element of bool NAT
T is non empty Relation-like NAT -defined I -valued bool Omega -valued Function-like V26( NAT ) V30( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
Union T is Element of bool Omega
rng T is non empty set
union (rng T) is set

T . u is Event of I
Sigma . (T . u) is ext-real V14() real Element of REAL
v is Element of P
(T . u) /\ v is Event of I
Sigma . ((T . u) /\ v) is ext-real V14() real Element of REAL
Sigma . v is ext-real V14() real Element of REAL
(Sigma . (T . u)) * (Sigma . v) is ext-real V14() real set
dom T is non empty V79() V80() V81() V82() V83() V84() Element of bool NAT
rng T is non empty Element of bool I
dom T is non empty V79() V80() V81() V82() V83() V84() Element of bool NAT
dom T is non empty V79() V80() V81() V82() V83() V84() Element of bool NAT
Ie is Element of I
Sigma . Ie is ext-real V14() real Element of REAL
u is Element of P
Ie /\ u is Event of I
Sigma . (Ie /\ u) is ext-real V14() real Element of REAL
Sigma . u is ext-real V14() real Element of REAL
(Sigma . Ie) * (Sigma . u) is ext-real V14() real set
F is Element of bool Omega
F ` is Element of bool Omega
Omega \ F is set
T is Event of I
T ` is Element of bool Omega
Omega \ T is set
Sigma . (T `) is ext-real V14() real set
u is Element of P
(T `) /\ u is Element of bool Omega
Sigma . ((T `) /\ u) is ext-real V14() real set
Sigma . u is ext-real V14() real Element of REAL
(Sigma . (T `)) * (Sigma . u) is ext-real V14() real set
u /\ T is Event of I
Sigma . (u /\ T) is ext-real V14() real Element of REAL
Sigma . T is ext-real V14() real Element of REAL
(Sigma . u) * (Sigma . T) is ext-real V14() real set
[#] I is Event of I
([#] I) \ T is Event of I
Ie is Element of I
a is Element of bool (bool Omega)
Omega is non empty set

I is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)

Sigma is non empty Relation-like I -defined REAL -valued Function-like V26(I) V30(I, REAL ) V33() V34() V35() V42() Probability of I
P is non empty Element of bool I
(Omega,I,P,Sigma) is Element of bool I
F is Element of bool (bool Omega)
sigma F is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
a is Dynkin_System of Omega
Omega is non empty set

I is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)

Sigma is non empty Relation-like I -defined REAL -valued Function-like V26(I) V30(I, REAL ) V33() V34() V35() V42() Probability of I
P is non empty Element of bool I
a is non empty Element of bool I
(Omega,I,a,Sigma) is Element of bool I
F is set
T is Event of I
Sigma . T is ext-real V14() real Element of REAL
Ie is Element of a
T /\ Ie is Event of I
Sigma . (T /\ Ie) is ext-real V14() real Element of REAL
Sigma . Ie is ext-real V14() real Element of REAL
(Sigma . T) * (Sigma . Ie) is ext-real V14() real set
u is Event of I
F is Event of I
T is Event of I
u is Element of I
Ie is Element of a
u /\ Ie is Event of I
Sigma . (u /\ Ie) is ext-real V14() real Element of REAL
Sigma . u is ext-real V14() real Element of REAL
Sigma . Ie is ext-real V14() real Element of REAL
(Sigma . u) * (Sigma . Ie) is ext-real V14() real set
F is Event of I
T is Event of I
Ie is Event of I
u is Event of I
Omega is non empty set

I is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)

Sigma is non empty Relation-like I -defined REAL -valued Function-like V26(I) V30(I, REAL ) V33() V34() V35() V42() Probability of I
P is non empty Element of bool I
a is non empty Element of bool I
(Omega,I,a,Sigma) is Element of bool I
(Omega,I,P,Sigma) is Element of bool I
F is Event of I
T is Event of I
Omega is non empty set

I is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)

Sigma is non empty Relation-like I -defined REAL -valued Function-like V26(I) V30(I, REAL ) V33() V34() V35() V42() Probability of I
P is Element of bool (bool Omega)
sigma P is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
F is non empty Element of bool I
(Omega,I,F,Sigma) is Element of bool I
T is Element of bool (bool Omega)
sigma T is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
Ie is non empty Element of bool I
(Omega,I,Ie,Sigma) is Element of bool I
u is Element of bool (bool Omega)
a is non empty Element of bool I
(Omega,I,a,Sigma) is Element of bool I
sigma u is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
Omega is non empty set

I is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)

Sigma is non empty Relation-like I -defined REAL -valued Function-like V26(I) V30(I, REAL ) V33() V34() V35() V42() Probability of I
P is Element of bool (bool Omega)
sigma P is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
a is Element of bool (bool Omega)
sigma a is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
T is non empty Element of bool I
F is non empty Element of bool I
(Omega,I,F,Sigma) is Element of bool I
u is Element of bool (bool Omega)
sigma u is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
Ie is Element of bool (bool Omega)
sigma Ie is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
v is non empty Element of bool I
(Omega,I,v,Sigma) is Element of bool I
x is Event of I
E is Event of I
I is non empty set

Omega is set
Sigma is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)

[:Omega,(bool Sigma):] is Relation-like set
bool [:Omega,(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
Omega --> Sigma is Relation-like Omega -defined bool (bool I) -valued Function-like V26(Omega) V30(Omega, bool (bool I)) Element of bool [:Omega,(bool (bool I)):]
[:Omega,(bool (bool I)):] is Relation-like set
bool [:Omega,(bool (bool I)):] is non empty cup-closed intersection_stable diff-closed preBoolean set
rng (Omega --> Sigma) is Element of bool (bool (bool I))

a is set
dom (Omega --> Sigma) is Element of bool Omega

F is set
(Omega --> Sigma) . F is set
a is set
(Omega --> Sigma) . a is set
dom (Omega --> Sigma) is Element of bool Omega

Omega is non empty set

I is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
P is set
[:P,I:] is Relation-like set

Omega is non empty set

Sigma is set

I is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)

P is Element of bool Sigma
[:P,I:] is Relation-like set

a is Relation-like Sigma -defined bool I -valued Function-like V26(Sigma) V30(Sigma, bool I) (Sigma,Omega,I)
P --> {} is Relation-like P -defined -valued Function-like V26(P) V30(P,) V33() V34() V35() V36() Element of bool [:P,:]
is non empty functional finite V52() V79() V80() V81() V82() V83() V84() set

T is set

a . T is Element of bool (bool Omega)
dom () is Element of bool P

rng () is V79() V80() V81() V82() V83() V84() Element of bool REAL
T is set
Ie is set

a . Ie is Element of bool (bool Omega)
Omega is non empty set

I is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
P is set

I is non empty set

Omega is set
Sigma is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)

P is Relation-like Omega -defined bool Sigma -valued Function-like V26(Omega) V30(Omega, bool Sigma) (Omega,I,Sigma)
a is Element of bool Omega
P | a is Relation-like a -defined Omega -defined bool Sigma -valued Function-like set
[:a,(bool Sigma):] is Relation-like set
bool [:a,(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
Omega is set

Sigma is non empty set

I is Element of bool Omega
P is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Sigma)

[:I,(bool P):] is Relation-like set

a is Relation-like I -defined bool P -valued Function-like V26(I) V30(I, bool P) Element of bool [:I,(bool P):]
Union a is set
rng a is set
union (rng a) is set

F is set
dom a is Element of bool I

T is set
a . T is Element of bool (bool Sigma)
I is non empty set

Omega is set
Sigma is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)

a is Element of bool Omega
P is Relation-like Omega -defined bool Sigma -valued Function-like V26(Omega) V30(Omega, bool Sigma) (Omega,I,Sigma)
(Omega,I,Sigma,P,a) is Relation-like a -defined Omega -defined bool Sigma -valued bool Sigma -valued Function-like V26(a) V30(a, bool Sigma) Element of bool [:a,(bool Sigma):]
[:a,(bool Sigma):] is Relation-like set
bool [:a,(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
(Omega,a,I,Sigma,(Omega,I,Sigma,P,a)) is Element of bool (bool I)
rng (Omega,I,Sigma,P,a) is set
union (rng (Omega,I,Sigma,P,a)) is set
sigma (Omega,a,I,Sigma,(Omega,I,Sigma,P,a)) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
I is non empty set

Omega is set
Sigma is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)

P is Relation-like Omega -defined bool Sigma -valued Function-like V26(Omega) V30(Omega, bool Sigma) (Omega,I,Sigma)

a is set

Omega \ ({} Omega) is Element of bool Omega
(Omega,I,Sigma,P,(Omega \ ({} Omega))) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
(Omega,I,Sigma,P,(Omega \ ({} Omega))) is Relation-like Omega \ ({} Omega) -defined Omega -defined bool Sigma -valued bool Sigma -valued Function-like V26(Omega \ ({} Omega)) V30(Omega \ ({} Omega), bool Sigma) Element of bool [:(Omega \ ({} Omega)),(bool Sigma):]
[:(Omega \ ({} Omega)),(bool Sigma):] is Relation-like set
bool [:(Omega \ ({} Omega)),(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
(Omega,(Omega \ ({} Omega)),I,Sigma,(Omega,I,Sigma,P,(Omega \ ({} Omega)))) is Element of bool (bool I)
rng (Omega,I,Sigma,P,(Omega \ ({} Omega))) is set
union (rng (Omega,I,Sigma,P,(Omega \ ({} Omega)))) is set
sigma (Omega,(Omega \ ({} Omega)),I,Sigma,(Omega,I,Sigma,P,(Omega \ ({} Omega)))) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
F is set
F is non empty Element of bool (bool (bool I))
T is Element of bool (bool I)
Ie is finite Element of bool Omega
Omega \ Ie is Element of bool Omega
(Omega,I,Sigma,P,(Omega \ Ie)) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
(Omega,I,Sigma,P,(Omega \ Ie)) is Relation-like Omega \ Ie -defined Omega -defined bool Sigma -valued bool Sigma -valued Function-like V26(Omega \ Ie) V30(Omega \ Ie, bool Sigma) Element of bool [:(Omega \ Ie),(bool Sigma):]
[:(Omega \ Ie),(bool Sigma):] is Relation-like set
bool [:(Omega \ Ie),(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
(Omega,(Omega \ Ie),I,Sigma,(Omega,I,Sigma,P,(Omega \ Ie))) is Element of bool (bool I)
rng (Omega,I,Sigma,P,(Omega \ Ie)) is set
union (rng (Omega,I,Sigma,P,(Omega \ Ie))) is set
sigma (Omega,(Omega \ Ie),I,Sigma,(Omega,I,Sigma,P,(Omega \ Ie))) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
a is Element of bool (bool (bool I))
F is Element of bool (bool (bool I))
T is Element of bool (bool I)
Ie is finite Element of bool Omega
Omega \ Ie is Element of bool Omega
(Omega,I,Sigma,P,(Omega \ Ie)) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
(Omega,I,Sigma,P,(Omega \ Ie)) is Relation-like Omega \ Ie -defined Omega -defined bool Sigma -valued bool Sigma -valued Function-like V26(Omega \ Ie) V30(Omega \ Ie, bool Sigma) Element of bool [:(Omega \ Ie),(bool Sigma):]
[:(Omega \ Ie),(bool Sigma):] is Relation-like set
bool [:(Omega \ Ie),(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
(Omega,(Omega \ Ie),I,Sigma,(Omega,I,Sigma,P,(Omega \ Ie))) is Element of bool (bool I)
rng (Omega,I,Sigma,P,(Omega \ Ie)) is set
union (rng (Omega,I,Sigma,P,(Omega \ Ie))) is set
sigma (Omega,(Omega \ Ie),I,Sigma,(Omega,I,Sigma,P,(Omega \ Ie))) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
Ie is finite Element of bool Omega
Omega \ Ie is Element of bool Omega
(Omega,I,Sigma,P,(Omega \ Ie)) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
(Omega,I,Sigma,P,(Omega \ Ie)) is Relation-like Omega \ Ie -defined Omega -defined bool Sigma -valued bool Sigma -valued Function-like V26(Omega \ Ie) V30(Omega \ Ie, bool Sigma) Element of bool [:(Omega \ Ie),(bool Sigma):]
[:(Omega \ Ie),(bool Sigma):] is Relation-like set
bool [:(Omega \ Ie),(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
(Omega,(Omega \ Ie),I,Sigma,(Omega,I,Sigma,P,(Omega \ Ie))) is Element of bool (bool I)
rng (Omega,I,Sigma,P,(Omega \ Ie)) is set
union (rng (Omega,I,Sigma,P,(Omega \ Ie))) is set
sigma (Omega,(Omega \ Ie),I,Sigma,(Omega,I,Sigma,P,(Omega \ Ie))) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
I is non empty set

Omega is set
Sigma is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)

P is Relation-like Omega -defined bool Sigma -valued Function-like V26(Omega) V30(Omega, bool Sigma) (Omega,I,Sigma)
(Omega,I,Sigma,P) is Element of bool (bool (bool I))

Omega \ ({} Omega) is Element of bool Omega
(Omega,I,Sigma,P,(Omega \ ({} Omega))) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
(Omega,I,Sigma,P,(Omega \ ({} Omega))) is Relation-like Omega \ ({} Omega) -defined Omega -defined bool Sigma -valued bool Sigma -valued Function-like V26(Omega \ ({} Omega)) V30(Omega \ ({} Omega), bool Sigma) Element of bool [:(Omega \ ({} Omega)),(bool Sigma):]
[:(Omega \ ({} Omega)),(bool Sigma):] is Relation-like set
bool [:(Omega \ ({} Omega)),(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
(Omega,(Omega \ ({} Omega)),I,Sigma,(Omega,I,Sigma,P,(Omega \ ({} Omega)))) is Element of bool (bool I)
rng (Omega,I,Sigma,P,(Omega \ ({} Omega))) is set
union (rng (Omega,I,Sigma,P,(Omega \ ({} Omega)))) is set
sigma (Omega,(Omega \ ({} Omega)),I,Sigma,(Omega,I,Sigma,P,(Omega \ ({} Omega)))) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
I is non empty set

Omega is set
Sigma is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)

P is Relation-like Omega -defined bool Sigma -valued Function-like V26(Omega) V30(Omega, bool Sigma) (Omega,I,Sigma)
(Omega,I,Sigma,P) is non empty Element of bool (bool (bool I))

meet (Omega,I,Sigma,P) is Element of bool (bool I)
I is non empty set

Omega is set
Sigma is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)

P is Relation-like Omega -defined bool Sigma -valued Function-like V26(Omega) V30(Omega, bool Sigma) (Omega,I,Sigma)
(Omega,I,Sigma,P) is Element of bool (bool I)

(Omega,I,Sigma,P) is non empty Element of bool (bool (bool I))

meet (Omega,I,Sigma,P) is Element of bool (bool I)
a is set

F is finite Element of bool Omega
Omega \ F is Element of bool Omega
(Omega,I,Sigma,P,(Omega \ F)) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
(Omega,I,Sigma,P,(Omega \ F)) is Relation-like Omega \ F -defined Omega -defined bool Sigma -valued bool Sigma -valued Function-like V26(Omega \ F) V30(Omega \ F, bool Sigma) Element of bool [:(Omega \ F),(bool Sigma):]
[:(Omega \ F),(bool Sigma):] is Relation-like set
bool [:(Omega \ F),(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
(Omega,(Omega \ F),I,Sigma,(Omega,I,Sigma,P,(Omega \ F))) is Element of bool (bool I)
rng (Omega,I,Sigma,P,(Omega \ F)) is set
union (rng (Omega,I,Sigma,P,(Omega \ F))) is set
sigma (Omega,(Omega \ F),I,Sigma,(Omega,I,Sigma,P,(Omega \ F))) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
Omega is non empty set

Sigma is non empty set

I is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)

a is non empty Relation-like Sigma -defined bool I -valued Function-like V26(Sigma) V30(Sigma, bool I) (Sigma,Omega,I)
P is non empty Element of bool Sigma

F is set
T is set
T is Element of bool (bool Omega)
Ie is Element of bool Omega
u is non empty finite Element of bool Sigma
v is non empty Relation-like u -defined I -valued Function-like V26(u) V30(u,I) finite (Omega,I,Sigma,u,a)
rng v is non empty finite Element of bool I
meet (rng v) is set
F is Element of bool (bool Omega)
T is Element of bool (bool Omega)
Ie is Element of bool Omega
u is non empty finite Element of bool Sigma
v is non empty Relation-like u -defined I -valued Function-like V26(u) V30(u,I) finite (Omega,I,Sigma,u,a)
rng v is non empty finite Element of bool I
meet (rng v) is set
u is non empty finite Element of bool Sigma
v is non empty Relation-like u -defined I -valued Function-like V26(u) V30(u,I) finite (Omega,I,Sigma,u,a)
rng v is non empty finite Element of bool I
meet (rng v) is set
Omega is non empty set

I is non empty set

Sigma is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)

P is non empty Relation-like I -defined bool Sigma -valued Function-like V26(I) V30(I, bool Sigma) (I,Omega,Sigma)
a is non empty Element of bool I
(Omega,Sigma,I,a,P) is Element of bool (bool Omega)
sigma (Omega,Sigma,I,a,P) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
(I,Omega,Sigma,P,a) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
(I,Omega,Sigma,P,a) is non empty Relation-like a -defined I -defined bool Sigma -valued bool Sigma -valued Function-like V26(a) V30(a, bool Sigma) Element of bool [:a,(bool Sigma):]
[:a,(bool Sigma):] is non empty Relation-like set
bool [:a,(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
(I,a,Omega,Sigma,(I,Omega,Sigma,P,a)) is Element of bool (bool Omega)
rng (I,Omega,Sigma,P,a) is non empty set
union (rng (I,Omega,Sigma,P,a)) is set
sigma (I,a,Omega,Sigma,(I,Omega,Sigma,P,a)) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
F is set
rng (I,Omega,Sigma,P,a) is non empty Element of bool (bool Sigma)

T is set
dom (I,Omega,Sigma,P,a) is non empty Element of bool a

Ie is set
(I,Omega,Sigma,P,a) . Ie is Element of bool (bool Omega)
u is Element of bool Omega
{Ie} is non empty finite set
v is finite Element of bool I
x is set
P . x is Element of bool (bool Omega)
P . Ie is Element of bool (bool Omega)
E is Element of bool Omega
[:v,Sigma:] is Relation-like set

x is Relation-like v -defined Sigma -valued Function-like V26(v) V30(v,Sigma) finite Element of bool [:v,Sigma:]
E is set
x . E is set
P . E is Element of bool (bool Omega)
E is Relation-like v -defined Sigma -valued Function-like V26(v) V30(v,Sigma) finite (Omega,Sigma,I,v,P)
dom E is finite Element of bool v

rng E is finite Element of bool Sigma
E . Ie is set
{(E . Ie)} is non empty finite set
meet (rng E) is set
F is set
T is non empty finite Element of bool I
Ie is non empty Relation-like T -defined Sigma -valued Function-like V26(T) V30(T,Sigma) finite (Omega,Sigma,I,T,P)
rng Ie is non empty finite Element of bool Sigma
meet (rng Ie) is set

v is finite Element of Fin T
Ie | v is Relation-like T -defined v -defined T -defined Sigma -valued Function-like finite Element of bool [:T,Sigma:]
[:T,Sigma:] is non empty Relation-like set

rng (Ie | v) is finite Element of bool Sigma
meet (rng (Ie | v)) is set
x is finite Element of Fin T
Ie | x is Relation-like T -defined x -defined T -defined Sigma -valued Function-like finite Element of bool [:T,Sigma:]
rng (Ie | x) is finite Element of bool Sigma
meet (rng (Ie | x)) is set
E is Element of T
{E} is non empty finite set
x \/ {E} is non empty finite set
Ie | (x \/ {E}) is Relation-like T -defined x \/ {E} -defined T -defined Sigma -valued Function-like finite Element of bool [:T,Sigma:]
rng (Ie | (x \/ {E})) is finite Element of bool Sigma
meet (rng (Ie | (x \/ {E}))) is set
Ie | {E} is Relation-like T -defined {E} -defined T -defined Sigma -valued Function-like finite Element of bool [:T,Sigma:]
rng (Ie | {E}) is finite Element of bool Sigma
(Ie | x) \/ (Ie | {E}) is Relation-like T -defined Sigma -valued finite Element of bool [:T,Sigma:]
rng ((Ie | x) \/ (Ie | {E})) is finite Element of bool Sigma
(rng (Ie | x)) \/ (rng (Ie | {E})) is finite Element of bool Sigma
dom (I,Omega,Sigma,P,a) is non empty Element of bool a

(I,Omega,Sigma,P,a) . E is Element of bool (bool Omega)
rng (I,Omega,Sigma,P,a) is non empty Element of bool (bool Sigma)

P . E is Element of bool (bool Omega)
dom Ie is non empty finite Element of bool T

(dom Ie) /\ {E} is finite Element of bool T
dom (Ie | {E}) is finite Element of bool T
(Ie | {E}) . E is set
{((Ie | {E}) . E)} is non empty finite set
Ie . E is Element of Sigma
{(Ie . E)} is non empty finite set
meet (rng (Ie | {E})) is set
y is set
E2 is set
meet E2 is set
E1 is set
meet E1 is set
meet y is set
(meet E1) /\ (meet y) is set

meet (rng (Ie | {})) is set

meet (rng (Ie | ({}. T))) is set
u is finite Element of Fin T
Ie | u is Relation-like T -defined u -defined T -defined Sigma -valued Function-like finite Element of bool [:T,Sigma:]
[:T,Sigma:] is non empty Relation-like set

rng (Ie | u) is finite Element of bool Sigma
meet (rng (Ie | u)) is set
Omega is non empty set

I is non empty set

Sigma is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)

P is non empty Relation-like Sigma -defined REAL -valued Function-like V26(Sigma) V30(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma
a is non empty Relation-like Omega -defined bool Sigma -valued Function-like V26(Omega) V30(Omega, bool Sigma) (Omega,I,Sigma)
F is non empty Element of bool Omega
T is non empty Element of bool Omega
(I,Sigma,Omega,F,a) is Element of bool (bool I)
(I,Sigma,Omega,T,a) is Element of bool (bool I)
u is Element of bool I
v is Element of bool I
u /\ v is Element of bool I
P . (u /\ v) is ext-real V14() real set
P . u is ext-real V14() real set
P . v is ext-real V14() real set
(P . u) * (P . v) is ext-real V14() real set
x is non empty finite Element of bool Omega
E is non empty Relation-like x -defined Sigma -valued Function-like V26(x) V30(x,Sigma) finite (I,Sigma,Omega,x,a)
rng E is non empty finite Element of bool Sigma
meet (rng E) is set
y is non empty finite Element of bool Omega
E1 is non empty Relation-like y -defined Sigma -valued Function-like V26(y) V30(y,Sigma) finite (I,Sigma,Omega,y,a)
rng E1 is non empty finite Element of bool Sigma
meet (rng E1) is set
E2 is set
[:x,E2:] is Relation-like set

E3 is set
[:y,E3:] is Relation-like set

Seg i is finite V55(i) V79() V80() V81() V82() V83() V84() Element of bool NAT

dom z is set
rng z is set
[:(Seg i),y:] is Relation-like finite set

B9 is Relation-like Seg i -defined y -valued Function-like V26( Seg i) V30( Seg i,y) finite Element of bool [:(Seg i),y:]
S is Relation-like y -defined E3 -valued Function-like V30(y,E3) finite Element of bool [:y,E3:]
S * B9 is Relation-like Seg i -defined E3 -valued Function-like V30( Seg i,E3) finite Element of bool [:(Seg i),E3:]
[:(Seg i),E3:] is Relation-like set

rng (S * B9) is finite Element of bool E3

rng S is finite Element of bool E3
Ie is set
[:y,Ie:] is Relation-like set

f2 is Relation-like y -defined Ie -valued Function-like V30(y,Ie) finite Element of bool [:y,Ie:]

rng b is finite Element of bool y

dom f2 is finite Element of bool y

x \/ y is non empty finite Element of bool Omega

Seg n is finite V55(n) V79() V80() V81() V82() V83() V84() Element of bool NAT

dom e1 is set
rng e1 is set
[:(Seg n),x:] is Relation-like finite set

e1 is Relation-like Seg n -defined x -valued Function-like V26( Seg n) V30( Seg n,x) finite Element of bool [:(Seg n),x:]
X is Relation-like x -defined E2 -valued Function-like V30(x,E2) finite Element of bool [:x,E2:]
X * e1 is Relation-like Seg n -defined E2 -valued Function-like V30( Seg n,E2) finite Element of bool [:(Seg n),E2:]
[:(Seg n),E2:] is Relation-like set

rng (X * e1) is finite Element of bool E2

rng X is finite Element of bool E2
[:x,Ie:] is Relation-like set

f1 is Relation-like x -defined Ie -valued Function-like V30(x,Ie) finite Element of bool [:x,Ie:]

rng e1 is finite Element of bool x

dom f1 is finite Element of bool x

dom h is set

dom (e1 ^ b) is finite V79() V80() V81() V82() V83() V84() Element of bool NAT

dom ((e1 ^ b) (#) h) is finite V79() V80() V81() V82() V83() V84() Element of bool NAT
h is set
rng (e1 ^ b) is finite set
(e1 ^ b) . h is set
h is set

dom (fe1 ^ fe2) is finite V79() V80() V81() V82() V83() V84() Element of bool NAT
(len fe1) + (len fe2) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
Seg ((len fe1) + (len fe2)) is finite V55((len fe1) + (len fe2)) V79() V80() V81() V82() V83() V84() Element of bool NAT
h is set
(fe1 ^ fe2) . h is set
((e1 ^ b) (#) h) . h is set

dom fe1 is finite V79() V80() V81() V82() V83() V84() Element of bool NAT
(fe1 ^ fe2) . h is set
fe1 . h is set
dom e1 is finite V79() V80() V81() V82() V83() V84() Element of bool NAT
e1 . h is set
h . (e1 . h) is set
f1 . (e1 . h) is set
(e1 ^ b) . h is set

dom fe1 is finite V79() V80() V81() V82() V83() V84() Element of bool NAT
dom fe2 is finite V79() V80() V81() V82() V83() V84() Element of bool NAT

(len fe1) + Pfe1 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
dom b is finite V79() V80() V81() V82() V83() V84() Element of bool NAT
b . Pfe1 is set
x /\ y is finite Element of bool Omega
F /\ T is Element of bool Omega
y \ x is finite Element of bool Omega
(y \ x) \/ {} is finite set
(fe1 ^ fe2) . h is set
fe2 . Pfe1 is set
f2 . (b . Pfe1) is set
h . (b . Pfe1) is set
(e1 ^ b) . h is set
h . ((e1 ^ b) . h) is set

dom fe1 is finite V79() V80() V81() V82() V83() V84() Element of bool NAT
h is set
h . h is set
f1 . h is set
f2 . h is set
[:(x \/ y),Sigma:] is non empty Relation-like set
bool [:(x \/ y),Sigma:] is non empty cup-closed intersection_stable diff-closed preBoolean set
h is non empty Relation-like x \/ y -defined Sigma -valued Function-like V26(x \/ y) V30(x \/ y,Sigma) finite Element of bool [:(x \/ y),Sigma:]
h is set
h . h is set
a . h is Element of bool (bool I)
f1 . h is set
f2 . h is set
h is non empty Relation-like x \/ y -defined Sigma -valued Function-like V26(x \/ y) V30(x \/ y,Sigma) finite (I,Sigma,Omega,x \/ y,a)

[:x,REAL:] is non empty Relation-like V33() V34() V35() set