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
[:REAL,REAL:] is non trivial non finite V65() V66() V67() set
bool [:REAL,REAL:] 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
[:COMPLEX,COMPLEX:] is non trivial non finite V65() set
bool [:COMPLEX,COMPLEX:] is non trivial non finite set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non trivial non finite V65() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non trivial non finite set
[:[:REAL,REAL:],REAL:] is non trivial non finite V65() V66() V67() set
bool [:[:REAL,REAL:],REAL:] is non trivial non finite set
[:RAT,RAT:] is RAT -valued non trivial non finite V65() V66() V67() set
bool [:RAT,RAT:] is non trivial non finite set
[:[:RAT,RAT:],RAT:] is RAT -valued non trivial non finite V65() V66() V67() set
bool [:[:RAT,RAT:],RAT:] is non trivial non finite set
[:INT,INT:] is RAT -valued INT -valued non trivial non finite V65() V66() V67() set
bool [:INT,INT:] is non trivial non finite set
[:[:INT,INT:],INT:] is RAT -valued INT -valued non trivial non finite V65() V66() V67() set
bool [:[:INT,INT:],INT:] is non trivial non finite set
[:NAT,NAT:] is RAT -valued INT -valued non trivial non finite V65() V66() V67() V68() set
[:[:NAT,NAT:],NAT:] is RAT -valued INT -valued non trivial non finite V65() V66() V67() V68() set
bool [:[:NAT,NAT:],NAT:] is non trivial non finite set
K612() is set
[:NAT,REAL:] is non trivial non finite V65() V66() V67() set
bool [:NAT,REAL:] is non trivial non finite set
K467() is Relation-like NAT -defined Function-like total 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
L is non empty right_complementable add-associative right_zeroed addLoopStr
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
p is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence 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
L is non empty Abelian add-associative right_zeroed addLoopStr
the carrier of L is non empty set
p is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of L
Sum p is Element of the carrier of L
Rev p is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of L
Sum (Rev p) is Element of the carrier of L
q is Element of the carrier of L
<*q*> is Relation-like NAT -defined the carrier of L -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like finite-support Element of the carrier of L *
the carrier of L * is functional non empty FinSequence-membered FinSequenceSet of the carrier of L
p ^ <*q*> is Relation-like NAT -defined the carrier of L -valued Function-like non empty finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of L
Sum (p ^ <*q*>) is Element of the carrier of L
Rev (p ^ <*q*>) is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence 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) + (Sum <*q*>) 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),(Sum <*q*>)) is Element of the carrier of L
<*q*> ^ (Rev p) is Relation-like NAT -defined the carrier of L -valued Function-like non empty finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of L
Sum (<*q*> ^ (Rev p)) is Element of the carrier of L
<*> the carrier of L is Relation-like NAT -defined the carrier of L -valued Function-like one-to-one constant functional empty Function-yielding V26() V27() V28() V30() V31() V32() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V45() V46() V47() ext-real non positive non negative V65() V66() V67() V68() V75() V76() V77() V78() V79() V80() V81() FinSequence-yielding finite-support 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
Rev (<*> the carrier of L) is Relation-like NAT -defined RAT -valued the carrier of L -valued Function-like one-to-one constant functional empty Function-yielding V26() V27() V28() V30() V31() V32() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V45() V46() V47() ext-real non positive non negative V65() V66() V67() V68() V75() V76() V77() V78() V79() V80() V81() FinSequence-yielding finite-support FinSequence of the carrier of L
Sum (Rev (<*> the carrier of L)) is Element of the carrier of L
L is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V65() V66() V67() finite-support FinSequence of REAL
Sum L is V45() V46() ext-real Element of REAL
Rev L is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V65() V66() V67() finite-support FinSequence of REAL
Sum (Rev L) is V45() V46() ext-real Element of REAL
p is V45() V46() ext-real Element of REAL
<*p*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V65() V66() V67() V69() V70() V71() V72() finite-support Element of REAL *
REAL * is functional non empty FinSequence-membered FinSequenceSet of REAL
L ^ <*p*> is Relation-like NAT -defined REAL -valued Function-like non empty finite FinSequence-like FinSubsequence-like V65() V66() V67() finite-support FinSequence of REAL
Sum (L ^ <*p*>) is V45() V46() ext-real Element of REAL
Rev (L ^ <*p*>) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V65() V66() V67() finite-support FinSequence 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) + (Sum <*p*>) is V45() V46() ext-real set
<*p*> ^ (Rev L) is Relation-like NAT -defined REAL -valued Function-like non empty finite FinSequence-like FinSubsequence-like V65() V66() V67() finite-support FinSequence of REAL
Sum (<*p*> ^ (Rev L)) is V45() V46() ext-real Element of REAL
<*> REAL is Relation-like NAT -defined REAL -valued Function-like one-to-one constant functional empty Function-yielding V26() V27() V28() V30() V31() V32() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V45() V46() V47() ext-real non positive non negative V65() V66() V67() V68() V75() V76() V77() V78() V79() V80() V81() FinSequence-yielding finite-support Element of REAL *
REAL * is functional non empty FinSequence-membered FinSequenceSet of REAL
Sum (<*> REAL) is V45() V46() ext-real Element of REAL
Rev (<*> REAL) is Relation-like NAT -defined REAL -valued RAT -valued Function-like one-to-one constant functional empty Function-yielding V26() V27() V28() V30() V31() V32() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V45() V46() V47() ext-real non positive non negative V65() V66() V67() V68() V75() V76() V77() V78() V79() V80() V81() FinSequence-yielding finite-support FinSequence of REAL
Sum (Rev (<*> REAL)) is V45() V46() ext-real Element of REAL
L is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V65() V66() V67() V68() V195() finite-support FinSequence of NAT
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
<*p*> is Relation-like NAT -defined NAT -valued Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V65() V66() V67() V68() V69() V70() V71() V72() V195() finite-support Element of NAT *
NAT * is functional non empty FinSequence-membered FinSequenceSet of NAT
L ^ <*p*> is Relation-like NAT -defined REAL -valued Function-like non empty finite FinSequence-like FinSubsequence-like V65() V66() V67() V195() finite-support FinSequence 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
<*> NAT is Relation-like NAT -defined NAT -valued Function-like one-to-one constant functional empty Function-yielding V26() V27() V28() V30() V31() V32() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V45() V46() V47() ext-real non positive non negative V65() V66() V67() V68() V75() V76() V77() V78() V79() V80() V81() V195() FinSequence-yielding finite-support Element of NAT *
NAT * is functional non empty FinSequence-membered FinSequenceSet of NAT
dom (<*> NAT) 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 (<*> NAT) 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
(<*> 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
q is Relation-like NAT -defined L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of L
Del (q,p) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
L is non empty set
p is Element of L
q is Element of L
<*p,q*> is Relation-like NAT -defined Function-like non empty non trivial finite 2 -element FinSequence-like FinSubsequence-like finite-support set
2 -tuples_on L is functional non empty FinSequence-membered V196() V197() FinSequenceSet of L
L * is functional non empty FinSequence-membered FinSequenceSet of L
{ b1 where b1 is Relation-like NAT -defined L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of L * : len b1 = 2 } 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
p -tuples_on L is functional non empty FinSequence-membered V196() V197() FinSequenceSet of L
L * is functional non empty FinSequence-membered FinSequenceSet of L
{ b1 where b1 is Relation-like NAT -defined L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of L * : len b1 = p } 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
q -tuples_on L is functional non empty FinSequence-membered V196() V197() FinSequenceSet of L
{ b1 where b1 is Relation-like NAT -defined L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of L * : len b1 = q } is set
r is Relation-like NAT -defined L -valued Function-like finite p -element FinSequence-like FinSubsequence-like finite-support Element of p -tuples_on L
p1 is Relation-like NAT -defined L -valued Function-like finite q -element FinSequence-like FinSubsequence-like finite-support Element of q -tuples_on L
r ^ p1 is Relation-like NAT -defined Function-like finite p + q -element FinSequence-like FinSubsequence-like finite-support 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
{ b1 where b1 is Relation-like NAT -defined L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of L * : len b1 = p + q } is set
r ^ p1 is Relation-like NAT -defined L -valued Function-like finite p + q -element FinSequence-like FinSubsequence-like finite-support FinSequence of 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
L is non empty set
p -tuples_on L is functional non empty FinSequence-membered V196() V197() FinSequenceSet of L
L * is functional non empty FinSequence-membered FinSequenceSet of L
{ b1 where b1 is Relation-like NAT -defined L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of L * : len b1 = p } 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
q -tuples_on L is functional non empty FinSequence-membered V196() V197() FinSequenceSet of L
{ b1 where b1 is Relation-like NAT -defined L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of L * : len b1 = q } is set
r is Relation-like NAT -defined p -tuples_on L -valued Function-like Function-yielding finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of p -tuples_on L
p1 is Relation-like NAT -defined q -tuples_on L -valued Function-like Function-yielding finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of q -tuples_on L
r ^^ p1 is Relation-like NAT -defined Function-like Function-yielding finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support 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
{ b1 where b1 is Relation-like NAT -defined L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of L * : len b1 = p + q } 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
r . r1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
p1 . r1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
(r . r1) ^ (p1 . r1) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
r /. r1 is Relation-like NAT -defined L -valued Function-like finite p -element FinSequence-like FinSubsequence-like finite-support Element of p -tuples_on L
(r /. r1) ^ (p1 . r1) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
p1 /. r1 is Relation-like NAT -defined L -valued Function-like finite q -element FinSequence-like FinSubsequence-like finite-support Element of q -tuples_on L
(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
p is Relation-like NAT -defined F1() -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of F1()
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
q is Relation-like NAT -defined F1() -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of F1() *
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()
L is Relation-like NAT -defined F1() * -valued Function-like Function-yielding finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence 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
L /. p is Relation-like NAT -defined F1() -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of F1() *
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
L -tuples_on NAT is functional non empty FinSequence-membered V196() V197() FinSequenceSet of NAT
NAT * is functional non empty FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of NAT * : len b1 = L } is set
Seg L is finite L -element V75() V76() V77() V78() V79() V80() Element of bool NAT
p1 is Relation-like NAT -defined NAT -valued Function-like finite L -element FinSequence-like FinSubsequence-like V65() V66() V67() V68() V195() finite-support Element of L -tuples_on NAT
r is Relation-like NAT -defined NAT -valued Function-like finite L -element FinSequence-like FinSubsequence-like V65() V66() V67() V68() V195() finite-support Element of L -tuples_on 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
L -tuples_on NAT is functional non empty FinSequence-membered V196() V197() FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of NAT * : len b1 = L } 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
L -tuples_on NAT is functional non empty FinSequence-membered V196() V197() FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of NAT * : len b1 = L } is set
r is Relation-like NAT -defined NAT -valued Function-like finite L -element FinSequence-like FinSubsequence-like V65() V66() V67() V68() V195() finite-support Element of L -tuples_on 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 -tuples_on NAT is functional non empty FinSequence-membered V196() V197() FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of NAT * : len b1 = L } 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
L -tuples_on NAT is functional non empty FinSequence-membered V196() V197() FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of NAT * : len b1 = L } is set
p is Relation-like NAT -defined NAT -valued Function-like finite L -element FinSequence-like FinSubsequence-like V65() V66() V67() V68() V195() finite-support Element of L -tuples_on NAT
q is Relation-like NAT -defined NAT -valued Function-like finite L -element FinSequence-like FinSubsequence-like V65() V66() V67() V68() V195() finite-support Element of L -tuples_on NAT
r is Relation-like NAT -defined NAT -valued Function-like finite L -element FinSequence-like FinSubsequence-like V65() V66() V67() V68() V195() finite-support Element of L -tuples_on NAT
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
L -tuples_on NAT is functional non empty FinSequence-membered V196() V197() FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of NAT * : len b1 = L } 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
(L + 1) -tuples_on NAT is functional non empty FinSequence-membered V196() V197() FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of NAT * : len b1 = L + 1 } 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
p is Relation-like NAT -defined NAT -valued Function-like finite L + 1 -element FinSequence-like FinSubsequence-like V65() V66() V67() V68() V195() finite-support Element of (L + 1) -tuples_on NAT
q is Relation-like NAT -defined NAT -valued Function-like finite L + 1 -element FinSequence-like FinSubsequence-like V65() V66() V67() V68() V195() finite-support Element of (L + 1) -tuples_on NAT
r is Relation-like NAT -defined NAT -valued Function-like finite L -element FinSequence-like FinSubsequence-like V65() V66() V67() V68() V195() finite-support Element of L -tuples_on 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
<*p1*> is Relation-like NAT -defined NAT -valued Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V65() V66() V67() V68() V69() V70() V71() V72() V195() finite-support Element of NAT *
r ^ <*p1*> is Relation-like NAT -defined REAL -valued Function-like non empty finite L + 1 -element FinSequence-like FinSubsequence-like V65() V66() V67() V195() finite-support FinSequence of NAT
q1 is Relation-like NAT -defined NAT -valued Function-like finite L -element FinSequence-like FinSubsequence-like V65() V66() V67() V68() V195() finite-support Element of L -tuples_on 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
<*r1*> is Relation-like NAT -defined NAT -valued Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V65() V66() V67() V68() V69() V70() V71() V72() V195() finite-support Element of NAT *
q1 ^ <*r1*> is Relation-like NAT -defined REAL -valued Function-like non empty finite L + 1 -element FinSequence-like FinSubsequence-like V65() V66() V67() V195() finite-support FinSequence 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
0 -tuples_on NAT is functional non empty FinSequence-membered V196() V197() FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of NAT * : len b1 = 0 } 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 Relation-like NAT -defined NAT -valued Function-like one-to-one constant functional empty Function-yielding V26() V27() V28() V30() V31() V32() finite finite-yielding V37() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered V45() V46() V47() ext-real non positive non negative V65() V66() V67() V68() V75() V76() V77() V78() V79() V80() V81() V195() FinSequence-yielding finite-support Element of 0 -tuples_on NAT
p is Relation-like NAT -defined NAT -valued Function-like one-to-one constant functional empty Function-yielding V26() V27() V28() V30() V31() V32() finite finite-yielding V37() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered V45() V46() V47() ext-real non positive non negative V65() V66() V67() V68() V75() V76() V77() V78() V79() V80() V81() V195() FinSequence-yielding finite-support Element of 0 -tuples_on 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 -tuples_on NAT is functional non empty FinSequence-membered V196() V197() FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of NAT * : len b1 = L } is set
p is Relation-like NAT -defined NAT -valued Function-like finite L -element FinSequence-like FinSubsequence-like V65() V66() V67() V68() V195() finite-support Element of L -tuples_on NAT
q is Relation-like NAT -defined NAT -valued Function-like finite L -element FinSequence-like FinSubsequence-like V65() V66() V67() V68() V195() finite-support Element of L -tuples_on NAT
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
L -tuples_on NAT is functional non empty FinSequence-membered V196() V197() FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of NAT * : len b1 = L } is set
[:(L -tuples_on NAT),(L -tuples_on NAT):] is set
bool [:(L -tuples_on NAT),(L -tuples_on NAT):] is set
p is Relation-like L -tuples_on NAT -defined L -tuples_on NAT -valued Element of bool [:(L -tuples_on NAT),(L -tuples_on NAT):]
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
q1 is Relation-like NAT -defined NAT -valued Function-like finite L -element FinSequence-like FinSubsequence-like V65() V66() V67() V68() V195() finite-support Element of L -tuples_on NAT
r1 is Relation-like NAT -defined NAT -valued Function-like finite L -element FinSequence-like FinSubsequence-like V65() V66() V67() V68() V195() finite-support Element of L -tuples_on NAT
p is Relation-like NAT -defined NAT -valued Function-like finite L -element FinSequence-like FinSubsequence-like V65() V66() V67() V68() V195() finite-support Element of L -tuples_on NAT
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
r is Relation-like NAT -defined NAT -valued Function-like finite L -element FinSequence-like FinSubsequence-like V65() V66() V67() V68() V195() finite-support Element of L -tuples_on NAT
dom p is functional FinSequence-membered Element of bool (L -tuples_on NAT)
bool (L -tuples_on NAT) 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
p1 is Relation-like NAT -defined NAT -valued Function-like finite L -element FinSequence-like FinSubsequence-like V65() V66() V67() V68() V195() finite-support Element of L -tuples_on NAT
q1 is Relation-like NAT -defined NAT -valued Function-like finite L -element FinSequence-like FinSubsequence-like V65() V66() V67() V68() V195() finite-support Element of L -tuples_on NAT
q is Relation-like L -tuples_on NAT -defined L -tuples_on NAT -valued total quasi_total reflexive antisymmetric transitive Element of bool [:(L -tuples_on NAT),(L -tuples_on NAT):]
r is Relation-like NAT -defined NAT -valued Function-like finite L -element FinSequence-like FinSubsequence-like V65() V66() V67() V68() V195() finite-support Element of L -tuples_on NAT
p1 is Relation-like NAT -defined NAT -valued Function-like finite L -element FinSequence-like FinSubsequence-like V65() V66() V67() V68() V195() finite-support Element of L -tuples_on NAT
[r,p1] is set
{r,p1} is functional finite V37() set
{r} is functional non empty trivial finite V37() 1 -element set
{{r,p1},{r}} is finite V37() set
q1 is Relation-like NAT -defined NAT -valued Function-like finite L -element FinSequence-like FinSubsequence-like V65() V66() V67() V68() V195() finite-support Element of L -tuples_on NAT
r1 is Relation-like NAT -defined NAT -valued Function-like finite L -element FinSequence-like FinSubsequence-like V65() V66() V67() V68() V195() finite-support Element of L -tuples_on NAT
[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
p is Relation-like L -tuples_on NAT -defined L -tuples_on NAT -valued total quasi_total reflexive antisymmetric transitive Element of bool [:(L -tuples_on NAT),(L -tuples_on NAT):]
q is Relation-like L -tuples_on NAT -defined L -tuples_on NAT -valued total quasi_total reflexive antisymmetric transitive Element of bool [:(L -tuples_on NAT),(L -tuples_on NAT):]
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
p is Relation-like NAT -defined NAT -valued Function-like finite L -element FinSequence-like FinSubsequence-like V65() V66() V67() V68() V195() finite-support Element of L -tuples_on NAT
q is Relation-like NAT -defined NAT -valued Function-like finite L -element FinSequence-like FinSubsequence-like V65() V66() V67() V68() V195() finite-support Element of L -tuples_on NAT
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
p is Relation-like NAT -defined NAT -valued Function-like finite L -element FinSequence-like FinSubsequence-like V65() V66() V67() V68() V195() finite-support Element of L -tuples_on NAT
q is Relation-like NAT -defined NAT -valued Function-like finite L -element FinSequence-like FinSubsequence-like V65() V66() V67() V68() V195() finite-support Element of L -tuples_on 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 Relation-like L -tuples_on NAT -defined L -tuples_on NAT -valued total quasi_total reflexive antisymmetric transitive Element of bool [:(L -tuples_on NAT),(L -tuples_on NAT):]
L -tuples_on NAT is functional non empty FinSequence-membered V196() V197() FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of NAT * : len b1 = L } is set
[:(L -tuples_on NAT),(L -tuples_on NAT):] is set
bool [:(L -tuples_on NAT),(L -tuples_on NAT):] 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
r is Relation-like NAT -defined NAT -valued Function-like finite L -element FinSequence-like FinSubsequence-like V65() V66() V67() V68() V195() finite-support Element of L -tuples_on NAT
p1 is Relation-like NAT -defined NAT -valued Function-like finite L -element FinSequence-like FinSubsequence-like V65() V66() V67() V68() V195() finite-support Element of L -tuples_on NAT
[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
L -tuples_on NAT is functional non empty FinSequence-membered V196() V197() FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of NAT * : len b1 = L } is set
bool (L -tuples_on NAT) is set
(L) is Relation-like L -tuples_on NAT -defined L -tuples_on NAT -valued total quasi_total reflexive antisymmetric transitive being_linear-order Element of bool [:(L -tuples_on NAT),(L -tuples_on NAT):]
[:(L -tuples_on NAT),(L -tuples_on NAT):] is set
bool [:(L -tuples_on NAT),(L -tuples_on NAT):] 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
r is functional FinSequence-membered Element of bool (L -tuples_on 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
{ b1 where b1 is Relation-like NAT -defined p + 1 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (p + 1) * : len b1 = L } is set
p1 is set
q1 is Relation-like NAT -defined NAT -valued Function-like finite L -element FinSequence-like FinSubsequence-like V65() V66() V67() V68() V195() finite-support Element of L -tuples_on NAT
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
L -tuples_on q is functional non empty FinSequence-membered V196() V197() FinSequenceSet of q
q * is functional non empty FinSequence-membered FinSequenceSet of q
{ b1 where b1 is Relation-like NAT -defined q -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of q * : len b1 = L } is set
p1 is functional finite FinSequence-membered Element of bool (L -tuples_on NAT)
SgmX ((L),p1) is Relation-like NAT -defined L -tuples_on NAT -valued Function-like Function-yielding finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of L -tuples_on NAT
q is Relation-like NAT -defined L -tuples_on NAT -valued Function-like Function-yielding finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of L -tuples_on NAT
r is Relation-like NAT -defined L -tuples_on NAT -valued Function-like Function-yielding finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of L -tuples_on NAT
p1 is functional finite FinSequence-membered Element of bool (L -tuples_on NAT)
SgmX ((L),p1) is Relation-like NAT -defined L -tuples_on NAT -valued Function-like Function-yielding finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of L -tuples_on NAT
q1 is functional finite FinSequence-membered Element of bool (L -tuples_on NAT)
SgmX ((L),q1) is Relation-like NAT -defined L -tuples_on NAT -valued Function-like Function-yielding finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of L -tuples_on NAT
r1 is set
p is Relation-like NAT -defined NAT -valued Function-like finite L -element FinSequence-like FinSubsequence-like V65() V66() V67() V68() V195() finite-support Element of L -tuples_on 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
p is Relation-like NAT -defined NAT -valued Function-like finite L -element FinSequence-like FinSubsequence-like V65() V66() V67() V68() V195() finite-support Element of L -tuples_on 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
(L,p) is Relation-like NAT -defined L -tuples_on NAT -valued Function-like Function-yielding finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of L -tuples_on NAT
L -tuples_on NAT is functional non empty FinSequence-membered V196() V197() FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of NAT * : len b1 = L } 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
(L -' 1) |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like finite L -' 1 -element FinSequence-like FinSubsequence-like V65() V66() V67() V68() V195() finite-support Element of (L -' 1) -tuples_on NAT
(L -' 1) -tuples_on NAT is functional non empty FinSequence-membered V196() V197() FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of NAT * : len b1 = L -' 1 } is set
Seg (L -' 1) is finite L -' 1 -element V75() V76() V77() V78() V79() V80() Element of bool NAT
(Seg (L -' 1)) --> 0 is Relation-like Seg (L -' 1) -defined RAT -valued INT -valued {0} -valued Function-like total quasi_total finite FinSequence-like FinSubsequence-like V65() V66() V67() V68() finite-support Element of bool [:(Seg (L -' 1)),{0}:]
{0} is non empty trivial finite V37() 1 -element V75() V76() V77() V78() V79() V80() set
[:(Seg (L -' 1)),{0}:] is RAT -valued INT -valued finite V65() V66() V67() V68() set
bool [:(Seg (L -' 1)),{0}:] 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
<*p*> is Relation-like NAT -defined NAT -valued Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V65() V66() V67() V68() V69() V70() V71() V72() V195() finite-support Element of NAT *
((L -' 1) |-> 0) ^ <*p*> is Relation-like NAT -defined REAL -valued Function-like non empty finite (L -' 1) + 1 -element FinSequence-like FinSubsequence-like V65() V66() V67() V195() finite-support FinSequence 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 (L -tuples_on NAT) is set
(L) is Relation-like L -tuples_on NAT -defined L -tuples_on NAT -valued total quasi_total reflexive antisymmetric transitive being_linear-order Element of bool [:(L -tuples_on NAT),(L -tuples_on NAT):]
[:(L -tuples_on NAT),(L -tuples_on NAT):] is set
bool [:(L -tuples_on NAT),(L -tuples_on NAT):] is set
p1 is functional finite FinSequence-membered Element of bool (L -tuples_on NAT)
SgmX ((L),p1) is Relation-like NAT -defined L -tuples_on NAT -valued Function-like Function-yielding finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of L -tuples_on NAT
r is Relation-like NAT -defined NAT -valued Function-like finite L -element FinSequence-like FinSubsequence-like V65() V66() V67() V68() V195() finite-support Element of L -tuples_on NAT
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
q is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V65() V66() V67() V195() finite-support FinSequence 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
q1 is functional non empty finite FinSequence-membered Element of bool (L -tuples_on NAT)
SgmX ((L),q1) is Relation-like NAT -defined L -tuples_on NAT -valued Function-like one-to-one non empty Function-yielding finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of L -tuples_on 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
(1,L) is Relation-like NAT -defined 1 -tuples_on NAT -valued Function-like one-to-one non empty Function-yielding finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of 1 -tuples_on NAT
1 -tuples_on NAT is functional non empty FinSequence-membered V196() V197() FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of NAT * : len b1 = 1 } 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 (1 -tuples_on NAT) is set
(1) is Relation-like 1 -tuples_on NAT -defined 1 -tuples_on NAT -valued total quasi_total reflexive antisymmetric transitive being_linear-order Element of bool [:(1 -tuples_on NAT),(1 -tuples_on NAT):]
[:(1 -tuples_on NAT),(1 -tuples_on NAT):] is set
bool [:(1 -tuples_on NAT),(1 -tuples_on NAT):] is set
p is functional finite FinSequence-membered Element of bool (1 -tuples_on NAT)
SgmX ((1),p) is Relation-like NAT -defined 1 -tuples_on NAT -valued Function-like Function-yielding finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of 1 -tuples_on NAT
<*L*> is Relation-like NAT -defined NAT -valued Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V65() V66() V67() V68() V69() V70() V71() V72() V195() finite-support Element of NAT *
{<*L*>} is functional non empty trivial finite V37() 1 -element set
q is set
r is Relation-like NAT -defined NAT -valued Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V65() V66() V67() V68() V69() V70() V71() V72() V195() finite-support Element of 1 -tuples_on NAT
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
<*p1*> is Relation-like NAT -defined NAT -valued Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V65() V66() V67() V68() V69() V70() V71() V72() V195() finite-support 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
(2,L) is Relation-like NAT -defined 2 -tuples_on NAT -valued Function-like one-to-one non empty Function-yielding finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support FinSequence of 2 -tuples_on NAT
2 -tuples_on NAT is functional non empty FinSequence-membered V196() V197() FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of NAT * : len b1 = 2 } 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
p is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
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
(NAT,0,L) is Relation-like NAT -defined NAT -valued Function-like non empty non trivial finite 2 -element FinSequence-like FinSubsequence-like V65() V66() V67() V68() V195() finite-support Element of 2 -tuples_on NAT
<*(NAT,0,L)*> is Relation-like NAT -defined NAT * -valued Function-like constant non empty trivial Function-yielding finite 1 -element FinSequence-like FinSubsequence-like FinSequence-yielding finite-support V214() M42( NAT ,1, len (NAT,0,L))
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
p ^ <*(NAT,0,L)*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like finite-support set
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
(NAT,q1,(L -' q1)) is Relation-like NAT -defined NAT -valued Function-like non empty non trivial finite 2 -element FinSequence-like FinSubsequence-like V65() V66() V67() V68() V195() finite-support Element of 2 -tuples_on 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
(NAT,r1,(L -' r1)) is Relation-like NAT -defined NAT -valued Function-like non empty non trivial finite 2 -element FinSequence-like FinSubsequence-like V65() V66() V67() V68() V195() finite-support Element of 2 -tuples_on 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
(NAT,q1,(L -' q1)) is Relation-like NAT -defined NAT -valued Function-like non empty non trivial finite 2 -element FinSequence-like FinSubsequence-like V65() V66() V67() V68() V195() finite-support Element of 2 -tuples_on 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