REAL is non empty V57() V131() V132() V133() V137() set
NAT is non empty V36() V37() V38() V131() V132() V133() V134() V135() V136() V137() Element of bool REAL
bool REAL is non empty V143() set
NAT is non empty V36() V37() V38() V131() V132() V133() V134() V135() V136() V137() set
bool NAT is non empty V143() set
[:NAT,REAL:] is non empty Relation-like set
bool [:NAT,REAL:] is non empty V143() set
bool (bool REAL) is non empty V143() set
COMPLEX is non empty V57() V131() V137() set
RAT is non empty V57() V131() V132() V133() V134() V137() set
INT is non empty V57() V131() V132() V133() V134() V135() V137() set
{} is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V36() V37() V38() V40() V41() V42() V131() V132() V133() V134() V135() V136() V137() set
1 is non empty ext-real positive V36() V37() V38() V42() V43() V44() V129() V130() V131() V132() V133() V134() V135() V136() Element of NAT
0 is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional ext-real V36() V37() V38() V40() V41() V42() V43() V44() V129() V130() V131() V132() V133() V134() V135() V136() V137() Element of NAT
Borel_Sets is non empty compl-closed sigma-multiplicative V143() Element of bool (bool REAL)
X is non empty set
bool X is non empty V143() set
bool (bool X) is non empty V143() set
P is non empty compl-closed sigma-multiplicative V143() Element of bool (bool X)
Funcs (P,REAL) is non empty FUNCTION_DOMAIN of P, REAL
P is set
f is set
P is set
f is set
Y is set
X is non empty set
bool X is non empty V143() set
bool (bool X) is non empty V143() set
P is non empty compl-closed sigma-multiplicative V143() Element of bool (bool X)
(X,P) is set
the Relation-like P -defined REAL -valued Function-like quasi_total V54() Probability of P is Relation-like P -defined REAL -valued Function-like quasi_total V54() Probability of P
(REAL,Borel_Sets) is non empty set
X is ()
the of X is non empty set
the of X is non empty set
X is ()
(X) is set
the of X is non empty set
(X) is set
the of X is non empty set
K105(REAL) is non empty compl-closed sigma-multiplicative V143() Element of bool (bool REAL)
[:NAT,K105(REAL):] is non empty Relation-like set
bool [:NAT,K105(REAL):] is non empty V143() set
X is ()
(X) is non empty set
the of X is non empty set
(X) is non empty set
the of X is non empty set
the of X is Relation-like [: the of X, the of X:] -defined (REAL,Borel_Sets) -valued Function-like quasi_total Element of bool [:[: the of X, the of X:],(REAL,Borel_Sets):]
[: the of X, the of X:] is non empty Relation-like set
[:[: the of X, the of X:],(REAL,Borel_Sets):] is non empty Relation-like set
bool [:[: the of X, the of X:],(REAL,Borel_Sets):] is non empty V143() set
P is Element of (X)
P is Element of (X)
[P,P] is V1() Element of [:(X),(X):]
[:(X),(X):] is non empty Relation-like set
the of X . [P,P] is set
f is Element of [: the of X, the of X:]
the of X . f is Element of (REAL,Borel_Sets)
{0} is non empty functional V131() V132() V133() V134() V135() V136() Element of bool NAT
bool NAT is non empty V143() set
[:Borel_Sets,REAL:] is non empty Relation-like set
bool [:Borel_Sets,REAL:] is non empty V143() set
P is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total Element of bool [:Borel_Sets,REAL:]
P is Event of Borel_Sets
P . P is ext-real V43() V44() Element of REAL
P . REAL is set
[#] REAL is non empty non proper V131() V132() V133() Element of bool REAL
P is Event of Borel_Sets
P . P is ext-real V43() V44() Element of REAL
f is Event of Borel_Sets
P \/ f is Event of Borel_Sets
P . (P \/ f) is ext-real V43() V44() Element of REAL
P . f is ext-real V43() V44() Element of REAL
(P . P) + (P . f) is ext-real V43() V44() Element of REAL
P is Relation-like NAT -defined Borel_Sets -valued K105(REAL) -valued Function-like quasi_total Element of bool [:NAT,K105(REAL):]
P * P is Relation-like NAT -defined REAL -valued Function-like quasi_total Element of bool [:NAT,REAL:]
lim (P * P) is ext-real V43() V44() Element of REAL
Intersection P is V131() V132() V133() Element of bool REAL
P . (Intersection P) is set
dom (P * P) is V131() V132() V133() V134() V135() V136() Element of bool NAT
f is ext-real V36() V37() V38() V42() V43() V44() V129() V130() V131() V132() V133() V134() V135() V136() Element of NAT
(P * P) . f is ext-real V43() V44() Element of REAL
P . f is V131() V132() V133() Element of K105(REAL)
P . (P . f) is set
proj2 P is set
Y is ext-real V36() V37() V38() V42() V43() V44() V129() V130() V131() V132() V133() V134() V135() V136() Element of NAT
P . Y is V131() V132() V133() Element of K105(REAL)
P . (P . Y) is set
(P * P) . Y is ext-real V43() V44() Element of REAL
f is ext-real V43() V44() Element of REAL
Y is ext-real V36() V37() V38() V42() V43() V44() V129() V130() V131() V132() V133() V134() V135() V136() Element of NAT
(P * P) . Y is ext-real V43() V44() Element of REAL
Y is ext-real V36() V37() V38() V42() V43() V44() V129() V130() V131() V132() V133() V134() V135() V136() Element of NAT
Y is ext-real V36() V37() V38() V42() V43() V44() V129() V130() V131() V132() V133() V134() V135() V136() Element of NAT
proj2 P is set
f is ext-real V36() V37() V38() V42() V43() V44() V129() V130() V131() V132() V133() V134() V135() V136() Element of NAT
P . f is V131() V132() V133() Element of K105(REAL)
f is ext-real V36() V37() V38() V42() V43() V44() V129() V130() V131() V132() V133() V134() V135() V136() Element of NAT
P . f is V131() V132() V133() Element of K105(REAL)
f is ext-real V36() V37() V38() V42() V43() V44() V129() V130() V131() V132() V133() V134() V135() V136() Element of NAT
P . f is V131() V132() V133() Element of K105(REAL)
Y is ext-real V36() V37() V38() V42() V43() V44() V129() V130() V131() V132() V133() V134() V135() V136() Element of NAT
(P * P) . Y is ext-real V43() V44() Element of REAL
P . Y is V131() V132() V133() Element of K105(REAL)
P . (P . Y) is set
Y is ext-real V36() V37() V38() V42() V43() V44() V129() V130() V131() V132() V133() V134() V135() V136() Element of NAT
(P * P) . Y is ext-real V43() V44() Element of REAL
f is ext-real V36() V37() V38() V42() V43() V44() V129() V130() V131() V132() V133() V134() V135() V136() Element of NAT
f is ext-real V36() V37() V38() V42() V43() V44() V129() V130() V131() V132() V133() V134() V135() V136() Element of NAT
f is ext-real V36() V37() V38() V42() V43() V44() V129() V130() V131() V132() V133() V134() V135() V136() Element of NAT
P . f is V131() V132() V133() Element of K105(REAL)
[:NAT,NAT:] is non empty Relation-like set
[:[:NAT,NAT:],(bool [:Borel_Sets,REAL:]):] is non empty Relation-like set
[0,0] is V1() Element of [:NAT,NAT:]
P is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets
[[0,0],P] is V1() Element of [:[:NAT,NAT:],(bool [:Borel_Sets,REAL:]):]
{[[0,0],P]} is non empty Relation-like [:NAT,NAT:] -defined bool [:Borel_Sets,REAL:] -valued Function-like Element of bool [:[:NAT,NAT:],(bool [:Borel_Sets,REAL:]):]
bool [:[:NAT,NAT:],(bool [:Borel_Sets,REAL:]):] is non empty V143() set
dom {[[0,0],P]} is non empty Relation-like NAT -defined NAT -valued Element of bool [:NAT,NAT:]
bool [:NAT,NAT:] is non empty V143() set
{[0,0]} is non empty Relation-like NAT -defined NAT -valued Function-like Element of bool [:NAT,NAT:]
[:{0},{0}:] is non empty Relation-like NAT -defined NAT -valued Element of bool [:NAT,NAT:]
proj2 {[[0,0],P]} is non empty set
{P} is non empty functional Element of bool (bool [:Borel_Sets,REAL:])
bool (bool [:Borel_Sets,REAL:]) is non empty V143() set
[:[:{0},{0}:],(REAL,Borel_Sets):] is non empty Relation-like set
bool [:[:{0},{0}:],(REAL,Borel_Sets):] is non empty V143() set
Y is Relation-like [:{0},{0}:] -defined (REAL,Borel_Sets) -valued Function-like quasi_total Element of bool [:[:{0},{0}:],(REAL,Borel_Sets):]
({0},{0},Y) is () ()
(({0},{0},Y)) is non empty set
the of ({0},{0},Y) is non empty set
(({0},{0},Y)) is non empty set
the of ({0},{0},Y) is non empty set
Q is Element of (({0},{0},Y))
x is Element of (({0},{0},Y))
Q is Element of (({0},{0},Y))
x is Element of (({0},{0},Y))
Q is Element of (({0},{0},Y))
x is Element of (({0},{0},Y))
p is ext-real V43() V44() Element of REAL
1 - p is ext-real V43() V44() Element of REAL
p is Element of (({0},{0},Y))
(({0},{0},Y),p,x) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets
the of ({0},{0},Y) is Relation-like [: the of ({0},{0},Y), the of ({0},{0},Y):] -defined (REAL,Borel_Sets) -valued Function-like quasi_total Element of bool [:[: the of ({0},{0},Y), the of ({0},{0},Y):],(REAL,Borel_Sets):]
[: the of ({0},{0},Y), the of ({0},{0},Y):] is non empty Relation-like set
[:[: the of ({0},{0},Y), the of ({0},{0},Y):],(REAL,Borel_Sets):] is non empty Relation-like set
bool [:[: the of ({0},{0},Y), the of ({0},{0},Y):],(REAL,Borel_Sets):] is non empty V143() set
[p,x] is V1() Element of [:(({0},{0},Y)),(({0},{0},Y)):]
[:(({0},{0},Y)),(({0},{0},Y)):] is non empty Relation-like set
the of ({0},{0},Y) . [p,x] is set
(({0},{0},Y),p,Q) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets
[p,Q] is V1() Element of [:(({0},{0},Y)),(({0},{0},Y)):]
the of ({0},{0},Y) . [p,Q] is set
q is Event of Borel_Sets
(({0},{0},Y),p,x) . q is ext-real V43() V44() Element of REAL
(({0},{0},Y),p,Q) . q is ext-real V43() V44() Element of REAL
p * ((({0},{0},Y),p,Q) . q) is ext-real V43() V44() Element of REAL
(1 - p) * ((({0},{0},Y),p,x) . q) is ext-real V43() V44() Element of REAL
(p * ((({0},{0},Y),p,Q) . q)) + ((1 - p) * ((({0},{0},Y),p,x) . q)) is ext-real V43() V44() Element of REAL
Q is set
[:Q,Q:] is Relation-like set
bool [:Q,Q:] is non empty V143() set
Q is () ()
(Q) is non empty set
the of Q is non empty set
[:(Q),Borel_Sets:] is non empty Relation-like set
Q is () ()
(Q) is set
(Q) is non empty set
the of Q is non empty set
[:(Q),Borel_Sets:] is non empty Relation-like set
Q is () ()
(Q) is non empty set
(Q) is non empty set
the of Q is non empty set
[:(Q),Borel_Sets:] is non empty Relation-like set
x is Element of (Q)
x `1 is set
x `2 is set
Q is () ()
(Q) is non empty set
the of Q is non empty set
(Q) is non empty set
(Q) is non empty set
the of Q is non empty set
[:(Q),Borel_Sets:] is non empty Relation-like set
x is Element of (Q)
p is Element of (Q)
(Q,p) is Event of Borel_Sets
(Q,p) ` is V131() V132() V133() Element of bool REAL
REAL \ (Q,p) is V131() V132() V133() set
(Q,p) is Element of (Q)
(Q,(Q,p),x) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets
the of Q is Relation-like [: the of Q, the of Q:] -defined (REAL,Borel_Sets) -valued Function-like quasi_total Element of bool [:[: the of Q, the of Q:],(REAL,Borel_Sets):]
[: the of Q, the of Q:] is non empty Relation-like set
[:[: the of Q, the of Q:],(REAL,Borel_Sets):] is non empty Relation-like set
bool [:[: the of Q, the of Q:],(REAL,Borel_Sets):] is non empty V143() set
[(Q,p),x] is V1() Element of [:(Q),(Q):]
[:(Q),(Q):] is non empty Relation-like set
the of Q . [(Q,p),x] is set
(Q,(Q,p),x) . (Q,p) is ext-real V43() V44() Element of REAL
p is Event of Borel_Sets
(Q,(Q,p),x) . p is ext-real V43() V44() Element of REAL
1 - ((Q,(Q,p),x) . p) is ext-real V43() V44() Element of REAL
[#] Borel_Sets is Event of Borel_Sets
REAL \ p is V131() V132() V133() Element of bool REAL
p ` is V131() V132() V133() Element of bool REAL
REAL \ p is V131() V132() V133() set
Q is () ()
(Q) is non empty set
(Q) is non empty set
the of Q is non empty set
[:(Q),Borel_Sets:] is non empty Relation-like set
x is Element of (Q)
(Q,x) is Element of (Q)
(Q,x) is Event of Borel_Sets
(Q,x) ` is V131() V132() V133() Element of bool REAL
REAL \ (Q,x) is V131() V132() V133() set
[(Q,x),((Q,x) `)] is V1() Element of [:(Q),(bool REAL):]
[:(Q),(bool REAL):] is non empty Relation-like set
p is Event of Borel_Sets
p is Element of (Q)
p is Element of (Q)
(Q,p) is Element of (Q)
(Q,p) is Event of Borel_Sets
(Q,p) ` is V131() V132() V133() Element of bool REAL
REAL \ (Q,p) is V131() V132() V133() set
[(Q,p),((Q,p) `)] is V1() Element of [:(Q),(bool REAL):]
(Q,p) is Element of (Q)
(Q,p) is Event of Borel_Sets
(Q,p) ` is V131() V132() V133() Element of bool REAL
REAL \ (Q,p) is V131() V132() V133() set
[(Q,p),((Q,p) `)] is V1() Element of [:(Q),(bool REAL):]
((Q,p) `) ` is V131() V132() V133() Element of bool REAL
REAL \ ((Q,p) `) is V131() V132() V133() set
[(Q,p),(((Q,p) `) `)] is V1() Element of [:(Q),(bool REAL):]
[(Q,p),(((Q,p) `) `)] is V1() Element of [:(Q),(bool REAL):]
Q is () ()
(Q) is non empty set
(Q) is non empty set
the of Q is non empty set
[:(Q),Borel_Sets:] is non empty Relation-like set
(Q) is non empty set
the of Q is non empty set
p is Element of (Q)
(Q,p) is Element of (Q)
q is Element of (Q)
(Q,(Q,p),q) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets
the of Q is Relation-like [: the of Q, the of Q:] -defined (REAL,Borel_Sets) -valued Function-like quasi_total Element of bool [:[: the of Q, the of Q:],(REAL,Borel_Sets):]
[: the of Q, the of Q:] is non empty Relation-like set
[:[: the of Q, the of Q:],(REAL,Borel_Sets):] is non empty Relation-like set
bool [:[: the of Q, the of Q:],(REAL,Borel_Sets):] is non empty V143() set
[(Q,p),q] is V1() Element of [:(Q),(Q):]
[:(Q),(Q):] is non empty Relation-like set
the of Q . [(Q,p),q] is set
(Q,p) is Event of Borel_Sets
(Q,(Q,p),q) . (Q,p) is ext-real V43() V44() Element of REAL
Q is () ()
(Q) is non empty set
(Q) is non empty set
the of Q is non empty set
[:(Q),Borel_Sets:] is non empty Relation-like set
p is Element of (Q)
q is Element of (Q)
p is Element of (Q)
q is Element of (Q)
Q is () ()
(Q) is non empty set
(Q) is non empty set
the of Q is non empty set
[:(Q),Borel_Sets:] is non empty Relation-like set
(Q) is non empty set
the of Q is non empty set
x is Element of (Q)
(Q,x) is Element of (Q)
(Q,x) is Event of Borel_Sets
p is Element of (Q)
(Q,p) is Element of (Q)
(Q,p) is Event of Borel_Sets
p is Element of (Q)
(Q,(Q,x),p) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets
the of Q is Relation-like [: the of Q, the of Q:] -defined (REAL,Borel_Sets) -valued Function-like quasi_total Element of bool [:[: the of Q, the of Q:],(REAL,Borel_Sets):]
[: the of Q, the of Q:] is non empty Relation-like set
[:[: the of Q, the of Q:],(REAL,Borel_Sets):] is non empty Relation-like set
bool [:[: the of Q, the of Q:],(REAL,Borel_Sets):] is non empty V143() set
[(Q,x),p] is V1() Element of [:(Q),(Q):]
[:(Q),(Q):] is non empty Relation-like set
the of Q . [(Q,x),p] is set
(Q,(Q,x),p) . (Q,x) is ext-real V43() V44() Element of REAL
(Q,(Q,p),p) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets
[(Q,p),p] is V1() Element of [:(Q),(Q):]
the of Q . [(Q,p),p] is set
(Q,(Q,p),p) . (Q,p) is ext-real V43() V44() Element of REAL
p is Element of (Q)
(Q,(Q,x),p) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets
the of Q is Relation-like [: the of Q, the of Q:] -defined (REAL,Borel_Sets) -valued Function-like quasi_total Element of bool [:[: the of Q, the of Q:],(REAL,Borel_Sets):]
[: the of Q, the of Q:] is non empty Relation-like set
[:[: the of Q, the of Q:],(REAL,Borel_Sets):] is non empty Relation-like set
bool [:[: the of Q, the of Q:],(REAL,Borel_Sets):] is non empty V143() set
[(Q,x),p] is V1() Element of [:(Q),(Q):]
[:(Q),(Q):] is non empty Relation-like set
the of Q . [(Q,x),p] is set
(Q,(Q,x),p) . (Q,x) is ext-real V43() V44() Element of REAL
(Q,(Q,p),p) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets
[(Q,p),p] is V1() Element of [:(Q),(Q):]
the of Q . [(Q,p),p] is set
(Q,(Q,p),p) . (Q,p) is ext-real V43() V44() Element of REAL
p is Element of (Q)
(Q,(Q,p),p) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets
the of Q is Relation-like [: the of Q, the of Q:] -defined (REAL,Borel_Sets) -valued Function-like quasi_total Element of bool [:[: the of Q, the of Q:],(REAL,Borel_Sets):]
[: the of Q, the of Q:] is non empty Relation-like set
[:[: the of Q, the of Q:],(REAL,Borel_Sets):] is non empty Relation-like set
bool [:[: the of Q, the of Q:],(REAL,Borel_Sets):] is non empty V143() set
[(Q,p),p] is V1() Element of [:(Q),(Q):]
[:(Q),(Q):] is non empty Relation-like set
the of Q . [(Q,p),p] is set
(Q,(Q,p),p) . (Q,p) is ext-real V43() V44() Element of REAL
(Q,(Q,x),p) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets
[(Q,x),p] is V1() Element of [:(Q),(Q):]
the of Q . [(Q,x),p] is set
(Q,(Q,x),p) . (Q,x) is ext-real V43() V44() Element of REAL
Q is () ()
(Q) is non empty set
(Q) is non empty set
the of Q is non empty set
[:(Q),Borel_Sets:] is non empty Relation-like set
x is Element of (Q)
Q is () ()
(Q) is non empty set
(Q) is non empty set
the of Q is non empty set
[:(Q),Borel_Sets:] is non empty Relation-like set
x is Element of (Q)
p is Element of (Q)
p is Element of (Q)
(Q) is non empty set
the of Q is non empty set
(Q,x) is Element of (Q)
q is Element of (Q)
(Q,(Q,x),q) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets
the of Q is Relation-like [: the of Q, the of Q:] -defined (REAL,Borel_Sets) -valued Function-like quasi_total Element of bool [:[: the of Q, the of Q:],(REAL,Borel_Sets):]
[: the of Q, the of Q:] is non empty Relation-like set
[:[: the of Q, the of Q:],(REAL,Borel_Sets):] is non empty Relation-like set
bool [:[: the of Q, the of Q:],(REAL,Borel_Sets):] is non empty V143() set
[(Q,x),q] is V1() Element of [:(Q),(Q):]
[:(Q),(Q):] is non empty Relation-like set
the of Q . [(Q,x),q] is set
(Q,x) is Event of Borel_Sets
(Q,(Q,x),q) . (Q,x) is ext-real V43() V44() Element of REAL
(Q,p) is Element of (Q)
(Q,(Q,p),q) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets
[(Q,p),q] is V1() Element of [:(Q),(Q):]
the of Q . [(Q,p),q] is set
(Q,p) is Event of Borel_Sets
(Q,(Q,p),q) . (Q,p) is ext-real V43() V44() Element of REAL
(Q,p) is Element of (Q)
(Q,(Q,p),q) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets
[(Q,p),q] is V1() Element of [:(Q),(Q):]
the of Q . [(Q,p),q] is set
(Q,p) is Event of Borel_Sets
(Q,(Q,p),q) . (Q,p) is ext-real V43() V44() Element of REAL
Q is () ()
(Q) is non empty set
(Q) is non empty set
the of Q is non empty set
[:(Q),Borel_Sets:] is non empty Relation-like set
x is Element of (Q)
Q is () ()
(Q) is non empty set
(Q) is non empty set
the of Q is non empty set
[:(Q),Borel_Sets:] is non empty Relation-like set
x is Element of (Q)
p is Element of (Q)
Q is () ()
(Q) is non empty set
(Q) is non empty set
the of Q is non empty set
[:(Q),Borel_Sets:] is non empty Relation-like set
x is Element of (Q)
p is Element of (Q)
p is Element of (Q)
Q is () ()
(Q) is non empty set
(Q) is non empty set
the of Q is non empty set
[:(Q),Borel_Sets:] is non empty Relation-like set
x is Element of (Q)
(Q,x) is Element of (Q)
(Q,x) is Element of (Q)
(Q,x) is Event of Borel_Sets
(Q,x) ` is V131() V132() V133() Element of bool REAL
REAL \ (Q,x) is V131() V132() V133() set
[(Q,x),((Q,x) `)] is V1() Element of [:(Q),(bool REAL):]
[:(Q),(bool REAL):] is non empty Relation-like set
p is Element of (Q)
(Q,p) is Element of (Q)
(Q,p) is Element of (Q)
(Q,p) is Event of Borel_Sets
(Q,p) ` is V131() V132() V133() Element of bool REAL
REAL \ (Q,p) is V131() V132() V133() set
[(Q,p),((Q,p) `)] is V1() Element of [:(Q),(bool REAL):]
(Q) is non empty set
the of Q is non empty set
(Q,(Q,p)) is Element of (Q)
p is Element of (Q)
(Q,(Q,(Q,p)),p) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets
the of Q is Relation-like [: the of Q, the of Q:] -defined (REAL,Borel_Sets) -valued Function-like quasi_total Element of bool [:[: the of Q, the of Q:],(REAL,Borel_Sets):]
[: the of Q, the of Q:] is non empty Relation-like set
[:[: the of Q, the of Q:],(REAL,Borel_Sets):] is non empty Relation-like set
bool [:[: the of Q, the of Q:],(REAL,Borel_Sets):] is non empty V143() set
[(Q,(Q,p)),p] is V1() Element of [:(Q),(Q):]
[:(Q),(Q):] is non empty Relation-like set
the of Q . [(Q,(Q,p)),p] is set
(Q,(Q,p)) is Event of Borel_Sets
(Q,(Q,(Q,p)),p) . (Q,(Q,p)) is ext-real V43() V44() Element of REAL
(Q,(Q,x)) is Element of (Q)
(Q,(Q,(Q,x)),p) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets
[(Q,(Q,x)),p] is V1() Element of [:(Q),(Q):]
the of Q . [(Q,(Q,x)),p] is set
(Q,(Q,x)) is Event of Borel_Sets
(Q,(Q,(Q,x)),p) . (Q,(Q,x)) is ext-real V43() V44() Element of REAL
(Q,(Q,x),p) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets
[(Q,x),p] is V1() Element of [:(Q),(Q):]
the of Q . [(Q,x),p] is set
r is Event of Borel_Sets
(Q,(Q,x),p) . r is ext-real V43() V44() Element of REAL
(Q,(Q,p),p) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets
[(Q,p),p] is V1() Element of [:(Q),(Q):]
the of Q . [(Q,p),p] is set
q is Event of Borel_Sets
(Q,(Q,p),p) . q is ext-real V43() V44() Element of REAL
1 - ((Q,(Q,x),p) . r) is ext-real V43() V44() Element of REAL
- (1 - ((Q,(Q,x),p) . r)) is ext-real V43() V44() Element of REAL
((Q,(Q,x),p) . r) - 1 is ext-real V43() V44() Element of REAL
1 - ((Q,(Q,p),p) . q) is ext-real V43() V44() Element of REAL
- (1 - ((Q,(Q,p),p) . q)) is ext-real V43() V44() Element of REAL
((Q,(Q,p),p) . q) - 1 is ext-real V43() V44() Element of REAL
(Q,(Q,p),p) . (Q,p) is ext-real V43() V44() Element of REAL
(Q,(Q,x),p) . (Q,x) is ext-real V43() V44() Element of REAL
Q is () ()
(Q) is non empty set
(Q) is non empty set
the of Q is non empty set
[:(Q),Borel_Sets:] is non empty Relation-like set
[:(Q),(Q):] is non empty Relation-like set
bool [:(Q),(Q):] is non empty V143() set
p is Element of (Q)
x is set
q is Element of (Q)
p is set
q is Element of (Q)
x is set
r is Element of (Q)
p is set
q is Element of (Q)
E is Element of (Q)
p is set
x is set
x is Relation-like (Q) -defined (Q) -valued reflexive symmetric transitive V31((Q)) Element of bool [:(Q),(Q):]
p is Element of (Q)
p is Element of (Q)
[p,p] is V1() Element of [:(Q),(Q):]
q is Element of (Q)
r is Element of (Q)
p is Element of (Q)
p is Element of (Q)
[p,p] is V1() Element of [:(Q),(Q):]
q is Element of (Q)
r is Element of (Q)
[q,r] is V1() Element of [:(Q),(Q):]
x is Relation-like (Q) -defined (Q) -valued reflexive symmetric transitive V31((Q)) Element of bool [:(Q),(Q):]
p is Relation-like (Q) -defined (Q) -valued reflexive symmetric transitive V31((Q)) Element of bool [:(Q),(Q):]
p is Element of (Q)
q is Element of (Q)
[p,q] is V1() Element of [:(Q),(Q):]
p is set
q is set
[p,q] is V1() set
Q is () ()
(Q) is non empty set
(Q) is non empty set
the of Q is non empty set
[:(Q),Borel_Sets:] is non empty Relation-like set
bool (Q) is non empty V143() set
(Q) is Relation-like (Q) -defined (Q) -valued reflexive symmetric transitive V31((Q)) Element of bool [:(Q),(Q):]
[:(Q),(Q):] is non empty Relation-like set
bool [:(Q),(Q):] is non empty V143() set
Class (Q) is non empty V20() a_partition of (Q)
x is Element of bool (Q)
p is Element of bool (Q)
p is Element of (Q)
q is Element of (Q)
r is Element of (Q)
q is Element of (Q)
(Q) is non empty set
the of Q is non empty set
(Q,q) is Element of (Q)
E is Element of (Q)
(Q,(Q,q),E) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets
the of Q is Relation-like [: the of Q, the of Q:] -defined (REAL,Borel_Sets) -valued Function-like quasi_total Element of bool [:[: the of Q, the of Q:],(REAL,Borel_Sets):]
[: the of Q, the of Q:] is non empty Relation-like set
[:[: the of Q, the of Q:],(REAL,Borel_Sets):] is non empty Relation-like set
bool [:[: the of Q, the of Q:],(REAL,Borel_Sets):] is non empty V143() set
[(Q,q),E] is V1() Element of [:(Q),(Q):]
[:(Q),(Q):] is non empty Relation-like set
the of Q . [(Q,q),E] is set
(Q,q) is Event of Borel_Sets
(Q,(Q,q),E) . (Q,q) is ext-real V43() V44() Element of REAL
(Q,q) is Element of (Q)
(Q,(Q,q),E) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets
[(Q,q),E] is V1() Element of [:(Q),(Q):]
the of Q . [(Q,q),E] is set
(Q,q) is Event of Borel_Sets
(Q,(Q,q),E) . (Q,q) is ext-real V43() V44() Element of REAL
[r,q] is V1() Element of [:(Q),(Q):]
s is set
Class ((Q),s) is Element of bool (Q)
(Q,r) is Element of (Q)
(Q,(Q,r),E) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets
[(Q,r),E] is V1() Element of [:(Q),(Q):]
the of Q . [(Q,r),E] is set
(Q,r) is Event of Borel_Sets
(Q,(Q,r),E) . (Q,r) is ext-real V43() V44() Element of REAL
[p,q] is V1() Element of [:(Q),(Q):]
s is set
Class ((Q),s) is Element of bool (Q)
(Q,p) is Element of (Q)
(Q,(Q,p),E) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets
[(Q,p),E] is V1() Element of [:(Q),(Q):]
the of Q . [(Q,p),E] is set
(Q,p) is Event of Borel_Sets
(Q,(Q,p),E) . (Q,p) is ext-real V43() V44() Element of REAL
Q is () ()
(Q) is non empty set
(Q) is non empty set
the of Q is non empty set
[:(Q),Borel_Sets:] is non empty Relation-like set
(Q) is Relation-like (Q) -defined (Q) -valued reflexive symmetric transitive V31((Q)) Element of bool [:(Q),(Q):]
[:(Q),(Q):] is non empty Relation-like set
bool [:(Q),(Q):] is non empty V143() set
Class (Q) is non empty V20() a_partition of (Q)
[:(Class (Q)),(Class (Q)):] is non empty Relation-like set
bool [:(Class (Q)),(Class (Q)):] is non empty V143() set
bool (Q) is non empty V143() set
x is Relation-like Class (Q) -defined Class (Q) -valued Element of bool [:(Class (Q)),(Class (Q)):]
p is Element of bool (Q)
p is Element of bool (Q)
[p,p] is V1() Element of [:(bool (Q)),(bool (Q)):]
[:(bool (Q)),(bool (Q)):] is non empty Relation-like set
q is Element of (Q)
r is Element of (Q)
q is Element of bool (Q)
E is Element of bool (Q)
x is Relation-like Class (Q) -defined Class (Q) -valued Element of bool [:(Class (Q)),(Class (Q)):]
p is Relation-like Class (Q) -defined Class (Q) -valued Element of bool [:(Class (Q)),(Class (Q)):]
p is Element of bool (Q)
q is Element of bool (Q)
[p,q] is V1() Element of [:(bool (Q)),(bool (Q)):]
[:(bool (Q)),(bool (Q)):] is non empty Relation-like set
r is Element of (Q)
q is Element of (Q)
r is Element of (Q)
q is Element of (Q)
p is set
q is set
[p,q] is V1() set
Q is () ()
(Q) is non empty set
(Q) is non empty set
the of Q is non empty set
[:(Q),Borel_Sets:] is non empty Relation-like set
bool (Q) is non empty V143() set
(Q) is Relation-like (Q) -defined (Q) -valued reflexive symmetric transitive V31((Q)) Element of bool [:(Q),(Q):]
[:(Q),(Q):] is non empty Relation-like set
bool [:(Q),(Q):] is non empty V143() set
(Q) is Relation-like Class (Q) -defined Class (Q) -valued Element of bool [:(Class (Q)),(Class (Q)):]
Class (Q) is non empty V20() a_partition of (Q)
[:(Class (Q)),(Class (Q)):] is non empty Relation-like set
bool [:(Class (Q)),(Class (Q)):] is non empty V143() set
x is Element of (Q)
Class ((Q),x) is Element of bool (Q)
p is Element of (Q)
Class ((Q),p) is Element of bool (Q)
[(Class ((Q),x)),(Class ((Q),p))] is V1() Element of [:(bool (Q)),(bool (Q)):]
[:(bool (Q)),(bool (Q)):] is non empty Relation-like set
[x,x] is V1() Element of [:(Q),(Q):]
[p,p] is V1() Element of [:(Q),(Q):]
p is Element of (Q)
q is Element of (Q)
Q is () ()
(Q) is non empty set
(Q) is non empty set
the of Q is non empty set
[:(Q),Borel_Sets:] is non empty Relation-like set
bool (Q) is non empty V143() set
(Q) is Relation-like (Q) -defined (Q) -valued reflexive symmetric transitive V31((Q)) Element of bool [:(Q),(Q):]
[:(Q),(Q):] is non empty Relation-like set
bool [:(Q),(Q):] is non empty V143() set
Class (Q) is non empty V20() a_partition of (Q)
x is Element of bool (Q)
p is Element of bool (Q)
p is set
Class ((Q),p) is Element of bool (Q)
q is Element of (Q)
(Q,q) is Element of (Q)
(Q,q) is Element of (Q)
(Q,q) is Event of Borel_Sets
(Q,q) ` is V131() V132() V133() Element of bool REAL
REAL \ (Q,q) is V131() V132() V133() set
[(Q,q),((Q,q) `)] is V1() Element of [:(Q),(bool REAL):]
[:(Q),(bool REAL):] is non empty Relation-like set
r is Element of (Q)
(Q,r) is Element of (Q)
(Q,r) is Element of (Q)
(Q,r) is Event of Borel_Sets
(Q,r) ` is V131() V132() V133() Element of bool REAL
REAL \ (Q,r) is V131() V132() V133() set
[(Q,r),((Q,r) `)] is V1() Element of [:(Q),(bool REAL):]
[q,r] is V1() Element of [:(Q),(Q):]
q is set
Class ((Q),q) is Element of bool (Q)
(Q) is non empty set
the of Q is non empty set
s is Element of (Q)
(Q,(Q,q),s) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets
the of Q is Relation-like [: the of Q, the of Q:] -defined (REAL,Borel_Sets) -valued Function-like quasi_total Element of bool [:[: the of Q, the of Q:],(REAL,Borel_Sets):]
[: the of Q, the of Q:] is non empty Relation-like set
[:[: the of Q, the of Q:],(REAL,Borel_Sets):] is non empty Relation-like set
bool [:[: the of Q, the of Q:],(REAL,Borel_Sets):] is non empty V143() set
[(Q,q),s] is V1() Element of [:(Q),(Q):]
[:(Q),(Q):] is non empty Relation-like set
the of Q . [(Q,q),s] is set
E is Event of Borel_Sets
(Q,(Q,q),s) . E is ext-real V43() V44() Element of REAL
(Q,(Q,r),s) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets
[(Q,r),s] is V1() Element of [:(Q),(Q):]
the of Q . [(Q,r),s] is set
q is Event of Borel_Sets
(Q,(Q,r),s) . q is ext-real V43() V44() Element of REAL
(Q,(Q,q)) is Element of (Q)
(Q,(Q,q)) is Event of Borel_Sets
(Q,(Q,r)) is Element of (Q)
1 - ((Q,(Q,q),s) . E) is ext-real V43() V44() Element of REAL
(Q,(Q,q),s) . (Q,q) is ext-real V43() V44() Element of REAL
(Q,(Q,r),s) . (Q,r) is ext-real V43() V44() Element of REAL
1 - ((Q,(Q,r),s) . q) is ext-real V43() V44() Element of REAL
(Q,(Q,(Q,q)),s) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets
[(Q,(Q,q)),s] is V1() Element of [:(Q),(Q):]
the of Q . [(Q,(Q,q)),s] is set
(Q,(Q,(Q,q)),s) . (Q,(Q,q)) is ext-real V43() V44() Element of REAL
(Q,(Q,(Q,r)),s) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets
[(Q,(Q,r)),s] is V1() Element of [:(Q),(Q):]
the of Q . [(Q,(Q,r)),s] is set
(Q,(Q,r)) is Event of Borel_Sets
(Q,(Q,(Q,r)),s) . (Q,(Q,r)) is ext-real V43() V44() Element of REAL
q is Element of (Q)
[(Q,q),q] is V1() Element of [:(Q),(Q):]
[(Q,r),q] is V1() Element of [:(Q),(Q):]
Q is () ()
(Q) is non empty set
(Q) is non empty set
the of Q is non empty set
[:(Q),Borel_Sets:] is non empty Relation-like set
bool (Q) is non empty V143() set
(Q) is Relation-like (Q) -defined (Q) -valued reflexive symmetric transitive V31((Q)) Element of bool [:(Q),(Q):]
[:(Q),(Q):] is non empty Relation-like set
bool [:(Q),(Q):] is non empty V143() set
Class (Q) is non empty V20() a_partition of (Q)
x is Element of bool (Q)
p is Element of bool (Q)
p is Element of (Q)
(Q,p) is Element of (Q)
(Q,p) is Element of (Q)
(Q,p) is Event of Borel_Sets
(Q,p) ` is V131() V132() V133() Element of bool REAL
REAL \ (Q,p) is V131() V132() V133() set
[(Q,p),((Q,p) `)] is V1() Element of [:(Q),(bool REAL):]
[:(Q),(bool REAL):] is non empty Relation-like set
q is Element of (Q)
(Q,q) is Element of (Q)
(Q,q) is Element of (Q)
(Q,q) is Event of Borel_Sets
(Q,q) ` is V131() V132() V133() Element of bool REAL
REAL \ (Q,q) is V131() V132() V133() set
[(Q,q),((Q,q) `)] is V1() Element of [:(Q),(bool REAL):]
(Q,(Q,p)) is Element of (Q)
(Q,(Q,p)) is Element of (Q)
(Q,(Q,p)) is Event of Borel_Sets
(Q,(Q,p)) ` is V131() V132() V133() Element of bool REAL
REAL \ (Q,(Q,p)) is V131() V132() V133() set
[(Q,(Q,p)),((Q,(Q,p)) `)] is V1() Element of [:(Q),(bool REAL):]
(Q,(Q,q)) is Element of (Q)
(Q,(Q,q)) is Element of (Q)
(Q,(Q,q)) is Event of Borel_Sets
(Q,(Q,q)) ` is V131() V132() V133() Element of bool REAL
REAL \ (Q,(Q,q)) is V131() V132() V133() set
[(Q,(Q,q)),((Q,(Q,q)) `)] is V1() Element of [:(Q),(bool REAL):]
Q is () ()
(Q) is non empty set
(Q) is non empty set
the of Q is non empty set
[:(Q),Borel_Sets:] is non empty Relation-like set
(Q) is Relation-like (Q) -defined (Q) -valued reflexive symmetric transitive V31((Q)) Element of bool [:(Q),(Q):]
[:(Q),(Q):] is non empty Relation-like set
bool [:(Q),(Q):] is non empty V143() set
Class (Q) is non empty V20() a_partition of (Q)
[:(Class (Q)),(Class (Q)):] is non empty Relation-like set
bool [:(Class (Q)),(Class (Q)):] is non empty V143() set
x is set
p is Element of (Q)
Class ((Q),p) is Element of bool (Q)
bool (Q) is non empty V143() set
(Q,p) is Element of (Q)
(Q,p) is Element of (Q)
(Q,p) is Event of Borel_Sets
(Q,p) ` is V131() V132() V133() Element of bool REAL
REAL \ (Q,p) is V131() V132() V133() set
[(Q,p),((Q,p) `)] is V1() Element of [:(Q),(bool REAL):]
[:(Q),(bool REAL):] is non empty Relation-like set
Class ((Q),(Q,p)) is Element of bool (Q)
p is set
q is Element of (Q)
Class ((Q),q) is Element of bool (Q)
(Q,q) is Element of (Q)
(Q,q) is Element of (Q)
(Q,q) is Event of Borel_Sets
(Q,q) ` is V131() V132() V133() Element of bool REAL
REAL \ (Q,q) is V131() V132() V133() set
[(Q,q),((Q,q) `)] is V1() Element of [:(Q),(bool REAL):]
Class ((Q),(Q,q)) is Element of bool (Q)
r is Element of bool (Q)
q is Element of bool (Q)
x is Relation-like Class (Q) -defined Class (Q) -valued Function-like quasi_total Element of bool [:(Class (Q)),(Class (Q)):]
p is Element of (Q)
Class ((Q),p) is Element of bool (Q)
bool (Q) is non empty V143() set
x . (Class ((Q),p)) is set
(Q,p) is Element of (Q)
(Q,p) is Element of (Q)
(Q,p) is Event of Borel_Sets
(Q,p) ` is V131() V132() V133() Element of bool REAL
REAL \ (Q,p) is V131() V132() V133() set
[(Q,p),((Q,p) `)] is V1() Element of [:(Q),(bool REAL):]
[:(Q),(bool REAL):] is non empty Relation-like set
Class ((Q),(Q,p)) is Element of bool (Q)
x is Relation-like Class (Q) -defined Class (Q) -valued Function-like quasi_total Element of bool [:(Class (Q)),(Class (Q)):]
p is Relation-like Class (Q) -defined Class (Q) -valued Function-like quasi_total Element of bool [:(Class (Q)),(Class (Q)):]
p is set
q is Element of (Q)
Class ((Q),q) is Element of bool (Q)
bool (Q) is non empty V143() set
x . p is set
(Q,q) is Element of (Q)
(Q,q) is Element of (Q)
(Q,q) is Event of Borel_Sets
(Q,q) ` is V131() V132() V133() Element of bool REAL
REAL \ (Q,q) is V131() V132() V133() set
[(Q,q),((Q,q) `)] is V1() Element of [:(Q),(bool REAL):]
[:(Q),(bool REAL):] is non empty Relation-like set
Class ((Q),(Q,q)) is Element of bool (Q)
p . p is set
Q is () ()
(Q) is non empty set
(Q) is non empty set
the of Q is non empty set
[:(Q),Borel_Sets:] is non empty Relation-like set
(Q) is Relation-like (Q) -defined (Q) -valued reflexive symmetric transitive V31((Q)) Element of bool [:(Q),(Q):]
[:(Q),(Q):] is non empty Relation-like set
bool [:(Q),(Q):] is non empty V143() set
Class (Q) is non empty V20() a_partition of (Q)
(Q) is Relation-like Class (Q) -defined Class (Q) -valued Element of bool [:(Class (Q)),(Class (Q)):]
[:(Class (Q)),(Class (Q)):] is non empty Relation-like set
bool [:(Class (Q)),(Class (Q)):] is non empty V143() set
(Q) is Relation-like Class (Q) -defined Class (Q) -valued Function-like quasi_total Element of bool [:(Class (Q)),(Class (Q)):]
((Class (Q)),(Q),(Q)) is () ()
x is set
p is set
[x,p] is V1() set
p is set
[p,p] is V1() set
[x,p] is V1() set
q is Element of (Q)
Class ((Q),q) is Element of bool (Q)
bool (Q) is non empty V143() set
r is Element of (Q)
Class ((Q),r) is Element of bool (Q)
q is Element of (Q)
Class ((Q),q) is Element of bool (Q)
x is set
p is set
[x,p] is V1() set
[p,x] is V1() set
p is Element of (Q)
Class ((Q),p) is Element of bool (Q)
bool (Q) is non empty V143() set
q is Element of (Q)
Class ((Q),q) is Element of bool (Q)
[p,q] is V1() Element of [:(Q),(Q):]
bool (Q) is non empty V143() set
x is Element of Class (Q)
p is Element of Class (Q)
[x,p] is V1() Element of [:(Class (Q)),(Class (Q)):]
(Q) . p is Element of Class (Q)
(Q) . x is Element of Class (Q)
[((Q) . p),((Q) . x)] is V1() Element of [:(Class (Q)),(Class (Q)):]
p is Element of (Q)
Class ((Q),p) is Element of bool (Q)
q is Element of (Q)
Class ((Q),q) is Element of bool (Q)
(Q,q) is Element of (Q)
(Q,q) is Element of (Q)
(Q,q) is Event of Borel_Sets
(Q,q) ` is V131() V132() V133() Element of bool REAL
REAL \ (Q,q) is V131() V132() V133() set
[(Q,q),((Q,q) `)] is V1() Element of [:(Q),(bool REAL):]
[:(Q),(bool REAL):] is non empty Relation-like set
(Q,p) is Element of (Q)
(Q,p) is Element of (Q)
(Q,p) is Event of Borel_Sets
(Q,p) ` is V131() V132() V133() Element of bool REAL
REAL \ (Q,p) is V131() V132() V133() set
[(Q,p),((Q,p) `)] is V1() Element of [:(Q),(bool REAL):]
(Q) . (Class ((Q),p)) is set
Class ((Q),(Q,p)) is Element of bool (Q)
(Q) . (Class ((Q),q)) is set
Class ((Q),(Q,q)) is Element of bool (Q)
x is Element of Class (Q)
(Q) . x is set
(Q) . ((Q) . x) is set
p is Element of (Q)
Class ((Q),p) is Element of bool (Q)
(Q) . x is Element of Class (Q)
(Q) . ((Q) . x) is Element of Class (Q)
(Q,p) is Element of (Q)
(Q,p) is Element of (Q)
(Q,p) is Event of Borel_Sets
(Q,p) ` is V131() V132() V133() Element of bool REAL
REAL \ (Q,p) is V131() V132() V133() set
[(Q,p),((Q,p) `)] is V1() Element of [:(Q),(bool REAL):]
[:(Q),(bool REAL):] is non empty Relation-like set
Class ((Q),(Q,p)) is Element of bool (Q)
(Q) . (Class ((Q),(Q,p))) is set
(Q,(Q,p)) is Element of (Q)
(Q,(Q,p)) is Element of (Q)
(Q,(Q,p)) is Event of Borel_Sets
(Q,(Q,p)) ` is V131() V132() V133() Element of bool REAL
REAL \ (Q,(Q,p)) is V131() V132() V133() set
[(Q,(Q,p)),((Q,(Q,p)) `)] is V1() Element of [:(Q),(bool REAL):]
Class ((Q),(Q,(Q,p))) is Element of bool (Q)
x is set
[x,x] is V1() set
p is Element of (Q)
Class ((Q),p) is Element of bool (Q)