:: REWRITE1 semantic presentation

REAL is set

NAT is non empty V23() V24() V25() V51() V56() V57() Element of K10(REAL)

K10(REAL) is set

NAT is non empty V23() V24() V25() V51() V56() V57() set

K10(NAT) is V51() set

K10(NAT) is V51() set

{} is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional ext-real non positive non negative V22() V23() V24() V25() V27() V28() V29() V30() V51() V56() V58( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set

1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

2 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

3 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

field {} is set

dom {} is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional ext-real non positive non negative V22() V23() V24() V25() V27() V28() V29() V30() V51() V56() V58( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set

rng {} is empty V2() V4() Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional ext-real non positive non negative V22() V23() V24() V25() V27() V28() V29() V30() V51() V56() V58( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set

(dom {}) \/ (rng {}) is Relation-like set

Seg 1 is non empty V2() V51() V58(1) Element of K10(NAT)

{1} is non empty V2() V58(1) set

Seg 2 is non empty V51() V58(2) Element of K10(NAT)

{1,2} is non empty set

len {} is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional ext-real non positive non negative V22() V23() V24() V25() V27() V28() V29() V30() V51() V56() V58( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set

R is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

C is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

R ^ C is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

len R is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

0 is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional ext-real non positive non negative V22() V23() V24() V25() V27() V28() V29() V30() V51() V56() V58( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT

0 + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

a is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() set

1 + a is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

b is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

Seg b is V51() V58(b) Element of K10(NAT)

R | (Seg b) is Relation-like NAT -defined Seg b -defined NAT -defined Function-like FinSubsequence-like set

x2 is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

x2 ^ C is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

b + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

a is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

b is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

X is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

X + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

P is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

Seg X is V51() V58(X) Element of K10(NAT)

R | (Seg X) is Relation-like NAT -defined Seg X -defined NAT -defined Function-like FinSubsequence-like set

x2 is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

P ^ C is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

P is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

P + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

a is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

Seg P is V51() V58(P) Element of K10(NAT)

R | (Seg P) is Relation-like NAT -defined Seg P -defined NAT -defined Function-like FinSubsequence-like set

Q is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

a ^ C is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

C is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() set

R is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

dom R is Element of K10(NAT)

len R is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

Seg (len R) is V51() V58( len R) Element of K10(NAT)

0 is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional ext-real non positive non negative V22() V23() V24() V25() V27() V28() V29() V30() V51() V56() V58( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT

0 + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

C is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() set

C + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

R is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

dom R is Element of K10(NAT)

len R is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

C is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() set

R is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

len R is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

Seg (len R) is V51() V58( len R) Element of K10(NAT)

dom R is Element of K10(NAT)

R is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

len R is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

C is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() set

C + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

dom R is Element of K10(NAT)

R is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

({},R) is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

(R,{}) is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

{} ^ R is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

R ^ {} is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

R is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

C is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

C ^ R is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

a is set

<*a*> is non empty V2() Relation-like NAT -defined Function-like constant V51() V58(1) FinSequence-like FinSubsequence-like set

C ^ <*a*> is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

((C ^ <*a*>),R) is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

len <*a*> is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

len (C ^ <*a*>) is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

len C is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

(len C) + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

b is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

b + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

x2 is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

Seg b is V51() V58(b) Element of K10(NAT)

(C ^ <*a*>) | (Seg b) is Relation-like NAT -defined Seg b -defined NAT -defined Function-like FinSubsequence-like set

x2 ^ R is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

len x2 is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

Q is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

x2 ^ Q is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

Q is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

C ^ Q is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

(len x2) + 0 is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

len Q is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

(len C) + (len Q) is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

R is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

C is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

a is set

<*a*> is non empty V2() Relation-like NAT -defined Function-like constant V51() V58(1) FinSequence-like FinSubsequence-like set

R ^ <*a*> is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

b is set

<*b*> is non empty V2() Relation-like NAT -defined Function-like constant V51() V58(1) FinSequence-like FinSubsequence-like set

<*b*> ^ C is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

((R ^ <*a*>),(<*b*> ^ C)) is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

R ^ <*b*> is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

(R ^ <*b*>) ^ C is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

R ^ (<*b*> ^ C) is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

R is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

C is set

<*C*> is non empty V2() Relation-like NAT -defined Function-like constant V51() V58(1) FinSequence-like FinSubsequence-like set

(<*C*>,R) is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

{} ^ <*C*> is non empty Relation-like NAT -defined Function-like V51() V58({} + 1) FinSequence-like FinSubsequence-like set

{} + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

{} ^ R is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

R is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

len R is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

C is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

a is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

len a is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

C + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

b is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

x2 is set

<*x2*> is non empty V2() Relation-like NAT -defined Function-like constant V51() V58(1) FinSequence-like FinSubsequence-like set

b ^ <*x2*> is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

len b is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

len <*x2*> is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

(len b) + (len <*x2*>) is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

<*x2*> ^ {} is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

Q is set

<*Q*> is non empty V2() Relation-like NAT -defined Function-like constant V51() V58(1) FinSequence-like FinSubsequence-like set

X is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

<*Q*> ^ X is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

len X is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

(len X) + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

X ^ <*x2*> is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

len (X ^ <*x2*>) is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

<*Q*> ^ (X ^ <*x2*>) is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

C is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

a is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

len a is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

C + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

C is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

len C is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

F

dom F

F

dom F

len F

len F

F

F

(F

dom (F

R is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

C is set

<*C*> is non empty V2() Relation-like NAT -defined Function-like constant V51() V58(1) FinSequence-like FinSubsequence-like set

R ^ <*C*> is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

R ^ F

Seg (len F

a is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

a + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

(F

(F

b is set

x2 is set

len R is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

len <*C*> is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

(len R) + (len <*C*>) is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

(len R) + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

F

F

Seg (len R) is V51() V58( len R) Element of K10(NAT)

dom R is Element of K10(NAT)

R . (a + 1) is set

R . a is set

Q is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() set

(len F

X is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

1 + X is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

(len R) + (1 + X) is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

len (F

(len R) + (len F

X + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

(X + 1) + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

F

((len R) + (1 + X)) + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

(len R) + ((X + 1) + 1) is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

F

R is Relation-like set

<*{}*> is non empty V2() Relation-like NAT -defined Function-like constant V51() V58(1) FinSequence-like FinSubsequence-like set

C is non empty V2() Relation-like NAT -defined Function-like constant V51() V58(1) FinSequence-like FinSubsequence-like set

len C is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

dom C is non empty V2() V58(1) Element of K10(NAT)

a is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

a + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

C . a is set

C . (a + 1) is set

[(C . a),(C . (a + 1))] is set

{(C . a),(C . (a + 1))} is non empty set

{(C . a)} is non empty V2() V58(1) set

{{(C . a),(C . (a + 1))},{(C . a)}} is non empty set

R is Relation-like set

C is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)

R is Relation-like set

C is set

<*C*> is non empty V2() Relation-like NAT -defined Function-like constant V51() V58(1) FinSequence-like FinSubsequence-like set

len <*C*> is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

dom <*C*> is non empty V2() V58(1) Element of K10(NAT)

b is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

b + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

<*C*> . b is set

<*C*> . (b + 1) is set

[(<*C*> . b),(<*C*> . (b + 1))] is set

{(<*C*> . b),(<*C*> . (b + 1))} is non empty set

{(<*C*> . b)} is non empty V2() V58(1) set

{{(<*C*> . b),(<*C*> . (b + 1))},{(<*C*> . b)}} is non empty set

R is Relation-like set

C is set

a is set

[C,a] is set

{C,a} is non empty set

{C} is non empty V2() V58(1) set

{{C,a},{C}} is non empty set

<*C,a*> is non empty Relation-like NAT -defined Function-like V51() V58(2) FinSequence-like FinSubsequence-like set

len <*C,a*> is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

dom <*C,a*> is non empty V58(2) Element of K10(NAT)

x2 is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

x2 + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

<*C,a*> . x2 is set

<*C,a*> . (x2 + 1) is set

[(<*C,a*> . x2),(<*C,a*> . (x2 + 1))] is set

{(<*C,a*> . x2),(<*C,a*> . (x2 + 1))} is non empty set

{(<*C,a*> . x2)} is non empty V2() V58(1) set

{{(<*C,a*> . x2),(<*C,a*> . (x2 + 1))},{(<*C,a*> . x2)}} is non empty set

1 + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

<*C,a*> . 1 is set

R is Relation-like set

C is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)

len C is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

C . (len C) is set

a is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)

a . 1 is set

(C,a) is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

x2 is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

Q is set

<*Q*> is non empty V2() Relation-like NAT -defined Function-like constant V51() V58(1) FinSequence-like FinSubsequence-like set

x2 ^ <*Q*> is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

len a is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

x2 ^ a is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

len (C,a) is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

dom (C,a) is Element of K10(NAT)

dom a is non empty Element of K10(NAT)

X is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

X + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

a . X is set

a . (X + 1) is set

[(a . X),(a . (X + 1))] is set

{(a . X),(a . (X + 1))} is non empty set

{(a . X)} is non empty V2() V58(1) set

{{(a . X),(a . (X + 1))},{(a . X)}} is non empty set

dom C is non empty Element of K10(NAT)

X is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

X + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

C . X is set

C . (X + 1) is set

[(C . X),(C . (X + 1))] is set

{(C . X),(C . (X + 1))} is non empty set

{(C . X)} is non empty V2() V58(1) set

{{(C . X),(C . (X + 1))},{(C . X)}} is non empty set

X is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

X + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

(C,a) . X is set

(C,a) . (X + 1) is set

[((C,a) . X),((C,a) . (X + 1))] is set

{((C,a) . X),((C,a) . (X + 1))} is non empty set

{((C,a) . X)} is non empty V2() V58(1) set

{{((C,a) . X),((C,a) . (X + 1))},{((C,a) . X)}} is non empty set

R is Relation-like set

R ~ is Relation-like set

C is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)

Rev C is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

len C is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

len (Rev C) is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

dom (Rev C) is Element of K10(NAT)

a is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

a + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

(Rev C) . a is set

(Rev C) . (a + 1) is set

[((Rev C) . a),((Rev C) . (a + 1))] is set

{((Rev C) . a),((Rev C) . (a + 1))} is non empty set

{((Rev C) . a)} is non empty V2() V58(1) set

{{((Rev C) . a),((Rev C) . (a + 1))},{((Rev C) . a)}} is non empty set

Seg (len C) is non empty V51() V58( len C) Element of K10(NAT)

(len C) - (a + 1) is ext-real V22() V30() set

((len C) - (a + 1)) + 1 is ext-real V22() V30() set

dom C is non empty Element of K10(NAT)

b is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

(len C) - a is ext-real V22() V30() set

b + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

C . b is set

C . (b + 1) is set

[(C . b),(C . (b + 1))] is set

{(C . b),(C . (b + 1))} is non empty set

{(C . b)} is non empty V2() V58(1) set

{{(C . b),(C . (b + 1))},{(C . b)}} is non empty set

((len C) - a) + 1 is ext-real V22() V30() set

C . (((len C) - a) + 1) is set

C . (((len C) - (a + 1)) + 1) is set

R is Relation-like set

C is Relation-like set

a is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)

len a is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

dom a is non empty Element of K10(NAT)

b is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

b + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

a . b is set

a . (b + 1) is set

[(a . b),(a . (b + 1))] is set

{(a . b),(a . (b + 1))} is non empty set

{(a . b)} is non empty V2() V58(1) set

{{(a . b),(a . (b + 1))},{(a . b)}} is non empty set

R is Relation-like set

C is set

a is set

b is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)

b . 1 is set

len b is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

b . (len b) is set

dom b is non empty Element of K10(NAT)

x2 is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

x2 + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

b . x2 is set

b . (x2 + 1) is set

[(b . x2),(b . (x2 + 1))] is set

{(b . x2),(b . (x2 + 1))} is non empty set

{(b . x2)} is non empty V2() V58(1) set

{{(b . x2),(b . (x2 + 1))},{(b . x2)}} is non empty set

b is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

len b is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

b . 1 is set

b . (len b) is set

dom b is Element of K10(NAT)

x2 is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)

x2 . 1 is set

len x2 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

x2 . (len x2) is set

R is Relation-like set

C is set

<*C*> is non empty V2() Relation-like NAT -defined Function-like constant V51() V58(1) FinSequence-like FinSubsequence-like set

a is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)

a . 1 is set

len a is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

a . (len a) is set

R is set

C is set

a is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like ( {} )

a . 1 is set

len a is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

a . (len a) is set

dom a is non empty Element of K10(NAT)

1 + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

R is Relation-like set

field R is set

dom R is set

rng R is set

(dom R) \/ (rng R) is set

C is set

a is set

b is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)

b . 1 is set

len b is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

b . (len b) is set

dom b is non empty Element of K10(NAT)

1 + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

b . (1 + 1) is set

[(b . 1),(b . (1 + 1))] is set

{(b . 1),(b . (1 + 1))} is non empty set

{(b . 1)} is non empty V2() V58(1) set

{{(b . 1),(b . (1 + 1))},{(b . 1)}} is non empty set

R is Relation-like set

C is set

a is set

[C,a] is set

{C,a} is non empty set

{C} is non empty V2() V58(1) set

{{C,a},{C}} is non empty set

<*C,a*> is non empty Relation-like NAT -defined Function-like V51() V58(2) FinSequence-like FinSubsequence-like set

b is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)

b . 1 is set

len b is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

b . (len b) is set

R is Relation-like set

C is set

a is set

b is set

x2 is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)

x2 . 1 is set

len x2 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

x2 . (len x2) is set

Q is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)

Q . 1 is set

len Q is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

Q . (len Q) is set

(x2,Q) is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

X is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)

X . 1 is set

len X is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

X . (len X) is set

P is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

P is set

<*P*> is non empty V2() Relation-like NAT -defined Function-like constant V51() V58(1) FinSequence-like FinSubsequence-like set

P ^ <*P*> is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

Seg (len Q) is non empty V51() V58( len Q) Element of K10(NAT)

dom Q is non empty Element of K10(NAT)

P ^ Q is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

len P is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

Seg (len P) is V51() V58( len P) Element of K10(NAT)

dom P is Element of K10(NAT)

P . 1 is set

(len P) + (len Q) is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

R is Relation-like set

C is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)

