:: 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

1 is non empty set
2 is non empty set
3 is non empty set

{1} is non empty trivial V38(1) set

{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

D is non empty set
P is set
A is Element of D

{A} is non empty trivial V38(1) set

[:P,D:] is Relation-like set
bool [:P,D:] is non empty set

dom (P --> A) is 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 set
dom A is set

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 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 set

F1() is set
D is set
P is set

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

A is set
x is set
D is 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

P is 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
P is V24() V25() V26() V30() V31() V36() countable Element of NAT
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 V24() V25() V26() V30() V31() V36() countable Element of NAT

len P is V24() V25() V26() V30() V31() V36() countable Element of NAT
D is set

rng P is set
D is set

rng P is set
D is V24() V25() V26() V30() V31() V36() countable Element of NAT

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

bool (D *) is non empty set
P is set
A is set

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

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

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

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

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

bool (D *) is non empty set
P is set
A is non empty set
x is 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
c7 is set
D is non empty set
(D) is non empty set
P is set
A is Element 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 non empty set
(D) is non empty set

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 non empty set
(D) is non empty set
P is Element of D
A is Element of D

[1,P] is set
{1,P} is non empty set
{{1,P},{1}} is non empty set

[1,A] is set
{1,A} is non empty set
{{1,A},{1}} is non empty set

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 non empty set
(D) is non empty set
P is Element of (D)
A is Element of (D)

x is set

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

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

P is set
P is Element of (F1())

D is non empty set
(D) is non empty 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
P is Element of (D)

P is Element of (D)
A is Element 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)

bool (D *) is non empty set

D is non empty set
(D) is non empty set
P is Element of (D)
(D) is Element 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
A is V24() V25() V26() V30() V31() V36() countable Element of NAT
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
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

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

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 set
P is Element of (F1())

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
{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 ()

P is set
D . P is set
dom D is set
dom D is set
rng D is set
dom D is set

dom D is 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

dom P is 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

dom P is 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

dom P is set
(dom D) /\ (dom P) is 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

dom A is 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

dom A is set

dom x is 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

dom A is set
(dom A) /\ (dom A) is set
x is 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

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 Function-like () set
dom (P) is set
dom P is non empty set
rng (P) is set

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

(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

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 *),D:] is Relation-like set
bool [:(D *),D:] is non empty set

dom (D | P) is set
D is non empty set

[:(D *),D:] is Relation-like non empty set
bool [:(D *),D:] is non empty set

dom P is set
D is non empty set

[:(D *),D:] is Relation-like non empty set
bool [:(D *),D:] is non empty set
the Element of D is Element of D

[:NAT,D:] is Relation-like non empty V31() 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}:]
{ 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

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

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 Relation-like non empty set
bool [:(),:] is non empty set

D is Relation-like () set
dom D is set
D is non empty set

[:NAT,D:] is Relation-like non empty V31() set

[:(D *),D:] is Relation-like non empty set
bool [:(D *),D:] is non empty set
P is Element of D

bool [:NAT,D:] is non empty V31() set

{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

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

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

[:NAT,D:] is Relation-like non empty V31() set

PFuncs ((D *),D) is functional non empty set
P is Element of D

bool [:NAT,D:] is non empty V31() set

{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

D is set

PFuncs ((D *),D) is functional non empty set
D is set

PFuncs ((D *),D) is functional non empty set
D is non empty set

PFuncs ((D *),D) is functional non empty set
P is Relation-like Function-like Element of PFuncs ((D *),D)

[1,P] is set
{1,P} is non empty set
{{1,P},{1}} is non empty set

D is non empty set

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

[:NAT,D:] is Relation-like non empty V31() 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}:]
{ 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

x is Relation-like Function-like Element of PFuncs ((D *),D)

[1,x] is set
{1,x} is non empty set
{{1,x},{1}} is non empty 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

(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

(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

PFuncs ((D *),D) is functional non empty set

A is set

rng P is set
[:(D *),D:] is Relation-like non empty set
bool [:(D *),D:] is non empty set

dom (P . A) is set
dom x is set

dom x is set

D is non empty set

PFuncs ((D *),D) is functional non empty set

[:NAT,D:] is Relation-like non empty V31() set
P is Element of D

bool [:NAT,D:] is non empty V31() set

{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)

[1,A] is set
{1,A} is non empty set
{{1,A},{1}} is non empty 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

(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

(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

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

P is V24() V25() V26() V30() V31() V36() countable set
A is V24() V25() V26() V30() V31() V36() countable set

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

(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

A is non empty Element of bool P

() /\ () is set
x is set
D is non empty set

[:(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:]

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

x is set

len x is V24() V25() V26() V30() V31() V36() countable Element of NAT
x is set
{ } is 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 *),D:] is Relation-like non empty set
bool [:(D *),D:] is non empty set
the Element of D is Element of D

[:NAT,D:] is Relation-like non empty V31() 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

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 *),D:] is Relation-like non empty set
bool [:(D *),D:] is non empty set
A is Element of P