:: MARGREL1 semantic presentation

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

F

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

c

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

F

(F

F

D is set

P is Relation-like NAT -defined F

A is Relation-like NAT -defined F

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 F

x is Relation-like NAT -defined F

P is set

P is Element of (F

A is Relation-like NAT -defined F

x is Relation-like NAT -defined F

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

F

(F

F

F

D is set

P is Relation-like NAT -defined F

A is Relation-like NAT -defined F

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 F

len x is V24() V25() V26() V30() V31() V36() countable Element of NAT

x is Relation-like NAT -defined F

len x is V24() V25() V26() V30() V31() V36() countable Element of NAT

P is set

P is Element of (F

A is Relation-like NAT -defined F

len A is V24() V25() V26() V30() V31() V36() countable Element of NAT

x is Relation-like NAT -defined F

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

c

c

c

K104(c

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

{ b

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