dom C is non empty Element of K10(NAT)

a is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

b is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

C . a is set

C . b is set

x2 is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() set

a + x2 is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

Q is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

a + Q is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

C . (a + Q) is set

Q + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

a + (Q + 1) is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

(a + Q) + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

len C is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

C . (a + (Q + 1)) is set

[(C . (a + Q)),(C . (a + (Q + 1)))] is set

{(C . (a + Q)),(C . (a + (Q + 1)))} is non empty set

{(C . (a + Q))} is non empty V2() V58(1) set

{{(C . (a + Q)),(C . (a + (Q + 1)))},{(C . (a + Q))}} is non empty set

Q is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

a + Q is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

C . (a + Q) is set

Q + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

a + (Q + 1) is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

C . (a + (Q + 1)) is set

a + 0 is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

C . (a + 0) is set

R is Relation-like set

field R is set

dom R is set

rng R is set

(dom R) \/ (rng R) is set

C is set

a is set

b is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)

b . 1 is set

len b is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

b . (len b) is set

1 + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

dom b is non empty Element of K10(NAT)

b . 2 is set

[C,(b . 2)] is set

{C,(b . 2)} is non empty set

{C} is non empty V2() V58(1) set

{{C,(b . 2)},{C}} is non empty set

x2 is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

b . x2 is set

