:: POLYNOM3 semantic presentation

REAL is non empty non trivial non finite V75() V76() V77() V81() set
NAT is non empty non trivial V26() V27() V28() non finite cardinal limit_cardinal V75() V76() V77() V78() V79() V80() V81() Element of bool REAL
bool REAL is non trivial non finite set
NAT is non empty non trivial V26() V27() V28() non finite cardinal limit_cardinal V75() V76() V77() V78() V79() V80() V81() set
bool NAT is non trivial non finite set
bool NAT is non trivial non finite set
COMPLEX is non empty non trivial non finite V75() V81() set
RAT is non empty non trivial non finite V75() V76() V77() V78() V81() set
INT is non empty non trivial non finite V75() V76() V77() V78() V79() V81() set
is non trivial non finite V65() V66() V67() set
bool is non trivial non finite set
{} is set
the Function-like functional empty V26() V27() V28() V30() V31() V32() finite V37() cardinal {} -element FinSequence-membered V45() V46() V47() ext-real non positive non negative V75() V76() V77() V78() V79() V80() V81() set is Function-like functional empty V26() V27() V28() V30() V31() V32() finite V37() cardinal {} -element FinSequence-membered V45() V46() V47() ext-real non positive non negative V75() V76() V77() V78() V79() V80() V81() set
1 is non empty V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real positive non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
{{},1} is finite set
K406() is set
bool K406() is set
K407() is Element of bool K406()
2 is non empty V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real positive non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
is non trivial non finite V65() set
bool is non trivial non finite set
is non trivial non finite V65() set
bool is non trivial non finite set
is non trivial non finite V65() V66() V67() set
bool is non trivial non finite set
is RAT -valued non trivial non finite V65() V66() V67() set
bool is non trivial non finite set
is RAT -valued non trivial non finite V65() V66() V67() set
bool is non trivial non finite set
is RAT -valued INT -valued non trivial non finite V65() V66() V67() set
bool is non trivial non finite set
is RAT -valued INT -valued non trivial non finite V65() V66() V67() set
bool is non trivial non finite set
is RAT -valued INT -valued non trivial non finite V65() V66() V67() V68() set
is RAT -valued INT -valued non trivial non finite V65() V66() V67() V68() set
bool is non trivial non finite set
K612() is set
is non trivial non finite V65() V66() V67() set
bool is non trivial non finite set

3 is non empty V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real positive non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
0 is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
Seg 1 is non empty trivial finite 1 -element V75() V76() V77() V78() V79() V80() Element of bool NAT
{1} is non empty trivial finite V37() 1 -element V75() V76() V77() V78() V79() V80() set
Seg 2 is non empty finite 2 -element V75() V76() V77() V78() V79() V80() Element of bool NAT
{1,2} is finite V37() V75() V76() V77() V78() V79() V80() set
Seg 3 is non empty finite 3 -element V75() V76() V77() V78() V79() V80() Element of bool NAT
K150(1,2,3) is finite V75() V76() V77() V78() V79() V80() set

the carrier of L is non empty set
0. L is V105(L) Element of the carrier of L
the ZeroF of L is Element of the carrier of L

dom p is finite V75() V76() V77() V78() V79() V80() Element of bool NAT
Sum p is Element of the carrier of L
q is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative set
p /. q is Element of the carrier of L
p . q is set

the carrier of L is non empty set

Sum p is Element of the carrier of L

Sum (Rev p) is Element of the carrier of L
q is Element of the carrier of L

the carrier of L * is functional non empty FinSequence-membered FinSequenceSet of the carrier of L

Sum (p ^ <*q*>) is Element of the carrier of L

Sum (Rev (p ^ <*q*>)) is Element of the carrier of L
Sum <*q*> is Element of the carrier of L
(Sum p) + () is Element of the carrier of L
the addF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like total quasi_total Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is set
the addF of L . ((Sum p),()) is Element of the carrier of L

Sum (<*q*> ^ (Rev p)) is Element of the carrier of L

the carrier of L * is functional non empty FinSequence-membered FinSequenceSet of the carrier of L
Sum (<*> the carrier of L) is Element of the carrier of L

Sum (Rev (<*> the carrier of L)) is Element of the carrier of L

Sum L is V45() V46() ext-real Element of REAL

