NAT is non empty V24() V25() V26() V31() V36() V37() countable denumerable Element of bool REAL
REAL is set
bool REAL is non empty set
NAT is non empty V24() V25() V26() V31() V36() V37() countable denumerable set
bool NAT is non empty V31() set
bool NAT is non empty V31() set
{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty Function-yielding V22() V24() V25() V26() V28() V29() V30() V31() V36() V38( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable set
the Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty Function-yielding V22() V24() V25() V26() V28() V29() V30() V31() V36() V38( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable set is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty Function-yielding V22() V24() V25() V26() V28() V29() V30() V31() V36() V38( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable set
1 is non empty set
2 is non empty set
3 is non empty set
0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty Function-yielding V22() V24() V25() V26() V28() V29() V30() V31() V36() V38( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable Element of NAT
Seg 1 is countable Element of bool NAT
{1} is non empty trivial V38(1) set
Seg 2 is countable Element of bool NAT
{1,2} is non empty set
FALSE is V24() V25() V26() V30() V31() V36() boolean countable set
TRUE is V24() V25() V26() V30() V31() V36() boolean countable set
dom {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty Function-yielding V22() V24() V25() V26() V28() V29() V30() V31() V36() V38( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable set
rng {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty trivial Function-yielding V22() V24() V25() V26() V28() V29() V30() V31() V36() V38( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable set
D is non empty set
P is set
A is Element of D
P --> A is Relation-like P -defined D -valued Function-like constant total set
{A} is non empty trivial V38(1) set
[:P,{A}:] is Relation-like set
[:P,D:] is Relation-like set
bool [:P,D:] is non empty set
P --> A is Relation-like P -defined D -valued Function-like constant total quasi_total Element of bool [:P,D:]
dom (P --> A) is set
D is functional FinSequence-membered set
P is Relation-like NAT -defined Function-like V31() FinSequence-like FinSubsequence-like countable set
A is Relation-like NAT -defined Function-like V31() FinSequence-like FinSubsequence-like countable set
len P is V24() V25() V26() V30() V31() V36() countable Element of NAT
len A is V24() V25() V26() V30() V31() V36() countable Element of NAT
dom P is countable Element of bool NAT
dom A is countable Element of bool NAT
P is Relation-like Function-like set
A is Relation-like Function-like set
dom P is set
dom A is set
x is Relation-like NAT -defined Function-like V31() FinSequence-like FinSubsequence-like countable set
len x is V24() V25() V26() V30() V31() V36() countable Element of NAT
x is Relation-like NAT -defined Function-like V31() FinSequence-like FinSubsequence-like countable set
len x is V24() V25() V26() V30() V31() V36() countable Element of NAT
D is set
P is Relation-like NAT -defined Function-like V31() FinSequence-like FinSubsequence-like countable set
A is Relation-like NAT -defined Function-like V31() FinSequence-like FinSubsequence-like countable set
len P is V24() V25() V26() V30() V31() V36() countable Element of NAT
len A is V24() V25() V26() V30() V31() V36() countable Element of NAT
D is set
P is functional FinSequence-membered with_common_domain set
D is Relation-like NAT -defined Function-like V31() FinSequence-like FinSubsequence-like countable set
{D} is functional non empty trivial V38(1) with_common_domain set
P is set
P is functional FinSequence-membered set
F1() is set
D is set
P is set
A is Relation-like NAT -defined Function-like V31() FinSequence-like FinSubsequence-like countable set
P is functional FinSequence-membered set
A is Relation-like NAT -defined Function-like V31() FinSequence-like FinSubsequence-like countable set
len A is V24() V25() V26() V30() V31() V36() countable Element of NAT
x is Relation-like NAT -defined Function-like V31() FinSequence-like FinSubsequence-like countable set
len x is V24() V25() V26() V30() V31() V36() countable Element of NAT
x is Relation-like NAT -defined Function-like V31() FinSequence-like FinSubsequence-like countable set
n is Relation-like NAT -defined Function-like V31() FinSequence-like FinSubsequence-like countable set
A is functional FinSequence-membered with_common_domain set
x is Relation-like NAT -defined Function-like V31() FinSequence-like FinSubsequence-like countable set
x is Relation-like NAT -defined Function-like V31() FinSequence-like FinSubsequence-like countable set
D is functional FinSequence-membered with_common_domain set
P is functional FinSequence-membered with_common_domain set
A is Relation-like NAT -defined Function-like V31() FinSequence-like FinSubsequence-like countable set
x is Relation-like NAT -defined Function-like V31() FinSequence-like FinSubsequence-like countable set
A is set
x is set
D is set
P is Relation-like NAT -defined Function-like V31() FinSequence-like FinSubsequence-like countable set
A is Relation-like NAT -defined Function-like V31() FinSequence-like FinSubsequence-like countable set
len P is V24() V25() V26() V30() V31() V36() countable Element of NAT
len A is V24() V25() V26() V30() V31() V36() countable Element of NAT
D is functional FinSequence-membered with_common_domain set
P is set
D is functional FinSequence-membered with_common_domain set
P is Relation-like NAT -defined Function-like V31() FinSequence-like FinSubsequence-like countable set
len P is V24() V25() V26() V30() V31() V36() countable Element of NAT
A is Relation-like NAT -defined Function-like V31() FinSequence-like FinSubsequence-like countable set
len A is V24() V25() V26() V30() V31() V36() countable Element of NAT
P is V24() V25() V26() V30() V31() V36() countable Element of NAT
A is V24() V25() V26() V30() V31() V36() countable Element of NAT
x is Relation-like NAT -defined Function-like V31() FinSequence-like FinSubsequence-like countable set
len x is V24() V25() V26() V30() V31() V36() countable Element of NAT
D is V24() V25() V26() V30() V31() V36() countable Element of NAT
P is Relation-like NAT -defined Function-like V31() FinSequence-like FinSubsequence-like countable set
len P is V24() V25() V26() V30() V31() V36() countable Element of NAT
D is set
P is Relation-like NAT -defined Function-like V31() FinSequence-like FinSubsequence-like countable set
rng P is set
D is set
P is Relation-like NAT -defined Function-like V31() FinSequence-like FinSubsequence-like countable set
rng P is set
D is V24() V25() V26() V30() V31() V36() countable Element of NAT
P is Relation-like NAT -defined Function-like V31() FinSequence-like FinSubsequence-like countable set
len P is V24() V25() V26() V30() V31() V36() countable Element of NAT
D is set
P is V24() V25() V26() V30() V31() V36() countable Element of NAT
D is non empty set
D * is functional non empty FinSequence-membered FinSequenceSet of D
bool (D *) is non empty set
P is set
A is set
x is Relation-like NAT -defined D -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of D
x is Relation-like NAT -defined D -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of D
len x is V24() V25() V26() V30() V31() V36() countable Element of NAT
len x is V24() V25() V26() V30() V31() V36() countable Element of NAT
n is set
A is set
x is Relation-like NAT -defined D -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of D
x is Relation-like NAT -defined D -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of D
len x is V24() V25() V26() V30() V31() V36() countable Element of NAT
len x is V24() V25() V26() V30() V31() V36() countable Element of NAT
n is set
P is set
A is set
x is set
x is Relation-like NAT -defined D -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of D
n is Relation-like NAT -defined D -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of D
len x is V24() V25() V26() V30() V31() V36() countable Element of NAT
len n is V24() V25() V26() V30() V31() V36() countable Element of NAT
x is Relation-like NAT -defined D -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of D
n is Relation-like NAT -defined D -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of D
len x is V24() V25() V26() V30() V31() V36() countable Element of NAT
len n is V24() V25() V26() V30() V31() V36() countable Element of NAT
D is non empty set
(D) is set
P is Relation-like NAT -defined D -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of D
A is Relation-like NAT -defined D -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of D
len P is V24() V25() V26() V30() V31() V36() countable Element of NAT
len A is V24() V25() V26() V30() V31() V36() countable Element of NAT
D * is functional non empty FinSequence-membered FinSequenceSet of D
bool (D *) is non empty set
P is set
A is non empty set
x is set
x is Relation-like NAT -defined D -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of D
n is Relation-like NAT -defined D -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of D
len x is V24() V25() V26() V30() V31() V36() countable Element of NAT
len n is V24() V25() V26() V30() V31() V36() countable Element of NAT
c7 is set
D is non empty set
(D) is non empty set
P is set
A is Element of (D)
x is Relation-like NAT -defined D -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of D
x is Relation-like NAT -defined D -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of D
len x is V24() V25() V26() V30() V31() V36() countable Element of NAT
len x is V24() V25() V26() V30() V31() V36() countable Element of NAT
D * is functional non empty FinSequence-membered FinSequenceSet of D
D is non empty set
(D) is non empty set
P is Relation-like NAT -defined D -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of D
{P} is functional non empty trivial V38(1) with_common_domain set
A is Relation-like NAT -defined D -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of D
x is Relation-like NAT -defined D -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of D
len A is V24() V25() V26() V30() V31() V36() countable Element of NAT
len x is V24() V25() V26() V30() V31() V36() countable Element of NAT
D * is functional non empty FinSequence-membered FinSequenceSet of D
D is non empty set
(D) is non empty set
P is Element of D
A is Element of D
<*P,A*> is Relation-like NAT -defined Function-like non empty V31() V38(2) FinSequence-like FinSubsequence-like countable set
<*P*> is Relation-like NAT -defined Function-like constant non empty trivial V31() V38(1) FinSequence-like FinSubsequence-like countable set
[1,P] is set
{1,P} is non empty set
{{1,P},{1}} is non empty set
{[1,P]} is Relation-like Function-like constant non empty trivial V38(1) set
<*A*> is Relation-like NAT -defined Function-like constant non empty trivial V31() V38(1) FinSequence-like FinSubsequence-like countable set
[1,A] is set
{1,A} is non empty set
{{1,A},{1}} is non empty set
{[1,A]} is Relation-like Function-like constant non empty trivial V38(1) set
<*P*> ^ <*A*> is Relation-like NAT -defined Function-like non empty V31() FinSequence-like FinSubsequence-like countable set
{<*P,A*>} is functional non empty trivial V38(1) with_common_domain set
x is Relation-like NAT -defined D -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of D
x is Relation-like NAT -defined D -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of D
len x is V24() V25() V26() V30() V31() V36() countable Element of NAT
len x is V24() V25() V26() V30() V31() V36() countable Element of NAT
<*P*> is Relation-like NAT -defined D -valued Function-like constant non empty trivial V31() V38(1) FinSequence-like FinSubsequence-like countable FinSequence of D
<*A*> is Relation-like NAT -defined D -valued Function-like constant non empty trivial V31() V38(1) FinSequence-like FinSubsequence-like countable FinSequence of D
<*P*> ^ <*A*> is Relation-like NAT -defined D -valued Function-like non empty V31() FinSequence-like FinSubsequence-like countable FinSequence of D
D * is functional non empty FinSequence-membered FinSequenceSet of D
D is non empty set
(D) is non empty set
P is Element of (D)
A is Element of (D)
x is Relation-like NAT -defined D -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of D
x is Relation-like NAT -defined D -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of D
x is set
D * is functional non empty FinSequence-membered FinSequenceSet of D
bool (D *) is non empty set
F1() is non empty set
(F1()) is non empty set
F1() * is functional non empty FinSequence-membered FinSequenceSet of F1()
D is set
P is Relation-like NAT -defined F1() -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of F1()
A is Relation-like NAT -defined F1() -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of F1()
len P is V24() V25() V26() V30() V31() V36() countable Element of NAT
len A is V24() V25() V26() V30() V31() V36() countable Element of NAT
x is Relation-like NAT -defined F1() -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of F1()
x is Relation-like NAT -defined F1() -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of F1()
P is set
P is Element of (F1())
A is Relation-like NAT -defined F1() -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of F1()
x is Relation-like NAT -defined F1() -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of F1()
D is non empty set
(D) is non empty set
P is Relation-like NAT -defined D -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of D
len P is V24() V25() V26() V30() V31() V36() countable Element of NAT
A is Relation-like NAT -defined D -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of D
len A is V24() V25() V26() V30() V31() V36() countable Element of NAT
P is Element of (D)
A is Relation-like NAT -defined D -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of D
P is Element of (D)
A is Element of (D)
x is Relation-like NAT -defined D -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of D
x is Relation-like NAT -defined D -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of D
D is non empty set
(D) is Element of (D)
(D) is non empty set
the Element of (D) is Element of (D)
D * is functional non empty FinSequence-membered FinSequenceSet of D
bool (D *) is non empty set
A is Relation-like NAT -defined D -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of D
D is non empty set
(D) is non empty set
P is Element of (D)
(D) is Element of (D)
A is Relation-like NAT -defined D -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of D
len A is V24() V25() V26() V30() V31() V36() countable Element of NAT
x is Relation-like NAT -defined D -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of D
len x is V24() V25() V26() V30() V31() V36() countable Element of NAT
A is V24() V25() V26() V30() V31() V36() countable Element of NAT
x is V24() V25() V26() V30() V31() V36() countable Element of NAT
x is Relation-like NAT -defined D -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of D
len x is V24() V25() V26() V30() V31() V36() countable Element of NAT
F1() is non empty set
(F1()) is non empty set
F2() is V24() V25() V26() V30() V31() V36() countable Element of NAT
F1() * is functional non empty FinSequence-membered FinSequenceSet of F1()
D is set
P is Relation-like NAT -defined F1() -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of F1()
A is Relation-like NAT -defined F1() -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of F1()
len P is V24() V25() V26() V30() V31() V36() countable Element of NAT
len A is V24() V25() V26() V30() V31() V36() countable Element of NAT
x is Relation-like NAT -defined F1() -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of F1()
len x is V24() V25() V26() V30() V31() V36() countable Element of NAT
x is Relation-like NAT -defined F1() -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of F1()
len x is V24() V25() V26() V30() V31() V36() countable Element of NAT
P is set
P is Element of (F1())
A is Relation-like NAT -defined F1() -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of F1()
len A is V24() V25() V26() V30() V31() V36() countable Element of NAT
x is Relation-like NAT -defined F1() -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of F1()
len x is V24() V25() V26() V30() V31() V36() countable Element of NAT
{0,1} is non empty set
() is set
D is set
() is V24() V25() V26() V30() V31() V36() boolean countable Element of ()
() is V24() V25() V26() V30() V31() V36() boolean countable Element of ()
D is Element of ()
D is V24() V25() V26() V30() V31() V36() boolean countable set
() is V24() V25() V26() V30() V31() V36() boolean countable Element of ()
'not' D is V24() V25() V26() V30() V31() V36() boolean countable set
K107(1,D) is set
() is V24() V25() V26() V30() V31() V36() boolean countable Element of ()
P is V24() V25() V26() V30() V31() V36() boolean countable set
P is V24() V25() V26() V30() V31() V36() boolean countable set
D '&' P is V24() V25() V26() V30() V31() V36() boolean countable set
K104(D,P) is set
A is set
D is V24() V25() V26() V30() V31() V36() boolean countable Element of ()
'not' D is V24() V25() V26() V30() V31() V36() boolean countable set
K107(1,D) is set
P is V24() V25() V26() V30() V31() V36() boolean countable Element of ()
D '&' P is V24() V25() V26() V30() V31() V36() boolean countable set
K104(D,P) is set
D is V24() V25() V26() V30() V31() V36() boolean countable set
'not' D is V24() V25() V26() V30() V31() V36() boolean countable set
K107(1,D) is set
P is V24() V25() V26() V30() V31() V36() boolean countable set
'not' P is V24() V25() V26() V30() V31() V36() boolean countable set
K107(1,P) is set
A is V24() V25() V26() V30() V31() V36() boolean countable set
'not' A is V24() V25() V26() V30() V31() V36() boolean countable set
K107(1,A) is set
x is V24() V25() V26() V30() V31() V36() boolean countable set
'not' x is V24() V25() V26() V30() V31() V36() boolean countable set
K107(1,x) is set
D is V24() V25() V26() V30() V31() V36() boolean countable set
P is V24() V25() V26() V30() V31() V36() boolean countable set
D '&' P is V24() V25() V26() V30() V31() V36() boolean countable set
K104(D,P) is set
A is V24() V25() V26() V30() V31() V36() boolean countable set
x is V24() V25() V26() V30() V31() V36() boolean countable set
A '&' x is V24() V25() V26() V30() V31() V36() boolean countable set
K104(A,x) is set
x is V24() V25() V26() V30() V31() V36() boolean countable set
n is V24() V25() V26() V30() V31() V36() boolean countable set
x '&' n is V24() V25() V26() V30() V31() V36() boolean countable set
K104(x,n) is set
c7 is V24() V25() V26() V30() V31() V36() boolean countable set
c8 is V24() V25() V26() V30() V31() V36() boolean countable set
c7 '&' c8 is V24() V25() V26() V30() V31() V36() boolean countable set
K104(c7,c8) is set
D is V24() V25() V26() V30() V31() V36() boolean countable set
() '&' D is V24() V25() V26() V30() V31() V36() boolean countable set
K104((),D) is set
D is V24() V25() V26() V30() V31() V36() boolean countable set
() '&' D is V24() V25() V26() V30() V31() V36() boolean countable set
K104((),D) is set
D is V24() V25() V26() V30() V31() V36() boolean countable set
D '&' D is V24() V25() V26() V30() V31() V36() boolean countable set
K104(D,D) is set
D is V24() V25() V26() V30() V31() V36() boolean countable set
P is V24() V25() V26() V30() V31() V36() boolean countable set
A is V24() V25() V26() V30() V31() V36() boolean countable set
P '&' A is V24() V25() V26() V30() V31() V36() boolean countable set
K104(P,A) is set
D '&' (P '&' A) is V24() V25() V26() V30() V31() V36() boolean countable set
K104(D,(P '&' A)) is set
D '&' P is V24() V25() V26() V30() V31() V36() boolean countable set
K104(D,P) is set
(D '&' P) '&' A is V24() V25() V26() V30() V31() V36() boolean countable set
K104((D '&' P),A) is set
D is set
D is set
(D) is set
D is set
(D) is V24() V25() V26() V30() V31() V36() boolean countable set
D is set
(D) is V24() V25() V26() V30() V31() V36() boolean countable Element of ()
P is set
(P) is V24() V25() V26() V30() V31() V36() boolean countable Element of ()
A is set
(A) is V24() V25() V26() V30() V31() V36() boolean countable Element of ()
x is set
(x) is V24() V25() V26() V30() V31() V36() boolean countable Element of ()
D is Relation-like Function-like () set
P is set
D . P is set
dom D is set
dom D is set
rng D is set
dom D is set
D is Relation-like Function-like () set
dom D is set
P is Relation-like Function-like set
dom P is set
A is set
rng P is set
x is set
P . x is set
D . x is V24() V25() V26() V30() V31() V36() boolean countable set
'not' (D . x) is V24() V25() V26() V30() V31() V36() boolean countable set
K107(1,(D . x)) is set
P is Relation-like Function-like () set
dom P is set
A is Relation-like Function-like () set
dom A is set
x is set
P . x is V24() V25() V26() V30() V31() V36() boolean countable set
A . x is V24() V25() V26() V30() V31() V36() boolean countable set
D . x is V24() V25() V26() V30() V31() V36() boolean countable set
'not' (D . x) is V24() V25() V26() V30() V31() V36() boolean countable set
K107(1,(D . x)) is set
P is Relation-like Function-like () set
dom P is set
A is Relation-like Function-like () set
dom A is set
x is set
A . x is V24() V25() V26() V30() V31() V36() boolean countable set
P . x is V24() V25() V26() V30() V31() V36() boolean countable set
'not' (P . x) is V24() V25() V26() V30() V31() V36() boolean countable set
K107(1,(P . x)) is set
'not' (A . x) is V24() V25() V26() V30() V31() V36() boolean countable set
K107(1,(A . x)) is set
'not' ('not' (A . x)) is V24() V25() V26() V30() V31() V36() boolean countable set
K107(1,('not' (A . x))) is set
P is Relation-like Function-like () set
dom P is set
(dom D) /\ (dom P) is set
A is Relation-like Function-like set
dom A is set
x is set
rng A is set
x is set
A . x is set
D . x is V24() V25() V26() V30() V31() V36() boolean countable set
P . x is V24() V25() V26() V30() V31() V36() boolean countable set
(D . x) '&' (P . x) is V24() V25() V26() V30() V31() V36() boolean countable set
K104((D . x),(P . x)) is set
A is Relation-like Function-like () set
dom A is set
x is Relation-like Function-like () set
dom x is set
x is set
A . x is V24() V25() V26() V30() V31() V36() boolean countable set
x . x is V24() V25() V26() V30() V31() V36() boolean countable set
D . x is V24() V25() V26() V30() V31() V36() boolean countable set
P . x is V24() V25() V26() V30() V31() V36() boolean countable set
(D . x) '&' (P . x) is V24() V25() V26() V30() V31() V36() boolean countable set
K104((D . x),(P . x)) is set
A is Relation-like Function-like () set
dom A is set
x is Relation-like Function-like () set
dom x is set
x is Relation-like Function-like () set
dom x is set
(dom x) /\ (dom x) is set
(dom x) /\ (dom x) is set
n is set
A . n is V24() V25() V26() V30() V31() V36() boolean countable set
x . n is V24() V25() V26() V30() V31() V36() boolean countable set
x . n is V24() V25() V26() V30() V31() V36() boolean countable set
(x . n) '&' (x . n) is V24() V25() V26() V30() V31() V36() boolean countable set
K104((x . n),(x . n)) is set
A is Relation-like Function-like () set
dom A is set
(dom A) /\ (dom A) is set
x is set
x is Relation-like Function-like () set
dom x is set
x . x is V24() V25() V26() V30() V31() V36() boolean countable set
(x . x) '&' (x . x) is V24() V25() V26() V30() V31() V36() boolean countable set
K104((x . x),(x . x)) is set
D is set
[:D,():] is Relation-like set
bool [:D,():] is non empty set
P is Relation-like D -defined () -valued Function-like total quasi_total Element of bool [:D,():]
rng P is set
D is non empty set
[:D,():] is Relation-like non empty set
bool [:D,():] is non empty set
P is Relation-like D -defined () -valued Function-like non empty total quasi_total () Element of bool [:D,():]
(P) is Relation-like Function-like () set
dom (P) is set
dom P is non empty set
rng (P) is set
A is Relation-like D -defined () -valued Function-like non empty total quasi_total () Element of bool [:D,():]
dom A is non empty set
x is Element of D
dom P is non empty set
A . x is V24() V25() V26() V30() V31() V36() boolean countable Element of ()
P . x is V24() V25() V26() V30() V31() V36() boolean countable Element of ()
((P . x)) is V24() V25() V26() V30() V31() V36() boolean countable Element of ()
K107(1,(P . x)) is set
x is set
A . x is V24() V25() V26() V30() V31() V36() boolean countable set
P . x is V24() V25() V26() V30() V31() V36() boolean countable set
'not' (P . x) is V24() V25() V26() V30() V31() V36() boolean countable set
K107(1,(P . x)) is set
A is Relation-like D -defined () -valued Function-like non empty total quasi_total () Element of bool [:D,():]
(P,A) is Relation-like Function-like () set
rng (P,A) is set
dom P is non empty set
dom A is non empty set
dom (P,A) is set
D /\ D is set
x is Relation-like D -defined () -valued Function-like non empty total quasi_total () Element of bool [:D,():]
dom x is non empty set
dom A is non empty set
dom P is non empty set
dom (P,A) is set
D /\ D is set
x is Element of D
x . x is V24() V25() V26() V30() V31() V36() boolean countable Element of ()
P . x is V24() V25() V26() V30() V31() V36() boolean countable Element of ()
A . x is V24() V25() V26() V30() V31() V36() boolean countable Element of ()
((P . x),(A . x)) is V24() V25() V26() V30() V31() V36() boolean countable Element of ()
K104((P . x),(A . x)) is set
(dom P) /\ (dom A) is set
x is set
x . x is V24() V25() V26() V30() V31() V36() boolean countable set
P . x is V24() V25() V26() V30() V31() V36() boolean countable set
A . x is V24() V25() V26() V30() V31() V36() boolean countable set
(P . x) '&' (A . x) is V24() V25() V26() V30() V31() V36() boolean countable set
K104((P . x),(A . x)) is set
D is set
D * is functional non empty FinSequence-membered FinSequenceSet of D
[:(D *),D:] is Relation-like set
bool [:(D *),D:] is non empty set
D is Relation-like set
P is with_common_domain set
D | P is Relation-like set
dom (D | P) is set
D is non empty set
D * is functional non empty FinSequence-membered FinSequenceSet of D
[:(D *),D:] is Relation-like non empty set
bool [:(D *),D:] is non empty set
P is Relation-like D * -defined D -valued Function-like Element of bool [:(D *),D:]
dom P is set
D is non empty set
D * is functional non empty FinSequence-membered FinSequenceSet of D
[:(D *),D:] is Relation-like non empty set
bool [:(D *),D:] is non empty set
the Element of D is Element of D
<*> D is Relation-like non-empty empty-yielding NAT -defined D -valued Function-like one-to-one constant functional empty proper Function-yielding V22() V24() V25() V26() V28() V29() V30() V31() V36() V38( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding with_common_domain countable FinSequence of D
[:NAT,D:] is Relation-like non empty V31() set
(<*> D) .--> the Element of D is Relation-like bool [:NAT,D:] -defined {(<*> D)} -defined D -valued Function-like one-to-one set
bool [:NAT,D:] is non empty V31() set
{(<*> D)} is functional non empty trivial V38(1) with_common_domain set
{(<*> D)} --> the Element of D is Relation-like {(<*> D)} -defined D -valued { the Element of D} -valued Function-like constant non empty total quasi_total Element of bool [:{(<*> D)},{ the Element of D}:]
{ the Element of D} is non empty trivial V38(1) set
[:{(<*> D)},{ the Element of D}:] is Relation-like non empty set
bool [:{(<*> D)},{ the Element of D}:] is non empty set
dom ((<*> D) .--> the Element of D) is set
x is set
rng ((<*> D) .--> the Element of D) is set
x is set
x is Relation-like D * -defined D -valued Function-like Element of bool [:(D *),D:]
x is Relation-like NAT -defined D -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of D
len x is V24() V25() V26() V30() V31() V36() countable Element of NAT
n is Relation-like NAT -defined D -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of D
len n is V24() V25() V26() V30() V31() V36() countable Element of NAT
dom x is functional FinSequence-membered set
x is Relation-like NAT -defined Function-like V31() FinSequence-like FinSubsequence-like countable set
dom x is functional FinSequence-membered set
n is Relation-like NAT -defined Function-like V31() FinSequence-like FinSubsequence-like countable set
len x is V24() V25() V26() V30() V31() V36() countable Element of NAT
len n is V24() V25() V26() V30() V31() V36() countable Element of NAT
{{}} is functional non empty trivial V38(1) with_common_domain set
{{}} * is functional non empty FinSequence-membered FinSequenceSet of {{}}
[:({{}} *),{{}}:] is Relation-like non empty set
bool [:({{}} *),{{}}:] is non empty set
the Relation-like {{}} * -defined {{}} -valued Function-like non empty Function-yielding V22() () Element of bool [:({{}} *),{{}}:] is Relation-like {{}} * -defined {{}} -valued Function-like non empty Function-yielding V22() () Element of bool [:({{}} *),{{}}:]
D is Relation-like () set
dom D is set
D is non empty set
<*> D is Relation-like non-empty empty-yielding NAT -defined D -valued Function-like one-to-one constant functional empty proper Function-yielding V22() V24() V25() V26() V28() V29() V30() V31() V36() V38( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding with_common_domain countable FinSequence of D
[:NAT,D:] is Relation-like non empty V31() set
D * is functional non empty FinSequence-membered FinSequenceSet of D
[:(D *),D:] is Relation-like non empty set
bool [:(D *),D:] is non empty set
P is Element of D
(<*> D) .--> P is Relation-like bool [:NAT,D:] -defined {(<*> D)} -defined D -valued Function-like one-to-one set
bool [:NAT,D:] is non empty V31() set
{(<*> D)} is functional non empty trivial V38(1) with_common_domain set
{(<*> D)} --> P is Relation-like {(<*> D)} -defined D -valued {P} -valued Function-like constant non empty total quasi_total Element of bool [:{(<*> D)},{P}:]
{P} is non empty trivial V38(1) set
[:{(<*> D)},{P}:] is Relation-like non empty set
bool [:{(<*> D)},{P}:] is non empty set
dom ((<*> D) .--> P) is set
x is set
rng ((<*> D) .--> P) is set
x is set
x is Relation-like D * -defined D -valued Function-like Element of bool [:(D *),D:]
x is Relation-like NAT -defined D -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of D
len x is V24() V25() V26() V30() V31() V36() countable Element of NAT
n is Relation-like NAT -defined D -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of D
len n is V24() V25() V26() V30() V31() V36() countable Element of NAT
dom x is functional FinSequence-membered set
x is Relation-like NAT -defined Function-like V31() FinSequence-like FinSubsequence-like countable set
dom x is functional FinSequence-membered set
n is Relation-like NAT -defined Function-like V31() FinSequence-like FinSubsequence-like countable set
len x is V24() V25() V26() V30() V31() V36() countable Element of NAT
len n is V24() V25() V26() V30() V31() V36() countable Element of NAT
D is non empty set
<*> D is Relation-like non-empty empty-yielding NAT -defined D -valued Function-like one-to-one constant functional empty proper Function-yielding V22() V24() V25() V26() V28() V29() V30() V31() V36() V38( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding with_common_domain countable FinSequence of D
[:NAT,D:] is Relation-like non empty V31() set
D * is functional non empty FinSequence-membered FinSequenceSet of D
PFuncs ((D *),D) is functional non empty set
P is Element of D
(<*> D) .--> P is Relation-like bool [:NAT,D:] -defined {(<*> D)} -defined D -valued Function-like one-to-one set
bool [:NAT,D:] is non empty V31() set
{(<*> D)} is functional non empty trivial V38(1) with_common_domain set
{(<*> D)} --> P is Relation-like {(<*> D)} -defined D -valued {P} -valued Function-like constant non empty total quasi_total Element of bool [:{(<*> D)},{P}:]
{P} is non empty trivial V38(1) set
[:{(<*> D)},{P}:] is Relation-like non empty set
bool [:{(<*> D)},{P}:] is non empty set
dom ((<*> D) .--> P) is set
x is set
rng ((<*> D) .--> P) is set
x is set
[:(D *),D:] is Relation-like non empty set
bool [:(D *),D:] is non empty set
x is Relation-like D * -defined D -valued Function-like Element of bool [:(D *),D:]
D is set
D * is functional non empty FinSequence-membered FinSequenceSet of D
PFuncs ((D *),D) is functional non empty set
D is set
D * is functional non empty FinSequence-membered FinSequenceSet of D
PFuncs ((D *),D) is functional non empty set
D is non empty set
D * is functional non empty FinSequence-membered FinSequenceSet of D
PFuncs ((D *),D) is functional non empty set
P is Relation-like Function-like Element of PFuncs ((D *),D)
<*P*> is Relation-like NAT -defined Function-like constant non empty trivial V31() V38(1) FinSequence-like FinSubsequence-like countable set
[1,P] is set
{1,P} is non empty set
{{1,P},{1}} is non empty set
{[1,P]} is Relation-like Function-like constant non empty trivial V38(1) set
<*P*> is Relation-like NAT -defined PFuncs ((D *),D) -valued Function-like constant non empty trivial Function-yielding V22() V31() V38(1) FinSequence-like FinSubsequence-like countable FinSequence of PFuncs ((D *),D)
D is non empty set
D * is functional non empty FinSequence-membered FinSequenceSet of D
PFuncs ((D *),D) is functional non empty set
the Element of D is Element of D
[:(D *),D:] is Relation-like non empty set
bool [:(D *),D:] is non empty set
<*> D is Relation-like non-empty empty-yielding NAT -defined D -valued Function-like one-to-one constant functional empty proper Function-yielding V22() V24() V25() V26() V28() V29() V30() V31() V36() V38( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding with_common_domain countable FinSequence of D
[:NAT,D:] is Relation-like non empty V31() set
(<*> D) .--> the Element of D is Relation-like bool [:NAT,D:] -defined {(<*> D)} -defined D -valued Function-like one-to-one set
bool [:NAT,D:] is non empty V31() set
{(<*> D)} is functional non empty trivial V38(1) with_common_domain set
{(<*> D)} --> the Element of D is Relation-like {(<*> D)} -defined D -valued { the Element of D} -valued Function-like constant non empty total quasi_total Element of bool [:{(<*> D)},{ the Element of D}:]
{ the Element of D} is non empty trivial V38(1) set
[:{(<*> D)},{ the Element of D}:] is Relation-like non empty set
bool [:{(<*> D)},{ the Element of D}:] is non empty set
A is Relation-like D * -defined D -valued Function-like Element of bool [:(D *),D:]
x is Relation-like Function-like Element of PFuncs ((D *),D)
(D,x) is Relation-like NAT -defined PFuncs ((D *),D) -valued Function-like constant non empty trivial Function-yielding V22() V31() V38(1) FinSequence-like FinSubsequence-like countable FinSequence of PFuncs ((D *),D)
[1,x] is set
{1,x} is non empty set
{{1,x},{1}} is non empty set
{[1,x]} is Relation-like Function-like constant non empty trivial V38(1) set
x is V24() V25() V26() V30() V31() V36() countable set
dom (D,x) is non empty trivial V38(1) countable Element of bool NAT
(D,x) . x is Relation-like Function-like set
n is Relation-like D * -defined D -valued Function-like Element of bool [:(D *),D:]
(D,x) . 1 is Relation-like Function-like set
x is V24() V25() V26() V30() V31() V36() countable set
dom (D,x) is non empty trivial V38(1) countable Element of bool NAT
(D,x) . x is Relation-like Function-like set
n is Relation-like D * -defined D -valued Function-like Element of bool [:(D *),D:]
(D,x) . 1 is Relation-like Function-like set
x is set
dom (D,x) is non empty trivial V38(1) set
(D,x) . x is Relation-like Function-like set
dom (D,x) is non empty trivial V38(1) countable Element of bool NAT
n is V24() V25() V26() V30() V31() V36() countable Element of NAT
D is non empty set
D * is functional non empty FinSequence-membered FinSequenceSet of D
PFuncs ((D *),D) is functional non empty set
P is Relation-like NAT -defined PFuncs ((D *),D) -valued Function-like Function-yielding V22() V31() FinSequence-like FinSubsequence-like countable (D) FinSequence of PFuncs ((D *),D)
A is set
P . A is Relation-like Function-like set
dom P is countable Element of bool NAT
rng P is set
[:(D *),D:] is Relation-like non empty set
bool [:(D *),D:] is non empty set
dom P is countable Element of bool NAT
x is Relation-like Function-like set
dom (P . A) is set
dom x is set
x is Relation-like Function-like set
dom x is set
dom P is countable Element of bool NAT
D is non empty set
D * is functional non empty FinSequence-membered FinSequenceSet of D
PFuncs ((D *),D) is functional non empty set
<*> D is Relation-like non-empty empty-yielding NAT -defined D -valued Function-like one-to-one constant functional empty proper Function-yielding V22() V24() V25() V26() V28() V29() V30() V31() V36() V38( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding with_common_domain countable FinSequence of D
[:NAT,D:] is Relation-like non empty V31() set
P is Element of D
(<*> D) .--> P is Relation-like bool [:NAT,D:] -defined {(<*> D)} -defined D -valued Function-like one-to-one set
bool [:NAT,D:] is non empty V31() set
{(<*> D)} is functional non empty trivial V38(1) with_common_domain set
{(<*> D)} --> P is Relation-like {(<*> D)} -defined D -valued {P} -valued Function-like constant non empty total quasi_total Element of bool [:{(<*> D)},{P}:]
{P} is non empty trivial V38(1) set
[:{(<*> D)},{P}:] is Relation-like non empty set
bool [:{(<*> D)},{P}:] is non empty set
A is Relation-like Function-like Element of PFuncs ((D *),D)
(D,A) is Relation-like NAT -defined PFuncs ((D *),D) -valued Function-like constant non empty trivial Function-yielding V22() V31() V38(1) FinSequence-like FinSubsequence-like countable FinSequence of PFuncs ((D *),D)
[1,A] is set
{1,A} is non empty set
{{1,A},{1}} is non empty set
{[1,A]} is Relation-like Function-like constant non empty trivial V38(1) set
[:(D *),D:] is Relation-like non empty set
bool [:(D *),D:] is non empty set
dom (D,A) is non empty trivial V38(1) countable Element of bool NAT
x is V24() V25() V26() V30() V31() V36() countable set
(D,A) . x is Relation-like Function-like set
x is Relation-like D * -defined D -valued Function-like Element of bool [:(D *),D:]
(D,A) . 1 is Relation-like Function-like set
x is V24() V25() V26() V30() V31() V36() countable set
(D,A) . x is Relation-like Function-like set
x is Relation-like D * -defined D -valued Function-like Element of bool [:(D *),D:]
(D,A) . 1 is Relation-like Function-like set
x is set
(D,A) . x is Relation-like Function-like set
(D,A) . 1 is Relation-like Function-like set
D is Relation-like () set
dom D is with_common_domain set
P is Relation-like NAT -defined Function-like V31() FinSequence-like FinSubsequence-like countable set
len P is V24() V25() V26() V30() V31() V36() countable Element of NAT
A is Relation-like NAT -defined Function-like V31() FinSequence-like FinSubsequence-like countable set
len A is V24() V25() V26() V30() V31() V36() countable Element of NAT
dom P is countable Element of bool NAT
dom A is countable Element of bool NAT
P is V24() V25() V26() V30() V31() V36() countable set
A is V24() V25() V26() V30() V31() V36() countable set
x is Relation-like NAT -defined Function-like V31() FinSequence-like FinSubsequence-like countable set
len x is V24() V25() V26() V30() V31() V36() countable Element of NAT
D is Relation-like Function-like () set
(D) is V24() V25() V26() V30() V31() V36() countable set
D is V24() V25() V26() V30() V31() V36() countable set
P is non empty set
bool P is non empty set
D -tuples_on P is functional non empty FinSequence-membered FinSequenceSet of P
A is non empty Element of bool P
D -tuples_on A is functional non empty FinSequence-membered FinSequenceSet of A
(D -tuples_on P) /\ (D -tuples_on A) is set
x is set
D is non empty set
D * is functional non empty FinSequence-membered FinSequenceSet of D
[:(D *),D:] is Relation-like non empty set
bool [:(D *),D:] is non empty set
P is Relation-like D * -defined D -valued Function-like non empty () (D) Element of bool [:(D *),D:]
dom P is functional non empty FinSequence-membered with_common_domain set
(P) is V24() V25() V26() V30() V31() V36() countable Element of NAT
(P) -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
the Relation-like NAT -defined Function-like V31() FinSequence-like FinSubsequence-like countable Element of dom P is Relation-like NAT -defined Function-like V31() FinSequence-like FinSubsequence-like countable Element of dom P
x is set
x is Relation-like NAT -defined D -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of D
len x is V24() V25() V26() V30() V31() V36() countable Element of NAT
x is set
{ b1 where b1 is Relation-like NAT -defined D -valued Function-like V31() FinSequence-like FinSubsequence-like countable Element of D * : len b1 = (P) } is set
x is Relation-like NAT -defined D -valued Function-like V31() FinSequence-like FinSubsequence-like countable FinSequence of D
len x is V24() V25() V26() V30() V31() V36() countable Element of NAT
n is Relation-like NAT -defined D -valued Function-like V31() FinSequence-like FinSubsequence-like countable Element of D *
len n is V24() V25() V26() V30() V31() V36() countable Element of NAT
D is non empty set
D * is functional non empty FinSequence-membered FinSequenceSet of D
[:(D *),D:] is Relation-like non empty set
bool [:(D *),D:] is non empty set
the Element of D is Element of D
<*> D is Relation-like non-empty empty-yielding NAT -defined D -valued Function-like one-to-one constant functional empty proper Function-yielding V22() V24() V25() V26() V28() V29() V30() V31() V36() V38( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding with_common_domain countable FinSequence of D
[:NAT,D:] is Relation-like non empty V31() set
{(<*> D)} is functional non empty trivial V38(1) with_common_domain set
(D,{(<*> D)}, the Element of D) is Relation-like {(<*> D)} -defined D -valued Function-like constant non empty total quasi_total Element of bool [:{(<*> D)},D:]
[:{(<*> D)},D:] is Relation-like non empty set
bool [:{(<*> D)},D:] is non empty set
{ the Element of D} is non empty trivial V38(1) set
[:{(<*> D)},{ the Element of D}:] is Relation-like non empty set
{(D,{(<*> D)}, the Element of D)} is functional non empty trivial V38(1) with_common_domain set
A is non empty set
x is Element of A
(<*> D) .--> the Element of D is Relation-like bool [:NAT,D:] -defined {(<*> D)} -defined D -valued Function-like one-to-one set
bool [:NAT,D:] is non empty V31() set
{(<*> D)} --> the Element of D is Relation-like {(<*> D)} -defined D -valued { the Element of D} -valued Function-like constant non empty total quasi_total Element of bool [:{(<*> D)},{ the Element of D}:]
bool [:{(<*> D)},{ the Element of D}:] is non empty set
D is non empty set
P is non empty (D)
D * is functional non empty FinSequence-membered FinSequenceSet of D
[:(D *),D:] is Relation-like non empty set
bool [:(D *),D:] is non empty set
A is Element of P