x2 + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

b . (x2 + 1) is set

b . (x2 + 1) is set

[(b . x2),(b . (x2 + 1))] is set

{(b . x2),(b . (x2 + 1))} is non empty set

{(b . x2)} is non empty V2() V58(1) set

{{(b . x2),(b . (x2 + 1))},{(b . x2)}} is non empty set

x2 is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

b . x2 is set

x2 + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

b . (x2 + 1) is set

b . 0 is set

R is Relation-like set

C is set

a is set

field R is set

dom R is set

rng R is set

(dom R) \/ (rng R) is set

R is Relation-like set

R [*] is Relation-like set

C is set

a is set

[C,a] is set

{C,a} is non empty set

{C} is non empty V2() V58(1) set

{{C,a},{C}} is non empty set

b is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)

b . 1 is set

len b is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

b . (len b) is set

x2 is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() set

dom b is non empty Element of K10(NAT)

x2 + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

b . x2 is set

b . (x2 + 1) is set

[(b . x2),(b . (x2 + 1))] is set

{(b . x2),(b . (x2 + 1))} is non empty set

{(b . x2)} is non empty V2() V58(1) set

{{(b . x2),(b . (x2 + 1))},{(b . x2)}} is non empty set

field R is set

dom R is set

rng R is set

(dom R) \/ (rng R) is set

