:: FINSEQ_5 semantic presentation

REAL is set
NAT is non empty V7() V8() V9() V34() V39() V40() Element of bool REAL
bool REAL is non empty set
NAT is non empty V7() V8() V9() V34() V39() V40() set
bool NAT is non empty V34() set
bool NAT is non empty V34() set
COMPLEX is set
{} is ext-real non positive non negative empty V7() V8() V9() V11() V12() V13() V14() Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V32() V33() V34() V39() V41( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set
the ext-real non positive non negative empty V7() V8() V9() V11() V12() V13() V14() Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V32() V33() V34() V39() V41( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set is ext-real non positive non negative empty V7() V8() V9() V11() V12() V13() V14() Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V32() V33() V34() V39() V41( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set
1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
2 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
3 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
0 is ext-real non positive non negative empty V7() V8() V9() V11() V12() V13() V14() Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V32() V33() V34() V39() V41( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT
Seg 1 is non empty trivial V34() V41(1) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= 1 ) } is set
{1} is non empty trivial V41(1) set
Seg 2 is non empty V34() V41(2) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= 2 ) } is set
{1,2} is non empty set
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
p is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
p - D is ext-real V14() V32() V33() set
(p - D) + 1 is ext-real V14() V32() V33() set
n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
n + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
p is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
Seg p is V34() V41(p) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= p ) } is set
p - D is ext-real V14() V32() V33() set
(p - D) + 1 is ext-real V14() V32() V33() set
n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
n + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
p + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
- 0 is ext-real non positive non negative empty V7() V8() V9() V11() V12() V13() V14() Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V32() V33() V34() V39() V41( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set
- D is ext-real non positive V14() V32() V33() set
0 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
D is Relation-like Function-like set
dom D is set
rng D is set
n is set
{n} is non empty trivial V41(1) set
D " {n} is set
p is set
{p} is non empty trivial V41(1) set
D . p is set
D is Relation-like Function-like set
dom D is set
p is set
D . p is set
{(D . p)} is non empty trivial V41(1) set
D " {(D . p)} is set
{p} is non empty trivial V41(1) set
p is set
D . p is set
{(D . p)} is non empty trivial V41(1) set
D " {(D . p)} is set
{p} is non empty trivial V41(1) set
p is set
D . p is set
{(D . p)} is non empty trivial V41(1) set
D " {(D . p)} is set
{p} is non empty trivial V41(1) set
n is set
d2 is set
D . d2 is set
{(D . d2)} is non empty trivial V41(1) set
D " {(D . d2)} is set
{d2} is non empty trivial V41(1) set
D is Relation-like Function-like set
rng D is set
p is set
{p} is non empty trivial V41(1) set
D " {p} is set
n is set
{n} is non empty trivial V41(1) set
D " {n} is set
d2 is set
{d2} is non empty trivial V41(1) set
D . d2 is set
D is set
<*D*> is non empty trivial Relation-like NAT -defined Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like set
[1,D] is set
{1,D} is non empty set
{{1,D},{1}} is non empty set
{[1,D]} is non empty trivial Relation-like Function-like constant V41(1) set
p is set
<*D,p*> is non empty Relation-like NAT -defined Function-like V34() V41(2) FinSequence-like FinSubsequence-like set
<*p*> is non empty trivial Relation-like NAT -defined Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like set
[1,p] is set
{1,p} is non empty set
{{1,p},{1}} is non empty set
{[1,p]} is non empty trivial Relation-like Function-like constant V41(1) set
<*D*> ^ <*p*> is non empty Relation-like NAT -defined Function-like V34() V41(1 + 1) FinSequence-like FinSubsequence-like set
1 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
len <*D,p*> is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
<*{}*> is non empty trivial Relation-like NAT -defined Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like set
[1,{}] is set
{1,{}} is non empty set
{{1,{}},{1}} is non empty set
{[1,{}]} is non empty trivial Relation-like Function-like constant V41(1) set
D is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
dom D is non empty Element of bool NAT
len D is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
D is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
len D is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
D is set
<*D*> is non empty trivial Relation-like NAT -defined Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like set
[1,D] is set
{1,D} is non empty set
{{1,D},{1}} is non empty set
{[1,D]} is non empty trivial Relation-like Function-like constant V41(1) set
p is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*D*> ^ p is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
len (<*D*> ^ p) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
len p is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
1 + (len p) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
len <*D*> is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(len <*D*>) + (len p) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
rng D is set
p is set
n is set
p .. D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
n .. D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
D . (n .. D) is set
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
D + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
Seg D is V34() V41(D) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
Seg (D + 1) is non empty V34() V41(D + 1) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= D + 1 ) } is set
p is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
dom p is Element of bool NAT
n is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
p | (Seg D) is Relation-like NAT -defined Seg D -defined NAT -defined Function-like FinSubsequence-like set
p | (Seg (D + 1)) is Relation-like NAT -defined Seg (D + 1) -defined NAT -defined Function-like FinSubsequence-like set
p . (D + 1) is set
<*(p . (D + 1))*> is non empty trivial Relation-like NAT -defined Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like set
[1,(p . (D + 1))] is set
{1,(p . (D + 1))} is non empty set
{{1,(p . (D + 1))},{1}} is non empty set
{[1,(p . (D + 1))]} is non empty trivial Relation-like Function-like constant V41(1) set
n ^ <*(p . (D + 1))*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
len p is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
d2 is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
len d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
d2 . (D + 1) is set
d2 | (Seg D) is Relation-like NAT -defined Seg D -defined NAT -defined Function-like FinSubsequence-like set
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
p is Relation-like NAT -defined Function-like one-to-one V34() FinSequence-like FinSubsequence-like set
dom p is Element of bool NAT
p . D is set
(p . D) .. p is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
rng p is set
p <- (p . D) is set
D is non empty set
the Element of D is Element of D
<* the Element of D*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1, the Element of D] is set
{1, the Element of D} is non empty set
{{1, the Element of D},{1}} is non empty set
{[1, the Element of D]} is non empty trivial Relation-like Function-like constant V41(1) set
D is non empty set
p is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
dom p is Element of bool NAT
n is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
dom n is Element of bool NAT
d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
p . d2 is set
p /. d2 is Element of D
n /. d2 is Element of D
n . d2 is set
D is non empty set
p is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len p is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
n is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
p . d2 is set
p /. d2 is Element of D
n /. d2 is Element of D
n . d2 is set
D is non empty set
p is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len p is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
p /. 1 is Element of D
<*(p /. 1)*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1,(p /. 1)] is set
{1,(p /. 1)} is non empty set
{{1,(p /. 1)},{1}} is non empty set
{[1,(p /. 1)]} is non empty trivial Relation-like Function-like constant V41(1) set
dom p is Element of bool NAT
p . 1 is set
D is non empty set
p is Element of D
<*p*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1,p] is set
{1,p} is non empty set
{{1,p},{1}} is non empty set
{[1,p]} is non empty trivial Relation-like Function-like constant V41(1) set
n is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*p*> ^ n is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(<*p*> ^ n) /. 1 is Element of D
len (<*p*> ^ n) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
len n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
1 + (len n) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
dom (<*p*> ^ n) is non empty Element of bool NAT
(<*p*> ^ n) . 1 is set
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
p is non empty set
n is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
dom n is Element of bool NAT
n /. D is Element of p
d2 is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
n ^ d2 is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
(n ^ d2) /. D is Element of p
dom (n ^ d2) is Element of bool NAT
(n ^ d2) . D is set
n . D is set
D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
len D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
p is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
D | p is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
Seg p is V34() V41(p) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= p ) } is set
D | (Seg p) is Relation-like NAT -defined Seg p -defined NAT -defined Function-like FinSubsequence-like set
len (D | p) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
p is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
D | p is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
Seg p is V34() V41(p) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= p ) } is set
D | (Seg p) is Relation-like NAT -defined Seg p -defined NAT -defined Function-like FinSubsequence-like set
len (D | p) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
len D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
dom D is Element of bool NAT
p is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
D | p is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
Seg p is V34() V41(p) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= p ) } is set
D | (Seg p) is Relation-like NAT -defined Seg p -defined NAT -defined Function-like FinSubsequence-like set
dom (D | p) is Element of bool NAT
D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
rng D is set
p is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
D | p is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
Seg p is V34() V41(p) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= p ) } is set
D | (Seg p) is Relation-like NAT -defined Seg p -defined NAT -defined Function-like FinSubsequence-like set
rng (D | p) is set
D is set
p is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
p | 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
p | (Seg 1) is Relation-like NAT -defined Seg 1 -defined NAT -defined D -valued Function-like FinSubsequence-like set
p /. 1 is Element of D
<*(p /. 1)*> is non empty trivial Relation-like NAT -defined Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like set
[1,(p /. 1)] is set
{1,(p /. 1)} is non empty set
{{1,(p /. 1)},{1}} is non empty set
{[1,(p /. 1)]} is non empty trivial Relation-like Function-like constant V41(1) set
dom p is Element of bool NAT
len p is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
len (p | 1) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
dom (p | 1) is Element of bool NAT
(p | 1) /. 1 is Element of D
(p | 1) . 1 is set
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
D + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
p is non empty set
n is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
len n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
n | D is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
Seg D is V34() V41(D) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
n | (Seg D) is Relation-like NAT -defined Seg D -defined NAT -defined p -valued Function-like FinSubsequence-like set
n /. (len n) is Element of p
<*(n /. (len n))*> is non empty trivial Relation-like NAT -defined p -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of p
[1,(n /. (len n))] is set
{1,(n /. (len n))} is non empty set
{{1,(n /. (len n))},{1}} is non empty set
{[1,(n /. (len n))]} is non empty trivial Relation-like Function-like constant V41(1) set
(n | D) ^ <*(n /. (len n))*> is non empty Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
dom n is Element of bool NAT
Seg (D + 1) is non empty V34() V41(D + 1) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= D + 1 ) } is set
n | (Seg (D + 1)) is Relation-like NAT -defined Seg (D + 1) -defined NAT -defined p -valued Function-like FinSubsequence-like Element of bool [:NAT,p:]
[:NAT,p:] is non empty Relation-like V34() set
bool [:NAT,p:] is non empty V34() set
n . (D + 1) is set
<*(n . (D + 1))*> is non empty trivial Relation-like NAT -defined Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like set
[1,(n . (D + 1))] is set
{1,(n . (D + 1))} is non empty set
{{1,(n . (D + 1))},{1}} is non empty set
{[1,(n . (D + 1))]} is non empty trivial Relation-like Function-like constant V41(1) set
(n | D) ^ <*(n . (D + 1))*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
p is non empty set
n is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
n | D is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
Seg D is V34() V41(D) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
n | (Seg D) is Relation-like NAT -defined Seg D -defined NAT -defined p -valued Function-like FinSubsequence-like set
dom (n | D) is Element of bool NAT
dom n is Element of bool NAT
d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(n | D) /. d2 is Element of p
(n | D) /. D is Element of p
n /. d2 is Element of p
n /. D is Element of p
p is non empty set
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
n is Relation-like NAT -defined p -valued Function-like one-to-one V34() FinSequence-like FinSubsequence-like FinSequence of p
n | D is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
Seg D is V34() V41(D) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
n | (Seg D) is Relation-like NAT -defined Seg D -defined NAT -defined p -valued Function-like FinSubsequence-like set
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
p is set
n is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
len n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
d2 is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
n ^ d2 is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
(n ^ d2) | D is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
Seg D is V34() V41(D) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
(n ^ d2) | (Seg D) is Relation-like NAT -defined Seg D -defined NAT -defined p -valued Function-like FinSubsequence-like set
n | D is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
n | (Seg D) is Relation-like NAT -defined Seg D -defined NAT -defined p -valued Function-like FinSubsequence-like set
len (n | D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
dom (n | D) is Element of bool NAT
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
Seg (len n) is V34() V41( len n) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= len n ) } is set
dom n is Element of bool NAT
((n ^ d2) | D) . D is set
(n ^ d2) . D is set
n . D is set
(n | D) . D is set
len d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(len n) + (len d2) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
len (n ^ d2) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
len ((n ^ d2) | D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
D is set
p is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len p is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
n is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
p ^ n is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(p ^ n) | (len p) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg (len p) is V34() V41( len p) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= len p ) } is set
(p ^ n) | (Seg (len p)) is Relation-like NAT -defined Seg (len p) -defined NAT -defined D -valued Function-like FinSubsequence-like set
p | (len p) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
p | (Seg (len p)) is Relation-like NAT -defined Seg (len p) -defined NAT -defined D -valued Function-like FinSubsequence-like set
D is non empty set
p is Element of D
<*p*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1,p] is set
{1,p} is non empty set
{{1,p},{1}} is non empty set
{[1,p]} is non empty trivial Relation-like Function-like constant V41(1) set
n is set
d2 is Relation-like NAT -defined n -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of n
rng d2 is set
d2 -| p is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(d2 -| p) ^ <*p*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
p .. d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
d2 | (p .. d2) is Relation-like NAT -defined n -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of n
Seg (p .. d2) is V34() V41(p .. d2) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= p .. d2 ) } is set
d2 | (Seg (p .. d2)) is Relation-like NAT -defined Seg (p .. d2) -defined NAT -defined n -valued Function-like FinSubsequence-like set
(p .. d2) - 1 is ext-real V14() V32() V33() set
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
Seg D is V34() V41(D) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
d2 | (Seg D) is Relation-like NAT -defined Seg D -defined NAT -defined n -valued Function-like FinSubsequence-like Element of bool [:NAT,n:]
[:NAT,n:] is Relation-like set
bool [:NAT,n:] is non empty set
D + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
dom d2 is Element of bool NAT
d2 . (D + 1) is set
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
p is non empty set
n is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
n /^ D is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
len (n /^ D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
len n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(len n) - D is ext-real V14() V32() V33() set
(len (n /^ D)) + D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
<*> p is ext-real non positive non negative empty proper V7() V8() V9() V11() V12() V13() V14() Relation-like non-empty empty-yielding NAT -defined p -valued Function-like one-to-one constant functional V32() V33() V34() V39() V41( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of p
[:NAT,p:] is non empty Relation-like V34() set
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
p is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
p + D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
n is set
d2 is Relation-like NAT -defined n -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of n
d2 /^ p is Relation-like NAT -defined n -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of n
dom (d2 /^ p) is Element of bool NAT
dom d2 is Element of bool NAT
len d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
len (d2 /^ p) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(len d2) - p is ext-real V14() V32() V33() set
D + p is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
len d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
<*> n is ext-real non positive non negative empty V7() V8() V9() V11() V12() V13() V14() Relation-like non-empty empty-yielding NAT -defined n -valued Function-like one-to-one constant functional V32() V33() V34() V39() V41( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of n
len d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
p is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
p + D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
n is set
d2 is Relation-like NAT -defined n -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of n
d2 /^ p is Relation-like NAT -defined n -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of n
dom (d2 /^ p) is Element of bool NAT
(d2 /^ p) /. D is Element of n
d2 /. (p + D) is Element of n
len d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
dom d2 is Element of bool NAT
(d2 /^ p) . D is set
d2 . (p + D) is set
len d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
<*> n is ext-real non positive non negative empty V7() V8() V9() V11() V12() V13() V14() Relation-like non-empty empty-yielding NAT -defined n -valued Function-like one-to-one constant functional V32() V33() V34() V39() V41( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of n
len d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
D is set
p is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
p /^ 0 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len p is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
len (p /^ 0) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
dom (p /^ 0) is Element of bool NAT
(p /^ 0) . n is set
n + 0 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
p . (n + 0) is set
p . n is set
(len p) - 0 is ext-real non negative V14() V32() V33() set
D is non empty set
p is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
p /. 1 is Element of D
<*(p /. 1)*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1,(p /. 1)] is set
{1,(p /. 1)} is non empty set
{{1,(p /. 1)},{1}} is non empty set
{[1,(p /. 1)]} is non empty trivial Relation-like Function-like constant V41(1) set
p /^ 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*(p /. 1)*> ^ (p /^ 1) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
p | 1 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
p | (Seg 1) is Relation-like NAT -defined Seg 1 -defined NAT -defined D -valued Function-like FinSubsequence-like set
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
D + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
p is non empty set
n is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
len n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
n /^ D is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
n /. (len n) is Element of p
<*(n /. (len n))*> is non empty trivial Relation-like NAT -defined p -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of p
[1,(n /. (len n))] is set
{1,(n /. (len n))} is non empty set
{{1,(n /. (len n))},{1}} is non empty set
{[1,(n /. (len n))]} is non empty trivial Relation-like Function-like constant V41(1) set
len (n /^ D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(len n) - D is ext-real V14() V32() V33() set
dom (n /^ D) is Element of bool NAT
(n /^ D) /. 1 is Element of p
<*((n /^ D) /. 1)*> is non empty trivial Relation-like NAT -defined p -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of p
[1,((n /^ D) /. 1)] is set
{1,((n /^ D) /. 1)} is non empty set
{{1,((n /^ D) /. 1)},{1}} is non empty set
{[1,((n /^ D) /. 1)]} is non empty trivial Relation-like Function-like constant V41(1) set
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
D + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
p is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
n is non empty set
d2 is Relation-like NAT -defined n -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of n
dom d2 is Element of bool NAT
d2 /. p is Element of n
<*(d2 /. p)*> is non empty trivial Relation-like NAT -defined n -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of n
[1,(d2 /. p)] is set
{1,(d2 /. p)} is non empty set
{{1,(d2 /. p)},{1}} is non empty set
{[1,(d2 /. p)]} is non empty trivial Relation-like Function-like constant V41(1) set
d2 /^ p is Relation-like NAT -defined n -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of n
<*(d2 /. p)*> ^ (d2 /^ p) is non empty Relation-like NAT -defined n -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of n
d2 /^ D is Relation-like NAT -defined n -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of n
len d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
len (<*(d2 /. p)*> ^ (d2 /^ p)) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
len (d2 /^ p) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(len (d2 /^ p)) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(len d2) - p is ext-real V14() V32() V33() set
((len d2) - p) + 1 is ext-real V14() V32() V33() set
(len d2) - D is ext-real V14() V32() V33() set
len (d2 /^ D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
dom (d2 /^ D) is Element of bool NAT
(<*(d2 /. p)*> ^ (d2 /^ p)) . f is set
d2 . p is set
(d2 /^ D) . f is set
f - 1 is ext-real V14() V32() V33() set
l is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(len (<*(d2 /. p)*> ^ (d2 /^ p))) - 1 is ext-real V14() V32() V33() set
l + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
dom (d2 /^ p) is Element of bool NAT
len <*(d2 /. p)*> is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(<*(d2 /. p)*> ^ (d2 /^ p)) . f is set
(d2 /^ p) . l is set
l + p is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
d2 . (l + p) is set
f + D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
d2 . (f + D) is set
(d2 /^ D) . f is set
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
p is set
n is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
len n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
n /^ D is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
len (n /^ D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(len n) - (len n) is ext-real V14() V32() V33() set
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
p is non empty set
n is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
n /^ D is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
rng (n /^ D) is set
rng n is set
d2 is set
dom (n /^ D) is Element of bool NAT
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(n /^ D) /. D is Element of p
D + D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
dom n is Element of bool NAT
n /. (D + D) is Element of p
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
p is non empty set
n is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
n /^ D is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
dom (n /^ D) is Element of bool NAT
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(n /^ D) /. d2 is Element of p
(n /^ D) /. D is Element of p
D + d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
dom n is Element of bool NAT
D + D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
n /. (D + d2) is Element of p
n /. (D + D) is Element of p
p is non empty set
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
n is Relation-like NAT -defined p -valued Function-like one-to-one V34() FinSequence-like FinSubsequence-like FinSequence of p
n /^ D is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
p is non empty set
n is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
n | D is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
Seg D is V34() V41(D) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
n | (Seg D) is Relation-like NAT -defined Seg D -defined NAT -defined p -valued Function-like FinSubsequence-like set
rng (n | D) is set
n /^ D is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
rng (n /^ D) is set
dom (n | D) is Element of bool NAT
dom n is Element of bool NAT
d2 is set
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(n | D) /. D is Element of p
dom (n /^ D) is Element of bool NAT
f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(n /^ D) /. f is Element of p
f + D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
len (n | D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
n /. (f + D) is Element of p
n /. D is Element of p
D is non empty set
p is Element of D
n is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng n is set
n |-- p is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
p .. n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
n /^ (p .. n) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len (n |-- p) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
len n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(len n) - (p .. n) is ext-real V14() V32() V33() set
len (n /^ (p .. n)) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
Seg (len (n |-- p)) is V34() V41( len (n |-- p)) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= len (n |-- p) ) } is set
dom (n |-- p) is Element of bool NAT
Seg (len (n /^ (p .. n))) is V34() V41( len (n /^ (p .. n))) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= len (n /^ (p .. n)) ) } is set
dom (n /^ (p .. n)) is Element of bool NAT
d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
(n |-- p) . d2 is set
d2 + (p .. n) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
n . (d2 + (p .. n)) is set
(n /^ (p .. n)) . d2 is set
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
p is non empty set
n is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
len n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(len n) + D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
d2 is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
n ^ d2 is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
(n ^ d2) /^ ((len n) + D) is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
d2 /^ D is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
len (n ^ d2) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
len d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(len n) + (len d2) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
len ((n ^ d2) /^ ((len n) + D)) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(len d2) + (len n) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
((len d2) + (len n)) - ((len n) + D) is ext-real V14() V32() V33() set
(len d2) - D is ext-real V14() V32() V33() set
len (d2 /^ D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
dom (d2 /^ D) is Element of bool NAT
D + D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
dom d2 is Element of bool NAT
dom ((n ^ d2) /^ ((len n) + D)) is Element of bool NAT
((n ^ d2) /^ ((len n) + D)) /. D is Element of p
((len n) + D) + D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(n ^ d2) /. (((len n) + D) + D) is Element of p
(len n) + (D + D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(n ^ d2) /. ((len n) + (D + D)) is Element of p
d2 /. (D + D) is Element of p
(d2 /^ D) /. D is Element of p
<*> p is ext-real non positive non negative empty proper V7() V8() V9() V11() V12() V13() V14() Relation-like non-empty empty-yielding NAT -defined p -valued Function-like one-to-one constant functional V32() V33() V34() V39() V41( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of p
[:NAT,p:] is non empty Relation-like V34() set
D is non empty set
p is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len p is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
n is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
p ^ n is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(p ^ n) /^ (len p) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(len p) + 0 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(p ^ n) /^ ((len p) + 0) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
n /^ 0 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
p is Element of D
n is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng n is set
p .. n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
n /. (p .. n) is Element of D
dom n is Element of bool NAT
n . (p .. n) is set
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
p is non empty set
n is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
dom n is Element of bool NAT
n /. D is Element of p
(n /. D) .. n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
{(n /. D)} is non empty trivial V41(1) set
n " {(n /. D)} is set
Sgm (n " {(n /. D)}) is Relation-like NAT -defined NAT -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of NAT
(Sgm (n " {(n /. D)})) . 1 is set
len n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
Seg (len n) is V34() V41( len n) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= len n ) } is set
n . D is set
rng (Sgm (n " {(n /. D)})) is set
dom (Sgm (n " {(n /. D)})) is Element of bool NAT
D is set
(Sgm (n " {(n /. D)})) . D is set
f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
len (Sgm (n " {(n /. D)})) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
p is non empty set
n is Element of p
d2 is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
d2 | D is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
Seg D is V34() V41(D) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
d2 | (Seg D) is Relation-like NAT -defined Seg D -defined NAT -defined p -valued Function-like FinSubsequence-like set
rng (d2 | D) is set
n .. (d2 | D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
n .. d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
dom (d2 | D) is Element of bool NAT
dom d2 is Element of bool NAT
d2 /. (n .. (d2 | D)) is Element of p
(d2 | D) /. (n .. (d2 | D)) is Element of p
len (d2 | D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
rng d2 is set
(d2 | D) /. (n .. d2) is Element of p
d2 /. (n .. d2) is Element of p
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
p is non empty set
n is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
dom n is Element of bool NAT
n /. D is Element of p
(n /. D) .. n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
n . D is set
(n . D) .. n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
D is non empty set
p is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
n is set
n .. p is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
p | (n .. p) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg (n .. p) is V34() V41(n .. p) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= n .. p ) } is set
p | (Seg (n .. p)) is Relation-like NAT -defined Seg (n .. p) -defined NAT -defined D -valued Function-like FinSubsequence-like set
D is non empty set
p is Element of D
n is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng n is set
(D,n,p) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
p .. n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
n | (p .. n) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg (p .. n) is V34() V41(p .. n) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= p .. n ) } is set
n | (Seg (p .. n)) is Relation-like NAT -defined Seg (p .. n) -defined NAT -defined D -valued Function-like FinSubsequence-like set
len (D,n,p) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
dom n is Element of bool NAT
len n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
p is non empty set
n is Element of p
d2 is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
rng d2 is set
n .. d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
Seg (n .. d2) is V34() V41(n .. d2) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= n .. d2 ) } is set
(p,d2,n) is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
d2 | (n .. d2) is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
d2 | (Seg (n .. d2)) is Relation-like NAT -defined Seg (n .. d2) -defined NAT -defined p -valued Function-like FinSubsequence-like set
(p,d2,n) /. D is Element of p
d2 /. D is Element of p
dom d2 is Element of bool NAT
D is non empty set
p is Element of D
n is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng n is set
(D,n,p) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
p .. n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
n | (p .. n) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg (p .. n) is V34() V41(p .. n) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= p .. n ) } is set
n | (Seg (p .. n)) is Relation-like NAT -defined Seg (p .. n) -defined NAT -defined D -valued Function-like FinSubsequence-like set
(D,n,p) /. 1 is Element of D
n /. 1 is Element of D
D is non empty set
p is Element of D
n is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng n is set
(D,n,p) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
p .. n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
n | (p .. n) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg (p .. n) is V34() V41(p .. n) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= p .. n ) } is set
n | (Seg (p .. n)) is Relation-like NAT -defined Seg (p .. n) -defined NAT -defined D -valued Function-like FinSubsequence-like set
(D,n,p) /. (p .. n) is Element of D
dom n is Element of bool NAT
n /. (p .. n) is Element of D
n . (p .. n) is set
D is non empty set
p is Element of D
n is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng n is set
p .. n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(D,n,p) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
n | (p .. n) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg (p .. n) is V34() V41(p .. n) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= p .. n ) } is set
n | (Seg (p .. n)) is Relation-like NAT -defined Seg (p .. n) -defined NAT -defined D -valued Function-like FinSubsequence-like set
rng (D,n,p) is set
d2 is set
d2 .. n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
len (D,n,p) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
Seg (len (D,n,p)) is V34() V41( len (D,n,p)) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= len (D,n,p) ) } is set
dom (D,n,p) is Element of bool NAT
(D,n,p) . (d2 .. n) is set
(D,n,p) /. (d2 .. n) is Element of D
n /. (d2 .. n) is Element of D
dom n is Element of bool NAT
n . (d2 .. n) is set
D is non empty set
p is Element of D
n is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng n is set
(D,n,p) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
p .. n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
n | (p .. n) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg (p .. n) is V34() V41(p .. n) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= p .. n ) } is set
n | (Seg (p .. n)) is Relation-like NAT -defined Seg (p .. n) -defined NAT -defined D -valued Function-like FinSubsequence-like set
len (D,n,p) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
D is non empty set
n is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
p is Element of D
(D,n,p) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
p .. n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
n | (p .. n) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg (p .. n) is V34() V41(p .. n) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= p .. n ) } is set
n | (Seg (p .. n)) is Relation-like NAT -defined Seg (p .. n) -defined NAT -defined D -valued Function-like FinSubsequence-like set
rng (D,n,p) is set
rng n is set
D is non empty set
n is Relation-like NAT -defined D -valued Function-like one-to-one V34() FinSequence-like FinSubsequence-like FinSequence of D
p is Element of D
(D,n,p) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
p .. n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
n | (p .. n) is Relation-like NAT -defined D -valued Function-like one-to-one V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg (p .. n) is V34() V41(p .. n) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= p .. n ) } is set
n | (Seg (p .. n)) is Relation-like NAT -defined Seg (p .. n) -defined NAT -defined D -valued Function-like FinSubsequence-like set
D is non empty set
n is Element of D
<*n*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1,n] is set
{1,n} is non empty set
{{1,n},{1}} is non empty set
{[1,n]} is non empty trivial Relation-like Function-like constant V41(1) set
p is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
n .. p is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
p /^ (n .. p) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*n*> ^ (p /^ (n .. p)) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
p is Element of D
n is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng n is set
p .. n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(D,n,p) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*p*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1,p] is set
{1,p} is non empty set
{{1,p},{1}} is non empty set
{[1,p]} is non empty trivial Relation-like Function-like constant V41(1) set
n /^ (p .. n) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*p*> ^ (n /^ (p .. n)) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(p .. n) - 1 is ext-real V14() V32() V33() set
dom n is Element of bool NAT
d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
d2 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
n /^ d2 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
n /. (p .. n) is Element of D
<*(n /. (p .. n))*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1,(n /. (p .. n))] is set
{1,(n /. (p .. n))} is non empty set
{{1,(n /. (p .. n))},{1}} is non empty set
{[1,(n /. (p .. n))]} is non empty trivial Relation-like Function-like constant V41(1) set
<*(n /. (p .. n))*> ^ (n /^ (p .. n)) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
p is Element of D
n is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng n is set
(D,n,p) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*p*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1,p] is set
{1,p} is non empty set
{{1,p},{1}} is non empty set
{[1,p]} is non empty trivial Relation-like Function-like constant V41(1) set
p .. n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
n /^ (p .. n) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*p*> ^ (n /^ (p .. n)) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len (D,n,p) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
len n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(len n) - (p .. n) is ext-real V14() V32() V33() set
((len n) - (p .. n)) + 1 is ext-real V14() V32() V33() set
d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
d2 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
n /^ d2 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(len n) - d2 is ext-real V14() V32() V33() set
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
D + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
p is non empty set
n is Element of p
d2 is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
rng d2 is set
(p,d2,n) is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
<*n*> is non empty trivial Relation-like NAT -defined p -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of p
[1,n] is set
{1,n} is non empty set
{{1,n},{1}} is non empty set
{[1,n]} is non empty trivial Relation-like Function-like constant V41(1) set
n .. d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
d2 /^ (n .. d2) is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
<*n*> ^ (d2 /^ (n .. d2)) is non empty Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
dom (p,d2,n) is Element of bool NAT
D + (n .. d2) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
dom d2 is Element of bool NAT
len (p,d2,n) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
len d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(len d2) - (n .. d2) is ext-real V14() V32() V33() set
((len d2) - (n .. d2)) + 1 is ext-real V14() V32() V33() set
D is non empty set
n is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
p is Element of D
(D,n,p) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*p*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1,p] is set
{1,p} is non empty set
{{1,p},{1}} is non empty set
{[1,p]} is non empty trivial Relation-like Function-like constant V41(1) set
p .. n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
n /^ (p .. n) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*p*> ^ (n /^ (p .. n)) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
D + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
p is non empty set
n is Element of p
d2 is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
rng d2 is set
(p,d2,n) is non empty Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
<*n*> is non empty trivial Relation-like NAT -defined p -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of p
[1,n] is set
{1,n} is non empty set
{{1,n},{1}} is non empty set
{[1,n]} is non empty trivial Relation-like Function-like constant V41(1) set
n .. d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
d2 /^ (n .. d2) is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
<*n*> ^ (d2 /^ (n .. d2)) is non empty Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
dom (p,d2,n) is non empty Element of bool NAT
(p,d2,n) /. (D + 1) is Element of p
D + (n .. d2) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
d2 /. (D + (n .. d2)) is Element of p
dom d2 is Element of bool NAT
len d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
f + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
d2 /^ f is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
(p,d2,n) . (D + 1) is set
(D + 1) + f is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
d2 . ((D + 1) + f) is set
D is non empty set
n is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
p is Element of D
(D,n,p) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*p*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1,p] is set
{1,p} is non empty set
{{1,p},{1}} is non empty set
{[1,p]} is non empty trivial Relation-like Function-like constant V41(1) set
p .. n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
n /^ (p .. n) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*p*> ^ (n /^ (p .. n)) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,n,p) /. 1 is Element of D
D is non empty set
p is Element of D
n is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng n is set
(D,n,p) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*p*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1,p] is set
{1,p} is non empty set
{{1,p},{1}} is non empty set
{[1,p]} is non empty trivial Relation-like Function-like constant V41(1) set
p .. n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
n /^ (p .. n) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*p*> ^ (n /^ (p .. n)) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len (D,n,p) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(D,n,p) /. (len (D,n,p)) is Element of D
len n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
n /. (len n) is Element of D
dom (D,n,p) is non empty Element of bool NAT
(len n) - (p .. n) is ext-real V14() V32() V33() set
d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
d2 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
d2 + (p .. n) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
n /. (d2 + (p .. n)) is Element of D
D is non empty set
p is Element of D
n is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng n is set
(D,n,p) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*p*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1,p] is set
{1,p} is non empty set
{{1,p},{1}} is non empty set
{[1,p]} is non empty trivial Relation-like Function-like constant V41(1) set
p .. n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
n /^ (p .. n) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*p*> ^ (n /^ (p .. n)) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng (D,n,p) is non empty set
d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
d2 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
n /^ d2 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
p is Element of D
n is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
rng n is set
(D,n,p) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*p*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1,p] is set
{1,p} is non empty set
{{1,p},{1}} is non empty set
{[1,p]} is non empty trivial Relation-like Function-like constant V41(1) set
p .. n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
n /^ (p .. n) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*p*> ^ (n /^ (p .. n)) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
d2 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
n /^ d2 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
len D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
p is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
len p is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
dom p is Element of bool NAT
dom D is Element of bool NAT
Seg (len D) is V34() V41( len D) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= len D ) } is set
p is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
len p is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
dom p is Element of bool NAT
n is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
len n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
dom n is Element of bool NAT
Seg (len p) is V34() V41( len p) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= len p ) } is set
Seg (len n) is V34() V41( len n) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= len n ) } is set
d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
p . d2 is set
(len D) - d2 is ext-real V14() V32() V33() set
((len D) - d2) + 1 is ext-real V14() V32() V33() set
D . (((len D) - d2) + 1) is set
n . d2 is set
p is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
len p is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
n is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
len n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
dom p is Element of bool NAT
dom n is Element of bool NAT
d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
n . d2 is set
(len p) - d2 is ext-real V14() V32() V33() set
((len p) - d2) + 1 is ext-real V14() V32() V33() set
p . (((len p) - d2) + 1) is set
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
D + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
D + d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(len n) - (D + 1) is ext-real V14() V32() V33() set
((len n) - (D + 1)) + 1 is ext-real V14() V32() V33() set
n . (((len n) - (D + 1)) + 1) is set
p . (D + 1) is set
D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
dom D is Element of bool NAT
(D) is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
dom (D) is Element of bool NAT
rng D is set
rng (D) is set
len D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
Seg (len D) is V34() V41( len D) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= len D ) } is set
len (D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
Seg (len (D)) is V34() V41( len (D)) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= len (D) ) } is set
p is set
n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
D . n is set
(len D) - n is ext-real V14() V32() V33() set
((len D) - n) + 1 is ext-real V14() V32() V33() set
d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(D) . d2 is set
(len D) - d2 is ext-real V14() V32() V33() set
((len D) - d2) + 1 is ext-real V14() V32() V33() set
D . (((len D) - d2) + 1) is set
p is set
n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
(D) . n is set
(len D) - n is ext-real V14() V32() V33() set
((len D) - n) + 1 is ext-real V14() V32() V33() set
d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
D . (((len D) - n) + 1) is set
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
p is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
dom p is Element of bool NAT
(p) is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(p) . D is set
len p is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(len p) - D is ext-real V14() V32() V33() set
((len p) - D) + 1 is ext-real V14() V32() V33() set
p . (((len p) - D) + 1) is set
dom (p) is Element of bool NAT
D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
dom D is Element of bool NAT
len D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(len D) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(D) is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
dom (D) is Element of bool NAT
p is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
p + n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
Seg (len D) is V34() V41( len D) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= len D ) } is set
(len D) - p is ext-real V14() V32() V33() set
((len D) - p) + 1 is ext-real V14() V32() V33() set
D is ext-real non positive non negative empty V7() V8() V9() V11() V12() V13() V14() Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V32() V33() V34() V39() V41( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set
(D) is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
len {} is ext-real non positive non negative empty V7() V8() V9() V11() V12() V13() V14() Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V32() V33() V34() V39() V41( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT
({}) is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
len ({}) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
D is set
<*D*> is non empty trivial Relation-like NAT -defined Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like set
[1,D] is set
{1,D} is non empty set
{{1,D},{1}} is non empty set
{[1,D]} is non empty trivial Relation-like Function-like constant V41(1) set
(<*D*>) is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
len <*D*> is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
dom <*D*> is non empty trivial V41(1) Element of bool NAT
Seg (len <*D*>) is non empty V34() V41( len <*D*>) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= len <*D*> ) } is set
<*D*> . n is set
(len <*D*>) - n is ext-real V14() V32() V33() set
((len <*D*>) - n) + 1 is ext-real V14() V32() V33() set
<*D*> . (((len <*D*>) - n) + 1) is set
D is set
p is set
<*D,p*> is non empty non trivial Relation-like NAT -defined Function-like V34() V41(2) FinSequence-like FinSubsequence-like set
<*D*> is non empty trivial Relation-like NAT -defined Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like set
[1,D] is set
{1,D} is non empty set
{{1,D},{1}} is non empty set
{[1,D]} is non empty trivial Relation-like Function-like constant V41(1) set
<*p*> is non empty trivial Relation-like NAT -defined Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like set
[1,p] is set
{1,p} is non empty set
{{1,p},{1}} is non empty set
{[1,p]} is non empty trivial Relation-like Function-like constant V41(1) set
<*D*> ^ <*p*> is non empty Relation-like NAT -defined Function-like V34() V41(1 + 1) FinSequence-like FinSubsequence-like set
(<*D,p*>) is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*p,D*> is non empty non trivial Relation-like NAT -defined Function-like V34() V41(2) FinSequence-like FinSubsequence-like set
<*p*> ^ <*D*> is non empty Relation-like NAT -defined Function-like V34() V41(1 + 1) FinSequence-like FinSubsequence-like set
len <*D,p*> is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
len <*p,D*> is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
dom <*p,D*> is non empty non trivial V41(2) Element of bool NAT
Seg (len <*D,p*>) is non empty V34() V41( len <*D,p*>) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= len <*D,p*> ) } is set
<*p,D*> . D is set
(len <*D,p*>) - D is ext-real V14() V32() V33() set
((len <*D,p*>) - D) + 1 is ext-real V14() V32() V33() set
<*D,p*> . (((len <*D,p*>) - D) + 1) is set
<*p,D*> . D is set
(len <*D,p*>) - D is ext-real V14() V32() V33() set
((len <*D,p*>) - D) + 1 is ext-real V14() V32() V33() set
<*D,p*> . (((len <*D,p*>) - D) + 1) is set
D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D . 1 is set
(D) is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
len D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(D) . (len D) is set
D . (len D) is set
(D) . 1 is set
dom (D) is Element of bool NAT
Seg (len D) is V34() V41( len D) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= len D ) } is set
dom D is Element of bool NAT
(len D) - (len D) is ext-real V14() V32() V33() set
((len D) - (len D)) + 1 is ext-real V14() V32() V33() set
D . (((len D) - (len D)) + 1) is set
(len D) - 1 is ext-real V14() V32() V33() set
((len D) - 1) + 1 is ext-real V14() V32() V33() set
D . (((len D) - 1) + 1) is set
D is Relation-like NAT -defined Function-like one-to-one V34() FinSequence-like FinSubsequence-like set
(D) is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
n is set
dom (D) is set
d2 is set
(D) . n is set
(D) . d2 is set
dom (D) is Element of bool NAT
len (D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
len D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(len D) - D is ext-real V14() V32() V33() set
((len D) - D) + 1 is ext-real V14() V32() V33() set
(len D) - f is ext-real V14() V32() V33() set
((len D) - f) + 1 is ext-real V14() V32() V33() set
l is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
D . l is set
k is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
D . k is set
Seg (len (D)) is V34() V41( len (D)) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= len (D) ) } is set
dom D is Element of bool NAT
Seg (len D) is V34() V41( len D) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= len D ) } is set
D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(D) is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
p is set
<*p*> is non empty trivial Relation-like NAT -defined Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like set
[1,p] is set
{1,p} is non empty set
{{1,p},{1}} is non empty set
{[1,p]} is non empty trivial Relation-like Function-like constant V41(1) set
D ^ <*p*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
((D ^ <*p*>)) is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*p*> ^ (D) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
len D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(len D) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
len (<*p*> ^ (D)) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
len <*p*> is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
len (D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(len <*p*>) + (len (D)) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
1 + (len (D)) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
len (D ^ <*p*>) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
len ((D ^ <*p*>)) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
dom ((D ^ <*p*>)) is Element of bool NAT
Seg (len <*p*>) is non empty V34() V41( len <*p*>) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= len <*p*> ) } is set
dom <*p*> is non empty trivial V41(1) Element of bool NAT
((D ^ <*p*>)) . D is set
((len D) + 1) - 1 is ext-real V14() V32() V33() set
(((len D) + 1) - 1) + 1 is ext-real V14() V32() V33() set
(D ^ <*p*>) . ((((len D) + 1) - 1) + 1) is set
<*p*> . 1 is set
(<*p*> ^ (D)) . D is set
D - 1 is ext-real V14() V32() V33() set
l is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
l + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
((len D) + 1) - D is ext-real V14() V32() V33() set
(((len D) + 1) - D) + 1 is ext-real V14() V32() V33() set
(len D) + D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
((len D) + D) - D is ext-real V14() V32() V33() set
k is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
D - D is ext-real V14() V32() V33() set
0 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
dom D is Element of bool NAT
f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
((len D) + 1) - 1 is ext-real V14() V32() V33() set
((D ^ <*p*>)) . D is set
(D ^ <*p*>) . ((((len D) + 1) - D) + 1) is set
(len D) - f is ext-real V14() V32() V33() set
((len D) - f) + 1 is ext-real V14() V32() V33() set
D . (((len D) - f) + 1) is set
(D) . f is set
(<*p*> ^ (D)) . D is set
D is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(D) is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D ^ {} is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
((D ^ {})) is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
({}) is ext-real non positive non negative empty V7() V8() V9() V11() V12() V13() V14() Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V32() V33() V34() V39() V41( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set
({}) ^ (D) is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
p is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D ^ p is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
((D ^ p)) is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(p) is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(p) ^ (D) is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
n is set
<*n*> is non empty trivial Relation-like NAT -defined Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like set
[1,n] is set
{1,n} is non empty set
{{1,n},{1}} is non empty set
{[1,n]} is non empty trivial Relation-like Function-like constant V41(1) set
p ^ <*n*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D ^ (p ^ <*n*>) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
((D ^ (p ^ <*n*>))) is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
((p ^ <*n*>)) is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
((p ^ <*n*>)) ^ (D) is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(D ^ p) ^ <*n*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(((D ^ p) ^ <*n*>)) is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*n*> ^ ((p) ^ (D)) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
<*n*> ^ (p) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(<*n*> ^ (p)) ^ (D) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D is set
p is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(p) is Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
len p is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
dom p is Element of bool NAT
Seg (len p) is V34() V41( len p) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= len p ) } is set
d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
(len p) - d2 is ext-real V14() V32() V33() set
((len p) - d2) + 1 is ext-real V14() V32() V33() set
dom (p) is Element of bool NAT
len (p) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
Seg (len (p)) is V34() V41( len (p)) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= len (p) ) } is set
p . (((len p) - d2) + 1) is set
(p) . d2 is set
D is non empty set
p is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
p /. 1 is Element of D
(D,p) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len p is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(D,p) /. (len p) is Element of D
p /. (len p) is Element of D
(D,p) /. 1 is Element of D
dom p is Element of bool NAT
dom (D,p) is Element of bool NAT
p . 1 is set
(D,p) . (len p) is set
p . (len p) is set
(D,p) . 1 is set
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
p is non empty set
n is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
dom n is Element of bool NAT
len n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(len n) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(p,n) is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
(p,n) /. D is Element of p
d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
d2 + D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
n /. d2 is Element of p
dom (p,n) is Element of bool NAT
(len n) - D is ext-real V14() V32() V33() set
((len n) - D) + 1 is ext-real V14() V32() V33() set
n . d2 is set
(p,n) . D is set
D is non empty set
d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
p is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
p | d2 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg d2 is V34() V41(d2) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= d2 ) } is set
p | (Seg d2) is Relation-like NAT -defined Seg d2 -defined NAT -defined D -valued Function-like FinSubsequence-like set
n is Element of D
<*n*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1,n] is set
{1,n} is non empty set
{{1,n},{1}} is non empty set
{[1,n]} is non empty trivial Relation-like Function-like constant V41(1) set
(p | d2) ^ <*n*> is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
p /^ d2 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((p | d2) ^ <*n*>) ^ (p /^ d2) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
D is non empty set
p is Element of D
<*p*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1,p] is set
{1,p} is non empty set
{{1,p},{1}} is non empty set
{[1,p]} is non empty trivial Relation-like Function-like constant V41(1) set
n is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(D,n,p,0) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
n | 0 is ext-real non positive non negative empty proper V7() V8() V9() V11() V12() V13() V14() Relation-like non-empty empty-yielding NAT -defined D -valued Function-like one-to-one constant functional V32() V33() V34() V39() V41( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D
[:NAT,D:] is non empty Relation-like V34() set
Seg 0 is ext-real non positive non negative empty proper V7() V8() V9() V11() V12() V13() V14() Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V32() V33() V34() V39() V41( 0 ) V41( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= 0 ) } is set
n | (Seg 0) is ext-real non positive non negative empty V7() V8() V9() V11() V12() V13() V14() Relation-like non-empty empty-yielding NAT -defined Seg 0 -defined NAT -defined D -valued Function-like one-to-one constant functional V32() V33() V34() V39() V41( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set
(n | 0) ^ <*p*> is non empty Relation-like NAT -defined D -valued Function-like V34() V41({} + 1) FinSequence-like FinSubsequence-like FinSequence of D
{} + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
n /^ 0 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((n | 0) ^ <*p*>) ^ (n /^ 0) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*p*> ^ n is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
<*p*> ^ (n /^ 0) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
p is non empty set
n is Element of p
<*n*> is non empty trivial Relation-like NAT -defined p -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of p
[1,n] is set
{1,n} is non empty set
{{1,n},{1}} is non empty set
{[1,n]} is non empty trivial Relation-like Function-like constant V41(1) set
d2 is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
len d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(p,d2,n,D) is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
d2 | D is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
Seg D is V34() V41(D) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
d2 | (Seg D) is Relation-like NAT -defined Seg D -defined NAT -defined p -valued Function-like FinSubsequence-like set
(d2 | D) ^ <*n*> is non empty Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
d2 /^ D is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
((d2 | D) ^ <*n*>) ^ (d2 /^ D) is non empty Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
d2 ^ <*n*> is non empty Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
p is non empty set
n is Element of p
d2 is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
(p,d2,n,D) is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
d2 | D is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
Seg D is V34() V41(D) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
d2 | (Seg D) is Relation-like NAT -defined Seg D -defined NAT -defined p -valued Function-like FinSubsequence-like set
<*n*> is non empty trivial Relation-like NAT -defined p -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of p
[1,n] is set
{1,n} is non empty set
{{1,n},{1}} is non empty set
{[1,n]} is non empty trivial Relation-like Function-like constant V41(1) set
(d2 | D) ^ <*n*> is non empty Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
d2 /^ D is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
((d2 | D) ^ <*n*>) ^ (d2 /^ D) is non empty Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
len (p,d2,n,D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
len d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(len d2) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
len ((d2 | D) ^ <*n*>) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
len (d2 /^ D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(len ((d2 | D) ^ <*n*>)) + (len (d2 /^ D)) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(len d2) - D is ext-real V14() V32() V33() set
(len ((d2 | D) ^ <*n*>)) + ((len d2) - D) is ext-real V14() V32() V33() set
len (d2 | D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
len <*n*> is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(len (d2 | D)) + (len <*n*>) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
((len (d2 | D)) + (len <*n*>)) + ((len d2) - D) is ext-real V14() V32() V33() set
(len (d2 | D)) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
((len (d2 | D)) + 1) + ((len d2) - D) is ext-real V14() V32() V33() set
D + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(D + 1) + ((len d2) - D) is ext-real V14() V32() V33() set
d2 ^ <*n*> is non empty Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
p is non empty set
n is Element of p
{n} is non empty trivial V41(1) set
d2 is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
(p,d2,n,D) is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
d2 | D is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
Seg D is V34() V41(D) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
d2 | (Seg D) is Relation-like NAT -defined Seg D -defined NAT -defined p -valued Function-like FinSubsequence-like set
<*n*> is non empty trivial Relation-like NAT -defined p -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of p
[1,n] is set
{1,n} is non empty set
{{1,n},{1}} is non empty set
{[1,n]} is non empty trivial Relation-like Function-like constant V41(1) set
(d2 | D) ^ <*n*> is non empty Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
d2 /^ D is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
((d2 | D) ^ <*n*>) ^ (d2 /^ D) is non empty Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
rng (p,d2,n,D) is set
rng d2 is set
{n} \/ (rng d2) is non empty set
rng ((d2 | D) ^ <*n*>) is non empty set
rng (d2 /^ D) is set
(rng ((d2 | D) ^ <*n*>)) \/ (rng (d2 /^ D)) is non empty set
rng (d2 | D) is set
rng <*n*> is non empty trivial V41(1) set
(rng (d2 | D)) \/ (rng <*n*>) is non empty set
((rng (d2 | D)) \/ (rng <*n*>)) \/ (rng (d2 /^ D)) is non empty set
(rng (d2 | D)) \/ (rng (d2 /^ D)) is set
((rng (d2 | D)) \/ (rng (d2 /^ D))) \/ (rng <*n*>) is non empty set
(d2 | D) ^ (d2 /^ D) is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
rng ((d2 | D) ^ (d2 /^ D)) is set
(rng ((d2 | D) ^ (d2 /^ D))) \/ (rng <*n*>) is non empty set
(rng <*n*>) \/ (rng d2) is non empty set
D is non empty set
p is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
d2 is Element of D
n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
(D,p,d2,n) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
p | n is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg n is V34() V41(n) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
p | (Seg n) is Relation-like NAT -defined Seg n -defined NAT -defined D -valued Function-like FinSubsequence-like set
<*d2*> is non empty trivial Relation-like NAT -defined D -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of D
[1,d2] is set
{1,d2} is non empty set
{{1,d2},{1}} is non empty set
{[1,d2]} is non empty trivial Relation-like Function-like constant V41(1) set
(p | n) ^ <*d2*> is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
p /^ n is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((p | n) ^ <*d2*>) ^ (p /^ n) is non empty Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
p is non empty set
n is Element of p
d2 is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
(p,d2,n,D) is non empty Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
d2 | D is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
Seg D is V34() V41(D) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
d2 | (Seg D) is Relation-like NAT -defined Seg D -defined NAT -defined p -valued Function-like FinSubsequence-like set
<*n*> is non empty trivial Relation-like NAT -defined p -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of p
[1,n] is set
{1,n} is non empty set
{{1,n},{1}} is non empty set
{[1,n]} is non empty trivial Relation-like Function-like constant V41(1) set
(d2 | D) ^ <*n*> is non empty Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
d2 /^ D is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
((d2 | D) ^ <*n*>) ^ (d2 /^ D) is non empty Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
rng (p,d2,n,D) is non empty set
{n} is non empty trivial V41(1) set
rng d2 is set
{n} \/ (rng d2) is non empty set
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
p is non empty set
n is Element of p
d2 is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
d2 | D is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
Seg D is V34() V41(D) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
d2 | (Seg D) is Relation-like NAT -defined Seg D -defined NAT -defined p -valued Function-like FinSubsequence-like set
dom (d2 | D) is Element of bool NAT
(p,d2,n,D) is non empty Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
<*n*> is non empty trivial Relation-like NAT -defined p -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of p
[1,n] is set
{1,n} is non empty set
{{1,n},{1}} is non empty set
{[1,n]} is non empty trivial Relation-like Function-like constant V41(1) set
(d2 | D) ^ <*n*> is non empty Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
d2 /^ D is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
((d2 | D) ^ <*n*>) ^ (d2 /^ D) is non empty Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
(p,d2,n,D) /. D is Element of p
d2 /. D is Element of p
<*n*> ^ (d2 /^ D) is non empty Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
(d2 | D) ^ (<*n*> ^ (d2 /^ D)) is non empty Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
((d2 | D) ^ (<*n*> ^ (d2 /^ D))) /. D is Element of p
(d2 | D) /. D is Element of p
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
D + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
p is non empty set
n is Element of p
d2 is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
len d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(p,d2,n,D) is non empty Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
d2 | D is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
Seg D is V34() V41(D) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
d2 | (Seg D) is Relation-like NAT -defined Seg D -defined NAT -defined p -valued Function-like FinSubsequence-like set
<*n*> is non empty trivial Relation-like NAT -defined p -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of p
[1,n] is set
{1,n} is non empty set
{{1,n},{1}} is non empty set
{[1,n]} is non empty trivial Relation-like Function-like constant V41(1) set
(d2 | D) ^ <*n*> is non empty Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
d2 /^ D is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
((d2 | D) ^ <*n*>) ^ (d2 /^ D) is non empty Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
(p,d2,n,D) /. (D + 1) is Element of p
len (d2 | D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
len ((d2 | D) ^ <*n*>) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
dom ((d2 | D) ^ <*n*>) is non empty Element of bool NAT
((d2 | D) ^ <*n*>) /. (D + 1) is Element of p
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
D + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
p is non empty set
n is Element of p
d2 is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
len d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(p,d2,n,D) is non empty Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
d2 | D is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
Seg D is V34() V41(D) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
d2 | (Seg D) is Relation-like NAT -defined Seg D -defined NAT -defined p -valued Function-like FinSubsequence-like set
<*n*> is non empty trivial Relation-like NAT -defined p -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of p
[1,n] is set
{1,n} is non empty set
{{1,n},{1}} is non empty set
{[1,n]} is non empty trivial Relation-like Function-like constant V41(1) set
(d2 | D) ^ <*n*> is non empty Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
d2 /^ D is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
((d2 | D) ^ <*n*>) ^ (d2 /^ D) is non empty Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
D + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(p,d2,n,D) /. (D + 1) is Element of p
d2 /. D is Element of p
D - (D + 1) is ext-real V14() V32() V33() set
f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
f + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
D + (f + 1) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(len d2) - D is ext-real V14() V32() V33() set
len (d2 | D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
len ((d2 | D) ^ <*n*>) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
len (d2 /^ D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
dom (d2 /^ D) is Element of bool NAT
(D + 1) + (f + 1) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(d2 /^ D) /. (f + 1) is Element of p
d2 /. (D + (f + 1)) is Element of p
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
p is non empty set
n is Element of p
d2 is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
(p,d2,n,D) is non empty Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
d2 | D is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
Seg D is V34() V41(D) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
d2 | (Seg D) is Relation-like NAT -defined Seg D -defined NAT -defined p -valued Function-like FinSubsequence-like set
<*n*> is non empty trivial Relation-like NAT -defined p -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of p
[1,n] is set
{1,n} is non empty set
{{1,n},{1}} is non empty set
{[1,n]} is non empty trivial Relation-like Function-like constant V41(1) set
(d2 | D) ^ <*n*> is non empty Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
d2 /^ D is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
((d2 | D) ^ <*n*>) ^ (d2 /^ D) is non empty Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
(p,d2,n,D) /. 1 is Element of p
d2 /. 1 is Element of p
len d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
len (d2 | D) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
dom (d2 | D) is Element of bool NAT
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
p is non empty set
n is Element of p
d2 is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
rng d2 is set
(p,d2,n,D) is non empty Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
d2 | D is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
Seg D is V34() V41(D) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
d2 | (Seg D) is Relation-like NAT -defined Seg D -defined NAT -defined p -valued Function-like FinSubsequence-like set
<*n*> is non empty trivial Relation-like NAT -defined p -valued Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like FinSequence of p
[1,n] is set
{1,n} is non empty set
{{1,n},{1}} is non empty set
{[1,n]} is non empty trivial Relation-like Function-like constant V41(1) set
(d2 | D) ^ <*n*> is non empty Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
d2 /^ D is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
((d2 | D) ^ <*n*>) ^ (d2 /^ D) is non empty Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
D is set
rng (d2 /^ D) is set
{n} is non empty trivial V41(1) set
rng <*n*> is non empty trivial V41(1) set
rng (d2 | D) is set
(rng (d2 | D)) \/ (rng <*n*>) is non empty set
rng ((d2 | D) ^ <*n*>) is non empty set
D is set
D is non empty set
p is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
p | n is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg n is V34() V41(n) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
p | (Seg n) is Relation-like NAT -defined Seg n -defined NAT -defined D -valued Function-like FinSubsequence-like set
(p | n) | d2 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg d2 is V34() V41(d2) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= d2 ) } is set
(p | n) | (Seg d2) is Relation-like NAT -defined Seg d2 -defined NAT -defined D -valued Function-like FinSubsequence-like set
p | d2 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
p | (Seg d2) is Relation-like NAT -defined Seg d2 -defined NAT -defined D -valued Function-like FinSubsequence-like set
(p | d2) | n is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(p | d2) | (Seg n) is Relation-like NAT -defined Seg n -defined NAT -defined D -valued Function-like FinSubsequence-like set
len (p | n) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
D is non empty set
p is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
<*> D is ext-real non positive non negative empty proper V7() V8() V9() V11() V12() V13() V14() Relation-like non-empty empty-yielding NAT -defined D -valued Function-like one-to-one constant functional V32() V33() V34() V39() V41( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D
[:NAT,D:] is non empty Relation-like V34() set
(<*> D) | p is Relation-like NAT -defined D -valued Function-like one-to-one V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg p is V34() V41(p) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= p ) } is set
(<*> D) | (Seg p) is ext-real non positive non negative empty V7() V8() V9() V11() V12() V13() V14() Relation-like non-empty empty-yielding NAT -defined Seg p -defined NAT -defined D -valued Function-like one-to-one constant functional V32() V33() V34() V39() V41( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set
D is non empty set
<*> D is ext-real non positive non negative empty proper V7() V8() V9() V11() V12() V13() V14() Relation-like non-empty empty-yielding NAT -defined D -valued Function-like one-to-one constant functional V32() V33() V34() V39() V41( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D
[:NAT,D:] is non empty Relation-like V34() set
(D,(<*> D)) is ext-real non positive non negative empty proper V7() V8() V9() V11() V12() V13() V14() Relation-like non-empty empty-yielding NAT -defined D -valued Function-like one-to-one constant functional V32() V33() V34() V39() V41( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D
<*0,0*> is non empty non trivial Relation-like NAT -defined NAT -valued Function-like V34() V41(2) FinSequence-like FinSubsequence-like FinSequence of NAT
<*0*> is non empty trivial Relation-like NAT -defined Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like set
[1,0] is set
{1,0} is non empty set
{{1,0},{1}} is non empty set
{[1,0]} is non empty trivial Relation-like Function-like constant V41(1) set
<*0*> ^ <*0*> is non empty Relation-like NAT -defined Function-like V34() V41(1 + 1) FinSequence-like FinSubsequence-like set
D is non empty set
p is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
d2 -' n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
p /^ n is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
(p /^ n) | (d2 -' n) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg (d2 -' n) is V34() V41(d2 -' n) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= d2 -' n ) } is set
(p /^ n) | (Seg (d2 -' n)) is Relation-like NAT -defined Seg (d2 -' n) -defined NAT -defined D -valued Function-like FinSubsequence-like set
p | d2 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg d2 is V34() V41(d2) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= d2 ) } is set
p | (Seg d2) is Relation-like NAT -defined Seg d2 -defined NAT -defined D -valued Function-like FinSubsequence-like set
(p | d2) /^ n is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len p is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
d2 - n is ext-real V14() V32() V33() set
(len p) - n is ext-real V14() V32() V33() set
len (p | d2) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
len ((p | d2) /^ n) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(len (p | d2)) - n is ext-real V14() V32() V33() set
len (p /^ n) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
((p /^ n) | (d2 -' n)) . D is set
((p | d2) /^ n) . D is set
dom ((p | d2) /^ n) is Element of bool NAT
D + n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
(d2 - n) + n is ext-real V14() V32() V33() set
dom (p /^ n) is Element of bool NAT
(p /^ n) . D is set
p . (D + n) is set
(p | d2) . (D + n) is set
len ((p /^ n) | (d2 -' n)) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
len p is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
len (p /^ n) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
(len p) -' n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
len p is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
n - n is ext-real V14() V32() V33() set
d2 - n is ext-real V14() V32() V33() set
dom ((p /^ n) | (d2 -' n)) is Element of bool NAT
dom (p /^ n) is Element of bool NAT
{} NAT is ext-real non positive non negative empty proper V7() V8() V9() V11() V12() V13() V14() Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V32() V33() V34() V39() V41( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of bool NAT
(dom (p /^ n)) /\ ({} NAT) is Relation-like Element of bool NAT
<*> D is ext-real non positive non negative empty proper V7() V8() V9() V11() V12() V13() V14() Relation-like non-empty empty-yielding NAT -defined D -valued Function-like one-to-one constant functional V32() V33() V34() V39() V41( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D
[:NAT,D:] is non empty Relation-like V34() set
len p is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
p | f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg f is V34() V41(f) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= f ) } is set
p | (Seg f) is Relation-like NAT -defined Seg f -defined NAT -defined D -valued Function-like FinSubsequence-like set
len (p | f) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
len p is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
f is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
p | f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg f is V34() V41(f) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= f ) } is set
p | (Seg f) is Relation-like NAT -defined Seg f -defined NAT -defined D -valued Function-like FinSubsequence-like set
len (p | f) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
len p is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
D is set
p is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len p is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
p | 2 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
p | (Seg 2) is Relation-like NAT -defined Seg 2 -defined NAT -defined D -valued Function-like FinSubsequence-like set
p /. 1 is Element of D
p /. 2 is Element of D
<*(p /. 1),(p /. 2)*> is non empty non trivial Relation-like NAT -defined Function-like V34() V41(2) FinSequence-like FinSubsequence-like set
<*(p /. 1)*> is non empty trivial Relation-like NAT -defined Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like set
[1,(p /. 1)] is set
{1,(p /. 1)} is non empty set
{{1,(p /. 1)},{1}} is non empty set
{[1,(p /. 1)]} is non empty trivial Relation-like Function-like constant V41(1) set
<*(p /. 2)*> is non empty trivial Relation-like NAT -defined Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like set
[1,(p /. 2)] is set
{1,(p /. 2)} is non empty set
{{1,(p /. 2)},{1}} is non empty set
{[1,(p /. 2)]} is non empty trivial Relation-like Function-like constant V41(1) set
<*(p /. 1)*> ^ <*(p /. 2)*> is non empty Relation-like NAT -defined Function-like V34() V41(1 + 1) FinSequence-like FinSubsequence-like set
len (p | 2) is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
D is non empty set
f is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f | 2 is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
f | (Seg 2) is Relation-like NAT -defined Seg 2 -defined NAT -defined D -valued Function-like FinSubsequence-like set
dom (f | 2) is Element of bool NAT
(f | 2) /. 2 is Element of D
(f | 2) . 2 is set
(f | 2) /. 1 is Element of D
(f | 2) . 1 is set
D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
D + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
p is set
n is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
len n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
n | (D + 1) is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
Seg (D + 1) is non empty V34() V41(D + 1) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= D + 1 ) } is set
n | (Seg (D + 1)) is Relation-like NAT -defined Seg (D + 1) -defined NAT -defined p -valued Function-like FinSubsequence-like set
n | D is Relation-like NAT -defined p -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of p
Seg D is V34() V41(D) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
n | (Seg D) is Relation-like NAT -defined Seg D -defined NAT -defined p -valued Function-like FinSubsequence-like set
n /. (D + 1) is Element of p
<*(n /. (D + 1))*> is non empty trivial Relation-like NAT -defined Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like set
[1,(n /. (D + 1))] is set
{1,(n /. (D + 1))} is non empty set
{{1,(n /. (D + 1))},{1}} is non empty set
{[1,(n /. (D + 1))]} is non empty trivial Relation-like Function-like constant V41(1) set
(n | D) ^ <*(n /. (D + 1))*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
dom n is Element of bool NAT
n | (Seg (D + 1)) is Relation-like NAT -defined Seg (D + 1) -defined NAT -defined p -valued Function-like FinSubsequence-like Element of bool [:NAT,p:]
[:NAT,p:] is Relation-like set
bool [:NAT,p:] is non empty set
n . (D + 1) is set
<*(n . (D + 1))*> is non empty trivial Relation-like NAT -defined Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like set
[1,(n . (D + 1))] is set
{1,(n . (D + 1))} is non empty set
{{1,(n . (D + 1))},{1}} is non empty set
{[1,(n . (D + 1))]} is non empty trivial Relation-like Function-like constant V41(1) set
(n | D) ^ <*(n . (D + 1))*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D is set
p is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len p is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
n + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
p | (n + 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg (n + 1) is non empty V34() V41(n + 1) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= n + 1 ) } is set
p | (Seg (n + 1)) is Relation-like NAT -defined Seg (n + 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
p | n is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg n is V34() V41(n) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
p | (Seg n) is Relation-like NAT -defined Seg n -defined NAT -defined D -valued Function-like FinSubsequence-like set
p . (n + 1) is set
<*(p . (n + 1))*> is non empty trivial Relation-like NAT -defined Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like set
[1,(p . (n + 1))] is set
{1,(p . (n + 1))} is non empty set
{{1,(p . (n + 1))},{1}} is non empty set
{[1,(p . (n + 1))]} is non empty trivial Relation-like Function-like constant V41(1) set
(p | n) ^ <*(p . (n + 1))*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
dom p is Element of bool NAT
p /. (n + 1) is Element of D
<*(p /. (n + 1))*> is non empty trivial Relation-like NAT -defined Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like set
[1,(p /. (n + 1))] is set
{1,(p /. (n + 1))} is non empty set
{{1,(p /. (n + 1))},{1}} is non empty set
{[1,(p /. (n + 1))]} is non empty trivial Relation-like Function-like constant V41(1) set
(p | n) ^ <*(p /. (n + 1))*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
D is non empty set
p is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
len p is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
n -' 1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
p | (n -' 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg (n -' 1) is V34() V41(n -' 1) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= n -' 1 ) } is set
p | (Seg (n -' 1)) is Relation-like NAT -defined Seg (n -' 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
p . n is set
<*(p . n)*> is non empty trivial Relation-like NAT -defined Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like set
[1,(p . n)] is set
{1,(p . n)} is non empty set
{{1,(p . n)},{1}} is non empty set
{[1,(p . n)]} is non empty trivial Relation-like Function-like constant V41(1) set
(p | (n -' 1)) ^ <*(p . n)*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
p /^ n is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
((p | (n -' 1)) ^ <*(p . n)*>) ^ (p /^ n) is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set
(n -' 1) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
p | n is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg n is V34() V41(n) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
p | (Seg n) is Relation-like NAT -defined Seg n -defined NAT -defined D -valued Function-like FinSubsequence-like set
p | ((n -' 1) + 1) is Relation-like NAT -defined D -valued Function-like V34() FinSequence-like FinSubsequence-like FinSequence of D
Seg ((n -' 1) + 1) is non empty V34() V41((n -' 1) + 1) Element of bool NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b₁ & b₁ <= (n -' 1) + 1 ) } is set
p | (Seg ((n -' 1) + 1)) is Relation-like NAT -defined Seg ((n -' 1) + 1) -defined NAT -defined D -valued Function-like FinSubsequence-like set
p . ((n -' 1) + 1) is set
<*(p . ((n -' 1) + 1))*> is non empty trivial Relation-like NAT -defined Function-like constant V34() V41(1) FinSequence-like FinSubsequence-like set
[1,(p . ((n -' 1) + 1))] is set
{1,(p . ((n -' 1) + 1))} is non empty set
{{1,(p . ((n -' 1) + 1))},{1}} is non empty set
{[1,(p . ((n -' 1) + 1))]} is non empty trivial Relation-like Function-like constant V41(1) set
(p | (n -' 1)) ^ <*(p . ((n -' 1) + 1))*> is non empty Relation-like NAT -defined Function-like V34() FinSequence-like FinSubsequence-like set