Sum (Rev L) is V45() V46() ext-real Element of REAL
p is V45() V46() ext-real Element of REAL

Sum (L ^ <*p*>) is V45() V46() ext-real Element of REAL

Sum (Rev (L ^ <*p*>)) is V45() V46() ext-real Element of REAL
Sum <*p*> is V45() V46() ext-real Element of REAL
(Sum L) + () is V45() V46() ext-real set

Sum (<*p*> ^ (Rev L)) is V45() V46() ext-real Element of REAL

Sum () is V45() V46() ext-real Element of REAL

Sum (Rev ()) is V45() V46() ext-real Element of REAL

dom L is finite V75() V76() V77() V78() V79() V80() Element of bool NAT
Sum L is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
p is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT

dom (L ^ <*p*>) is finite V75() V76() V77() V78() V79() V80() Element of bool NAT
Sum (L ^ <*p*>) is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
q is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
(L ^ <*p*>) . q is V45() V46() ext-real set
L . q is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
(L . q) + p is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
len (L ^ <*p*>) is non empty V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real positive non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
len L is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
(len L) + 1 is non empty V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real positive non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
Seg ((len L) + 1) is non empty finite (len L) + 1 -element (len L) + 1 -element V75() V76() V77() V78() V79() V80() Element of bool NAT
(len L) + 1 is non empty V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real positive non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
Seg (len L) is finite len L -element V75() V76() V77() V78() V79() V80() Element of bool NAT
{((len L) + 1)} is non empty trivial finite V37() 1 -element V75() V76() V77() V78() V79() V80() set
(Seg (len L)) \/ {((len L) + 1)} is finite V75() V76() V77() V78() V79() V80() set
(dom L) \/ {((len L) + 1)} is finite V75() V76() V77() V78() V79() V80() set
(Sum L) + p is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
(Sum L) + p is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT

dom () is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V75() V76() V77() V78() V79() V80() Element of bool NAT
Sum () is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
L is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
() . L is V26() V27() V28() V32() finite cardinal FinSequence-like V45() V46() V47() ext-real non negative set
L is non empty set
p is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT

L is non empty set
p is Element of L
q is Element of L

{ } is set
L is non empty set
p is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT

{ } is set
q is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT

{ } is set

p + q is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
p + q is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
(p + q) -tuples_on L is functional non empty FinSequence-membered V196() V197() FinSequenceSet of L
{ } is set

p is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
L is non empty set

{ } is set
q is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT

{ } is set

p + q is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
(p + q) -tuples_on L is functional non empty FinSequence-membered V196() V197() FinSequenceSet of L
{ } is set
((p + q) -tuples_on L) * is functional non empty FinSequence-membered FinSequenceSet of (p + q) -tuples_on L
rng (r ^^ p1) is finite set
q1 is set
dom (r ^^ p1) is finite V75() V76() V77() V78() V79() V80() Element of bool NAT
r1 is set
(r ^^ p1) . r1 is FinSequence-like set
dom r is finite V75() V76() V77() V78() V79() V80() Element of bool NAT
dom p1 is finite V75() V76() V77() V78() V79() V80() Element of bool NAT
(dom r) /\ (dom p1) is finite V75() V76() V77() V78() V79() V80() Element of bool NAT

(L,p,q,(r /. r1),(p1 /. r1)) is Relation-like NAT -defined L -valued Function-like finite p + q -element p + q -element FinSequence-like FinSubsequence-like finite-support Element of (p + q) -tuples_on L
p + q is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
F1() is non empty set
F1() * is functional non empty FinSequence-membered FinSequenceSet of F1()
F2() is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
Seg F2() is finite F2() -element V75() V76() V77() V78() V79() V80() Element of bool NAT
L is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
F3(L) is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT

len p is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
dom p is finite V75() V76() V77() V78() V79() V80() Element of bool NAT

len q is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
dom q is finite V75() V76() V77() V78() V79() V80() Element of bool NAT
r is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
q . r is set
F4(L,r) is Element of F1()

dom L is finite V75() V76() V77() V78() V79() V80() Element of bool NAT
len L is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
p is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT

len (L /. p) is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
F3(p) is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
dom (L /. p) is finite V75() V76() V77() V78() V79() V80() Element of bool NAT
q is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
(L /. p) . q is set
F4(p,q) is Element of F1()
L is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT

