REAL is set
NAT is non empty non trivial V24() V25() V26() V33() cardinal limit_cardinal Element of bool REAL
bool REAL is set
NAT is non empty non trivial V24() V25() V26() V33() cardinal limit_cardinal set
bool NAT is non trivial V33() set
bool NAT is non trivial V33() set
INT is set
1 is non empty V24() V25() V26() V30() V31() V33() cardinal ext-real positive non negative V141() Element of NAT
2 is non empty V24() V25() V26() V30() V31() V33() cardinal ext-real positive non negative V141() Element of NAT
COMPLEX is set
RAT is set
[:REAL,REAL:] is Relation-like set
bool [:REAL,REAL:] is set
{} is Relation-like non-empty empty-yielding RAT -valued functional empty V24() V25() V26() V28() V29() V30() V31() V33() V34() V37() cardinal {} -element FinSequence-like FinSequence-membered ext-real non positive non negative V141() V186() V187() V188() V189() set
{{},1} is non empty V33() V37() set
K577() is set
bool K577() is set
K578() is Element of bool K577()
[:COMPLEX,COMPLEX:] is Relation-like set
bool [:COMPLEX,COMPLEX:] is set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is set
[:[:REAL,REAL:],REAL:] is Relation-like set
bool [:[:REAL,REAL:],REAL:] is set
[:RAT,RAT:] is Relation-like set
bool [:RAT,RAT:] is set
[:[:RAT,RAT:],RAT:] is Relation-like set
bool [:[:RAT,RAT:],RAT:] is set
[:INT,INT:] is Relation-like set
bool [:INT,INT:] is set
[:[:INT,INT:],INT:] is Relation-like set
bool [:[:INT,INT:],INT:] is set
[:NAT,NAT:] is Relation-like non trivial V33() set
[:[:NAT,NAT:],NAT:] is Relation-like non trivial V33() set
bool [:[:NAT,NAT:],NAT:] is non trivial V33() set
K680() is set
3 is non empty V24() V25() V26() V30() V31() V33() cardinal ext-real positive non negative V141() Element of NAT
0 is Relation-like non-empty empty-yielding RAT -valued functional empty V24() V25() V26() V28() V29() V30() V31() V33() V34() V37() cardinal {} -element FinSequence-like FinSequence-membered ext-real non positive non negative V141() V186() V187() V188() V189() Element of NAT
Seg 1 is non empty trivial V15() V33() 1 -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set
{1} is non empty trivial V33() V37() 1 -element set
Seg 2 is non empty V15() V33() 2 -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= 2 ) } is set
{1,2} is non empty V33() V37() set
<*> REAL is Relation-like non-empty empty-yielding NAT -defined REAL -valued RAT -valued Function-like functional empty V24() V25() V26() V28() V29() V30() V31() V33() V34() V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V141() V186() V187() V188() V189() FinSequence of REAL
K539((<*> REAL)) is V31() ext-real V141() Element of REAL
card {} is Relation-like non-empty empty-yielding RAT -valued functional empty V24() V25() V26() V28() V29() V30() V31() V33() V34() V37() cardinal {} -element FinSequence-like FinSequence-membered ext-real non positive non negative V141() V186() V187() V188() V189() set
K is non empty addLoopStr
the carrier of K is non empty set
R1 is Relation-like NAT -defined the carrier of K -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of K
R2 is Relation-like NAT -defined the carrier of K -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of K
R1 + R2 is Relation-like NAT -defined the carrier of K -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of K
the addF of K is Relation-like Function-like V21([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is Relation-like set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is Relation-like set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is set
the addF of K .: (R1,R2) is Relation-like NAT -defined the carrier of K -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of K
dom (R1 + R2) is V33() Element of bool NAT
dom R1 is V33() Element of bool NAT
dom R2 is V33() Element of bool NAT
(dom R1) /\ (dom R2) is V33() Element of bool NAT
rng R2 is V33() set
rng R1 is V33() set
[:(rng R1),(rng R2):] is Relation-like V33() set
dom the addF of K is set
K is non empty addLoopStr
the carrier of K is non empty set
R1 is Relation-like NAT -defined the carrier of K -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of K
len R1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
R2 is Relation-like NAT -defined the carrier of K -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of K
len R2 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
R1 + R2 is Relation-like NAT -defined the carrier of K -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of K
the addF of K is Relation-like Function-like V21([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is Relation-like set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is Relation-like set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is set
the addF of K .: (R1,R2) is Relation-like NAT -defined the carrier of K -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of K
R1 is Relation-like NAT -defined the carrier of K -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of K
R2 is Relation-like NAT -defined the carrier of K -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of K
R1 + R2 is Relation-like NAT -defined the carrier of K -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of K
the addF of K .: (R1,R2) is Relation-like NAT -defined the carrier of K -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of K
(R1 + R2) ^ (R1 + R2) is Relation-like NAT -defined the carrier of K -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of K
R1 ^ R1 is Relation-like NAT -defined the carrier of K -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of K
R2 ^ R2 is Relation-like NAT -defined the carrier of K -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of K
(R1 ^ R1) + (R2 ^ R2) is Relation-like NAT -defined the carrier of K -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of K
the addF of K .: ((R1 ^ R1),(R2 ^ R2)) is Relation-like NAT -defined the carrier of K -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the carrier of K
dom R1 is V33() Element of bool NAT
dom R2 is V33() Element of bool NAT
dom R2 is V33() Element of bool NAT
len R2 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
Seg (len R2) is V15() V33() len R2 -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= len R2 ) } is set
dom R1 is V33() Element of bool NAT
len R1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
Seg (len R1) is V15() V33() len R1 -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= len R1 ) } is set
dom (R1 ^ R1) is V33() Element of bool NAT
(len R1) + (len R1) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
Seg ((len R1) + (len R1)) is V15() V33() (len R1) + (len R1) -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= (len R1) + (len R1) ) } is set
dom (R2 ^ R2) is V33() Element of bool NAT
(len R2) + (len R2) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
Seg ((len R2) + (len R2)) is V15() V33() (len R2) + (len R2) -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= (len R2) + (len R2) ) } is set
dom (R1 + R2) is V33() Element of bool NAT
(dom R1) /\ (dom R2) is V33() Element of bool NAT
dom (R1 + R2) is V33() Element of bool NAT
(dom R1) /\ (dom R2) is V33() Element of bool NAT
len (R1 + R2) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
dom ((R1 ^ R1) + (R2 ^ R2)) is V33() Element of bool NAT
(dom (R1 ^ R1)) /\ (dom (R2 ^ R2)) is V33() Element of bool NAT
len (R1 + R2) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
dom ((R1 + R2) ^ (R1 + R2)) is V33() Element of bool NAT
len (R1 + R2) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
dom ((R1 + R2) ^ (R1 + R2)) is V33() Element of bool NAT
dom ((R1 + R2) ^ (R1 + R2)) is V33() Element of bool NAT
dom ((R1 + R2) ^ (R1 + R2)) is V33() Element of bool NAT
b2 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() set
R2 . b2 is set
(R2 ^ R2) . b2 is set
R2 /. b2 is Element of the carrier of K
R1 . b2 is set
(R1 ^ R1) . b2 is set
R1 /. b2 is Element of the carrier of K
((R1 + R2) ^ (R1 + R2)) . b2 is set
(R1 + R2) . b2 is set
(R1 /. b2) + (R2 /. b2) is Element of the carrier of K
((R1 ^ R1) + (R2 ^ R2)) . b2 is set
b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() set
(len (R1 + R2)) + b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() set
(len (R1 + R2)) + b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
(R1 ^ R1) . b2 is set
R1 . b1 is set
R1 /. b1 is Element of the carrier of K
(R2 ^ R2) . b2 is set
R2 . b1 is set
R2 /. b1 is Element of the carrier of K
((R1 + R2) ^ (R1 + R2)) . b2 is set
(R1 + R2) . b1 is set
(R1 /. b1) + (R2 /. b1) is Element of the carrier of K
((R1 ^ R1) + (R2 ^ R2)) . b2 is set
((R1 + R2) ^ (R1 + R2)) . b2 is set
((R1 ^ R1) + (R2 ^ R2)) . b2 is set
((R1 + R2) ^ (R1 + R2)) . b2 is set
((R1 ^ R1) + (R2 ^ R2)) . b2 is set
K is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() set
R1 is non empty set
R2 is Relation-like NAT -defined R1 -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of R1
dom R2 is V33() Element of bool NAT
R1 is Relation-like NAT -defined R1 -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of R1
R2 ^ R1 is Relation-like NAT -defined R1 -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of R1
Del ((R2 ^ R1),K) is Relation-like NAT -defined R1 -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of R1
Del (R2,K) is Relation-like NAT -defined R1 -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of R1
(Del (R2,K)) ^ R1 is Relation-like NAT -defined R1 -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of R1
len R2 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
len (Del (R2,K)) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
b2 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() set
b2 + 1 is non empty V24() V25() V26() V30() V31() V33() cardinal ext-real positive non negative V141() Element of NAT
len (R2 ^ R1) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
Seg (len (R2 ^ R1)) is V15() V33() len (R2 ^ R1) -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= len (R2 ^ R1) ) } is set
dom (R2 ^ R1) is V33() Element of bool NAT
len R1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
(len R2) + (len R1) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
Seg (len R2) is V15() V33() len R2 -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= len R2 ) } is set
(len R1) + b2 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
((len R1) + b2) + 1 is non empty V24() V25() V26() V30() V31() V33() cardinal ext-real positive non negative V141() Element of NAT
b2n is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() set
b2 + (len R1) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
dom (Del (R2,K)) is V33() Element of bool NAT
(Del ((R2 ^ R1),K)) . b2n is set
(R2 ^ R1) . b2n is set
R2 . b2n is set
(Del (R2,K)) . b2n is set
((Del (R2,K)) ^ R1) . b2n is set
{} + 1 is non empty V24() V25() V26() V30() V31() V33() cardinal ext-real positive non negative V141() Element of NAT
b2n + 1 is non empty V24() V25() V26() V30() V31() V33() cardinal ext-real positive non negative V141() Element of NAT
dom (Del (R2,K)) is V33() Element of bool NAT
(Del ((R2 ^ R1),K)) . b2n is set
(R2 ^ R1) . (b2n + 1) is set
R2 . (b2n + 1) is set
(Del (R2,K)) . b2n is set
((Del (R2,K)) ^ R1) . b2n is set
b2n + 1 is non empty V24() V25() V26() V30() V31() V33() cardinal ext-real positive non negative V141() Element of NAT
(b2n + 1) - (len R2) is V31() ext-real V141() set
(b2 + (len R1)) + 1 is non empty V24() V25() V26() V30() V31() V33() cardinal ext-real positive non negative V141() Element of NAT
b1n is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
b1n + (len R2) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
dom R1 is V33() Element of bool NAT
(Del ((R2 ^ R1),K)) . b2n is set
(R2 ^ R1) . (b1n + (len R2)) is set
R1 . b1n is set
b2 + b1n is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
((Del (R2,K)) ^ R1) . (b2 + b1n) is set
((Del (R2,K)) ^ R1) . b2n is set
(Del ((R2 ^ R1),K)) . b2n is set
((Del (R2,K)) ^ R1) . b2n is set
(Del ((R2 ^ R1),K)) . b2n is set
((Del (R2,K)) ^ R1) . b2n is set
(Del ((R2 ^ R1),K)) . b2n is set
((Del (R2,K)) ^ R1) . b2n is set
(Del ((R2 ^ R1),K)) . b2n is set
((Del (R2,K)) ^ R1) . b2n is set
len ((Del (R2,K)) ^ R1) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
(len (Del (R2,K))) + (len R1) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
len (Del ((R2 ^ R1),K)) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
K is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() set
R1 is non empty set
R1 is Relation-like NAT -defined R1 -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of R1
dom R1 is V33() Element of bool NAT
R2 is Relation-like NAT -defined R1 -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of R1
len R2 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
K + (len R2) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
R2 ^ R1 is Relation-like NAT -defined R1 -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of R1
Del ((R2 ^ R1),(K + (len R2))) is Relation-like NAT -defined R1 -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of R1
Del (R1,K) is Relation-like NAT -defined R1 -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of R1
R2 ^ (Del (R1,K)) is Relation-like NAT -defined R1 -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of R1
len R1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
len (Del (R1,K)) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
b2 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() set
b2 + 1 is non empty V24() V25() V26() V30() V31() V33() cardinal ext-real positive non negative V141() Element of NAT
dom (R2 ^ R1) is V33() Element of bool NAT
len (R2 ^ R1) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
Seg (len (R2 ^ R1)) is V15() V33() len (R2 ^ R1) -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= len (R2 ^ R1) ) } is set
(len R2) + (len R1) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
b2 + (len R2) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
(b2 + (len R2)) + 1 is non empty V24() V25() V26() V30() V31() V33() cardinal ext-real positive non negative V141() Element of NAT
Seg (len R1) is V15() V33() len R1 -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= len R1 ) } is set
b1n is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() set
dom R2 is V33() Element of bool NAT
{} + (len R2) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
(Del ((R2 ^ R1),(K + (len R2)))) . b1n is set
(R2 ^ R1) . b1n is set
R2 . b1n is set
(R2 ^ (Del (R1,K))) . b1n is set
b1n - (len R2) is V31() ext-real V141() set
ab is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
ab + 1 is non empty V24() V25() V26() V30() V31() V33() cardinal ext-real positive non negative V141() Element of NAT
ab + (len R2) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
dom (Del (R1,K)) is V33() Element of bool NAT
(Del ((R2 ^ R1),(K + (len R2)))) . b1n is set
(R2 ^ R1) . (ab + (len R2)) is set
R1 . ab is set
(Del (R1,K)) . ab is set
(R2 ^ (Del (R1,K))) . (ab + (len R2)) is set
(R2 ^ (Del (R1,K))) . b1n is set
(Del ((R2 ^ R1),(K + (len R2)))) . b1n is set
(ab + (len R2)) + 1 is non empty V24() V25() V26() V30() V31() V33() cardinal ext-real positive non negative V141() Element of NAT
(R2 ^ R1) . ((ab + (len R2)) + 1) is set
(ab + 1) + (len R2) is non empty V24() V25() V26() V30() V31() V33() cardinal ext-real positive non negative V141() Element of NAT
(R2 ^ R1) . ((ab + 1) + (len R2)) is set
R1 . (ab + 1) is set
(Del (R1,K)) . ab is set
(R2 ^ (Del (R1,K))) . (ab + (len R2)) is set
(R2 ^ (Del (R1,K))) . b1n is set
(Del ((R2 ^ R1),(K + (len R2)))) . b1n is set
(R2 ^ (Del (R1,K))) . b1n is set
(Del ((R2 ^ R1),(K + (len R2)))) . b1n is set
(R2 ^ (Del (R1,K))) . b1n is set
(Del ((R2 ^ R1),(K + (len R2)))) . b1n is set
(R2 ^ (Del (R1,K))) . b1n is set
(Del ((R2 ^ R1),(K + (len R2)))) . b1n is set
(R2 ^ (Del (R1,K))) . b1n is set
len (R2 ^ (Del (R1,K))) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
(len R2) + (len (Del (R1,K))) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
len (Del ((R2 ^ R1),(K + (len R2)))) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
K is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() set
R1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() set
R1 + 1 is non empty V24() V25() V26() V30() V31() V33() cardinal ext-real positive non negative V141() Element of NAT
Seg (R1 + 1) is non empty V15() V33() R1 + 1 -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= R1 + 1 ) } is set
R2 is non empty set
R1 is Element of R2
(R1 + 1) |-> R1 is Relation-like NAT -defined R2 -valued Function-like V33() R1 + 1 -element FinSequence-like FinSubsequence-like Element of (R1 + 1) -tuples_on R2
(R1 + 1) -tuples_on R2 is functional non empty FinSequence-membered FinSequenceSet of R2
Del (((R1 + 1) |-> R1),K) is Relation-like NAT -defined R2 -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of R2
R1 |-> R1 is Relation-like NAT -defined R2 -valued Function-like V33() R1 -element FinSequence-like FinSubsequence-like Element of R1 -tuples_on R2
R1 -tuples_on R2 is functional non empty FinSequence-membered FinSequenceSet of R2
len ((R1 + 1) |-> R1) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
dom ((R1 + 1) |-> R1) is V33() R1 + 1 -element Element of bool NAT
Seg (len ((R1 + 1) |-> R1)) is V15() V33() len ((R1 + 1) |-> R1) -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= len ((R1 + 1) |-> R1) ) } is set
len (R1 |-> R1) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
R2n is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() set
Seg R1 is V15() V33() R1 -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= R1 ) } is set
R2n + 1 is non empty V24() V25() V26() V30() V31() V33() cardinal ext-real positive non negative V141() Element of NAT
(Del (((R1 + 1) |-> R1),K)) . R2n is set
((R1 + 1) |-> R1) . R2n is set
(R1 |-> R1) . R2n is set
(Del (((R1 + 1) |-> R1),K)) . R2n is set
((R1 + 1) |-> R1) . (R2n + 1) is set
(R1 |-> R1) . R2n is set
(Del (((R1 + 1) |-> R1),K)) . R2n is set
(R1 |-> R1) . R2n is set
(Del (((R1 + 1) |-> R1),K)) . R2n is set
(R1 |-> R1) . R2n is set
len (Del (((R1 + 1) |-> R1),K)) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
K is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() set
R1 is non empty non degenerated non trivial right_complementable almost_left_invertible unital V127() V129() V144() V145() V146() right-distributive left-distributive right_unital well-unital V158() left_unital doubleLoopStr
the carrier of R1 is non empty non trivial set
power R1 is Relation-like Function-like V21([: the carrier of R1,NAT:], the carrier of R1) Element of bool [:[: the carrier of R1,NAT:], the carrier of R1:]
[: the carrier of R1,NAT:] is Relation-like non trivial V33() set
[:[: the carrier of R1,NAT:], the carrier of R1:] is Relation-like non trivial V33() set
bool [:[: the carrier of R1,NAT:], the carrier of R1:] is non trivial V33() set
R2 is Element of the carrier of R1
K |-> R2 is Relation-like NAT -defined the carrier of R1 -valued Function-like V33() K -element FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of R1
K -tuples_on the carrier of R1 is functional non empty FinSequence-membered FinSequenceSet of the carrier of R1
Product (K |-> R2) is Element of the carrier of R1
(power R1) . (R2,K) is Element of the carrier of R1
R1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() set
R1 |-> R2 is Relation-like NAT -defined the carrier of R1 -valued Function-like V33() R1 -element FinSequence-like FinSubsequence-like Element of R1 -tuples_on the carrier of R1
R1 -tuples_on the carrier of R1 is functional non empty FinSequence-membered FinSequenceSet of the carrier of R1
Product (R1 |-> R2) is Element of the carrier of R1
(power R1) . (R2,R1) is Element of the carrier of R1
R1 + 1 is non empty V24() V25() V26() V30() V31() V33() cardinal ext-real positive non negative V141() Element of NAT
(R1 + 1) |-> R2 is Relation-like NAT -defined the carrier of R1 -valued Function-like V33() R1 + 1 -element FinSequence-like FinSubsequence-like Element of (R1 + 1) -tuples_on the carrier of R1
(R1 + 1) -tuples_on the carrier of R1 is functional non empty FinSequence-membered FinSequenceSet of the carrier of R1
Product ((R1 + 1) |-> R2) is Element of the carrier of R1
(power R1) . (R2,(R1 + 1)) is Element of the carrier of R1
1 |-> R2 is Relation-like NAT -defined the carrier of R1 -valued Function-like non empty trivial V33() 1 -element FinSequence-like FinSubsequence-like Element of 1 -tuples_on the carrier of R1
1 -tuples_on the carrier of R1 is functional non empty FinSequence-membered FinSequenceSet of the carrier of R1
Product (1 |-> R2) is Element of the carrier of R1
(Product (R1 |-> R2)) * (Product (1 |-> R2)) is Element of the carrier of R1
<*R2*> is Relation-like NAT -defined the carrier of R1 -valued Function-like non empty trivial V33() 1 -element FinSequence-like FinSubsequence-like Element of 1 -tuples_on the carrier of R1
[1,R2] is set
{1,R2} is non empty V33() set
{{1,R2},{1}} is non empty V33() V37() set
{[1,R2]} is Relation-like non empty trivial V33() 1 -element set
Product <*R2*> is Element of the carrier of R1
(Product (R1 |-> R2)) * (Product <*R2*>) is Element of the carrier of R1
((power R1) . (R2,R1)) * R2 is Element of the carrier of R1
{} |-> R2 is Relation-like non-empty empty-yielding NAT -defined the carrier of R1 -valued Function-like functional empty V24() V25() V26() V28() V29() V30() V31() V33() V34() V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V141() V186() V187() V188() V189() Element of {} -tuples_on the carrier of R1
{} -tuples_on the carrier of R1 is functional non empty FinSequence-membered FinSequenceSet of the carrier of R1
<*> the carrier of R1 is Relation-like non-empty empty-yielding NAT -defined RAT -valued the carrier of R1 -valued Function-like functional empty V24() V25() V26() V28() V29() V30() V31() V33() V34() V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V141() V186() V187() V188() V189() FinSequence of the carrier of R1
Product ({} |-> R2) is Element of the carrier of R1
1_ R1 is Element of the carrier of R1
1. R1 is V61(R1) Element of the carrier of R1
(power R1) . (R2,{}) is Element of the carrier of R1
R1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() set
K is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
Sum K is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
Seg (Sum K) is V15() V33() Sum K -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= Sum K ) } is set
dom K is V33() Element of bool NAT
len K is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
K | (len K) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
Seg (len K) is V15() V33() len K -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= len K ) } is set
K | (Seg (len K)) is Relation-like Seg (len K) -defined NAT -defined NAT -valued RAT -valued V33() FinSubsequence-like V186() V187() V188() V189() set
R2 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() set
K | R2 is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
Seg R2 is V15() V33() R2 -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= R2 ) } is set
K | (Seg R2) is Relation-like Seg R2 -defined NAT -defined NAT -valued RAT -valued V33() FinSubsequence-like V186() V187() V188() V189() set
Sum (K | R2) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
R1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
K | R1 is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
Seg R1 is V15() V33() R1 -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= R1 ) } is set
K | (Seg R1) is Relation-like Seg R1 -defined NAT -defined NAT -valued RAT -valued V33() FinSubsequence-like V186() V187() V188() V189() set
Sum (K | R1) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
R2 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() set
K | R2 is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
Seg R2 is V15() V33() R2 -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= R2 ) } is set
K | (Seg R2) is Relation-like Seg R2 -defined NAT -defined NAT -valued RAT -valued V33() FinSubsequence-like V186() V187() V188() V189() set
Sum (K | R2) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
R2 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
K | R2 is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
Seg R2 is V15() V33() R2 -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= R2 ) } is set
K | (Seg R2) is Relation-like Seg R2 -defined NAT -defined NAT -valued RAT -valued V33() FinSubsequence-like V186() V187() V188() V189() set
Sum (K | R2) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
R1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
K | R1 is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
Seg R1 is V15() V33() R1 -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= R1 ) } is set
K | (Seg R1) is Relation-like Seg R1 -defined NAT -defined NAT -valued RAT -valued V33() FinSubsequence-like V186() V187() V188() V189() set
Sum (K | R1) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
K is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() set
R1 is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
dom R1 is V33() Element of bool NAT
R1 . K is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() set
R1 | K is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
Seg K is V15() V33() K -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= K ) } is set
R1 | (Seg K) is Relation-like Seg K -defined NAT -defined NAT -valued RAT -valued V33() FinSubsequence-like V186() V187() V188() V189() set
Sum (R1 | K) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
(R1,(Sum (R1 | K))) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
len R1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
len (R1 | K) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
dom (R1 | K) is V33() Element of bool NAT
(R1 | K) . K is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() set
R1 | (len R1) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
Seg (len R1) is V15() V33() len R1 -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= len R1 ) } is set
R1 | (Seg (len R1)) is Relation-like Seg (len R1) -defined NAT -defined NAT -valued RAT -valued V33() FinSubsequence-like V186() V187() V188() V189() set
Sum (R1 | (len R1)) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
Sum R1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
Seg (Sum R1) is V15() V33() Sum R1 -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= Sum R1 ) } is set
K - 1 is V31() ext-real V141() set
R2 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
R2 + 1 is non empty V24() V25() V26() V30() V31() V33() cardinal ext-real positive non negative V141() Element of NAT
R1 | (R1,(Sum (R1 | K))) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
Seg (R1,(Sum (R1 | K))) is V15() V33() (R1,(Sum (R1 | K))) -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= (R1,(Sum (R1 | K))) ) } is set
R1 | (Seg (R1,(Sum (R1 | K)))) is Relation-like Seg (R1,(Sum (R1 | K))) -defined NAT -defined NAT -valued RAT -valued V33() FinSubsequence-like V186() V187() V188() V189() set
Sum (R1 | (R1,(Sum (R1 | K)))) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
R1 | R2 is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
Seg R2 is V15() V33() R2 -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= R2 ) } is set
R1 | (Seg R2) is Relation-like Seg R2 -defined NAT -defined NAT -valued RAT -valued V33() FinSubsequence-like V186() V187() V188() V189() set
Sum (R1 | R2) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
R1 | (R2 + 1) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
Seg (R2 + 1) is non empty V15() V33() R2 + 1 -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= R2 + 1 ) } is set
R1 | (Seg (R2 + 1)) is Relation-like Seg (R2 + 1) -defined NAT -defined NAT -valued RAT -valued V33() FinSubsequence-like V186() V187() V188() V189() set
<*(R1 . K)*> is Relation-like NAT -defined Function-like non empty trivial V33() 1 -element FinSequence-like FinSubsequence-like set
[1,(R1 . K)] is set
{1,(R1 . K)} is non empty V33() V37() set
{{1,(R1 . K)},{1}} is non empty V33() V37() set
{[1,(R1 . K)]} is Relation-like non empty trivial V33() 1 -element set
(R1 | R2) ^ <*(R1 . K)*> is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(Sum (R1 | R2)) + (R1 . K) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
K is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() set
R1 is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
Sum R1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
Seg (Sum R1) is V15() V33() Sum R1 -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= Sum R1 ) } is set
(R1,K) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
(R1,K) -' 1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
(R1,K) - 1 is V31() ext-real V141() set
R1 | ((R1,K) -' 1) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
Seg ((R1,K) -' 1) is V15() V33() (R1,K) -' 1 -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= (R1,K) -' 1 ) } is set
R1 | (Seg ((R1,K) -' 1)) is Relation-like Seg ((R1,K) -' 1) -defined NAT -defined NAT -valued RAT -valued V33() FinSubsequence-like V186() V187() V188() V189() set
Sum (R1 | ((R1,K) -' 1)) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
dom R1 is V33() Element of bool NAT
(R1,K) - {} is V31() ext-real non negative V141() set
K is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() set
R1 is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
Sum R1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
Seg (Sum R1) is V15() V33() Sum R1 -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= Sum R1 ) } is set
(R1,K) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
R2 is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
R1 ^ R2 is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
((R1 ^ R2),K) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
R1 | (R1,K) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
Seg (R1,K) is V15() V33() (R1,K) -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= (R1,K) ) } is set
R1 | (Seg (R1,K)) is Relation-like Seg (R1,K) -defined NAT -defined NAT -valued RAT -valued V33() FinSubsequence-like V186() V187() V188() V189() set
Sum (R1 | (R1,K)) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
R1 is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
Sum R1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
Sum R2 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
(Sum R1) + (Sum R2) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
(Sum R1) + {} is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
Seg (Sum R1) is V15() V33() Sum R1 -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= Sum R1 ) } is set
dom R1 is V33() Element of bool NAT
len R1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
R1 | (R1,K) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
R1 | (Seg (R1,K)) is Relation-like Seg (R1,K) -defined NAT -defined NAT -valued RAT -valued V33() FinSubsequence-like V186() V187() V188() V189() set
(R1,K) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
R1 | (R1,K) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
Seg (R1,K) is V15() V33() (R1,K) -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= (R1,K) ) } is set
R1 | (Seg (R1,K)) is Relation-like Seg (R1,K) -defined NAT -defined NAT -valued RAT -valued V33() FinSubsequence-like V186() V187() V188() V189() set
R1 | (R1,K) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
R1 | (Seg (R1,K)) is Relation-like Seg (R1,K) -defined NAT -defined NAT -valued RAT -valued V33() FinSubsequence-like V186() V187() V188() V189() set
Sum (R1 | (R1,K)) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
K is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() set
R1 is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
Sum R1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
Seg (Sum R1) is V15() V33() Sum R1 -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= Sum R1 ) } is set
K -' (Sum R1) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
len R1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
K - (Sum R1) is V31() ext-real V141() set
R2 is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
Sum R2 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
(Sum R1) + (Sum R2) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
Seg ((Sum R1) + (Sum R2)) is V15() V33() (Sum R1) + (Sum R2) -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= (Sum R1) + (Sum R2) ) } is set
(Seg ((Sum R1) + (Sum R2))) \ (Seg (Sum R1)) is V15() V33() Element of bool NAT
R1 ^ R2 is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
((R1 ^ R2),K) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
(R2,(K -' (Sum R1))) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
(R2,(K -' (Sum R1))) + (len R1) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
R1 is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
Sum R1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
Seg (Sum R1) is V15() V33() Sum R1 -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= Sum R1 ) } is set
R2 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
R2 + (Sum R1) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
(R2,R2) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
(len R1) + (R2,R2) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
R1 | ((len R1) + (R2,R2)) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
Seg ((len R1) + (R2,R2)) is V15() V33() (len R1) + (R2,R2) -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= (len R1) + (R2,R2) ) } is set
R1 | (Seg ((len R1) + (R2,R2))) is Relation-like Seg ((len R1) + (R2,R2)) -defined NAT -defined NAT -valued RAT -valued V33() FinSubsequence-like V186() V187() V188() V189() set
R2 | (R2,R2) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
Seg (R2,R2) is V15() V33() (R2,R2) -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= (R2,R2) ) } is set
R2 | (Seg (R2,R2)) is Relation-like Seg (R2,R2) -defined NAT -defined NAT -valued RAT -valued V33() FinSubsequence-like V186() V187() V188() V189() set
R1 ^ (R2 | (R2,R2)) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
Sum (R1 | ((len R1) + (R2,R2))) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
Sum (R2 | (R2,R2)) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
(Sum R1) + (Sum (R2 | (R2,R2))) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
Seg (Sum R2) is V15() V33() Sum R2 -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= Sum R2 ) } is set
(Sum R1) + R2 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
(R1,K) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
R1 | (R1,K) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
Seg (R1,K) is V15() V33() (R1,K) -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= (R1,K) ) } is set
R1 | (Seg (R1,K)) is Relation-like Seg (R1,K) -defined NAT -defined NAT -valued RAT -valued V33() FinSubsequence-like V186() V187() V188() V189() set
Sum (R1 | (R1,K)) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
R1 | (len R1) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
Seg (len R1) is V15() V33() len R1 -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= len R1 ) } is set
R1 | (Seg (len R1)) is Relation-like Seg (len R1) -defined NAT -defined NAT -valued RAT -valued V33() FinSubsequence-like V186() V187() V188() V189() set
R1 | (R1,K) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
R1 | (Seg (R1,K)) is Relation-like Seg (R1,K) -defined NAT -defined NAT -valued RAT -valued V33() FinSubsequence-like V186() V187() V188() V189() set
Sum (R1 | (R1,K)) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
Sum (R1 | (len R1)) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
(R1,K) - (len R1) is V31() ext-real V141() set
b2 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
(len R1) + b2 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
R1 | ((len R1) + b2) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
Seg ((len R1) + b2) is V15() V33() (len R1) + b2 -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= (len R1) + b2 ) } is set
R1 | (Seg ((len R1) + b2)) is Relation-like Seg ((len R1) + b2) -defined NAT -defined NAT -valued RAT -valued V33() FinSubsequence-like V186() V187() V188() V189() set
R2 | b2 is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
Seg b2 is V15() V33() b2 -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= b2 ) } is set
R2 | (Seg b2) is Relation-like Seg b2 -defined NAT -defined NAT -valued RAT -valued V33() FinSubsequence-like V186() V187() V188() V189() set
R1 ^ (R2 | b2) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
Sum (R2 | b2) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
(Sum R1) + (Sum (R2 | b2)) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
((Sum R1) + (Sum (R2 | b2))) - (Sum R1) is V31() ext-real V141() set
(R2,R2) + (len R1) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
b2 + (len R1) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
K is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() set
K -' 1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
R1 is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
dom R1 is V33() Element of bool NAT
R1 | K is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
Seg K is V15() V33() K -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= K ) } is set
R1 | (Seg K) is Relation-like Seg K -defined NAT -defined NAT -valued RAT -valued V33() FinSubsequence-like V186() V187() V188() V189() set
Sum (R1 | K) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
R1 | (K -' 1) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
Seg (K -' 1) is V15() V33() K -' 1 -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= K -' 1 ) } is set
R1 | (Seg (K -' 1)) is Relation-like Seg (K -' 1) -defined NAT -defined NAT -valued RAT -valued V33() FinSubsequence-like V186() V187() V188() V189() set
Sum (R1 | (K -' 1)) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
R1 . K is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() set
(Sum (R1 | (K -' 1))) + (R1 . K) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
R1 /. K is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
<*(R1 /. K)*> is Relation-like NAT -defined NAT -valued Function-like one-to-one non empty trivial V33() 1 -element FinSequence-like FinSubsequence-like V186() V187() V188() V189() V190() V191() V192() V193() Element of 1 -tuples_on NAT
1 -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
[1,(R1 /. K)] is set
{1,(R1 /. K)} is non empty V33() V37() set
{{1,(R1 /. K)},{1}} is non empty V33() V37() set
{[1,(R1 /. K)]} is Relation-like non empty trivial V33() 1 -element set
K - 1 is V31() ext-real V141() set
(K -' 1) + 1 is non empty V24() V25() V26() V30() V31() V33() cardinal ext-real positive non negative V141() Element of NAT
(R1 | (K -' 1)) ^ <*(R1 /. K)*> is Relation-like NAT -defined NAT -valued Function-like non empty V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
Sum ((R1 | (K -' 1)) ^ <*(R1 /. K)*>) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
K is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() set
K -' 1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
R1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() set
R2 is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
dom R2 is V33() Element of bool NAT
R2 /. K is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
Seg (R2 /. K) is V15() V33() R2 /. K -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= R2 /. K ) } is set
R2 | (K -' 1) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
Seg (K -' 1) is V15() V33() K -' 1 -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= K -' 1 ) } is set
R2 | (Seg (K -' 1)) is Relation-like Seg (K -' 1) -defined NAT -defined NAT -valued RAT -valued V33() FinSubsequence-like V186() V187() V188() V189() set
Sum (R2 | (K -' 1)) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
R1 + (Sum (R2 | (K -' 1))) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
R2 | K is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
Seg K is V15() V33() K -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= K ) } is set
R2 | (Seg K) is Relation-like Seg K -defined NAT -defined NAT -valued RAT -valued V33() FinSubsequence-like V186() V187() V188() V189() set
Sum (R2 | K) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
Seg (Sum (R2 | K)) is V15() V33() Sum (R2 | K) -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= Sum (R2 | K) ) } is set
(R2,(R1 + (Sum (R2 | (K -' 1))))) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
R2 . K is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() set
(R2 /. K) + (Sum (R2 | (K -' 1))) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
len R2 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
R2 | (len R2) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
Seg (len R2) is V15() V33() len R2 -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= len R2 ) } is set
R2 | (Seg (len R2)) is Relation-like Seg (len R2) -defined NAT -defined NAT -valued RAT -valued V33() FinSubsequence-like V186() V187() V188() V189() set
Sum (R2 | (len R2)) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
Sum R2 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
Seg (Sum R2) is V15() V33() Sum R2 -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= Sum R2 ) } is set
1 + {} is non empty V24() V25() V26() V30() V31() V33() cardinal ext-real positive non negative V141() Element of NAT
K - 1 is V31() ext-real V141() set
(K -' 1) + 1 is non empty V24() V25() V26() V30() V31() V33() cardinal ext-real positive non negative V141() Element of NAT
R2 | (R2,(R1 + (Sum (R2 | (K -' 1))))) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
Seg (R2,(R1 + (Sum (R2 | (K -' 1))))) is V15() V33() (R2,(R1 + (Sum (R2 | (K -' 1))))) -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= (R2,(R1 + (Sum (R2 | (K -' 1))))) ) } is set
R2 | (Seg (R2,(R1 + (Sum (R2 | (K -' 1)))))) is Relation-like Seg (R2,(R1 + (Sum (R2 | (K -' 1))))) -defined NAT -defined NAT -valued RAT -valued V33() FinSubsequence-like V186() V187() V188() V189() set
Sum (R2 | (R2,(R1 + (Sum (R2 | (K -' 1)))))) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
(Sum (R2 | (K -' 1))) + {} is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
K is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
len K is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
dom K is V33() Element of bool NAT
R1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() set
R2 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() set
K | R1 is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
Seg R1 is V15() V33() R1 -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= R1 ) } is set
K | (Seg R1) is Relation-like Seg R1 -defined NAT -defined NAT -valued RAT -valued V33() FinSubsequence-like V186() V187() V188() V189() set
Sum (K | R1) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
K | R2 is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
Seg R2 is V15() V33() R2 -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= R2 ) } is set
K | (Seg R2) is Relation-like Seg R2 -defined NAT -defined NAT -valued RAT -valued V33() FinSubsequence-like V186() V187() V188() V189() set
Sum (K | R2) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
K . R1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() set
K . R2 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() set
R1 - 1 is V31() ext-real V141() set
R1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
R1 + 1 is non empty V24() V25() V26() V30() V31() V33() cardinal ext-real positive non negative V141() Element of NAT
K | R1 is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
Seg R1 is V15() V33() R1 -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= R1 ) } is set
K | (Seg R1) is Relation-like Seg R1 -defined NAT -defined NAT -valued RAT -valued V33() FinSubsequence-like V186() V187() V188() V189() set
Sum (K | R1) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
K | (R1 + 1) is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
Seg (R1 + 1) is non empty V15() V33() R1 + 1 -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1 <= R1 + 1 ) } is set
K | (Seg (R1 + 1)) is Relation-like Seg (R1 + 1) -defined NAT -defined NAT -valued RAT -valued V33() FinSubsequence-like V186() V187() V188() V189() set
<*(K . R1)*> is Relation-like NAT -defined Function-like non empty trivial V33() 1 -element FinSequence-like FinSubsequence-like set
[1,(K . R1)] is set
{1,(K . R1)} is non empty V33() V37() set
{{1,(K . R1)},{1}} is non empty V33() V37() set
{[1,(K . R1)]} is Relation-like non empty trivial V33() 1 -element set
(K | R1) ^ <*(K . R1)*> is Relation-like NAT -defined Function-like non empty V33() FinSequence-like FinSubsequence-like set
(Sum (K | R1)) + (K . R1) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT
R1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() set
K | R1 is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V186() V187() V188() V189() FinSequence of NAT
Seg R1 is V15() V33() R1 -element Element of bool NAT
{ b1 where b1 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element of NAT : ( 1 <= b1 & b1