b is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

len b is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

b . 1 is set

b . (len b) is set

dom b is Element of K10(NAT)

x2 is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

x2 + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

b . x2 is set

b . (x2 + 1) is set

[(b . x2),(b . (x2 + 1))] is set

{(b . x2),(b . (x2 + 1))} is non empty set

{(b . x2)} is non empty V2() V58(1) set

{{(b . x2),(b . (x2 + 1))},{(b . x2)}} is non empty set

R is Relation-like set

R [*] is Relation-like set

C is set

a is set

[C,a] is set

{C,a} is non empty set

{C} is non empty V2() V58(1) set

{{C,a},{C}} is non empty set

b is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R [*] )

b . 1 is set

len b is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

b . (len b) is set

dom b is non empty Element of K10(NAT)

x2 is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

b . x2 is set

x2 + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

b . (x2 + 1) is set

b . (x2 + 1) is set

[(b . x2),(b . (x2 + 1))] is set

{(b . x2),(b . (x2 + 1))} is non empty set

{(b . x2)} is non empty V2() V58(1) set

{{(b . x2),(b . (x2 + 1))},{(b . x2)}} is non empty set

x2 is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

b . x2 is set

x2 + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

b . (x2 + 1) is set

b . 0 is set

R is Relation-like set

C is Relation-like set