{ } is set
Seg L is finite L -element V75() V76() V77() V78() V79() V80() Element of bool NAT

q1 is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
p1 . q1 is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
r . q1 is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
r1 is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
r . r1 is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
p1 . r1 is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
L is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT

{ } is set
L is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT

{ } is set

L is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT

{ } is set
L is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT

{ } is set

Seg L is finite L -element V75() V76() V77() V78() V79() V80() Element of bool NAT
p1 is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
q . p1 is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
p . p1 is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
q1 is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
r . q1 is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
q . q1 is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
min (p1,q1) is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
r1 is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
r . r1 is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
p . r1 is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
p is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
p . p is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
r . p is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
q . p is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
L is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT

{ } is set
Seg L is finite L -element V75() V76() V77() V78() V79() V80() Element of bool NAT
L + 1 is non empty V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real positive non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT

{ } is set
Seg (L + 1) is non empty finite L + 1 -element L + 1 -element V75() V76() V77() V78() V79() V80() Element of bool NAT
L + 1 is non empty V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real positive non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT

p1 is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT

r1 is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT

len r is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
len q1 is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
p is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
r . p is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
q1 . p is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
p . p is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
q . p is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
dom r is finite L -element V75() V76() V77() V78() V79() V80() Element of bool NAT
dom q1 is finite L -element V75() V76() V77() V78() V79() V80() Element of bool NAT
q is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
p . q is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
q . q is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
r . q is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
q1 . q is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
p is non empty V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real positive non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
p . p is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
q . p is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
q is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
p . q is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
q . q is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
dom q1 is finite L -element V75() V76() V77() V78() V79() V80() Element of bool NAT
dom r is finite L -element V75() V76() V77() V78() V79() V80() Element of bool NAT
q1 . q is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT

{ } is set
Seg 0 is Function-like functional empty V26() V27() V28() V30() V31() V32() finite V37() cardinal 0 -element FinSequence-membered V45() V46() V47() ext-real non positive non negative V75() V76() V77() V78() V79() V80() V81() Element of bool NAT

L is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT

{ } is set

Seg L is finite L -element V75() V76() V77() V78() V79() V80() Element of bool NAT
r is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
p . r is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
q . r is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
p1 is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
q . p1 is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
p . p1 is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
L is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT

{ } is set
[:(),():] is set
bool [:(),():] is set

q is set
r is set
p1 is set
[q,r] is set
{q,r} is finite set
{q} is non empty trivial finite 1 -element set
{{q,r},{q}} is finite V37() set
[r,p1] is set
{r,p1} is finite set
{r} is non empty trivial finite 1 -element set
{{r,p1},{r}} is finite V37() set
[q,p1] is set
{q,p1} is finite set
{{q,p1},{q}} is finite V37() set

q is set
[q,q] is set
{q,q} is finite set
{q} is non empty trivial finite 1 -element set
{{q,q},{q}} is finite V37() set

bool () is set
field p is set
dom p is set
rng p is set
(dom p) \/ (rng p) is set
q is set
r is set
[q,r] is set
{q,r} is finite set
{q} is non empty trivial finite 1 -element set
{{q,r},{q}} is finite V37() set
[r,q] is set
{r,q} is finite set
{r} is non empty trivial finite 1 -element set
{{r,q},{r}} is finite V37() set

[r,p1] is set
{r,p1} is functional finite V37() set

{{r,p1},{r}} is finite V37() set

[q1,r1] is set
{q1,r1} is functional finite V37() set
{q1} is functional non empty trivial finite V37() 1 -element set
{{q1,r1},{q1}} is finite V37() set

r is set
p1 is set
[r,p1] is set
{r,p1} is finite set
{r} is non empty trivial finite 1 -element set
{{r,p1},{r}} is finite V37() set
q1 is set
r1 is set
[q1,r1] is set
{q1,r1} is finite set
{q1} is non empty trivial finite 1 -element set
{{q1,r1},{q1}} is finite V37() set

q1 is set
r1 is set
[q1,r1] is set
{q1,r1} is finite set
{q1} is non empty trivial finite 1 -element set
{{q1,r1},{q1}} is finite V37() set

L is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT

{ } is set
[:(),():] is set
bool [:(),():] is set
p is set
q is set
[p,q] is set
{p,q} is finite set
{p} is non empty trivial finite 1 -element set
{{p,q},{p}} is finite V37() set

