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
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)))
(Omega,Z1) is non empty Relation-like NAT -defined bool Omega -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 Z -defined REAL -valued Function-like V17(Z) V21(Z, REAL ) V43() V44() V45() V52() Probability of Z
y * (Omega,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))
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)))
(Omega,Z1) is non empty Relation-like NAT -defined bool Omega -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 Z -defined REAL -valued Function-like V17(Z) V21(Z, REAL ) V43() V44() V45() V52() Probability of Z
y * (Omega,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))
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))
Partial_Sums (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))
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 * Z1) . z 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)))
(Omega,Z1) is non empty Relation-like NAT -defined bool Omega -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 Z -defined REAL -valued Function-like V17(Z) V21(Z, REAL ) V43() V44() V45() V52() Probability of Z
y * (Omega,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))
(y * (Omega,Z1)) . 0 is ext-real V39() real Element of REAL
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))
Partial_Sums (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))
(Partial_Sums (y * Z1)) . 0 is ext-real V39() real Element of REAL
dom (y * Z1) is V78() V79() V80() V81() V82() V83() Element of K10(NAT)
dom (y * (Omega,Z1)) is V78() V79() V80() V81() V82() V83() Element of K10(NAT)
(Omega,Z1) . 0 is Event of Z
y . ((Omega,Z1) . 0) is ext-real V39() real Element of REAL
Z1 . 0 is Event of Z
y . (Z1 . 0) is ext-real V39() real Element of REAL
(y * Z1) . 0 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)))
(Omega,Z1) is non empty Relation-like NAT -defined bool Omega -valued bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
Union Z1 is Element of K10(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 * (Omega,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))
lim (y * (Omega,Z1)) is ext-real V39() real Element of REAL
upper_bound (y * (Omega,Z1)) is ext-real V39() real Element of REAL
y . (Union Z1) is ext-real V39() real set
Union (Omega,Z1) is Element of K10(Omega)
y . (Union (Omega,Z1)) 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)))
(Omega,Z1) is non empty Relation-like NAT -defined bool Omega -valued 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
z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
Z1 . z is set
Y is set
Y1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
Z1 . Y1 is set
(Z1 . Y1) /\ (Z1 . z) is 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)))
(Z,y) is non empty Relation-like NAT -defined bool Z -valued bool Z -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 * (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 * (Z,y)) . Omega is ext-real V39() real set
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))
Partial_Sums (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))
(Partial_Sums (z * y)) . Omega is ext-real V39() real set
dom (z * y) is V78() V79() V80() V81() V82() V83() Element of K10(NAT)
dom (z * (Z,y)) is V78() V79() V80() V81() V82() V83() Element of K10(NAT)
Y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
(z * (Z,y)) . Y is ext-real V39() real set
(Partial_Sums (z * y)) . Y is ext-real 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 * (Z,y)) . (Y + 1) is ext-real V39() real set
(Partial_Sums (z * y)) . (Y + 1) is ext-real V39() real set
(Z,y) . Y is set
y . (Y + 1) is Event of Z1
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
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
(Partial_Sums (z * y)) . (Y1 + 1) is ext-real V39() real Element of REAL
(Partial_Sums (z * y)) . Y1 is ext-real V39() real Element of REAL
(z * y) . (Y1 + 1) is ext-real V39() real Element of REAL
((Partial_Sums (z * y)) . Y1) + ((z * y) . (Y1 + 1)) is ext-real V39() real Element of REAL
y . (Y1 + 1) is Event of Z1
z . (y . (Y1 + 1)) is ext-real V39() real Element of REAL
((Partial_Sums (z * y)) . Y1) + (z . (y . (Y1 + 1))) is ext-real V39() real Element of REAL
(z * (Z,y)) . (Y1 + 1) is ext-real V39() real Element of REAL
(Z,y) . (Y1 + 1) is Event of Z1
z . ((Z,y) . (Y1 + 1)) is ext-real V39() real Element of REAL
(Z,y) . Y1 is Event of Z1
((Z,y) . Y1) \/ (y . (Y1 + 1)) is Event of Z1
z . (((Z,y) . Y1) \/ (y . (Y1 + 1))) is ext-real V39() real Element of REAL
z . ((Z,y) . Y1) is ext-real V39() real Element of REAL
(z . ((Z,y) . Y1)) + (z . (y . (Y1 + 1))) is ext-real V39() real Element of REAL
(z * (Z,y)) . Y1 is ext-real V39() real Element of REAL
((z * (Z,y)) . Y1) + (z . (y . (Y1 + 1))) is ext-real V39() real Element of REAL
(z * (Z,y)) . 0 is ext-real V39() real set
(Partial_Sums (z * y)) . 0 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)))
(Omega,Z1) is non empty Relation-like NAT -defined bool Omega -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 Z -defined REAL -valued Function-like V17(Z) V21(Z, REAL ) V43() V44() V45() V52() Probability of Z
y * (Omega,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))
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))
Partial_Sums (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))
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 * (Omega,Z1)) . z is ext-real V39() real Element of REAL
(Partial_Sums (y * Z1)) . z 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)))
Union Z1 is Element of K10(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))
Partial_Sums (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))
lim (Partial_Sums (y * Z1)) is ext-real V39() real Element of REAL
upper_bound (Partial_Sums (y * Z1)) is ext-real V39() real Element of REAL
y . (Union Z1) is ext-real V39() real set
(Omega,Z1) is non empty Relation-like NAT -defined bool Omega -valued bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
y * (Omega,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))
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)))
Union Z1 is Element of K10(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 . (Union Z1) is ext-real V39() real set
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))
Sum (y * Z1) is ext-real V39() real Element of REAL
Partial_Sums (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))
lim (Partial_Sums (y * Z1)) 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
Z is Relation-like NAT -defined bool Omega -valued Function-like V56() FinSequence-like FinSubsequence-like FinSequence of bool Omega
Z1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
Z . Z1 is set
dom Z is V78() V79() V80() V81() V82() V83() Element of K10(NAT)
dom Z is V78() V79() V80() V81() V82() V83() Element of K10(NAT)
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
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
Z |-> Omega is Relation-like NAT -defined Function-like V56() FinSequence-like FinSubsequence-like set
Seg Z is V56() V63(Z) 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 <= Z ) } is set
K423((Seg Z),Omega) is Relation-like Seg Z -defined {Omega} -valued Function-like V21( Seg Z,{Omega}) Element of K10(K11((Seg Z),{Omega}))
{Omega} is set
K11((Seg Z),{Omega}) is set
K10(K11((Seg Z),{Omega})) is non empty V25() set
dom (Z |-> Omega) is V78() V79() V80() V81() V82() V83() Element of K10(NAT)
rng (Z |-> Omega) is set
y is set
z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
(Z |-> Omega) . z is set
y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
(Z |-> Omega) . y 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
Z is Relation-like NAT -defined bool Omega -valued Function-like V56() FinSequence-like FinSubsequence-like FinSequence of bool Omega
rng Z is Element of K10((bool Omega))
K10((bool Omega)) is non empty V25() set
union (rng 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
Z is Relation-like NAT -defined bool Omega -valued Function-like V56() FinSequence-like FinSubsequence-like FinSequence of bool Omega
Union Z is set
rng Z is Element of K10((bool Omega))
K10((bool Omega)) is non empty V25() set
union (rng 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
Z is set
Z1 is Relation-like NAT -defined bool Omega -valued Function-like V56() FinSequence-like FinSubsequence-like FinSequence of bool Omega
(Omega,Z1) is Element of K10(Omega)
dom Z1 is V78() V79() V80() V81() V82() V83() Element of K10(NAT)
rng Z1 is Element of K10((bool Omega))
K10((bool Omega)) is non empty V25() set
union (rng Z1) is Element of K10(Omega)
z is set
Y is set
Y1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
(Omega,Z1,Y1) is Element of K10(Omega)
Y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
(Omega,Z1,Y) is Element of K10(Omega)
z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
(Omega,Z1,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
Z is Relation-like NAT -defined bool Omega -valued Function-like V56() FinSequence-like FinSubsequence-like FinSequence of bool Omega
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
Z1 is Relation-like NAT -defined bool Omega -valued Function-like V56() FinSequence-like FinSubsequence-like FinSequence of bool Omega
len 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
dom Z1 is V78() V79() V80() V81() V82() V83() Element of K10(NAT)
y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
(Omega,Z1,y) is Element of K10(Omega)
(Omega,Z,y) is Element of K10(Omega)
(Omega,Z,y) ` is Element of K10(Omega)
Z1 is Relation-like NAT -defined bool Omega -valued Function-like V56() FinSequence-like FinSubsequence-like FinSequence of bool Omega
len 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
dom Z1 is V78() V79() V80() V81() V82() V83() Element of K10(NAT)
y is Relation-like NAT -defined bool Omega -valued Function-like V56() FinSequence-like FinSubsequence-like FinSequence of bool Omega
len 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
dom y is V78() V79() V80() V81() V82() V83() Element of K10(NAT)
Seg (len y) is V56() V63( len y) 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 y ) } is set
z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
(Omega,Z1,z) is Element of K10(Omega)
(Omega,y,z) is Element of K10(Omega)
(Omega,Z,z) is Element of K10(Omega)
(Omega,Z,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
Z is Relation-like NAT -defined bool Omega -valued Function-like V56() FinSequence-like FinSubsequence-like FinSequence of bool Omega
(Omega,Z) is Relation-like NAT -defined bool Omega -valued Function-like V56() FinSequence-like FinSubsequence-like FinSequence of bool Omega
(Omega,(Omega,Z)) is Element of K10(Omega)
(Omega,(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
Z is Relation-like NAT -defined bool Omega -valued Function-like V56() FinSequence-like FinSubsequence-like FinSequence of bool Omega
(Omega,Z) is Relation-like NAT -defined bool Omega -valued Function-like V56() FinSequence-like FinSubsequence-like FinSequence of bool Omega
dom (Omega,Z) is V78() V79() V80() V81() V82() V83() Element of K10(NAT)
dom Z is V78() V79() V80() V81() V82() V83() Element of K10(NAT)
len (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
Seg (len (Omega,Z)) is V56() V63( len (Omega,Z)) 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,Z) ) } is set
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
Seg (len Z) is V56() V63( len Z) 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 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
Z is set
Z1 is Relation-like NAT -defined bool Omega -valued Function-like V56() FinSequence-like FinSubsequence-like FinSequence of bool Omega
(Omega,Z1) is Element of K10(Omega)
dom Z1 is V78() V79() V80() V81() V82() V83() Element of K10(NAT)
(Omega,Z1) is Relation-like NAT -defined bool Omega -valued Function-like V56() FinSequence-like FinSubsequence-like FinSequence of bool Omega
y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
(Omega,(Omega,Z1),y) is Element of K10(Omega)
Omega \ (Omega,(Omega,Z1),y) is Element of K10(Omega)
(Omega,Z1,y) is Element of K10(Omega)
dom (Omega,Z1) is V78() V79() V80() V81() V82() V83() Element of K10(NAT)
(Omega,(Omega,Z1),y) ` is Element of K10(Omega)
(Omega,Z1,y) ` is Element of K10(Omega)
((Omega,Z1,y) `) ` is Element of K10(Omega)
y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
(Omega,(Omega,Z1),y) is Element of K10(Omega)
Omega \ (Omega,(Omega,Z1),y) is Element of K10(Omega)
(Omega,Z1,y) 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
(Omega,Z1,y) is Element of K10(Omega)
(Omega,(Omega,Z1),y) is Element of K10(Omega)
Omega \ (Omega,(Omega,Z1),y) is Element of K10(Omega)
y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
(Omega,(Omega,Z1),y) is Element of K10(Omega)
z is set
dom (Omega,Z1) is V78() V79() V80() V81() V82() V83() Element of K10(NAT)
(Omega,(Omega,Z1)) is Element of K10(Omega)
y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
(Omega,(Omega,Z1),y) is Element of K10(Omega)
(Omega,(Omega,Z1)) ` is Element of K10(Omega)
Omega \ (Omega,(Omega,Z1)) is Element of K10(Omega)
y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
(Omega,Z1,y) is Element of K10(Omega)
z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
(Omega,(Omega,Z1),z) is Element of K10(Omega)
Y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
(Omega,(Omega,Z1),Y) is Element of K10(Omega)
Y1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
(Omega,Z1,Y1) 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
Z is set
Z1 is Relation-like NAT -defined bool Omega -valued Function-like V56() FinSequence-like FinSubsequence-like FinSequence of bool Omega
rng Z1 is Element of K10((bool Omega))
K10((bool Omega)) is non empty V25() set
meet (rng Z1) is Element of K10(Omega)
dom Z1 is V78() V79() V80() V81() V82() V83() Element of K10(NAT)
y is set
z is set
Y is set
Z1 . Y is set
y is set
z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
(Omega,Z1,z) is Element of K10(Omega)
z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
(Omega,Z1,z) is Element of K10(Omega)
y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
(Omega,Z1,y) 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
Z is Relation-like NAT -defined bool Omega -valued Function-like V56() FinSequence-like FinSubsequence-like FinSequence of bool Omega
(Omega,Z) is Element of K10(Omega)
rng Z is Element of K10((bool Omega))
K10((bool Omega)) is non empty V25() set
meet (rng Z) is Element of K10(Omega)
Z1 is set
dom Z is V78() V79() V80() V81() V82() V83() Element of K10(NAT)
y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
(Omega,Z,y) is Element of K10(Omega)
y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
(Omega,Z,y) 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 Relation-like NAT -defined bool Omega -valued Function-like V56() FinSequence-like FinSubsequence-like FinSequence of bool Omega
dom Z is V78() V79() V80() V81() V82() V83() Element of K10(NAT)
Z1 is Relation-like Function-like set
dom Z1 is set
Z1 is Relation-like Function-like set
dom Z1 is set
y is set
Z . y is set
rng Z is Element of K10((bool Omega))
K10((bool Omega)) is non empty V25() set
y is set
Z1 . y is set
Z . y is set
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)))
z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
y . z is set
(Omega,Z,z) is Element of K10(Omega)
z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
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 Relation-like NAT -defined bool Omega -valued Function-like V56() FinSequence-like FinSubsequence-like FinSequence of bool Omega
dom Z is V78() V79() V80() V81() V82() V83() Element of K10(NAT)
(Omega,Z) 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
Union Z1 is Element of K10(Omega)
y 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
(Omega,Z,z) is Element of K10(Omega)
y is set
z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
(Omega,Z,z) is Element of K10(Omega)
Z1 . z 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))
Z1 is Relation-like NAT -defined Z -valued Function-like V56() FinSequence-like FinSubsequence-like FinSequence of Z
rng Z1 is Element of K10(Z)
K10(Z) is non empty V25() set
Omega is 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))
Z is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
Z1 is Relation-like NAT -defined bool Omega -valued Function-like V56() FinSequence-like FinSubsequence-like (Omega,Z)
y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
Z1 . y is set
dom Z1 is V78() V79() V80() V81() V82() V83() Element of K10(NAT)
dom Z1 is V78() V79() V80() V81() V82() V83() Element of K10(NAT)
(Omega,Z1,y) is Element of K10(Omega)
dom Z1 is V78() V79() V80() V81() V82() V83() Element of K10(NAT)
Omega is 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 Relation-like NAT -defined bool Omega -valued Function-like V56() FinSequence-like FinSubsequence-like (Omega,Z)
dom Z1 is V78() V79() V80() V81() V82() V83() Element of K10(NAT)
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)))
z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
y . z is set
(Omega,Z,Z1,z) is Event of Z
rng y is Element of K10((bool Omega))
K10((bool Omega)) is non empty V25() set
z 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 ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
z . Y is set
(Omega,Z,Z1,Y) is Event of Z
Y1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
z . Y1 is set
Omega is 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))
Z is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
Z1 is Relation-like NAT -defined bool Omega -valued Function-like V56() FinSequence-like FinSubsequence-like (Omega,Z)
(Omega,Z1) is Element of K10(Omega)
K11(NAT,(bool Omega)) is non empty set
K10(K11(NAT,(bool Omega))) is non empty V25() set
dom Z1 is V78() V79() V80() V81() V82() V83() Element of K10(NAT)
y 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)))
Union y is Element of K10(Omega)
Omega is 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))
Z is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
Z1 is Relation-like NAT -defined bool Omega -valued Function-like V56() FinSequence-like FinSubsequence-like (Omega,Z)
(Omega,Z1) is Relation-like NAT -defined bool Omega -valued Function-like V56() FinSequence-like FinSubsequence-like FinSequence of bool Omega
z is set
rng (Omega,Z1) is set
rng (Omega,Z1) is Element of K10((bool Omega))
K10((bool Omega)) is non empty V25() set
dom (Omega,Z1) is V78() V79() V80() V81() V82() V83() Element of K10(NAT)
Y is set
(Omega,Z1) . Y is set
Y1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
(Omega,(bool Omega),(Omega,Z1),Y1) is Event of bool Omega
(Omega,Z,Z1,Y1) is Event of Z
(Omega,Z,Z1,Y1) ` is Element of K10(Omega)
Omega is 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))
Z is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
Z1 is Relation-like NAT -defined bool Omega -valued Function-like V56() FinSequence-like FinSubsequence-like (Omega,Z)
(Omega,Z1) is Element of K10(Omega)
(Omega,Z1) is Relation-like NAT -defined Z -valued bool Omega -valued Function-like V56() FinSequence-like FinSubsequence-like FinSequence of bool Omega
rng (Omega,Z1) is Element of K10(Z)
K10(Z) is non empty V25() set
y is Relation-like NAT -defined bool Omega -valued Function-like V56() FinSequence-like FinSubsequence-like (Omega,Z)
(Omega,y) is Element of K10(Omega)
(Omega,(Omega,Z1)) is Element of K10(Omega)
(Omega,(Omega,Z1)) ` is Element of K10(Omega)
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))
Z is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
Z1 is non empty Relation-like Z -defined REAL -valued Function-like V17(Z) V21(Z, REAL ) V43() V44() V45() V52() Probability of Z
y is Relation-like NAT -defined bool Omega -valued Function-like V56() FinSequence-like FinSubsequence-like (Omega,Z)
Z1 * y is Relation-like NAT -defined REAL -valued Function-like V43() V44() V45() Element of K10(K11(NAT,REAL))
dom (Z1 * y) is V78() V79() V80() V81() V82() V83() Element of K10(NAT)
dom y is V78() V79() V80() V81() V82() V83() Element of K10(NAT)
z 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,Y) is Event of Z
dom Z1 is Element of K10(Z)
K10(Z) is non empty V25() 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))
Z is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
Z1 is non empty Relation-like Z -defined REAL -valued Function-like V17(Z) V21(Z, REAL ) V43() V44() V45() V52() Probability of Z
y is Relation-like NAT -defined bool Omega -valued Function-like V56() FinSequence-like FinSubsequence-like (Omega,Z)
Z1 * y is Relation-like NAT -defined REAL -valued Function-like V43() V44() V45() Element of K10(K11(NAT,REAL))
dom (Z1 * y) is V78() V79() V80() V81() V82() V83() Element of K10(NAT)
dom y is V78() V79() V80() V81() V82() V83() Element of K10(NAT)
Y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
Seg Y is V56() V63(Y) 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 <= Y ) } is set
rng (Z1 * y) is V78() V79() V80() Element of K10(REAL)
z is Relation-like NAT -defined Function-like V56() FinSequence-like FinSubsequence-like set
rng z is 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))
Z is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
Z1 is Relation-like NAT -defined bool Omega -valued Function-like V56() FinSequence-like FinSubsequence-like (Omega,Z)
y is non empty Relation-like Z -defined REAL -valued Function-like V17(Z) V21(Z, REAL ) V43() V44() V45() V52() Probability of Z
Z1 * y is Relation-like V43() V44() V45() 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))
Z is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
Z1 is non empty Relation-like Z -defined REAL -valued Function-like V17(Z) V21(Z, REAL ) V43() V44() V45() V52() Probability of Z
y is Relation-like NAT -defined bool Omega -valued Function-like V56() FinSequence-like FinSubsequence-like (Omega,Z)
(Omega,Z,y,Z1) is Relation-like NAT -defined REAL -valued Function-like V43() V44() V45() V56() FinSequence-like FinSubsequence-like FinSequence of REAL
len (Omega,Z,y,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
len 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
dom (Omega,Z,y,Z1) is V78() V79() V80() V81() V82() V83() Element of K10(NAT)
dom y is V78() V79() V80() V81() V82() V83() Element of K10(NAT)
Seg (len (Omega,Z,y,Z1)) is V56() V63( len (Omega,Z,y,Z1)) 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,Z,y,Z1) ) } is set
Omega is Relation-like NAT -defined REAL -valued Function-like V43() V44() V45() V56() FinSequence-like FinSubsequence-like FinSequence of REAL
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
Sum Omega is ext-real V39() real Element of REAL
addreal "**" Omega is ext-real V39() real Element of REAL
Omega is Relation-like NAT -defined REAL -valued Function-like V43() V44() V45() V56() FinSequence-like FinSubsequence-like FinSequence of REAL
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
Omega . 1 is ext-real V39() real set
Sum Omega is ext-real V39() real Element of REAL
addreal "**" Omega is ext-real V39() real Element of REAL
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))
Z . 1 is ext-real V39() real Element of REAL
Z . (len Omega) is ext-real V39() real Element of REAL
Z1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
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 ext-real V39() real Element of REAL
Z . Z1 is ext-real V39() real set
Omega . (Z1 + 1) is ext-real V39() real set
(Z . Z1) + (Omega . (Z1 + 1)) is ext-real V39() real Element of REAL
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 ext-real V39() real Element of REAL
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 . (y + 1) is ext-real V39() real set
addreal . ((Z . y),(Omega . (y + 1))) is set
Z1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
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 ext-real V39() real Element of REAL
Z . Z1 is ext-real V39() real set
Omega . (Z1 + 1) is ext-real V39() real set
(Z . Z1) + (Omega . (Z1 + 1)) 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 Z -defined REAL -valued Function-like V17(Z) V21(Z, REAL ) V43() V44() V45() V52() Probability of Z
y is Relation-like NAT -defined bool Omega -valued Function-like V56() FinSequence-like FinSubsequence-like (Omega,Z)
dom y is V78() V79() V80() V81() V82() V83() Element of K10(NAT)
len 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,Z1) is Relation-like NAT -defined REAL -valued Function-like V43() V44() V45() V56() FinSequence-like FinSubsequence-like FinSequence of REAL
Sum (Omega,Z,y,Z1) is ext-real V39() real Element of REAL
z 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)))
Z1 * 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))
Partial_Sums (Z1 * 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))
Sum (Z1 * z) is ext-real V39() real Element of REAL
(Partial_Sums (Z1 * z)) . (len y) is ext-real V39() real Element of REAL
Union z is Element of K10(Omega)
Z1 . (Union z) is ext-real V39() real set
z . 0 is Event of Z
(Z1 * z) . 0 is ext-real V39() real Element of REAL
Z1 . (z . 0) is ext-real V39() real Element of REAL
Y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
(Z1 * z) . Y is ext-real V39() real set
(Omega,Z,y,Z1) . Y is ext-real V39() real set
z . Y is set
Z1 . (z . Y) is ext-real V39() real set
(Omega,Z,y,Y) is Event of Z
Z1 . (Omega,Z,y,Y) is ext-real V39() real Element of REAL
0 + 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
(Partial_Sums (Z1 * z)) . 1 is ext-real V39() real Element of REAL
(Partial_Sums (Z1 * z)) . 0 is ext-real V39() real Element of REAL
(Z1 * z) . 1 is ext-real V39() real Element of REAL
((Partial_Sums (Z1 * z)) . 0) + ((Z1 * z) . 1) is ext-real V39() real Element of REAL
((Z1 * z) . 0) + ((Z1 * z) . 1) is ext-real V39() real Element of REAL
(Omega,Z,y,Z1) . 1 is ext-real V39() real 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
(Partial_Sums (Z1 * z)) . (Y + 1) is ext-real V39() real Element of REAL
(Partial_Sums (Z1 * z)) . Y is ext-real V39() real set
(Omega,Z,y,Z1) . (Y + 1) is ext-real V39() real set
((Partial_Sums (Z1 * z)) . Y) + ((Omega,Z,y,Z1) . (Y + 1)) is ext-real V39() real Element of REAL
Seg (len y) is V56() V63( len y) 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 y ) } is set
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
(Partial_Sums (Z1 * z)) . Y1 is ext-real V39() real Element of REAL
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 * z) . (Y1 + 1) is ext-real V39() real Element of REAL
((Partial_Sums (Z1 * z)) . Y1) + ((Z1 * z) . (Y1 + 1)) is ext-real V39() real Element of REAL
(len 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
Y1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
((len y) + 1) + Y1 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) . (((len y) + 1) + Y1) is ext-real V39() real Element of REAL
z . (((len y) + 1) + Y1) is Event of Z
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
((len y) + 1) + k 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 . (((len y) + 1) + k) is Event of Z
Z1 . (z . (((len y) + 1) + k)) is ext-real V39() real Element of REAL
Y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
((len y) + 1) + Y 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
(Partial_Sums (Z1 * z)) . (((len y) + 1) + Y) is ext-real V39() real Element of REAL
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
((len y) + 1) + (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
(Partial_Sums (Z1 * z)) . (((len y) + 1) + (Y + 1)) is ext-real V39() real Element of REAL
(((len y) + 1) + 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
(Partial_Sums (Z1 * z)) . ((((len y) + 1) + Y) + 1) is ext-real V39() real Element of REAL
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
((len y) + 1) + Y1 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
(Partial_Sums (Z1 * z)) . (((len y) + 1) + Y1) is ext-real V39() real Element of REAL
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
((len y) + 1) + (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 * z) . (((len y) + 1) + (Y1 + 1)) is ext-real V39() real Element of REAL
((Partial_Sums (Z1 * z)) . (((len y) + 1) + Y1)) + ((Z1 * z) . (((len y) + 1) + (Y1 + 1))) is ext-real V39() real Element of REAL
((Partial_Sums (Z1 * z)) . (((len y) + 1) + Y)) + 0 is ext-real V39() real Element of REAL
(Omega,z) is non empty Relation-like NAT -defined bool Omega -valued bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) disjoint_valued 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,z) . Y is Event of Z
z . Y is Event of Z
Z1 * (Omega,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))
(Z1 * (Omega,z)) . Y is ext-real V39() real Element of REAL
(Z1 * z) . Y is ext-real V39() real Element of REAL
Partial_Sums (Z1 * (Omega,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 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
(Partial_Sums (Z1 * (Omega,z))) . Y is ext-real V39() real Element of REAL
(Partial_Sums (Z1 * z)) . Y is ext-real V39() real Element of REAL
((len y) + 1) + 0 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
(Partial_Sums (Z1 * z)) . (((len y) + 1) + 0) is ext-real V39() real Element of REAL
(Z1 * z) . (((len y) + 1) + 0) is ext-real V39() real Element of REAL
((Partial_Sums (Z1 * z)) . (len y)) + ((Z1 * z) . (((len y) + 1) + 0)) is ext-real V39() real Element of REAL
((Partial_Sums (Z1 * z)) . (len y)) + 0 is ext-real V39() real Element of REAL
Y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
(Partial_Sums (Z1 * z)) . Y is ext-real V39() real set
Y1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
((len y) + 1) + Y1 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
lim (Partial_Sums (Z1 * z)) is ext-real V39() real Element of REAL
len (Omega,Z,y,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
len (Omega,Z,y,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 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 . 1 is ext-real V39() real Element of REAL
Y . (len (Omega,Z,y,Z1)) is ext-real V39() real Element of REAL
(Partial_Sums (Z1 * z)) . (len (Omega,Z,y,Z1)) is ext-real V39() real Element of REAL
Y1 is set
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
k 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 . k is ext-real V39() real Element of REAL
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real V41() V42() V78() V79() V80() V81() V82() V83() Element of NAT
k 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 . k is ext-real V39() real Element of REAL
k 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 . k is ext-real V39() real Element of REAL
i is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
Y . i is ext-real V39() real set
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
Y . n is ext-real V39() real set
c11 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
Y . c11 is ext-real V39() real set
Y1 is Relation-like Function-like set
dom Y1 is set
k is set
Y1 . k is set
i is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
Y . i is ext-real V39() real set
k 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))
i 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))
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
i . n is ext-real V39() real set
Y . n is ext-real V39() real set
c11 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
Y . c11 is ext-real V39() real set
Y1 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))
Y1 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))
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
Y1 . k is ext-real V39() real set
(Partial_Sums (Z1 * z)) . k is ext-real V39() real set
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
Y1 . (k + 1) is ext-real V39() real set
(Partial_Sums (Z1 * z)) . (k + 1) is ext-real V39() real set
Y1 . 1 is ext-real V39() real Element of REAL
(len (Omega,Z,y,Z1)) - 1 is ext-real V39() real V41() V42() Element of INT
((len (Omega,Z,y,Z1)) - 1) + 1 is ext-real V39() real V41() V42() Element of INT
k + 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
Y1 . (k + 1) is ext-real V39() real Element of REAL
Y . (k + 1) is ext-real V39() real Element of REAL
Y . k is ext-real V39() real set
(Omega,Z,y,Z1) . (k + 1) is ext-real V39() real set
(Y . k) + ((Omega,Z,y,Z1) . (k + 1)) is ext-real V39() real Element of REAL
((Partial_Sums (Z1 * z)) . k) + ((Omega,Z,y,Z1) . (k + 1)) is ext-real V39() real Element of REAL
(Partial_Sums (Z1 * z)) . (k + 1) is ext-real V39() real Element of REAL
(len (Omega,Z,y,Z1)) - 1 is ext-real V39() real V41() V42() Element of INT
((len (Omega,Z,y,Z1)) - 1) + 1 is ext-real V39() real V41() V42() Element of INT
(len (Omega,Z,y,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
i is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
((len (Omega,Z,y,Z1)) + 1) + i 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
Y1 . (k + 1) is ext-real V39() real Element of REAL
((len y) + 1) + i 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
(Partial_Sums (Z1 * z)) . (((len y) + 1) + i) is ext-real V39() real Element of REAL
(Partial_Sums (Z1 * z)) . (k + 1) is ext-real V39() real Element of REAL
(len (Omega,Z,y,Z1)) - 1 is ext-real V39() real V41() V42() Element of INT
Y1 . 1 is ext-real V39() real Element of REAL
Y1 . (k + 1) is ext-real V39() real Element of REAL
(Partial_Sums (Z1 * z)) . (k + 1) is ext-real V39() real Element of REAL
Y1 . 1 is ext-real V39() real Element of REAL
(len (Omega,Z,y,Z1)) - 1 is ext-real V39() real V41() V42() Element of INT
Y1 . (k + 1) is ext-real V39() real Element of REAL
(Partial_Sums (Z1 * z)) . (k + 1) is ext-real V39() real Element of REAL
Y1 . 0 is ext-real V39() real Element of REAL
Y1 . 0 is ext-real V39() real set
(Partial_Sums (Z1 * z)) . 0 is ext-real V39() real set
Y1 . (len (Omega,Z,y,Z1)) is ext-real V39() real Element of REAL
lim (Partial_Sums (Z1 * (Omega,z))) is ext-real V39() real Element of REAL
Sum (Z1 * (Omega,z)) is ext-real V39() real Element of REAL
Union (Omega,z) is Element of K10(Omega)
Z1 . (Union (Omega,z)) 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))
Z is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
Z1 is non empty Relation-like Z -defined REAL -valued Function-like V17(Z) V21(Z, REAL ) V43() V44() V45() V52() Probability of Z
y is Relation-like NAT -defined bool Omega -valued Function-like V56() FinSequence-like FinSubsequence-like (Omega,Z)
(Omega,y) is Element of K10(Omega)
Z1 . (Omega,y) is ext-real V39() real set
(Omega,Z,y,Z1) is Relation-like NAT -defined REAL -valued Function-like V43() V44() V45() V56() FinSequence-like FinSubsequence-like FinSequence of REAL
Sum (Omega,Z,y,Z1) is ext-real V39() real Element of REAL
K11(NAT,(bool Omega)) is non empty set
K10(K11(NAT,(bool Omega))) is non empty V25() set
dom y is V78() V79() V80() V81() V82() V83() Element of K10(NAT)
z 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)))
Union z is Element of K10(Omega)
Z1 . (Union z) is ext-real V39() real set
Z1 * 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))
Sum (Z1 * z) is ext-real V39() real Element of REAL
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 . Y is Event of Z
z . Y1 is Event of Z
(Omega,Z,y,Y) is Event of Z
(Omega,Z,y,Y1) is Event of Z
Omega is set
K10(Omega) is non empty V25() set
K10(K10(Omega)) is non empty V25() set
Omega is 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 Element of K10(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)))
rng Z1 is Element of K10((bool Omega))
K10((bool Omega)) is non empty V25() set
Union Z1 is Element of K10(Omega)
lim_sup Z1 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)))
rng Z1 is Element of K10((bool Omega))
lim_sup Z1 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)))
rng Z1 is Element of K10((bool Omega))
K10((bool Omega)) is non empty V25() set
Union Z1 is Element of K10(Omega)
lim_sup Z1 is Element of K10(Omega)
Omega is 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 Element of K10(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)))
rng Z1 is Element of K10((bool Omega))
K10((bool Omega)) is non empty V25() set
Intersection Z1 is Element of K10(Omega)
lim_sup Z1 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)))
rng Z1 is Element of K10((bool Omega))
lim_sup Z1 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)))
rng Z1 is Element of K10((bool Omega))
K10((bool Omega)) is non empty V25() set
Intersection Z1 is Element of K10(Omega)
lim_sup Z1 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)))
rng Z is Element of K10((bool Omega))
K10((bool Omega)) is non empty V25() set
Union Z is Element of K10(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)))
rng Z is Element of K10((bool Omega))
K10((bool Omega)) is non empty V25() set
Intersection Z is Element of K10(Omega)
Omega is 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))
Omega is set
Z is 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 Element of K10(K10(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)))
rng y is Element of K10((bool Z))
K10((bool Z)) is non empty V25() set
lim_sup y is Element of K10(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)))
rng y is Element of K10((bool Z))
K10((bool Z)) is non empty V25() set
lim_sup y is Element of K10(Z)
Z1 is Element of K10(K10(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)))
rng y is Element of K10((bool Z))
K10((bool Z)) is non empty V25() set
lim_sup y is Element of K10(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)))
rng y is Element of K10((bool Z))
K10((bool Z)) is non empty V25() set
lim_sup y is Element of K10(Z)
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 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 V25() compl-closed sigma-multiplicative Element of K10(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)))
rng y is Element of K10((bool Omega))
K10((bool Omega)) is non empty V25() set
Union y is Element of K10(Omega)
z is non empty Relation-like NAT -defined bool Omega -valued Z1 -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
Union z 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)))
rng y is Element of K10((bool Omega))
K10((bool Omega)) is non empty V25() set
Intersection y is Element of 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 bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
rng Z1 is Element of K10((bool Omega))
K10((bool Omega)) is non empty V25() set
Intersection Z1 is Element of K10(Omega)
(Omega,Z1) is non empty Relation-like NAT -defined bool Omega -valued bool Omega -valued Function-like V17( NAT ) V21( NAT , bool Omega) Element of K10(K11(NAT,(bool Omega)))
z is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
(Omega,Z1) . 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
(Omega,Z1) . (z + 1) is set
Z1 . (z + 1) is Event of bool Omega
(Omega,Z1) . (z + 1) is Event of bool Omega
((Omega,Z1) . z) /\ (Z1 . (z + 1)) is Element of K10(Omega)
Z1 . 0 is Event of bool Omega
(Omega,Z1) . 0 is Event of bool Omega
(Omega,Z1) . 0 is set
rng (Omega,Z1) is Element of K10((bool Omega))
Intersection (Omega,Z1) is Element of K10(Omega)
Omega is non empty 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
Omega is non empty set
K10(Omega) is non empty V25() set
K10(K10(Omega)) is non empty V25() set
Z is Element of K10(K10(Omega))
{ b1 where b1 is Element of K10(K10(Omega)) : ( Z c= b1 & b1 is (Omega) (Omega) Element of K10(K10(Omega)) ) } is set
meet { b1 where b1 is Element of K10(K10(Omega)) : ( Z c= b1 & b1 is (Omega) (Omega) Element of K10(K10(Omega)) ) } is set
z is set
Y is 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
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)))
rng z is Element of K10((bool Omega))
K10((bool Omega)) is non empty V25() set
lim_sup z is Element of K10(Omega)
Y is set
Y1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
z . Y1 is set
Y1 is Element of K10(K10(Omega))
z is (Omega) (Omega) Element of K10(K10(Omega))
Y is set
Y is set
Z1 is (Omega) (Omega) Element of K10(K10(Omega))
y is (Omega) (Omega) Element of K10(K10(Omega))
Omega is non empty set
K10(Omega) is non empty V25() set
K10(K10(Omega)) is non empty V25() set
Z is non empty V25() compl-closed Element of K10(K10(Omega))
(Omega,Z) is (Omega) (Omega) Element of K10(K10(Omega))
Z1 is non empty Element of K10(K10(Omega))
y is set
{ b1 where b1 is Element of Z1 : ( y \ b1 in Z1 & b1 \ y in Z1 & b1 /\ y in Z1 ) } is set
z is set
Y is set
y \ Y is Element of K10(y)
K10(y) is non empty V25() set
Y \ y is Element of K10(Y)
K10(Y) is non empty V25() set
Y /\ y is set
Y1 is Element of Z1
y \ Y1 is Element of K10(y)
Y1 \ y is Element of K10(Omega)
Y1 /\ y is Element of K10(Omega)
y is Element of Z1
{ b1 where b1 is Element of Z1 : ( y \ b1 in Z1 & b1 \ y in Z1 & b1 /\ y in Z1 ) } is set
z is 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
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)))
rng Y is Element of K10((bool Omega))
K10((bool Omega)) is non empty V25() set
lim_sup Y is Element of K10(Omega)
Y1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
Y . Y1 is set
Y (\) 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)))
Y1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
(Y (\) y) . Y1 is set
Y . Y1 is set
(Y . Y1) \ y is Element of K10((Y . Y1))
K10((Y . Y1)) is non empty V25() set
rng (Y (\) y) is Element of K10((bool Omega))
y (/\) 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)))
Y1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
(y (/\) Y) . Y1 is set
Y . Y1 is set
y /\ (Y . Y1) is Element of K10(Omega)
rng (y (/\) Y) is Element of K10((bool Omega))
lim_sup (y (/\) Y) is Element of K10(Omega)
y /\ (lim_sup Y) is Element of K10(Omega)
y (\) 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)))
Y1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V39() real set
(y (\) Y) . Y1 is set
Y . Y1 is set
y \ (Y . Y1) is Element of K10(Omega)
rng (y (\) Y) is Element of K10((bool Omega))
lim_sup (y (\) Y) is Element of K10(Omega)
y \ (lim_sup Y) is Element of K10(Omega)
lim_sup (Y (\) y) is Element of K10(Omega)
(lim_sup Y) \ y is Element of K10(Omega)
Y is set
y is Element of Z
{ b1 where b1 is Element of Z1 : ( y \ b1 in Z1 & b1 \ y in Z1 & b1 /\ y in Z1 ) } is set
z is set
Y is set
Y /\ y is Element of K10(Omega)
Y \ y is Element of K10(Y)
K10(Y) is non empty V25() set
y \ Y is Element of K10(Omega)
y is Element of Z1
{ b1 where b1 is Element of Z1 : ( y \ b1 in Z1 & b1 \ y in Z1 & b1 /\ y in Z1 ) } is set
z is set
Y is set
{ b1 where b1 is Element of Z1 : ( Y \ b1 in Z1 & b1 \ Y in Z1 & b1 /\ Y in Z1 ) } is set
Y /\ y is Element of K10(Omega)
Y \ y is Element of K10(Y)
K10(Y) is non empty V25() set
y \ Y is Element of K10(Omega)
y is Element of K10(Omega)
y ` is Element of K10(Omega)
{ b1 where b1 is Element of Z1 : ( y \ b1 in Z1 & b1 \ y in Z1 & b1 /\ y in Z1 ) } is set
Omega \ y is Element of K10(Omega)
y is set
z is set
{ b1 where b1 is Element of Z1 : ( y \ b1 in Z1 & b1 \ y in Z1 & b1 /\ y in Z1 ) } is set
y /\ z is set
Omega is non empty set
K10(Omega) is non empty V25() set
K10(K10(Omega)) is non empty V25() set
Z is non empty V25() compl-closed Element of K10(K10(Omega))
sigma Z is non empty V25() compl-closed sigma-multiplicative Element of K10(K10(Omega))
(Omega,Z) is (Omega) (Omega) Element of K10(K10(Omega))