:: FINSEQ_7 semantic presentation

REAL is set
NAT is non empty V24() V25() V26() Element of K19(REAL)
K19(REAL) is set
NAT is non empty V24() V25() V26() set
K19(NAT) is set
K19(NAT) is set

1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
2 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
3 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT

D is non empty set

len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
i is ext-real V24() V25() V26() V30() V31() V32() V33() set
i -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT

Seg (i -' 1) is V34() V41(i -' 1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= i -' 1 ) } is set

f . i is set

[1,(f . i)] is set
{[1,(f . i)]} is Relation-like Function-like non empty set
(f | (i -' 1)) ^ <*(f . i)*> is Relation-like NAT -defined Function-like non empty V34() FinSequence-like FinSubsequence-like set

k is ext-real V24() V25() V26() V30() V31() V32() V33() set
k -' i is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(k -' i) -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(f /^ i) | ((k -' i) -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg ((k -' i) -' 1) is V34() V41((k -' i) -' 1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= (k -' i) -' 1 ) } is set
(f /^ i) | (Seg ((k -' i) -' 1)) is Relation-like NAT -defined Seg ((k -' i) -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
((f | (i -' 1)) ^ <*(f . i)*>) ^ ((f /^ i) | ((k -' i) -' 1)) is Relation-like NAT -defined Function-like non empty V34() FinSequence-like FinSubsequence-like set
f . k is set

[1,(f . k)] is set
{[1,(f . k)]} is Relation-like Function-like non empty set
(((f | (i -' 1)) ^ <*(f . i)*>) ^ ((f /^ i) | ((k -' i) -' 1))) ^ <*(f . k)*> is Relation-like NAT -defined Function-like non empty V34() FinSequence-like FinSubsequence-like set

((((f | (i -' 1)) ^ <*(f . i)*>) ^ ((f /^ i) | ((k -' i) -' 1))) ^ <*(f . k)*>) ^ (f /^ k) is Relation-like NAT -defined Function-like non empty V34() FinSequence-like FinSubsequence-like set
dom f is Element of K19(NAT)
i -' i is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
((k -' i) -' 1) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(len f) -' i is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
len (f /^ i) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
F is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT

Seg F is V34() V41(F) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= F ) } is set

len (f | F) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
l is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT

dom (f /^ l) is Element of K19(NAT)
(((k -' i) -' 1) + 1) + l is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(f /^ l) /. (((k -' i) -' 1) + 1) is Element of D
f /. F is Element of D

((f | F) ^ (f /^ F)) /^ l is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D

((f | F) /^ l) ^ (f /^ F) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ l) | (((k -' i) -' 1) + 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg (((k -' i) -' 1) + 1) is non empty V34() V41(((k -' i) -' 1) + 1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= ((k -' i) -' 1) + 1 ) } is set
(f /^ l) | (Seg (((k -' i) -' 1) + 1)) is Relation-like NAT -defined Seg (((k -' i) -' 1) + 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
((f /^ l) | (((k -' i) -' 1) + 1)) ^ (f /^ F) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ l) | ((k -' i) -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f /^ l) | (Seg ((k -' i) -' 1)) is Relation-like NAT -defined Seg ((k -' i) -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
<*((f /^ l) /. (((k -' i) -' 1) + 1))*> is Relation-like NAT -defined D -valued Function-like non empty V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1,((f /^ l) /. (((k -' i) -' 1) + 1))] is set
{[1,((f /^ l) /. (((k -' i) -' 1) + 1))]} is Relation-like Function-like non empty set
((f /^ l) | ((k -' i) -' 1)) ^ <*((f /^ l) /. (((k -' i) -' 1) + 1))*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((f /^ l) | ((k -' i) -' 1)) ^ <*((f /^ l) /. (((k -' i) -' 1) + 1))*>) ^ (f /^ F) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
f . F is set

[1,(f . F)] is set
{[1,(f . F)]} is Relation-like Function-like non empty set
((f /^ l) | ((k -' i) -' 1)) ^ <*(f . F)*> is Relation-like NAT -defined Function-like non empty V34() FinSequence-like FinSubsequence-like set
(((f /^ l) | ((k -' i) -' 1)) ^ <*(f . F)*>) ^ (f /^ F) is Relation-like NAT -defined Function-like non empty V34() FinSequence-like FinSubsequence-like set
l -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT

Seg (l -' 1) is V34() V41(l -' 1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= l -' 1 ) } is set

f . l is set

[1,(f . l)] is set
{[1,(f . l)]} is Relation-like Function-like non empty set
(f | (l -' 1)) ^ <*(f . l)*> is Relation-like NAT -defined Function-like non empty V34() FinSequence-like FinSubsequence-like set
((f | (l -' 1)) ^ <*(f . l)*>) ^ (f /^ l) is Relation-like NAT -defined Function-like non empty V34() FinSequence-like FinSubsequence-like set

((f /^ l) | ((k -' i) -' 1)) ^ (<*(f . F)*> ^ (f /^ F)) is Relation-like NAT -defined Function-like non empty V34() FinSequence-like FinSubsequence-like set
((f | (l -' 1)) ^ <*(f . l)*>) ^ (((f /^ l) | ((k -' i) -' 1)) ^ (<*(f . F)*> ^ (f /^ F))) is Relation-like NAT -defined Function-like non empty V34() FinSequence-like FinSubsequence-like set
((f | (l -' 1)) ^ <*(f . l)*>) ^ ((f /^ l) | ((k -' i) -' 1)) is Relation-like NAT -defined Function-like non empty V34() FinSequence-like FinSubsequence-like set
(((f | (l -' 1)) ^ <*(f . l)*>) ^ ((f /^ l) | ((k -' i) -' 1))) ^ (<*(f . F)*> ^ (f /^ F)) is Relation-like NAT -defined Function-like non empty V34() FinSequence-like FinSubsequence-like set
(((f | (l -' 1)) ^ <*(f . l)*>) ^ ((f /^ l) | ((k -' i) -' 1))) ^ <*(f . F)*> is Relation-like NAT -defined Function-like non empty V34() FinSequence-like FinSubsequence-like set
((((f | (l -' 1)) ^ <*(f . l)*>) ^ ((f /^ l) | ((k -' i) -' 1))) ^ <*(f . F)*>) ^ (f /^ F) is Relation-like NAT -defined Function-like non empty V34() FinSequence-like FinSubsequence-like set
D is ext-real V24() V25() V26() V30() V31() V32() V33() set

len i is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT

len k is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT

len (i ^ f) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(i ^ f) . D is set

(k ^ f) . D is set
len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(len i) + (len f) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
D - (len i) is ext-real V31() V32() V33() set
((len i) + (len f)) - (len i) is ext-real V31() V32() V33() set
(len i) - (len i) is ext-real V31() V32() V33() set
0 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
l is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
dom f is Element of K19(NAT)
l + (len i) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(i ^ f) . (l + (len i)) is set
f . l is set
(len k) + l is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(k ^ f) . ((len k) + l) is set
D is ext-real V24() V25() V26() V30() V31() V32() V33() set

len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
f . D is set

len i is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(len i) + D is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(i ^ f) . ((len i) + D) is set
dom f is Element of K19(NAT)
D is non empty set

i is ext-real V24() V25() V26() V30() V31() V32() V33() set
k is ext-real V24() V25() V26() V30() V31() V32() V33() set

dom (f /^ k) is Element of K19(NAT)
(f /^ k) . i is set
k + i is ext-real V31() V32() V33() set
f . (k + i) is set
l is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
j is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
l + j is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
dom f is Element of K19(NAT)

(f /^ l) /. j is Element of D
f /. (l + j) is Element of D
(f /^ l) . j is set
D is ext-real V24() V25() V26() V30() V31() V32() V33() set
D -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
f is ext-real V24() V25() V26() V30() V31() V32() V33() set
D -' f is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(D -' f) -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(D -' 1) -' f is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
f + 1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
D -' (f + 1) is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
D is non empty set
D is non empty set
i is ext-real V24() V25() V26() V30() V31() V32() V33() set

len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
k is Element of D

i -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT

Seg (i -' 1) is V34() V41(i -' 1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= i -' 1 ) } is set

[1,k] is set

((f | (i -' 1)) ^ <*k*>) ^ (f /^ i) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
dom f is Element of K19(NAT)
dom f is Element of K19(NAT)

j is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT

D is non empty set

k is ext-real V24() V25() V26() V30() V31() V32() V33() set
i is Element of D

len (D,f,k,i) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
D is non empty set

k is ext-real V24() V25() V26() V30() V31() V32() V33() set
i is Element of D

rng (D,f,k,i) is set
rng f is set
{i} is non empty set
(rng f) \/ {i} is non empty set
D is non empty set

len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
i is Element of D
k is ext-real V24() V25() V26() V30() V31() V32() V33() set

rng (D,f,k,i) is set
dom f is Element of K19(NAT)
D is non empty set

len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
i is Element of D
k is ext-real V24() V25() V26() V30() V31() V32() V33() set

(D,f,k,i) . k is set
dom f is Element of K19(NAT)
D is non empty set

len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
i is Element of D
k is ext-real V24() V25() V26() V30() V31() V32() V33() set

(D,f,k,i) /. k is Element of D
dom f is Element of K19(NAT)
D is non empty set

len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
i is Element of D
k is ext-real V24() V25() V26() V30() V31() V32() V33() set
(len f) - k is ext-real V31() V32() V33() set

k - 1 is ext-real V31() V32() V33() set
k -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT

Seg (k -' 1) is V34() V41(k -' 1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= k -' 1 ) } is set

[1,i] is set

len ((f | (k -' 1)) ^ <*i*>) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
len (f | (k -' 1)) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
len <*i*> is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(len (f | (k -' 1))) + () is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(k -' 1) + () is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(k -' 1) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
j is ext-real V24() V25() V26() V30() V31() V32() V33() set
k + j is ext-real V31() V32() V33() set
(D,f,k,i) . (k + j) is set
(f /^ k) . j is set
0 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
len (D,f,k,i) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
((f | (k -' 1)) ^ <*i*>) ^ (f /^ k) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
len (((f | (k -' 1)) ^ <*i*>) ^ (f /^ k)) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
len (f /^ k) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
k + (len (f /^ k)) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
dom (f /^ k) is Element of K19(NAT)
(len ((f | (k -' 1)) ^ <*i*>)) + j is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(((f | (k -' 1)) ^ <*i*>) ^ (f /^ k)) . ((len ((f | (k -' 1)) ^ <*i*>)) + j) is set
D is non empty set

len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
i is Element of D
k is ext-real V24() V25() V26() V30() V31() V32() V33() set
f /. k is Element of D
j is ext-real V24() V25() V26() V30() V31() V32() V33() set

(D,f,j,i) /. k is Element of D
F is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
l is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
dom f is Element of K19(NAT)
D is non empty set

len f is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
i is Element of D

[1,i] is set

k is Element of D

[1,k] is set

j is ext-real V24() V25() V26() V30() V31() V32() V33() set
j -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT

Seg (j -' 1) is V34() V41(j -' 1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= j -' 1 ) } is set

l is ext-real V24() V25() V26() V30() V31() V32() V33() set

(D,(D,f,l,i),j,k) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
l -' j is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(l -' j) -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(f /^ j) | ((l -' j) -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg ((l -' j) -' 1) is V34() V41((l -' j) -' 1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= (l -' j) -' 1 ) } is set
(f /^ j) | (Seg ((l -' j) -' 1)) is Relation-like NAT -defined Seg ((l -' j) -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
((f | (j -' 1)) ^ <*k*>) ^ ((f /^ j) | ((l -' j) -' 1)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((f | (j -' 1)) ^ <*k*>) ^ ((f /^ j) | ((l -' j) -' 1))) ^ <*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D

((((f | (j -' 1)) ^ <*k*>) ^ ((f /^ j) | ((l -' j) -' 1))) ^ <*i*>) ^ (f /^ l) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
l -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT

Seg (l -' 1) is V34() V41(l -' 1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= l -' 1 ) } is set

1 + j is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
len (f | (l -' 1)) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT

len ((f | (l -' 1)) ^ <*i*>) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
len <*i*> is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(len (f | (l -' 1))) + () is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(len (f | (l -' 1))) + 1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
(l -' 1) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
len (D,f,l,i) is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT

(D,f,l,i) | (Seg (j -' 1)) is Relation-like NAT -defined Seg (j -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
((D,f,l,i) | (j -' 1)) ^ <*k*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D

(((D,f,l,i) | (j -' 1)) ^ <*k*>) ^ ((D,f,l,i) /^ j) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((f | (l -' 1)) ^ <*i*>) ^ (f /^ l) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((f | (l -' 1)) ^ <*i*>) ^ (f /^ l)) /^ j is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(((D,f,l,i) | (j -' 1)) ^ <*k*>) ^ ((((f | (l -' 1)) ^ <*i*>) ^ (f /^ l)) /^ j) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D

(((f | (l -' 1)) ^ <*i*>) /^ j) ^ (f /^ l) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(((D,f,l,i) | (j -' 1)) ^ <*k*>) ^ ((((f | (l -' 1)) ^ <*i*>) /^ j) ^ (f /^ l)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D

((f | (l -' 1)) /^ j) ^ <*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((f | (l -' 1)) /^ j) ^ <*i*>) ^ (f /^ l) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((D,f,l,i) | (j -' 1)) ^ <*k*>) ^ ((((f | (l -' 1)) /^ j) ^ <*i*>) ^ (f /^ l)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(l -' 1) -' j is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(f /^ j) | ((l -' 1) -' j) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg ((l -' 1) -' j) is V34() V41((l -' 1) -' j) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= (l -' 1) -' j ) } is set
(f /^ j) | (Seg ((l -' 1) -' j)) is Relation-like NAT -defined Seg ((l -' 1) -' j) -defined NAT -defined D -valued Function-like FinSubsequence-like set
((f /^ j) | ((l -' 1) -' j)) ^ <*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((f /^ j) | ((l -' 1) -' j)) ^ <*i*>) ^ (f /^ l) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((D,f,l,i) | (j -' 1)) ^ <*k*>) ^ ((((f /^ j) | ((l -' 1) -' j)) ^ <*i*>) ^ (f /^ l)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((D,f,l,i) | (j -' 1)) ^ <*k*>) ^ (((f /^ j) | ((l -' 1) -' j)) ^ <*i*>) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((((D,f,l,i) | (j -' 1)) ^ <*k*>) ^ (((f /^ j) | ((l -' 1) -' j)) ^ <*i*>)) ^ (f /^ l) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((D,f,l,i) | (j -' 1)) ^ <*k*>) ^ ((f /^ j) | ((l -' 1) -' j)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((((D,f,l,i) | (j -' 1)) ^ <*k*>) ^ ((f /^ j) | ((l -' 1) -' j))) ^ <*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((((D,f,l,i) | (j -' 1)) ^ <*k*>) ^ ((f /^ j) | ((l -' 1) -' j))) ^ <*i*>) ^ (f /^ l) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((f | (l -' 1)) ^ <*i*>) ^ (f /^ l)) | (j -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(((f | (l -' 1)) ^ <*i*>) ^ (f /^ l)) | (Seg (j -' 1)) is Relation-like NAT -defined Seg (j -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
((((f | (l -' 1)) ^ <*i*>) ^ (f /^ l)) | (j -' 1)) ^ <*k*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((((f | (l -' 1)) ^ <*i*>) ^ (f /^ l)) | (j -' 1)) ^ <*k*>) ^ ((f /^ j) | ((l -' 1) -' j)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((((((f | (l -' 1)) ^ <*i*>) ^ (f /^ l)) | (j -' 1)) ^ <*k*>) ^ ((f /^ j) | ((l -' 1) -' j))) ^ <*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((((((f | (l -' 1)) ^ <*i*>) ^ (f /^ l)) | (j -' 1)) ^ <*k*>) ^ ((f /^ j) | ((l -' 1) -' j))) ^ <*i*>) ^ (f /^ l) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((f | (l -' 1)) ^ <*i*>) | (j -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((f | (l -' 1)) ^ <*i*>) | (Seg (j -' 1)) is Relation-like NAT -defined Seg (j -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
(((f | (l -' 1)) ^ <*i*>) | (j -' 1)) ^ <*k*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((((f | (l -' 1)) ^ <*i*>) | (j -' 1)) ^ <*k*>) ^ ((f /^ j) | ((l -' 1) -' j)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((((f | (l -' 1)) ^ <*i*>) | (j -' 1)) ^ <*k*>) ^ ((f /^ j) | ((l -' 1) -' j))) ^ <*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((((((f | (l -' 1)) ^ <*i*>) | (j -' 1)) ^ <*k*>) ^ ((f /^ j) | ((l -' 1) -' j))) ^ <*i*>) ^ (f /^ l) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(f | (l -' 1)) | (j -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(f | (l -' 1)) | (Seg (j -' 1)) is Relation-like NAT -defined Seg (j -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
((f | (l -' 1)) | (j -' 1)) ^ <*k*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((f | (l -' 1)) | (j -' 1)) ^ <*k*>) ^ ((f /^ j) | ((l -' 1) -' j)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((((f | (l -' 1)) | (j -' 1)) ^ <*k*>) ^ ((f /^ j) | ((l -' 1) -' j))) ^ <*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((((f | (l -' 1)) | (j -' 1)) ^ <*k*>) ^ ((f /^ j) | ((l -' 1) -' j))) ^ <*i*>) ^ (f /^ l) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((f | (j -' 1)) ^ <*k*>) ^ ((f /^ j) | ((l -' 1) -' j)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
(((f | (j -' 1)) ^ <*k*>) ^ ((f /^ j) | ((l -' 1) -' j))) ^ <*i*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
((((f | (j -' 1)) ^ <*k*>) ^ ((f /^ j) | ((l -' 1) -' j))) ^ <*i*>) ^ (f /^ l) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
f is Element of D

[1,f] is set

i is Element of D

[1,i] is set

1 - 1 is ext-real V31() V32() V33() set

len <*f*> is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
1 -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT

Seg (1 -' 1) is V34() V41(1 -' 1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= 1 -' 1 ) } is set

((<*f*> | (1 -' 1)) ^ <*i*>) ^ (<*f*> /^ 1) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D

{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= 0 ) } is set

D is non empty set
f is Element of D
i is Element of D

[1,f] is set

[1,i] is set

1 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
k is Element of D

[1,k] is set

len <*f,i*> is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
dom <*f,i*> is non empty Element of K19(NAT)
1 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT

<*f,i*> /. 2 is Element of D

[1,(<*f,i*> /. 2)] is set
{[1,(<*f,i*> /. 2)]} is Relation-like Function-like non empty set
<*f,i*> . 2 is set

[1,(<*f,i*> . 2)] is set
{[1,(<*f,i*> . 2)]} is Relation-like Function-like non empty set
1 -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT

Seg (1 -' 1) is V34() V41(1 -' 1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= 1 -' 1 ) } is set

((<*f,i*> | (1 -' 1)) ^ <*k*>) ^ (<*f,i*> /^ 1) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D

{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= 0 ) } is set

((<*f,i*> | 0) ^ <*k*>) ^ (<*f,i*> /^ 1) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D

D is non empty set
f is Element of D
i is Element of D

[1,f] is set

[1,i] is set

1 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
k is Element of D

[1,k] is set

2 -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
1 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(1 + 1) -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
len <*f,i*> is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
dom <*f,i*> is non empty Element of K19(NAT)

Seg (2 -' 1) is V34() V41(2 -' 1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= 2 -' 1 ) } is set

((<*f,i*> | (2 -' 1)) ^ <*k*>) ^ (<*f,i*> /^ 2) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D

Seg 1 is non empty V34() V41(1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set

((<*f,i*> | 1) ^ <*k*>) ^ (<*f,i*> /^ (len <*f,i*>)) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D

<*f,i*> /. 1 is Element of D

[1,(<*f,i*> /. 1)] is set
{[1,(<*f,i*> /. 1)]} is Relation-like Function-like non empty set

<*f,i*> . 1 is set

[1,(<*f,i*> . 1)] is set
{[1,(<*f,i*> . 1)]} is Relation-like Function-like non empty set

D is non empty set
f is Element of D
i is Element of D
k is Element of D

[1,f] is set

[1,i] is set

1 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT

[1,k] is set

(1 + 1) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
j is Element of D

[1,j] is set

len <*f,i,k*> is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
1 -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT

Seg (1 -' 1) is V34() V41(1 -' 1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= 1 -' 1 ) } is set

((<*f,i,k*> | (1 -' 1)) ^ <*j*>) ^ (<*f,i,k*> /^ 1) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D

{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= 0 ) } is set

((<*f,i,k*> | 0) ^ <*j*>) ^ (<*f,i,k*> /^ 1) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D

1 + 2 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT

D is non empty set
f is Element of D
i is Element of D
k is Element of D

[1,f] is set

[1,i] is set

1 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT

[1,k] is set

(1 + 1) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
j is Element of D

[1,j] is set

2 -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
1 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(1 + 1) -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
len <*f,i,k*> is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT
2 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
dom <*f,i,k*> is non empty Element of K19(NAT)

Seg (2 -' 1) is V34() V41(2 -' 1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= 2 -' 1 ) } is set

((<*f,i,k*> | (2 -' 1)) ^ <*j*>) ^ (<*f,i,k*> /^ 2) is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D

Seg 1 is non empty V34() V41(1) Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() V33() Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set

<*f,i,k*> /. 3 is Element of D

[1,(<*f,i,k*> /. 3)] is set
{[1,(<*f,i,k*> /. 3)]} is Relation-like Function-like non empty set
((<*f,i,k*> | 1) ^ <*j*>) ^ <*(<*f,i,k*> /. 3)*> is Relation-like NAT -defined D -valued Function-like non empty V34() FinSequence-like FinSubsequence-like FinSequence of D
<*f,i,k*> . 3 is set

[1,(<*f,i,k*> . 3)] is set