a is set

b is set

x2 is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)

x2 . 1 is set

len x2 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

x2 . (len x2) is set

R is Relation-like set

C is set

id C is Relation-like C -defined C -valued Function-like one-to-one reflexive symmetric antisymmetric transitive set

R \/ (id C) is Relation-like set

a is set

b is set

x2 is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R \/ (id C))

x2 . 1 is set

len x2 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

x2 . (len x2) is set

dom x2 is non empty Element of K10(NAT)

Q is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

x2 . Q is set

Q + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

x2 . (Q + 1) is set

[(x2 . Q),(x2 . (Q + 1))] is set

{(x2 . Q),(x2 . (Q + 1))} is non empty set

{(x2 . Q)} is non empty V2() V58(1) set

{{(x2 . Q),(x2 . (Q + 1))},{(x2 . Q)}} is non empty set

x2 . (Q + 1) is set

Q is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

x2 . Q is set

Q + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

x2 . (Q + 1) is set

x2 . 0 is set

R is Relation-like set

R ~ is Relation-like set

C is set

a is set

b is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)

b . 1 is set

len b is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

b . (len b) is set

Rev b is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

x2 is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R ~ )

x2 . 1 is set

len x2 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

x2 . (len x2) is set

dom x2 is non empty Element of K10(NAT)

(len b) - 1 is ext-real V22() V30() set

((len b) - 1) + 1 is ext-real V22() V30() set

b . (((len b) - 1) + 1) is set

(len b) - (len b) is ext-real V22() V30() set

((len b) - (len b)) + 1 is ext-real V22() V30() set

b . (((len b) - (len b)) + 1) is set

R is Relation-like set

C is set

a is set

R ~ is Relation-like set

R \/ (R ~) is Relation-like set

(R \/ (R ~)) ~ is Relation-like set

(R ~) ~ is Relation-like set

(R ~) \/ ((R ~) ~) is Relation-like set

R is Relation-like set

C is set

a is set

b is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)

b . 1 is set

len b is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

b . (len b) is set

R ~ is Relation-like set

R \/ (R ~) is Relation-like set

dom b is non empty Element of K10(NAT)

x2 is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

x2 + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

b . x2 is set

b . (x2 + 1) is set

[(b . x2),(b . (x2 + 1))] is set

{(b . x2),(b . (x2 + 1))} is non empty set

{(b . x2)} is non empty V2() V58(1) set

{{(b . x2),(b . (x2 + 1))},{(b . x2)}} is non empty set

R is Relation-like set

C is set

R is set

C is set

