:: MATRIXJ1 semantic presentation

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

{ b

{1} is non empty trivial V33() V37() 1 -element set

Seg 2 is non empty V15() V33() 2 -element Element of bool NAT

{ b

{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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

(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

{ b

(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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

(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

{ b

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

{ b

(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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

(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

{ b

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

{ b

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

{ b

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

{ b

(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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

(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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b