[q,p] is set
{q,p} is finite set
{q} is non empty trivial finite 1 -element set
{{q,p},{q}} is finite V37() set
field (L) is set
dom (L) is set
rng (L) is set
(dom (L)) \/ (rng (L)) is set
L is non empty V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real positive non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT

{ } is set
bool () is set

[:(),():] is set
bool [:(),():] is set
p is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
p + 1 is non empty V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real positive non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT

L -tuples_on (p + 1) is functional non empty finite FinSequence-membered V196() V197() FinSequenceSet of p + 1
(p + 1) * is functional non empty FinSequence-membered FinSequenceSet of p + 1
{ } is set
p1 is set

Sum q1 is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
rng q1 is finite V75() V76() V77() V78() V79() V80() Element of bool REAL
r1 is set
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT : not p + 1 <= b1 } is set
p is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
dom q1 is finite L -element V75() V76() V77() V78() V79() V80() Element of bool NAT
q is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative set
q1 . q is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
len q1 is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
q is non empty set

{ } is set

r1 is set

Sum p is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT

Sum p is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
L is non empty V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real positive non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
p is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT

{ } is set
L -' 1 is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT

{ } is set
Seg (L -' 1) is finite L -' 1 -element V75() V76() V77() V78() V79() V80() Element of bool NAT

is non empty trivial finite V37() 1 -element V75() V76() V77() V78() V79() V80() set
[:(Seg (L -' 1)),:] is RAT -valued INT -valued finite V65() V66() V67() V68() set
bool [:(Seg (L -' 1)),:] is finite V37() set
(L -' 1) + 1 is non empty V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real positive non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT

(L -' 1) + 1 is non empty V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real positive non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
bool () is set

[:(),():] is set
bool [:(),():] is set

Sum r is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT

Sum q is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
(Sum q) + p is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
0 + p is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT

L is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT

{ } is set
len (1,L) is non empty V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real positive non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
bool () is set

[:(),():] is set
bool [:(),():] is set

q is set

Sum r is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
p1 is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT

q is set
Sum <*L*> is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
field (1) is set
dom (1) is set
rng (1) is set
(dom (1)) \/ (rng (1)) is set
card p is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
L is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT

{ } is set
len (2,L) is non empty V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real positive non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
L + 1 is non empty V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real positive non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT

len p is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
dom p is finite V75() V76() V77() V78() V79() V80() Element of bool NAT
Seg L is finite L -element V75() V76() V77() V78() V79() V80() Element of bool NAT

len (NAT,0,L) is non empty V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real positive non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT

len (p ^ <*(NAT,0,L)*>) is non empty V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real positive non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
dom (p ^ <*(NAT,0,L)*>) is finite V75() V76() V77() V78() V79() V80() Element of bool NAT
Seg (L + 1) is non empty finite L + 1 -element L + 1 -element V75() V76() V77() V78() V79() V80() Element of bool NAT
L + 1 is non empty V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real positive non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
r is set
p1 is set
(p ^ <*(NAT,0,L)*>) . r is set
(p ^ <*(NAT,0,L)*>) . p1 is set
{(L + 1)} is non empty trivial finite V37() 1 -element V75() V76() V77() V78() V79() V80() set
(Seg L) \/ {(L + 1)} is finite V75() V76() V77() V78() V79() V80() set
q1 is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
(p ^ <*(NAT,0,L)*>) . q1 is set
p . q1 is set
r1 is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
(p ^ <*(NAT,0,L)*>) . r1 is set
p . r1 is set
L -' q1 is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT

L -' r1 is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT

r1 is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
(p ^ <*(NAT,0,L)*>) . r1 is set
q1 is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
(p ^ <*(NAT,0,L)*>) . q1 is set
p . q1 is set
L -' q1 is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT

q1 is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
(p ^ <*(NAT,0,L)*>) . q1 is set
r1 is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
(p ^ <*(NAT,0,L)*>) . r1 is set
p . r1 is set
L -' r1 is V26() V27() V28() V32() finite cardinal V45() V46() V47() ext-real non negative V52() V75() V76() V77() V78() V79() V80() Element of NAT
(NAT,r1,(L -' r1)) is Relation-like NAT -defined NAT -valued Function-like non empty non