REAL is non empty V56() V78() V79() V80() V84() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V78() V79() V80() V81() V82() V83() V84() Element of K10(REAL)
K10(REAL) is non empty V25() set
COMPLEX is non empty V56() V78() V84() set
RAT is non empty V56() V78() V79() V80() V81() V84() set
INT is non empty V56() V78() V79() V80() V81() V82() V84() set
K11(COMPLEX,COMPLEX) is non empty V43() set
K10(K11(COMPLEX,COMPLEX)) is non empty V25() set
K11(K11(COMPLEX,COMPLEX),COMPLEX) is non empty V43() set
K10(K11(K11(COMPLEX,COMPLEX),COMPLEX)) is non empty V25() set
K11(REAL,REAL) is non empty V43() V44() V45() set
K10(K11(REAL,REAL)) is non empty V25() set
K11(K11(REAL,REAL),REAL) is non empty V43() V44() V45() set
K10(K11(K11(REAL,REAL),REAL)) is non empty V25() set
K11(RAT,RAT) is non empty RAT -valued V43() V44() V45() set
K10(K11(RAT,RAT)) is non empty V25() set
K11(K11(RAT,RAT),RAT) is non empty RAT -valued V43() V44() V45() set
K10(K11(K11(RAT,RAT),RAT)) is non empty V25() set
K11(INT,INT) is non empty RAT -valued INT -valued V43() V44() V45() set
K10(K11(INT,INT)) is non empty V25() set
K11(K11(INT,INT),INT) is non empty RAT -valued INT -valued V43() V44() V45() set
K10(K11(K11(INT,INT),INT)) is non empty V25() set
K11(NAT,NAT) is non empty RAT -valued INT -valued V43() V44() V45() V46() set
K11(K11(NAT,NAT),NAT) is non empty RAT -valued INT -valued V43() V44() V45() V46() set
K10(K11(K11(NAT,NAT),NAT)) is non empty V25() set
omega is non empty epsilon-transitive epsilon-connected ordinal V78() V79() V80() V81() V82() V83() V84() set
K10(omega) is non empty V25() set
K11(NAT,REAL) is non empty V43() V44() V45() set
K10(K11(NAT,REAL)) is non empty V25() set
K10(K10(REAL)) is non empty V25() set
K10(NAT) is non empty V25() set
K105(NAT) is V27() set
1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
3 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
{} is set
the empty functional ext-real non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V39() real FinSequence-membered V78() V79() V80() V81() V82() V83() V84() set is empty functional ext-real non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V39() real FinSequence-membered V78() V79() V80() V81() V82() V83() V84() set
0 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
dom {} is set
rng {} is set
meet {} is set
addreal is non empty Relation-like K11(REAL,REAL) -defined REAL -valued Function-like V17(K11(REAL,REAL)) V21(K11(REAL,REAL), REAL ) V43() V44() V45() Element of K10(K11(K11(REAL,REAL),REAL))
K415(REAL,addreal) is ext-real V39() real Element of REAL
Omega is ext-real V39() real set
Z is ext-real V39() real set
Z1 is ext-real V39() real set
Z + Z1 is ext-real V39() real Element of REAL
Omega - Z1 is ext-real V39() real Element of REAL
Omega + 0 is ext-real V39() real Element of REAL
Omega is Relation-like NAT -defined Function-like V56() FinSequence-like FinSubsequence-like set
dom Omega is V78() V79() V80() V81() V82() V83() Element of K10(NAT)
len Omega is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
Seg (len Omega) is V56() V63( len Omega) V78() V79() V80() V81() V82() V83() Element of K10(NAT)
{ b1 where b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT : ( 1 <= b1 & b1 <= len Omega ) } is set
Omega is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
Z is Relation-like NAT -defined Function-like V56() FinSequence-like FinSubsequence-like set
dom Z is V78() V79() V80() V81() V82() V83() Element of K10(NAT)
len Z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
Omega is ext-real V39() real set
Z is non empty Relation-like NAT -defined REAL -valued Function-like V17( NAT ) V21( NAT , REAL ) V43() V44() V45() Element of K10(K11(NAT,REAL))
lim Z is ext-real V39() real Element of REAL
Z1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
z is ext-real V39() real set
y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
Y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
Y1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
Z . Y1 is ext-real V39() real Element of REAL
(Z . Y1) - Omega is ext-real V39() real Element of REAL
abs ((Z . Y1) - Omega) is ext-real V39() real Element of REAL
Omega is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
Z is non empty set
K10(Z) is non empty V25() set
K10(K10(Z)) is non empty V25() set
bool Z is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Z))
K11(NAT,(bool Z)) is non empty set
K10(K11(NAT,(bool Z))) is non empty V25() set
Z1 is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Z))
y is non empty Relation-like NAT -defined bool Z -valued Z1 -valued Function-like V17( NAT ) V21( NAT , bool Z) Element of K10(K11(NAT,(bool Z)))
z is non empty Relation-like Z1 -defined REAL -valued Function-like V17(Z1) V21(Z1, REAL ) V43() V44() V45() V52() Probability of Z1
z * y is non empty Relation-like NAT -defined REAL -valued Function-like V17( NAT ) V21( NAT , REAL ) V43() V44() V45() Element of K10(K11(NAT,REAL))
(z * y) . Omega is ext-real V39() real set
y . Omega is set
dom (z * y) is V78() V79() V80() V81() V82() V83() Element of K10(NAT)
z . (y . Omega) is ext-real V39() real set
Omega is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
Z is non empty set
K10(Z) is non empty V25() set
K10(K10(Z)) is non empty V25() set
bool Z is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Z))
K11(NAT,(bool Z)) is non empty set
K10(K11(NAT,(bool Z))) is non empty V25() set
Z1 is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Z))
y is non empty Relation-like NAT -defined bool Z -valued Z1 -valued Function-like V17( NAT ) V21( NAT , bool Z) Element of K10(K11(NAT,(bool Z)))
y . Omega is set
z is non empty Relation-like NAT -defined bool Z -valued Z1 -valued Function-like V17( NAT ) V21( NAT , bool Z) Element of K10(K11(NAT,(bool Z)))
z . Omega is set
Y is non empty Relation-like Z1 -defined REAL -valued Function-like V17(Z1) V21(Z1, REAL ) V43() V44() V45() V52() Probability of Z1
Y * y is non empty Relation-like NAT -defined REAL -valued Function-like V17( NAT ) V21( NAT , REAL ) V43() V44() V45() Element of K10(K11(NAT,REAL))
(Y * y) . Omega is ext-real V39() real set
Y * z is non empty Relation-like NAT -defined REAL -valued Function-like V17( NAT ) V21( NAT , REAL ) V43() V44() V45() Element of K10(K11(NAT,REAL))
(Y * z) . Omega is ext-real V39() real set
rng y is Element of K10(Z1)
K10(Z1) is non empty V25() set
rng z is Element of K10(Z1)
Y . (y . Omega) is ext-real V39() real set
Y . (z . Omega) is ext-real V39() real set
Omega is non empty set
K10(Omega) is non empty V25() set
K10(K10(Omega)) is non empty V25() set
bool Omega is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
K11(NAT,(bool Omega)) is non empty set
K10(K11(NAT,(bool Omega))) is non empty V25() set
Z is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
Z1 is non empty Relation-like NAT -defined bool Omega -valued Z -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
y is non empty Relation-like Z -defined REAL -valued Function-like V17(Z) V21(Z, REAL ) V43() V44() V45() V52() Probability of Z
y * Z1 is non empty Relation-like NAT -defined REAL -valued Function-like V17( NAT ) V21( NAT , REAL ) V43() V44() V45() Element of K10(K11(NAT,REAL))
dom (y * Z1) is V78() V79() V80() V81() V82() V83() Element of K10(NAT)
z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
Y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
Z1 . z is Event of Z
Z1 . Y is Event of Z
(y * Z1) . z is ext-real V39() real Element of REAL
y . (Z1 . z) is ext-real V39() real Element of REAL
(y * Z1) . Y is ext-real V39() real Element of REAL
y . (Z1 . Y) is ext-real V39() real Element of REAL
Omega is non empty set
K10(Omega) is non empty V25() set
K10(K10(Omega)) is non empty V25() set
bool Omega is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
K11(NAT,(bool Omega)) is non empty set
K10(K11(NAT,(bool Omega))) is non empty V25() set
Z is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
Z1 is non empty Relation-like NAT -defined bool Omega -valued Z -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
y is non empty Relation-like Z -defined REAL -valued Function-like V17(Z) V21(Z, REAL ) V43() V44() V45() V52() Probability of Z
y * Z1 is non empty Relation-like NAT -defined REAL -valued Function-like V17( NAT ) V21( NAT , REAL ) V43() V44() V45() Element of K10(K11(NAT,REAL))
dom (y * Z1) is V78() V79() V80() V81() V82() V83() Element of K10(NAT)
z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
Y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
Z1 . Y is Event of Z
Z1 . z is Event of Z
(y * Z1) . z is ext-real V39() real Element of REAL
y . (Z1 . z) is ext-real V39() real Element of REAL
(y * Z1) . Y is ext-real V39() real Element of REAL
y . (Z1 . Y) is ext-real V39() real Element of REAL
Omega is set
bool Omega is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
K10(Omega) is non empty V25() set
K10(K10(Omega)) is non empty V25() set
K11(NAT,(bool Omega)) is non empty set
K10(K11(NAT,(bool Omega))) is non empty V25() set
Z is non empty Relation-like NAT -defined bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
Z . 0 is Event of bool Omega
Z1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
y is Element of K10(Omega)
Z1 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
Z . (Z1 + 1) is Event of bool Omega
y /\ (Z . (Z1 + 1)) is Event of bool Omega
Y1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
z is Element of K10(Omega)
Y is Element of K10(Omega)
Y1 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
Z . (Y1 + 1) is Event of bool Omega
z /\ (Z . (Y1 + 1)) is Event of bool Omega
Z1 is non empty Relation-like NAT -defined bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
Z1 . 0 is Event of bool Omega
y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
y + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
Z1 . (y + 1) is Event of bool Omega
Z1 . y is set
Z . (y + 1) is Event of bool Omega
(Z1 . y) /\ (Z . (y + 1)) is Element of K10(Omega)
z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
Z1 . z is Event of bool Omega
z + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
Z1 . (z + 1) is Event of bool Omega
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
Y is Element of K10(Omega)
Y1 is Element of K10(Omega)
k + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
Z . (k + 1) is Event of bool Omega
Y /\ (Z . (k + 1)) is Event of bool Omega
Z1 is non empty Relation-like NAT -defined bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
Z1 . 0 is Event of bool Omega
y is non empty Relation-like NAT -defined bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
y . 0 is Event of bool Omega
z is set
Z1 . z is set
y . z is set
Y1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
Z1 . Y1 is set
y . Y1 is set
Y1 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
Z1 . (Y1 + 1) is set
y . (Y1 + 1) is set
Z1 . (Y1 + 1) is Event of bool Omega
Z . (Y1 + 1) is Event of bool Omega
(y . Y1) /\ (Z . (Y1 + 1)) is Element of K10(Omega)
y . (Y1 + 1) is Event of bool Omega
Z1 . 0 is set
y . 0 is set
Y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
Z1 . Y is Event of bool Omega
y . Y is Event of bool Omega
Omega is set
bool Omega is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
K10(Omega) is non empty V25() set
K10(K10(Omega)) is non empty V25() set
K11(NAT,(bool Omega)) is non empty set
K10(K11(NAT,(bool Omega))) is non empty V25() set
Z is non empty Relation-like NAT -defined bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
Z . 0 is Event of bool Omega
Z1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
y is Element of K10(Omega)
Z1 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
Z . (Z1 + 1) is Event of bool Omega
y \/ (Z . (Z1 + 1)) is Event of bool Omega
Y1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
z is Element of K10(Omega)
Y is Element of K10(Omega)
Y1 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
Z . (Y1 + 1) is Event of bool Omega
z \/ (Z . (Y1 + 1)) is Event of bool Omega
Z1 is non empty Relation-like NAT -defined bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
Z1 . 0 is Event of bool Omega
y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
y + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
Z1 . (y + 1) is Event of bool Omega
Z1 . y is set
Z . (y + 1) is Event of bool Omega
(Z1 . y) \/ (Z . (y + 1)) is set
z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
Z1 . z is Event of bool Omega
z + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
Z1 . (z + 1) is Event of bool Omega
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
Y is Element of K10(Omega)
Y1 is Element of K10(Omega)
k + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
Z . (k + 1) is Event of bool Omega
Y \/ (Z . (k + 1)) is Event of bool Omega
Z1 is non empty Relation-like NAT -defined bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
Z1 . 0 is Event of bool Omega
y is non empty Relation-like NAT -defined bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
y . 0 is Event of bool Omega
z is set
Z1 . z is set
y . z is set
Y1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
Z1 . Y1 is set
y . Y1 is set
Y1 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
Z1 . (Y1 + 1) is set
y . (Y1 + 1) is set
Z1 . (Y1 + 1) is Event of bool Omega
Z . (Y1 + 1) is Event of bool Omega
(y . Y1) \/ (Z . (Y1 + 1)) is set
y . (Y1 + 1) is Event of bool Omega
Z1 . 0 is set
y . 0 is set
Y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
Z1 . Y is Event of bool Omega
y . Y is Event of bool Omega
Omega is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
Z is set
bool Z is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Z))
K10(Z) is non empty V25() set
K10(K10(Z)) is non empty V25() set
K11(NAT,(bool Z)) is non empty set
K10(K11(NAT,(bool Z))) is non empty V25() set
Z1 is non empty Relation-like NAT -defined bool Z -valued Function-like V17( NAT ) V21( NAT , bool Z) Element of K10(K11(NAT,(bool Z)))
(Z,Z1) is non empty Relation-like NAT -defined bool Z -valued Function-like V17( NAT ) V21( NAT , bool Z) Element of K10(K11(NAT,(bool Z)))
(Z,Z1) . Omega is set
Z1 . Omega is set
y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
y + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
y + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
(Z,Z1) . (y + 1) is Event of bool Z
(Z,Z1) . y is set
Z1 . (y + 1) is Event of bool Z
((Z,Z1) . y) /\ (Z1 . (y + 1)) is Element of K10(Z)
Omega is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
Z is set
bool Z is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Z))
K10(Z) is non empty V25() set
K10(K10(Z)) is non empty V25() set
K11(NAT,(bool Z)) is non empty set
K10(K11(NAT,(bool Z))) is non empty V25() set
Z1 is non empty Relation-like NAT -defined bool Z -valued Function-like V17( NAT ) V21( NAT , bool Z) Element of K10(K11(NAT,(bool Z)))
Z1 . Omega is set
(Z,Z1) is non empty Relation-like NAT -defined bool Z -valued Function-like V17( NAT ) V21( NAT , bool Z) Element of K10(K11(NAT,(bool Z)))
(Z,Z1) . Omega is set
y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
y + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
y + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
(Z,Z1) . (y + 1) is Event of bool Z
(Z,Z1) . y is set
Z1 . (y + 1) is Event of bool Z
((Z,Z1) . y) \/ (Z1 . (y + 1)) is set
Omega is set
bool Omega is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
K10(Omega) is non empty V25() set
K10(K10(Omega)) is non empty V25() set
K11(NAT,(bool Omega)) is non empty set
K10(K11(NAT,(bool Omega))) is non empty V25() set
Z is non empty Relation-like NAT -defined bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
(Omega,Z) is non empty Relation-like NAT -defined bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
Z1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
Z1 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
(Omega,Z) . (Z1 + 1) is Event of bool Omega
(Omega,Z) . Z1 is Event of bool Omega
Z . (Z1 + 1) is Event of bool Omega
((Omega,Z) . Z1) /\ (Z . (Z1 + 1)) is Event of bool Omega
Omega is set
bool Omega is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
K10(Omega) is non empty V25() set
K10(K10(Omega)) is non empty V25() set
K11(NAT,(bool Omega)) is non empty set
K10(K11(NAT,(bool Omega))) is non empty V25() set
Z is non empty Relation-like NAT -defined bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
(Omega,Z) is non empty Relation-like NAT -defined bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
Z1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
Z1 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
(Omega,Z) . (Z1 + 1) is Event of bool Omega
(Omega,Z) . Z1 is Event of bool Omega
Z . (Z1 + 1) is Event of bool Omega
((Omega,Z) . Z1) \/ (Z . (Z1 + 1)) is Event of bool Omega
Omega is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
Z is set
bool Z is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Z))
K10(Z) is non empty V25() set
K10(K10(Z)) is non empty V25() set
K11(NAT,(bool Z)) is non empty set
K10(K11(NAT,(bool Z))) is non empty V25() set
Z1 is set
y is non empty Relation-like NAT -defined bool Z -valued Function-like V17( NAT ) V21( NAT , bool Z) Element of K10(K11(NAT,(bool Z)))
(Z,y) is non empty Relation-like NAT -defined bool Z -valued Function-like V17( NAT ) V21( NAT , bool Z) Element of K10(K11(NAT,(bool Z)))
(Z,y) . Omega is set
z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
(Z,y) . z is set
z + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
(Z,y) . (z + 1) is set
y . (z + 1) is Event of bool Z
Y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
y . Y is set
(Z,y) . (z + 1) is Event of bool Z
((Z,y) . z) /\ (y . (z + 1)) is Element of K10(Z)
Y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
y . Y is set
z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
y . z is set
(Z,y) . z is set
z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
y . z is set
(Z,y) . 0 is set
y . 0 is Event of bool Z
Omega is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
Z is set
bool Z is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Z))
K10(Z) is non empty V25() set
K10(K10(Z)) is non empty V25() set
K11(NAT,(bool Z)) is non empty set
K10(K11(NAT,(bool Z))) is non empty V25() set
Z1 is set
y is non empty Relation-like NAT -defined bool Z -valued Function-like V17( NAT ) V21( NAT , bool Z) Element of K10(K11(NAT,(bool Z)))
(Z,y) is non empty Relation-like NAT -defined bool Z -valued Function-like V17( NAT ) V21( NAT , bool Z) Element of K10(K11(NAT,(bool Z)))
(Z,y) . Omega is set
z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
(Z,y) . z is set
z + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
(Z,y) . (z + 1) is set
(Z,y) . (z + 1) is Event of bool Z
y . (z + 1) is Event of bool Z
((Z,y) . z) \/ (y . (z + 1)) is set
Y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
y . Y is set
Y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
y . Y is set
Y1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
y . Y1 is set
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
y . k is set
(Z,y) . 0 is set
(Z,y) . 0 is Event of bool Z
y . 0 is set
z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
y . z is set
(Z,y) . z is set
Omega is set
bool Omega is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
K10(Omega) is non empty V25() set
K10(K10(Omega)) is non empty V25() set
K11(NAT,(bool Omega)) is non empty set
K10(K11(NAT,(bool Omega))) is non empty V25() set
Z is non empty Relation-like NAT -defined bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
(Omega,Z) is non empty Relation-like NAT -defined bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
Intersection (Omega,Z) is Element of K10(Omega)
Intersection Z is Element of K10(Omega)
Z1 is set
y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
Z . y is Event of bool Omega
(Omega,Z) . y is Event of bool Omega
Z1 is set
y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
(Omega,Z) . y is Event of bool Omega
z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
Z . z is set
Omega is set
bool Omega is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
K10(Omega) is non empty V25() set
K10(K10(Omega)) is non empty V25() set
K11(NAT,(bool Omega)) is non empty set
K10(K11(NAT,(bool Omega))) is non empty V25() set
Z is non empty Relation-like NAT -defined bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
(Omega,Z) is non empty Relation-like NAT -defined bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
Union (Omega,Z) is Element of K10(Omega)
Union Z is Element of K10(Omega)
Z1 is set
y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
(Omega,Z) . y is Event of bool Omega
z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
Z . z is set
Z1 is set
y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
Z . y is Event of bool Omega
(Omega,Z) . y is Event of bool Omega
Omega is set
bool Omega is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
K10(Omega) is non empty V25() set
K10(K10(Omega)) is non empty V25() set
K11(NAT,(bool Omega)) is non empty set
K10(K11(NAT,(bool Omega))) is non empty V25() set
Z is non empty Relation-like NAT -defined bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
Z . 0 is Event of bool Omega
(Omega,Z) is non empty Relation-like NAT -defined bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
z is Element of K10(Omega)
y + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
Z . (y + 1) is Event of bool Omega
(Omega,Z) . y is Event of bool Omega
(Z . (y + 1)) \ ((Omega,Z) . y) is Event of bool Omega
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
Y is Element of K10(Omega)
Y1 is Element of K10(Omega)
k + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
Z . (k + 1) is Event of bool Omega
(Omega,Z) . k is set
(Z . (k + 1)) \ ((Omega,Z) . k) is Element of K10(Omega)
y is non empty Relation-like NAT -defined bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
y . 0 is Event of bool Omega
z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
z + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
y . (z + 1) is Event of bool Omega
Z . (z + 1) is Event of bool Omega
(Omega,Z) . z is set
(Z . (z + 1)) \ ((Omega,Z) . z) is Element of K10(Omega)
Y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
y . Y is Event of bool Omega
Y + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
y . (Y + 1) is Event of bool Omega
i is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
Y1 is Element of K10(Omega)
k is Element of K10(Omega)
i + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
Z . (i + 1) is Event of bool Omega
(Omega,Z) . i is set
(Z . (i + 1)) \ ((Omega,Z) . i) is Element of K10(Omega)
Z1 is non empty Relation-like NAT -defined bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
Z1 . 0 is Event of bool Omega
y is non empty Relation-like NAT -defined bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
y . 0 is Event of bool Omega
z is set
Z1 . z is set
y . z is set
Y1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
Z1 . Y1 is set
y . Y1 is set
Y1 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
Z1 . (Y1 + 1) is set
y . (Y1 + 1) is set
Z1 . (Y1 + 1) is Event of bool Omega
Z . (Y1 + 1) is Event of bool Omega
(Omega,Z) . Y1 is set
(Z . (Y1 + 1)) \ ((Omega,Z) . Y1) is Element of K10(Omega)
y . (Y1 + 1) is Event of bool Omega
Z1 . 0 is set
y . 0 is set
Y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
Z1 . Y is Event of bool Omega
y . Y is Event of bool Omega
Omega is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
Z is set
bool Z is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Z))
K10(Z) is non empty V25() set
K10(K10(Z)) is non empty V25() set
K11(NAT,(bool Z)) is non empty set
K10(K11(NAT,(bool Z))) is non empty V25() set
Z1 is set
y is non empty Relation-like NAT -defined bool Z -valued Function-like V17( NAT ) V21( NAT , bool Z) Element of K10(K11(NAT,(bool Z)))
(Z,y) is non empty Relation-like NAT -defined bool Z -valued Function-like V17( NAT ) V21( NAT , bool Z) Element of K10(K11(NAT,(bool Z)))
(Z,y) . Omega is set
y . Omega is set
z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
y . z is set
z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
z + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
z + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
y . (z + 1) is Event of bool Z
(Z,y) is non empty Relation-like NAT -defined bool Z -valued Function-like V17( NAT ) V21( NAT , bool Z) Element of K10(K11(NAT,(bool Z)))
(Z,y) . z is set
(y . (z + 1)) \ ((Z,y) . z) is Element of K10(Z)
Y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
y . Y is set
Y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
y . Y is set
z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
y . z is set
Y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
Y + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
z + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
z + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
Y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
y . Y is set
(Z,y) is non empty Relation-like NAT -defined bool Z -valued Function-like V17( NAT ) V21( NAT , bool Z) Element of K10(K11(NAT,(bool Z)))
(Z,y) . z is set
y . (z + 1) is Event of bool Z
(y . (z + 1)) \ ((Z,y) . z) is Element of K10(Z)
z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
z + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
Omega is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
Z is set
bool Z is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Z))
K10(Z) is non empty V25() set
K10(K10(Z)) is non empty V25() set
K11(NAT,(bool Z)) is non empty set
K10(K11(NAT,(bool Z))) is non empty V25() set
Z1 is non empty Relation-like NAT -defined bool Z -valued Function-like V17( NAT ) V21( NAT , bool Z) Element of K10(K11(NAT,(bool Z)))
(Z,Z1) is non empty Relation-like NAT -defined bool Z -valued Function-like V17( NAT ) V21( NAT , bool Z) Element of K10(K11(NAT,(bool Z)))
(Z,Z1) . Omega is set
Z1 . Omega is set
y is set
Omega is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
Z is set
bool Z is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Z))
K10(Z) is non empty V25() set
K10(K10(Z)) is non empty V25() set
K11(NAT,(bool Z)) is non empty set
K10(K11(NAT,(bool Z))) is non empty V25() set
Z1 is non empty Relation-like NAT -defined bool Z -valued Function-like V17( NAT ) V21( NAT , bool Z) Element of K10(K11(NAT,(bool Z)))
(Z,Z1) is non empty Relation-like NAT -defined bool Z -valued Function-like V17( NAT ) V21( NAT , bool Z) Element of K10(K11(NAT,(bool Z)))
(Z,Z1) . Omega is set
(Z,Z1) is non empty Relation-like NAT -defined bool Z -valued Function-like V17( NAT ) V21( NAT , bool Z) Element of K10(K11(NAT,(bool Z)))
(Z,Z1) . Omega is set
Z1 . Omega is set
Omega is set
bool Omega is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
K10(Omega) is non empty V25() set
K10(K10(Omega)) is non empty V25() set
K11(NAT,(bool Omega)) is non empty set
K10(K11(NAT,(bool Omega))) is non empty V25() set
Z is non empty Relation-like NAT -defined bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
(Omega,Z) is non empty Relation-like NAT -defined bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
(Omega,(Omega,Z)) is non empty Relation-like NAT -defined bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
(Omega,Z) is non empty Relation-like NAT -defined bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
(Omega,(Omega,Z)) . y is set
(Omega,Z) . y is set
y + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
(Omega,(Omega,Z)) . (y + 1) is set
(Omega,Z) . (y + 1) is set
(Omega,(Omega,Z)) . y is Event of bool Omega
(Omega,Z) . y is Event of bool Omega
(Omega,(Omega,Z)) . (y + 1) is Event of bool Omega
(Omega,Z) . (y + 1) is Event of bool Omega
((Omega,Z) . (y + 1)) \/ ((Omega,(Omega,Z)) . y) is Event of bool Omega
Z . (y + 1) is Event of bool Omega
(Z . (y + 1)) \ ((Omega,Z) . y) is Event of bool Omega
((Z . (y + 1)) \ ((Omega,Z) . y)) \/ ((Omega,Z) . y) is Event of bool Omega
(Z . (y + 1)) \/ ((Omega,Z) . y) is Event of bool Omega
(Omega,Z) . (y + 1) is Event of bool Omega
(Omega,(Omega,Z)) . 0 is Event of bool Omega
(Omega,Z) . 0 is Event of bool Omega
Z . 0 is Event of bool Omega
(Omega,Z) . 0 is Event of bool Omega
(Omega,(Omega,Z)) . 0 is set
(Omega,Z) . 0 is set
Omega is set
bool Omega is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
K10(Omega) is non empty V25() set
K10(K10(Omega)) is non empty V25() set
K11(NAT,(bool Omega)) is non empty set
K10(K11(NAT,(bool Omega))) is non empty V25() set
Z is non empty Relation-like NAT -defined bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
(Omega,Z) is non empty Relation-like NAT -defined bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
Union (Omega,Z) is Element of K10(Omega)
Union Z is Element of K10(Omega)
(Omega,(Omega,Z)) is non empty Relation-like NAT -defined bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
Union (Omega,(Omega,Z)) is Element of K10(Omega)
(Omega,Z) is non empty Relation-like NAT -defined bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
Union (Omega,Z) is Element of K10(Omega)
Omega is set
bool Omega is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
K10(Omega) is non empty V25() set
K10(K10(Omega)) is non empty V25() set
K11(NAT,(bool Omega)) is non empty set
K10(K11(NAT,(bool Omega))) is non empty V25() set
Z is non empty Relation-like NAT -defined bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
Z1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
Z . Z1 is set
Z . y is set
Z1 is set
y is set
dom Z is V78() V79() V80() V81() V82() V83() Element of K10(NAT)
Z . Z1 is set
Z . y is set
dom Z is V78() V79() V80() V81() V82() V83() Element of K10(NAT)
Z . Z1 is set
Z . y is set
dom Z is V78() V79() V80() V81() V82() V83() Element of K10(NAT)
Omega is set
bool Omega is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
K10(Omega) is non empty V25() set
K10(K10(Omega)) is non empty V25() set
K11(NAT,(bool Omega)) is non empty set
K10(K11(NAT,(bool Omega))) is non empty V25() set
Z is non empty Relation-like NAT -defined bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
(Omega,Z) is non empty Relation-like NAT -defined bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
Z1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
(Omega,Z) . Z1 is set
y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
(Omega,Z) . y is set
z is set
Z . Z1 is set
Z . y is set
Omega is set
K10(Omega) is non empty V25() set
K10(K10(Omega)) is non empty V25() set
Z is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
bool Omega is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
K11(NAT,(bool Omega)) is non empty set
K10(K11(NAT,(bool Omega))) is non empty V25() set
Z1 is non empty Relation-like NAT -defined Z -valued bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
(Omega,Z1) is non empty Relation-like NAT -defined bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
(Omega,Z1) . y is set
y + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
(Omega,Z1) . (y + 1) is set
Z1 . (y + 1) is Event of Z
((Omega,Z1) . y) /\ (Z1 . (y + 1)) is Element of K10(Omega)
Z1 . 0 is Event of Z
rng Z1 is Element of K10(Z)
K10(Z) is non empty V25() set
(Omega,Z1) . 0 is Event of bool Omega
(Omega,Z1) . 0 is set
rng (Omega,Z1) is Element of K10((bool Omega))
K10((bool Omega)) is non empty V25() set
Omega is set
K10(Omega) is non empty V25() set
K10(K10(Omega)) is non empty V25() set
Z is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
bool Omega is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
K11(NAT,(bool Omega)) is non empty set
K10(K11(NAT,(bool Omega))) is non empty V25() set
Z1 is non empty Relation-like NAT -defined Z -valued bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
(Omega,Z1) is non empty Relation-like NAT -defined bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
(Omega,Z1) . y is set
y + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
(Omega,Z1) . (y + 1) is set
Z1 . (y + 1) is Event of Z
((Omega,Z1) . y) \/ (Z1 . (y + 1)) is set
Z1 . 0 is Event of Z
rng Z1 is Element of K10(Z)
K10(Z) is non empty V25() set
(Omega,Z1) . 0 is Event of bool Omega
(Omega,Z1) . 0 is set
rng (Omega,Z1) is Element of K10((bool Omega))
K10((bool Omega)) is non empty V25() set
Omega is set
K10(Omega) is non empty V25() set
K10(K10(Omega)) is non empty V25() set
Z is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
bool Omega is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
K11(NAT,(bool Omega)) is non empty set
K10(K11(NAT,(bool Omega))) is non empty V25() set
Z1 is non empty Relation-like NAT -defined Z -valued bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
(Omega,Z1) is non empty Relation-like NAT -defined bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) disjoint_valued Element of K10(K11(NAT,(bool Omega)))
Z1 . 0 is Event of Z
rng Z1 is Element of K10(Z)
K10(Z) is non empty V25() set
(Omega,Z1) . 0 is Event of bool Omega
y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
(Omega,Z1) . y is set
z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
z + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
z + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
Y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
Y + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
Z1 . (Y + 1) is Event of Z
(Omega,Z1) is non empty Relation-like NAT -defined Z -valued bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
(Omega,Z1) . Y is Event of Z
(Z1 . (Y + 1)) \ ((Omega,Z1) . Y) is Event of Z
z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
z + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
rng (Omega,Z1) is Element of K10((bool Omega))
K10((bool Omega)) is non empty V25() set
Omega is set
K10(Omega) is non empty V25() set
K10(K10(Omega)) is non empty V25() set
Z is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
bool Omega is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
K11(NAT,(bool Omega)) is non empty set
K10(K11(NAT,(bool Omega))) is non empty V25() set
Z1 is non empty Relation-like NAT -defined Z -valued bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
y is non empty Relation-like NAT -defined Z -valued bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
(Omega,y) is non empty Relation-like NAT -defined Z -valued bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
Z1 . 0 is Event of Z
y . 0 is Event of Z
z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
z + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
Z1 . (z + 1) is Event of Z
Z1 . z is set
y . (z + 1) is Event of Z
(Z1 . z) /\ (y . (z + 1)) is Element of K10(Omega)
Omega is set
K10(Omega) is non empty V25() set
K10(K10(Omega)) is non empty V25() set
Z is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
bool Omega is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
K11(NAT,(bool Omega)) is non empty set
K10(K11(NAT,(bool Omega))) is non empty V25() set
Z1 is non empty Relation-like NAT -defined Z -valued bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
y is non empty Relation-like NAT -defined Z -valued bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
(Omega,y) is non empty Relation-like NAT -defined Z -valued bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
Z1 . 0 is Event of Z
y . 0 is Event of Z
z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
z + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
Z1 . (z + 1) is Event of Z
Z1 . z is set
y . (z + 1) is Event of Z
(Z1 . z) \/ (y . (z + 1)) is set
Z is set
K10(Z) is non empty V25() set
K10(K10(Z)) is non empty V25() set
Z1 is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Z))
bool Z is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Z))
K11(NAT,(bool Z)) is non empty set
K10(K11(NAT,(bool Z))) is non empty V25() set
y is non empty Relation-like NAT -defined Z1 -valued bool Z -valued Function-like V17( NAT ) V21( NAT , bool Z) Element of K10(K11(NAT,(bool Z)))
(Z,y) is non empty Relation-like NAT -defined Z1 -valued bool Z -valued Function-like V17( NAT ) V21( NAT , bool Z) Element of K10(K11(NAT,(bool Z)))
Omega is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
(Z,y) . Omega is set
y . Omega is set
Z is set
K10(Z) is non empty V25() set
K10(K10(Z)) is non empty V25() set
Z1 is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Z))
bool Z is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Z))
K11(NAT,(bool Z)) is non empty set
K10(K11(NAT,(bool Z))) is non empty V25() set
y is non empty Relation-like NAT -defined Z1 -valued bool Z -valued Function-like V17( NAT ) V21( NAT , bool Z) Element of K10(K11(NAT,(bool Z)))
Omega is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
y . Omega is set
(Z,y) is non empty Relation-like NAT -defined Z1 -valued bool Z -valued Function-like V17( NAT ) V21( NAT , bool Z) Element of K10(K11(NAT,(bool Z)))
(Z,y) . Omega is set
Z is set
K10(Z) is non empty V25() set
K10(K10(Z)) is non empty V25() set
y is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Z))
bool Z is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Z))
K11(NAT,(bool Z)) is non empty set
K10(K11(NAT,(bool Z))) is non empty V25() set
k is set
K10(k) is non empty V25() set
K10(K10(k)) is non empty V25() set
n is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(k))
bool k is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(k))
K11(NAT,(bool k)) is non empty set
K10(K11(NAT,(bool k))) is non empty V25() set
Z1 is set
z is non empty Relation-like NAT -defined y -valued bool Z -valued Function-like V17( NAT ) V21( NAT , bool Z) Element of K10(K11(NAT,(bool Z)))
(Z,z) is non empty Relation-like NAT -defined y -valued bool Z -valued Function-like V17( NAT ) V21( NAT , bool Z) Element of K10(K11(NAT,(bool Z)))
Omega is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
(Z,z) . Omega is set
Y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
z . Y is set
Y1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
i is set
c11 is non empty Relation-like NAT -defined n -valued bool k -valued Function-like V17( NAT ) V21( NAT , bool k) Element of K10(K11(NAT,(bool k)))
(k,c11) is non empty Relation-like NAT -defined n -valued bool k -valued Function-like V17( NAT ) V21( NAT , bool k) Element of K10(K11(NAT,(bool k)))
(k,c11) . Y1 is set
Z is set
K10(Z) is non empty V25() set
K10(K10(Z)) is non empty V25() set
y is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Z))
bool Z is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Z))
K11(NAT,(bool Z)) is non empty set
K10(K11(NAT,(bool Z))) is non empty V25() set
Y1 is set
K10(Y1) is non empty V25() set
K10(K10(Y1)) is non empty V25() set
i is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Y1))
bool Y1 is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Y1))
K11(NAT,(bool Y1)) is non empty set
K10(K11(NAT,(bool Y1))) is non empty V25() set
Z1 is set
z is non empty Relation-like NAT -defined y -valued bool Z -valued Function-like V17( NAT ) V21( NAT , bool Z) Element of K10(K11(NAT,(bool Z)))
(Z,z) is non empty Relation-like NAT -defined y -valued bool Z -valued Function-like V17( NAT ) V21( NAT , bool Z) Element of K10(K11(NAT,(bool Z)))
Omega is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
(Z,z) . Omega is set
c11 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
Y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
k is set
n is non empty Relation-like NAT -defined i -valued bool Y1 -valued Function-like V17( NAT ) V21( NAT , bool Y1) Element of K10(K11(NAT,(bool Y1)))
n . c11 is set
(Y1,n) is non empty Relation-like NAT -defined i -valued bool Y1 -valued Function-like V17( NAT ) V21( NAT , bool Y1) Element of K10(K11(NAT,(bool Y1)))
(Y1,n) . Y is set
Omega is set
K10(Omega) is non empty V25() set
K10(K10(Omega)) is non empty V25() set
Z is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
bool Omega is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
K11(NAT,(bool Omega)) is non empty set
K10(K11(NAT,(bool Omega))) is non empty V25() set
Z1 is non empty Relation-like NAT -defined Z -valued bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
(Omega,Z1) is non empty Relation-like NAT -defined Z -valued bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
Omega is set
K10(Omega) is non empty V25() set
K10(K10(Omega)) is non empty V25() set
Z is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
bool Omega is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
K11(NAT,(bool Omega)) is non empty set
K10(K11(NAT,(bool Omega))) is non empty V25() set
Z1 is non empty Relation-like NAT -defined Z -valued bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
(Omega,Z1) is non empty Relation-like NAT -defined Z -valued bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
Omega is set
K10(Omega) is non empty V25() set
K10(K10(Omega)) is non empty V25() set
Z is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
bool Omega is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
K11(NAT,(bool Omega)) is non empty set
K10(K11(NAT,(bool Omega))) is non empty V25() set
Z1 is non empty Relation-like NAT -defined Z -valued bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
(Omega,Z1) is non empty Relation-like NAT -defined Z -valued bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
Intersection (Omega,Z1) is Element of K10(Omega)
Intersection Z1 is Element of K10(Omega)
Omega is set
K10(Omega) is non empty V25() set
K10(K10(Omega)) is non empty V25() set
Z is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
bool Omega is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
K11(NAT,(bool Omega)) is non empty set
K10(K11(NAT,(bool Omega))) is non empty V25() set
Z1 is non empty Relation-like NAT -defined Z -valued bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
(Omega,Z1) is non empty Relation-like NAT -defined Z -valued bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
Union (Omega,Z1) is Element of K10(Omega)
Union Z1 is Element of K10(Omega)
Omega is set
K10(Omega) is non empty V25() set
K10(K10(Omega)) is non empty V25() set
Z is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
bool Omega is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
K11(NAT,(bool Omega)) is non empty set
K10(K11(NAT,(bool Omega))) is non empty V25() set
Z1 is non empty Relation-like NAT -defined Z -valued bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
y is non empty Relation-like NAT -defined Z -valued bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
(Omega,y) is non empty Relation-like NAT -defined Z -valued bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) disjoint_valued Element of K10(K11(NAT,(bool Omega)))
Z1 . 0 is Event of Z
y . 0 is Event of Z
z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
z + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
Z1 . (z + 1) is Event of Z
y . (z + 1) is Event of Z
(Omega,y) is non empty Relation-like NAT -defined Z -valued bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
(Omega,y) . z is set
(y . (z + 1)) \ ((Omega,y) . z) is Element of K10(Omega)
Z is set
K10(Z) is non empty V25() set
K10(K10(Z)) is non empty V25() set
y is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Z))
bool Z is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Z))
K11(NAT,(bool Z)) is non empty set
K10(K11(NAT,(bool Z))) is non empty V25() set
k is set
K10(k) is non empty V25() set
K10(K10(k)) is non empty V25() set
n is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(k))
bool k is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(k))
K11(NAT,(bool k)) is non empty set
K10(K11(NAT,(bool k))) is non empty V25() set
Z1 is set
z is non empty Relation-like NAT -defined y -valued bool Z -valued Function-like V17( NAT ) V21( NAT , bool Z) Element of K10(K11(NAT,(bool Z)))
(Z,z) is non empty Relation-like NAT -defined y -valued bool Z -valued Function-like V17( NAT ) V21( NAT , bool Z) disjoint_valued Element of K10(K11(NAT,(bool Z)))
Omega is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
(Z,z) . Omega is set
z . Omega is set
Y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
z . Y is set
i is set
c11 is non empty Relation-like NAT -defined n -valued bool k -valued Function-like V17( NAT ) V21( NAT , bool k) Element of K10(K11(NAT,(bool k)))
Y1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
c11 . Y1 is set
(k,c11) is non empty Relation-like NAT -defined n -valued bool k -valued Function-like V17( NAT ) V21( NAT , bool k) disjoint_valued Element of K10(K11(NAT,(bool k)))
(k,c11) . Y1 is set
Z is set
K10(Z) is non empty V25() set
K10(K10(Z)) is non empty V25() set
Z1 is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Z))
bool Z is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Z))
K11(NAT,(bool Z)) is non empty set
K10(K11(NAT,(bool Z))) is non empty V25() set
y is non empty Relation-like NAT -defined Z1 -valued bool Z -valued Function-like V17( NAT ) V21( NAT , bool Z) Element of K10(K11(NAT,(bool Z)))
(Z,y) is non empty Relation-like NAT -defined Z1 -valued bool Z -valued Function-like V17( NAT ) V21( NAT , bool Z) disjoint_valued Element of K10(K11(NAT,(bool Z)))
Omega is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
(Z,y) . Omega is set
y . Omega is set
Z is set
K10(Z) is non empty V25() set
K10(K10(Z)) is non empty V25() set
Z1 is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Z))
bool Z is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Z))
K11(NAT,(bool Z)) is non empty set
K10(K11(NAT,(bool Z))) is non empty V25() set
y is non empty Relation-like NAT -defined Z1 -valued bool Z -valued Function-like V17( NAT ) V21( NAT , bool Z) Element of K10(K11(NAT,(bool Z)))
(Z,y) is non empty Relation-like NAT -defined Z1 -valued bool Z -valued Function-like V17( NAT ) V21( NAT , bool Z) disjoint_valued Element of K10(K11(NAT,(bool Z)))
Omega is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
(Z,y) . Omega is set
(Z,y) is non empty Relation-like NAT -defined Z1 -valued bool Z -valued Function-like V17( NAT ) V21( NAT , bool Z) Element of K10(K11(NAT,(bool Z)))
(Z,y) . Omega is set
Omega is set
K10(Omega) is non empty V25() set
K10(K10(Omega)) is non empty V25() set
Z is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
bool Omega is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
K11(NAT,(bool Omega)) is non empty set
K10(K11(NAT,(bool Omega))) is non empty V25() set
Z1 is non empty Relation-like NAT -defined Z -valued bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
(Omega,Z1) is non empty Relation-like NAT -defined Z -valued bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) disjoint_valued Element of K10(K11(NAT,(bool Omega)))
(Omega,(Omega,Z1)) is non empty Relation-like NAT -defined Z -valued bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
(Omega,Z1) is non empty Relation-like NAT -defined Z -valued bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
Omega is set
K10(Omega) is non empty V25() set
K10(K10(Omega)) is non empty V25() set
Z is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
bool Omega is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
K11(NAT,(bool Omega)) is non empty set
K10(K11(NAT,(bool Omega))) is non empty V25() set
Z1 is non empty Relation-like NAT -defined Z -valued bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
(Omega,Z1) is non empty Relation-like NAT -defined Z -valued bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) disjoint_valued Element of K10(K11(NAT,(bool Omega)))
Union (Omega,Z1) is Element of K10(Omega)
Union Z1 is Element of K10(Omega)
Omega is non empty set
K10(Omega) is non empty V25() set