{} ~ is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional ext-real non positive non negative V22() V23() V24() V25() V27() V28() V29() V30() V51() V56() V58( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set

{} \/ ({} ~) is Relation-like set

R is Relation-like set

field R is set

dom R is set

rng R is set

(dom R) \/ (rng R) is set

C is set

a is set

R ~ is Relation-like set

field (R ~) is set

dom (R ~) is set

rng (R ~) is set

(dom (R ~)) \/ (rng (R ~)) is set

R \/ (R ~) is Relation-like set

field (R \/ (R ~)) is set

dom (R \/ (R ~)) is set

rng (R \/ (R ~)) is set

(dom (R \/ (R ~))) \/ (rng (R \/ (R ~))) is set

(field R) \/ (field (R ~)) is set

R is Relation-like set

C is set

a is set

[C,a] is set

{C,a} is non empty set

{C} is non empty V2() V58(1) set

{{C,a},{C}} is non empty set

R is Relation-like set

C is set

a is set

b is set

R ~ is Relation-like set

R \/ (R ~) is Relation-like set

R is Relation-like set

C is set

a is set

R is Relation-like set

field R is set

dom R is set

rng R is set

(dom R) \/ (rng R) is set

C is set

a is set

R ~ is Relation-like set

R \/ (R ~) is Relation-like set

field (R \/ (R ~)) is set

dom (R \/ (R ~)) is set

rng (R \/ (R ~)) is set

(dom (R \/ (R ~))) \/ (rng (R \/ (R ~))) is set

field (R ~) is set

dom (R ~) is set

rng (R ~) is set

(dom (R ~)) \/ (rng (R ~)) is set

(field R) \/ (field (R ~)) is set

(field R) \/ (field R) is set

R is Relation-like set

C is set

a is set

b is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set

len b is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

b . 1 is set

b . (len b) is set

dom b is Element of K10(NAT)

1 + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

b . (1 + 1) is set

[C,(b . (1 + 1))] is set

{C,(b . (1 + 1))} is non empty set

{C} is non empty V2() V58(1) set

{{C,(b . (1 + 1))},{C}} is non empty set

R is Relation-like set

field R is set

dom R is set

rng R is set

(dom R) \/ (rng R) is set

C is set

a is set

[C,a] is set

{C,a} is non empty set

{C} is non empty V2() V58(1) set

{{C,a},{C}} is non empty set

R is Relation-like set

field R is set

dom R is set

rng R is set

(dom R) \/ (rng R) is set

C is set

R is Relation-like set

C is set

a is set

R is Relation-like set

C is set

a is set

b is set

b is set

R is Relation-like set

C is set

R is set

C is set

a is set

a is set

R is Relation-like set

C is set

a is set

b is set

R is Relation-like set

C is set

a is set

b is set

R is Relation-like set

C is set

a is set

b is set

x2 is set

x2 is set

R is Relation-like set

a is set

C is set

b is set

x2 is set

x2 is set

R is Relation-like set

C is set

a is set

b is set

[C,b] is set

{C,b} is non empty set

{C} is non empty V2() V58(1) set

{{C,b},{C}} is non empty set

[a,b] is set

{a,b} is non empty set

{a} is non empty V2() V58(1) set

{{a,b},{a}} is non empty set

R is Relation-like set

C is set

a is set

b is set

[b,C] is set

{b,C} is non empty set

{b} is non empty V2() V58(1) set

{{b,C},{b}} is non empty set

[b,a] is set

{b,a} is non empty set

{{b,a},{b}} is non empty set

R is Relation-like set

field R is set

dom R is set

rng R is set

(dom R) \/ (rng R) is set

C is set

R is Relation-like set

C is set

a is set

b is set

R is Relation-like set

field R is set

dom R is set

rng R is set

(dom R) \/ (rng R) is set

R ~ is Relation-like set

field (R ~) is set

dom (R ~) is set

rng (R ~) is set

(dom (R ~)) \/ (rng (R ~)) is set

C is set

a is set

(R ~) -Seg a is set

Coim ((R ~),a) is set

{a} is non empty V2() V58(1) set

(R ~) " {a} is set

(Coim ((R ~),a)) \ {a} is Element of K10((Coim ((R ~),a)))

K10((Coim ((R ~),a))) is set

b is set

x2 is set

(R ~) -Seg b is set

Coim ((R ~),b) is set

{b} is non empty V2() V58(1) set

(R ~) " {b} is set

(Coim ((R ~),b)) \ {b} is Element of K10((Coim ((R ~),b)))

K10((Coim ((R ~),b))) is set

[x2,b] is set

{x2,b} is non empty set

{x2} is non empty V2() V58(1) set

{{x2,b},{x2}} is non empty set

[b,x2] is set

{b,x2} is non empty set

{{b,x2},{b}} is non empty set

C is set

a is set

(R ~) -Seg a is set

Coim ((R ~),a) is set

{a} is non empty V2() V58(1) set

(R ~) " {a} is set

(Coim ((R ~),a)) \ {a} is Element of K10((Coim ((R ~),a)))

K10((Coim ((R ~),a))) is set

((R ~) -Seg a) /\ C is set

b is non empty set

the Element of b is Element of b

[a, the Element of b] is set

{a, the Element of b} is non empty set

{{a, the Element of b},{a}} is non empty set

[ the Element of b,a] is set

{ the Element of b,a} is non empty set

{ the Element of b} is non empty V2() V58(1) set

{{ the Element of b,a},{ the Element of b}} is non empty set

F

field F

dom F

rng F

(dom F

R is set

C is non empty set

{ b

a is Element of C

x2 is set

Q is Element of C

x2 is set

Q is set

[x2,Q] is set

{x2,Q} is non empty set

{x2} is non empty V2() V58(1) set

{{x2,Q},{x2}} is non empty set

Q is Element of C

R is Relation-like set

field R is set

dom R is set

rng R is set

(dom R) \/ (rng R) is set

C is set

[C,C] is set

{C,C} is non empty set

{C} is non empty V2() V58(1) set

{{C,C},{C}} is non empty set

NAT --> C is Relation-like Function-like V27() V35( NAT ,{C}) Element of K10(K11(NAT,{C}))

K11(NAT,{C}) is Relation-like V51() set

K10(K11(NAT,{C})) is V51() set

dom (NAT --> C) is V23() V24() V25() set

a is Relation-like NAT -defined Function-like V31( NAT ) set

b is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

a . b is set

b + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

a . (b + 1) is set

[(a . b),(a . (b + 1))] is set

{(a . b),(a . (b + 1))} is non empty set

{(a . b)} is non empty V2() V58(1) set

{{(a . b),(a . (b + 1))},{(a . b)}} is non empty set

C is set

field R is set

dom R is set

rng R is set

(dom R) \/ (rng R) is set

b is set

a is non empty set

x2 is set

[b,x2] is set

{b,x2} is non empty set

{b} is non empty V2() V58(1) set

{{b,x2},{b}} is non empty set

b is set

the Element of a is Element of a

x2 is Relation-like Function-like set

dom x2 is set

rng x2 is set

x2 . 0 is set

R is Relation-like set

field R is set

dom R is set

rng R is set

(dom R) \/ (rng R) is set

C is Relation-like NAT -defined Function-like V31( NAT ) set

rng C is set

a is set

dom C is set

b is set

C . b is set

x2 is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

x2 + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

C . (x2 + 1) is set

[a,(C . (x2 + 1))] is set

{a,(C . (x2 + 1))} is non empty set

{a} is non empty V2() V58(1) set

{{a,(C . (x2 + 1))},{a}} is non empty set

dom C is set

C . 0 is set

a is set

b is set

C . b is set

x2 is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

x2 + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

C . (x2 + 1) is set

[a,(C . (x2 + 1))] is set

{a,(C . (x2 + 1))} is non empty set

{a} is non empty V2() V58(1) set

{{a,(C . (x2 + 1))},{a}} is non empty set

R is Relation-like set

C is set

field R is set

dom R is set

rng R is set

(dom R) \/ (rng R) is set

C is Relation-like NAT -defined Function-like V31( NAT ) set

C . 0 is set

C . (0 + 1) is set

[(C . 0),(C . (0 + 1))] is set

{(C . 0),(C . (0 + 1))} is non empty set

{(C . 0)} is non empty V2() V58(1) set

{{(C . 0),(C . (0 + 1))},{(C . 0)}} is non empty set

R is Relation-like () set

C is Relation-like set

a is set

field C is set

dom C is set

rng C is set

(dom C) \/ (rng C) is set

field R is set

dom R is set

rng R is set

(dom R) \/ (rng R) is set

b is set

x2 is set

[b,x2] is set

{b,x2} is non empty set

{b} is non empty V2() V58(1) set

{{b,x2},{b}} is non empty set

R is Relation-like set

C is set

field R is set

dom R is set

rng R is set

(dom R) \/ (rng R) is set

a is non empty set

{ b

x2 is set

Q is Element of a

x2 is set

[x2,x2] is set

{x2,x2} is non empty set

{x2} is non empty V2() V58(1) set

{{x2,x2},{x2}} is non empty set

Q is set

[x2,Q] is set

{x2,Q} is non empty set

{{x2,Q},{x2}} is non empty set

X is Element of a

Q is Element of a

a is Relation-like set

b is Relation-like set

x2 is set

Q is set

[x2,Q] is set

{x2,Q} is non empty set

{x2} is non empty V2() V58(1) set

{{x2,Q},{x2}} is non empty set

X is set

[x2,X] is set

{x2,X} is non empty set

{{x2,X},{x2}} is non empty set

P is set

a is Relation-like set

b is Relation-like set

x2 is set

Q is set

X is set

P is set

R is Relation-like set

C is Relation-like set

a is set

b is set

[a,b] is set

{a,b} is non empty set

{a} is non empty V2() V58(1) set

{{a,b},{a}} is non empty set

x2 is set

[a,x2] is set

{a,x2} is non empty set

{{a,x2},{a}} is non empty set

R is Relation-like set

C is set

a is set

b is set

[C,b] is set

{C,b} is non empty set

{C} is non empty V2() V58(1) set

{{C,b},{C}} is non empty set

x2 is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)

x2 . 1 is set

len x2 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

x2 . (len x2) is set

dom x2 is non empty Element of K10(NAT)

Q is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

x2 . Q is set

Q + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

x2 . (Q + 1) is set

X is set

[(x2 . Q),X] is set

{(x2 . Q),X} is non empty set

{(x2 . Q)} is non empty V2() V58(1) set

{{(x2 . Q),X},{(x2 . Q)}} is non empty set

X is set

[(x2 . Q),X] is set

{(x2 . Q),X} is non empty set

{(x2 . Q)} is non empty V2() V58(1) set

{{(x2 . Q),X},{(x2 . Q)}} is non empty set

x2 . (Q + 1) is set

[(x2 . Q),(x2 . (Q + 1))] is set

{(x2 . Q),(x2 . (Q + 1))} is non empty set

{{(x2 . Q),(x2 . (Q + 1))},{(x2 . Q)}} is non empty set

P is set

[(x2 . (Q + 1)),P] is set

{(x2 . (Q + 1)),P} is non empty set

{(x2 . (Q + 1))} is non empty V2() V58(1) set

{{(x2 . (Q + 1)),P},{(x2 . (Q + 1))}} is non empty set

[X,P] is set

{X,P} is non empty set

{X} is non empty V2() V58(1) set

{{X,P},{X}} is non empty set

P is set

[(x2 . (Q + 1)),P] is set

{(x2 . (Q + 1)),P} is non empty set

{{(x2 . (Q + 1)),P},{(x2 . (Q + 1))}} is non empty set

P is set

[(x2 . (Q + 1)),P] is set

{(x2 . (Q + 1)),P} is non empty set

{{(x2 . (Q + 1)),P},{(x2 . (Q + 1))}} is non empty set

Q is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

x2 . Q is set

X is set

[(x2 . Q),X] is set

{(x2 . Q),X} is non empty set

{(x2 . Q)} is non empty V2() V58(1) set

{{(x2 . Q),X},{(x2 . Q)}} is non empty set

Q + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

x2 . (Q + 1) is set

x2 . 0 is set

Q is set

[a,Q] is set

{a,Q} is non empty set

{a} is non empty V2() V58(1) set

{{a,Q},{a}} is non empty set

R is Relation-like set

C is set

a is set

b is set

C is set

a is set

b is set

R is Relation-like set

C is set

a is set

b is set

[C,b] is set

{C,b} is non empty set

{C} is non empty V2() V58(1) set

{{C,b},{C}} is non empty set

C is set

a is set

b is set

x2 is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)

x2 . 1 is set

len x2 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

x2 . (len x2) is set

Q is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)

Q . 1 is set

len Q is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

Q . (len Q) is set

dom x2 is non empty Element of K10(NAT)

dom Q is non empty Element of K10(NAT)

X is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

x2 . X is set

X + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

x2 . (X + 1) is set

P is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

Q . P is set

P + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

Q . (P + 1) is set

P is set

[(Q . P),(Q . (P + 1))] is set

{(Q . P),(Q . (P + 1))} is non empty set

{(Q . P)} is non empty V2() V58(1) set

{{(Q . P),(Q . (P + 1))},{(Q . P)}} is non empty set

Q . 0 is set

x2 . 0 is set

X is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT

Q . X is set

R is Relation-like set

C is set

a is set

[C,a] is set

{C,a} is non empty set

{C} is non empty V2() V58(1) set

{{C,a},{C}} is non empty set

b is set

[C,b] is set

{C,b} is non empty set

{{C,b},{C}} is non empty set

C is set

a is set

[C,a] is set

{C,a} is non empty set

{C} is non empty V2() V58(1) set

{{C,a},{C}} is non empty set

b is set

[C,b] is set

{C,b} is non empty set

{{C,b},{C