:: MATRIXJ1 semantic presentation

REAL is set
NAT is non empty non trivial V24() V25() V26() V33() cardinal limit_cardinal Element of bool REAL

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

RAT is set

{{},1} is non empty V33() V37() set
K577() is set
bool K577() is set
K578() is Element of bool K577()

bool 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

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

K539(()) is V31() ext-real V141() Element of REAL

K is non empty addLoopStr
the carrier of K is non empty set

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

len R1 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

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

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

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

dom R1 is V33() Element of bool NAT

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

Del ((R2 ^ R1),(K + (len R2))) 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

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

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

[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)) * () is Element of the carrier of R1
((power R1) . (R2,R1)) * R2 is Element of the carrier of R1

{} -tuples_on the carrier of R1 is functional non empty FinSequence-membered FinSequenceSet 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

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

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

R2 is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() set

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

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

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

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

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

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

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

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

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

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

dom R1 is V33() Element of bool NAT
R1 . K is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() set

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

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

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

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

Sum (R1 | R2) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element 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

[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

(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

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

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

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 ^ R2),K) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element 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

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

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

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

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

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

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

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

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

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

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

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

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

dom R1 is V33() Element of bool 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

Sum (R1 | K) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element 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

[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

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

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

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

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

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

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

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

Sum (K | R1) is V24() V25() V26() V30() V31() V33() cardinal ext-real non negative V141() Element 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

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

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

Sum (K | R1) is V24() V25() V26() V30() V31() V33() cardinal ext-real 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
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

[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

(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

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