:: 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
bool REAL is non empty cup-closed intersection_stable diff-closed preBoolean set
ExtREAL is non empty V80() set
[:NAT,ExtREAL:] is non empty Relation-like V34() set
bool [:NAT,ExtREAL:] is non empty cup-closed intersection_stable diff-closed preBoolean set
bool ExtREAL is non empty cup-closed intersection_stable diff-closed preBoolean set
omega is non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() set
bool omega is non empty cup-closed intersection_stable diff-closed preBoolean set
[:NAT,REAL:] is non empty Relation-like V33() V34() V35() set
bool [:NAT,REAL:] is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool REAL) is non empty cup-closed intersection_stable diff-closed preBoolean set
bool NAT is non empty cup-closed intersection_stable diff-closed preBoolean 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
[:COMPLEX,COMPLEX:] is non empty Relation-like V33() set
bool [:COMPLEX,COMPLEX:] is non empty cup-closed intersection_stable diff-closed preBoolean set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty Relation-like V33() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty cup-closed intersection_stable diff-closed preBoolean set
[:REAL,REAL:] is non empty Relation-like V33() V34() V35() set
bool [:REAL,REAL:] is non empty cup-closed intersection_stable diff-closed preBoolean set
[:[:REAL,REAL:],REAL:] is non empty Relation-like V33() V34() V35() set
bool [:[:REAL,REAL:],REAL:] is non empty cup-closed intersection_stable diff-closed preBoolean set
[:RAT,RAT:] is non empty Relation-like RAT -valued V33() V34() V35() set
bool [:RAT,RAT:] is non empty cup-closed intersection_stable diff-closed preBoolean set
[:[:RAT,RAT:],RAT:] is non empty Relation-like RAT -valued V33() V34() V35() set
bool [:[:RAT,RAT:],RAT:] is non empty cup-closed intersection_stable diff-closed preBoolean set
[:INT,INT:] is non empty Relation-like RAT -valued INT -valued V33() V34() V35() set
bool [:INT,INT:] is non empty cup-closed intersection_stable diff-closed preBoolean set
[:[:INT,INT:],INT:] is non empty Relation-like RAT -valued INT -valued V33() V34() V35() set
bool [:[:INT,INT:],INT:] is non empty cup-closed intersection_stable diff-closed preBoolean set
[:NAT,NAT:] is non empty Relation-like RAT -valued INT -valued V33() V34() V35() V36() set
[:[:NAT,NAT:],NAT:] is non empty Relation-like RAT -valued INT -valued V33() V34() V35() V36() set
bool [:[:NAT,NAT:],NAT:] is non empty cup-closed intersection_stable diff-closed preBoolean 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
0 is ext-real empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V33() V34() V35() V36() finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V77() V78() V79() V80() V81() V82() V83() V84() V85() Element of NAT
the ext-real empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V33() V34() V35() V36() finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() V81() V82() V83() V84() V85() set is ext-real empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V33() V34() V35() V36() finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() V81() V82() V83() V84() V85() set
{} is ext-real empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V33() V34() V35() V36() finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() V81() V82() V83() V84() V85() set
union {} is epsilon-transitive epsilon-connected ordinal finite set
Omega is Relation-like Function-like set
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
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Omega) is non empty cup-closed intersection_stable diff-closed preBoolean 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)
bool Omega is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool Omega)
[:NAT,(bool Omega):] is non empty Relation-like set
bool [:NAT,(bool Omega):] is non empty cup-closed intersection_stable diff-closed preBoolean 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)
bool (bool Omega) is non empty cup-closed intersection_stable diff-closed preBoolean set
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):]
P 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) . P is Event of bool Omega
a is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real set
(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 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
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
a 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 is Event of bool Omega
P 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) . P is Event of bool Omega
P 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) . P is Event of bool Omega
a is set
P 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) . 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
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Omega) is non empty cup-closed intersection_stable diff-closed preBoolean set
I is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
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
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Omega) is non empty cup-closed intersection_stable diff-closed preBoolean set
bool Omega is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool Omega)
[:NAT,(bool Omega):] is non empty Relation-like set
bool [:NAT,(bool Omega):] is non empty cup-closed intersection_stable diff-closed preBoolean set
I is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
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 /\ (Union F) is Element of bool Omega
Sigma . (a /\ (Union F)) is ext-real V14() real set
Sigma . (Union F) is ext-real V14() real set
(Sigma . a) * (Sigma . (Union F)) 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):]
u is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
(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,(Partial_Union 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):]
v is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
(seqIntersection (T,(Partial_Union F))) . v is Event of bool Omega
(Partial_Union F) . v is Event of I
T /\ ((Partial_Union F) . v) is Event of I
T /\ (Union F) is Element of bool Omega
Union (Partial_Union F) is Element of bool Omega
rng (Partial_Union F) is non empty set
union (rng (Partial_Union F)) is set
T /\ (Union (Partial_Union F)) 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 [:NAT,REAL:]
x is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
(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 [:NAT,REAL:]
(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 [:NAT,REAL:]
(Ie (#) (Sigma * F)) . x is ext-real V14() real Element of REAL
x is set
y is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
(Partial_Union F) . y is Event of I
E1 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
(Partial_Union F) . 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
x is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
(seqIntersection (T,(Partial_Union F))) . x is Event of bool Omega
E is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
(seqIntersection (T,(Partial_Union F))) . E is Event of bool Omega
y is set
(Partial_Union F) . x is Event of I
T /\ ((Partial_Union F) . x) is Event of I
(Partial_Union F) . E is Event of I
T /\ ((Partial_Union F) . 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 ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
(Partial_Union u) . x is Event of I
(seqIntersection (T,(Partial_Union F))) . x is Event of bool Omega
E is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real set
(Partial_Union u) . E is set
(seqIntersection (T,(Partial_Union F))) . 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
(Partial_Union u) . (E + 1) is set
(seqIntersection (T,(Partial_Union F))) . (E + 1) is set
y 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 ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
(Partial_Union u) . (y + 1) is Event of I
(Partial_Union u) . y is Event of I
u . (y + 1) is Event of I
((Partial_Union u) . y) \/ (u . (y + 1)) is Event of I
(Partial_Union F) . y is Event of I
T /\ ((Partial_Union F) . y) is Event of I
(T /\ ((Partial_Union F) . y)) \/ (u . (y + 1)) is Event of I
F . (y + 1) is Event of I
T /\ (F . (y + 1)) is Event of I
(T /\ ((Partial_Union F) . y)) \/ (T /\ (F . (y + 1))) is Event of I
((Partial_Union F) . y) \/ (F . (y + 1)) is Event of I
T /\ (((Partial_Union F) . y) \/ (F . (y + 1))) is Event of I
(Partial_Union F) . (y + 1) is Event of I
T /\ ((Partial_Union F) . (y + 1)) is Event of I
(seqIntersection (T,(Partial_Union F))) . (y + 1) is Event of bool Omega
(Partial_Union u) . 0 is Event of I
u . 0 is Event of I
F . 0 is Event of I
T /\ (F . 0) is Event of I
(Partial_Union F) . 0 is Event of I
T /\ ((Partial_Union F) . 0) is Event of I
(seqIntersection (T,(Partial_Union F))) . 0 is Event of bool Omega
(Partial_Union u) . 0 is set
(seqIntersection (T,(Partial_Union F))) . 0 is set
Sigma * (seqIntersection (T,(Partial_Union F))) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() Element of bool [:NAT,REAL:]
Sigma * (Partial_Union u) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
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 [:NAT,REAL:]
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 [:NAT,REAL:]
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 [:NAT,REAL:]
Sigma * (Partial_Union F) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Ie (#) (Sigma * (Partial_Union F)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
lim (Sigma * (Partial_Union F)) is ext-real V14() real Element of REAL
Ie * (lim (Sigma * (Partial_Union F))) 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 [:NAT,REAL:]
lim (Sigma * v) is ext-real V14() real Element of REAL
Sigma . (T /\ (Union F)) is ext-real V14() real set
Omega is non empty set
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Omega) is non empty cup-closed intersection_stable diff-closed preBoolean set
I is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
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
bool Omega is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool Omega)
[:NAT,(bool Omega):] is non empty Relation-like set
bool [:NAT,(bool Omega):] is non empty cup-closed intersection_stable diff-closed preBoolean 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)
bool (bool Omega) is non empty cup-closed intersection_stable diff-closed preBoolean set
Union F is Element of bool Omega
rng F is non empty set
union (rng F) is set
T is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
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
u is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
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
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Omega) is non empty cup-closed intersection_stable diff-closed preBoolean set
I is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
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
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Omega) is non empty cup-closed intersection_stable diff-closed preBoolean set
I is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
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
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Omega) is non empty cup-closed intersection_stable diff-closed preBoolean set
I is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
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
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Omega) is non empty cup-closed intersection_stable diff-closed preBoolean set
I is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
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
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Omega) is non empty cup-closed intersection_stable diff-closed preBoolean set
I is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
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
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool I) is non empty cup-closed intersection_stable diff-closed preBoolean set
Omega is set
Sigma is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
bool Sigma is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool Sigma)
bool Sigma is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Sigma) is non empty cup-closed intersection_stable diff-closed preBoolean set
[: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))
bool (bool (bool I)) is non empty cup-closed intersection_stable diff-closed preBoolean set
a is set
dom (Omega --> Sigma) is Element of bool Omega
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
F is set
(Omega --> Sigma) . F is set
a is set
(Omega --> Sigma) . a is set
dom (Omega --> Sigma) is Element of bool Omega
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
Omega is non empty set
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Omega) is non empty cup-closed intersection_stable diff-closed preBoolean 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
bool [:P,I:] is non empty cup-closed intersection_stable diff-closed preBoolean set
Omega is non empty set
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Omega) is non empty cup-closed intersection_stable diff-closed preBoolean set
Sigma is set
bool Sigma is non empty cup-closed intersection_stable diff-closed preBoolean set
I is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
bool I is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool I)
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool I) is non empty cup-closed intersection_stable diff-closed preBoolean set
P is Element of bool Sigma
[:P,I:] is Relation-like set
bool [:P,I:] is non empty cup-closed intersection_stable diff-closed preBoolean 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
[:P,{{}}:] is Relation-like RAT -valued INT -valued V33() V34() V35() V36() set
bool [:P,{{}}:] is non empty cup-closed intersection_stable diff-closed preBoolean set
T is set
(P --> {}) . T is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real Relation-like Function-like set
a . T is Element of bool (bool Omega)
dom (P --> {}) is Element of bool P
bool P is non empty cup-closed intersection_stable diff-closed preBoolean set
rng (P --> {}) is V79() V80() V81() V82() V83() V84() Element of bool REAL
T is set
Ie is set
(P --> {}) . Ie is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real Relation-like Function-like set
a . Ie is Element of bool (bool Omega)
Omega is non empty set
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Omega) is non empty cup-closed intersection_stable diff-closed preBoolean set
I is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
P is set
bool I is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool I)
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool I) is non empty cup-closed intersection_stable diff-closed preBoolean set
I is non empty set
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool I) is non empty cup-closed intersection_stable diff-closed preBoolean set
Omega is set
Sigma is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
bool Sigma is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool Sigma)
bool Sigma is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Sigma) is non empty cup-closed intersection_stable diff-closed preBoolean set
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
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
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
Sigma is non empty set
bool Sigma is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Sigma) is non empty cup-closed intersection_stable diff-closed preBoolean set
I is Element of bool Omega
P is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Sigma)
bool P is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool P)
bool P is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool P) is non empty cup-closed intersection_stable diff-closed preBoolean set
[:I,(bool P):] is Relation-like set
bool [:I,(bool P):] is non empty cup-closed intersection_stable diff-closed preBoolean 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
bool Sigma is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool Sigma)
F is set
dom a is Element of bool I
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
T is set
a . T is Element of bool (bool Sigma)
I is non empty set
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool I) is non empty cup-closed intersection_stable diff-closed preBoolean set
Omega is set
Sigma is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
bool Sigma is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool Sigma)
bool Sigma is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Sigma) is non empty cup-closed intersection_stable diff-closed preBoolean set
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
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
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool I) is non empty cup-closed intersection_stable diff-closed preBoolean set
Omega is set
Sigma is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
bool Sigma is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool Sigma)
bool Sigma is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Sigma) is non empty cup-closed intersection_stable diff-closed preBoolean set
bool I is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool I)
bool (bool I) is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool (bool I)) is non empty cup-closed intersection_stable diff-closed preBoolean set
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
P is Relation-like Omega -defined bool Sigma -valued Function-like V26(Omega) V30(Omega, bool Sigma) (Omega,I,Sigma)
bool (bool I) is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool (bool I))
a is set
{} Omega is ext-real empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V33() V34() V35() V36() finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() V81() V82() V83() V84() V85() Element of bool Omega
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
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool I) is non empty cup-closed intersection_stable diff-closed preBoolean set
Omega is set
Sigma is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
bool Sigma is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool Sigma)
bool Sigma is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Sigma) is non empty cup-closed intersection_stable diff-closed preBoolean set
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))
bool I is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool I)
bool (bool I) is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool (bool I)) is non empty cup-closed intersection_stable diff-closed preBoolean set
{} Omega is ext-real empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V33() V34() V35() V36() finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() V81() V82() V83() V84() V85() Element of bool Omega
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean 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)
I is non empty set
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool I) is non empty cup-closed intersection_stable diff-closed preBoolean set
Omega is set
Sigma is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
bool Sigma is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool Sigma)
bool Sigma is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Sigma) is non empty cup-closed intersection_stable diff-closed preBoolean set
bool I is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean 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))
bool (bool I) is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool (bool I)) is non empty cup-closed intersection_stable diff-closed preBoolean set
meet (Omega,I,Sigma,P) is Element of bool (bool I)
I is non empty set
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool I) is non empty cup-closed intersection_stable diff-closed preBoolean set
Omega is set
Sigma is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
bool Sigma is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool Sigma)
bool Sigma is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Sigma) is non empty cup-closed intersection_stable diff-closed preBoolean set
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)
bool I is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool I)
(Omega,I,Sigma,P) is non empty Element of bool (bool (bool I))
bool (bool I) is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool (bool I)) is non empty cup-closed intersection_stable diff-closed preBoolean set
meet (Omega,I,Sigma,P) is Element of bool (bool I)
a is set
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean 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
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Omega) is non empty cup-closed intersection_stable diff-closed preBoolean set
Sigma is non empty set
bool Sigma is non empty cup-closed intersection_stable diff-closed preBoolean set
I is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
bool I is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool I)
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool I) is non empty cup-closed intersection_stable diff-closed preBoolean set
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
bool Omega is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool Omega)
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
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Omega) is non empty cup-closed intersection_stable diff-closed preBoolean set
I is non empty set
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
Sigma is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
bool Sigma is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool Sigma)
bool Sigma is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Sigma) is non empty cup-closed intersection_stable diff-closed preBoolean set
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)
bool (bool Sigma) is non empty cup-closed intersection_stable diff-closed preBoolean set
T is set
dom (I,Omega,Sigma,P,a) is non empty Element of bool a
bool a is non empty cup-closed intersection_stable diff-closed preBoolean set
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
bool [:v,Sigma:] is non empty cup-closed intersection_stable diff-closed preBoolean 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
bool v is non empty finite V52() cup-closed intersection_stable diff-closed preBoolean set
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
Fin T is non empty cup-closed diff-closed preBoolean 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
bool [:T,Sigma:] is non empty cup-closed intersection_stable diff-closed preBoolean 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
bool a is non empty cup-closed intersection_stable diff-closed preBoolean set
(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)
bool (bool Sigma) is non empty cup-closed intersection_stable diff-closed preBoolean set
P . E is Element of bool (bool Omega)
dom Ie is non empty finite Element of bool T
bool T is non empty finite V52() cup-closed intersection_stable diff-closed preBoolean set
(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
Ie | {} is ext-real empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT -defined {} -defined T -defined RAT -valued Sigma -valued Function-like one-to-one constant functional V33() V34() V35() V36() finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() V81() V82() V83() V84() V85() Element of bool [:T,Sigma:]
rng (Ie | {}) is ext-real empty trivial proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V33() V34() V35() V36() V37() V38() V39() V40() with_non-empty_elements finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() V81() V82() V83() V84() V85() Element of bool REAL
meet (rng (Ie | {})) is set
{}. T is ext-real empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V33() V34() V35() V36() finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() V81() V82() V83() V84() V85() Element of Fin T
Ie | ({}. T) is ext-real empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT -defined T -defined {}. T -defined T -defined RAT -valued Sigma -valued Function-like one-to-one constant functional V33() V34() V35() V36() finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() V81() V82() V83() V84() V85() Element of bool [:T,Sigma:]
rng (Ie | ({}. T)) is ext-real empty trivial proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V33() V34() V35() V36() V37() V38() V39() V40() with_non-empty_elements finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() V81() V82() V83() V84() V85() Element of bool Sigma
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
bool [:T,Sigma:] is non empty cup-closed intersection_stable diff-closed preBoolean set
rng (Ie | u) is finite Element of bool Sigma
meet (rng (Ie | u)) is set
Omega is non empty set
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
I is non empty set
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool I) is non empty cup-closed intersection_stable diff-closed preBoolean set
Sigma is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
bool Sigma is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool Sigma)
bool Sigma is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Sigma) is non empty cup-closed intersection_stable diff-closed preBoolean set
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
bool [:x,E2:] is non empty cup-closed intersection_stable diff-closed preBoolean set
E3 is set
[:y,E3:] is Relation-like set
bool [:y,E3:] is non empty cup-closed intersection_stable diff-closed preBoolean set
i is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real set
Seg i is finite V55(i) V79() V80() V81() V82() V83() V84() Element of bool NAT
z is Relation-like Function-like set
dom z is set
rng z is set
[:(Seg i),y:] is Relation-like finite set
bool [:(Seg i),y:] is non empty finite V52() cup-closed intersection_stable diff-closed preBoolean 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
bool [:(Seg i),E3:] is non empty cup-closed intersection_stable diff-closed preBoolean set
rng (S * B9) is finite Element of bool E3
bool E3 is non empty cup-closed intersection_stable diff-closed preBoolean set
rng S is finite Element of bool E3
Ie is set
[:y,Ie:] is Relation-like set
bool [:y,Ie:] is non empty cup-closed intersection_stable diff-closed preBoolean set
f2 is Relation-like y -defined Ie -valued Function-like V30(y,Ie) finite Element of bool [:y,Ie:]
b is Relation-like NAT -defined y -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like FinSequence of y
f2 * b is Relation-like NAT -defined Ie -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Ie
rng b is finite Element of bool y
bool y is non empty finite V52() cup-closed intersection_stable diff-closed preBoolean set
dom f2 is finite Element of bool y
fe2 is Relation-like NAT -defined Ie -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Ie
len fe2 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
len b is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
x \/ y is non empty finite Element of bool Omega
n is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real set
Seg n is finite V55(n) V79() V80() V81() V82() V83() V84() Element of bool NAT
e1 is Relation-like Function-like set
dom e1 is set
rng e1 is set
[:(Seg n),x:] is Relation-like finite set
bool [:(Seg n),x:] is non empty finite V52() cup-closed intersection_stable diff-closed preBoolean 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
bool [:(Seg n),E2:] is non empty cup-closed intersection_stable diff-closed preBoolean set
rng (X * e1) is finite Element of bool E2
bool E2 is non empty cup-closed intersection_stable diff-closed preBoolean set
rng X is finite Element of bool E2
[:x,Ie:] is Relation-like set
bool [:x,Ie:] is non empty cup-closed intersection_stable diff-closed preBoolean set
f1 is Relation-like x -defined Ie -valued Function-like V30(x,Ie) finite Element of bool [:x,Ie:]
e1 is Relation-like NAT -defined x -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like FinSequence of x
f1 * e1 is Relation-like NAT -defined Ie -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Ie
rng e1 is finite Element of bool x
bool x is non empty finite V52() cup-closed intersection_stable diff-closed preBoolean set
dom f1 is finite Element of bool x
fe1 is Relation-like NAT -defined Ie -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Ie
len fe1 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
len e1 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
h is Relation-like Function-like set
dom h is set
e1 ^ b is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom (e1 ^ b) is finite V79() V80() V81() V82() V83() V84() Element of bool NAT
(e1 ^ b) (#) h is Relation-like NAT -defined Function-like finite set
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
fe1 ^ fe2 is Relation-like NAT -defined Ie -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Ie
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
h is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
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
h is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
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
Pfe1 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real set
(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
h is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
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)
P * f1 is Relation-like x -defined REAL -valued Function-like V33() V34() V35() finite Element of bool [:x,REAL:]
[:x,REAL:] is non empty Relation-like V33() V34() V35() set
bool [:x,REAL