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