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

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

Seg 1 is non empty trivial V34() V41(1) Element of bool NAT
{ b1 where b1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set
{1} is non empty trivial V41(1) set
Seg 2 is non empty V34() V41(2) Element of bool NAT
{ b1 where b1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b1 & b1 <= 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

- 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

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

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

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

[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

[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

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

[1,{}] is set
{1,{}} is non empty set
{{1,{}},{1}} is non empty 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

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

[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

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 p) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT

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
{ b1 where b1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b1 & b1 <= D ) } is set
Seg (D + 1) is non empty V34() V41(D + 1) Element of bool NAT
{ b1 where b1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b1 & b1 <= D + 1 ) } is set

dom p is Element of bool NAT

p . (D + 1) is 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

len p 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
d2 . (D + 1) is set

D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() 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

[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

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

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

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

[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

[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) /. 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

dom n is Element of bool NAT
n /. D is Element 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

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

Seg p is V34() V41(p) Element of bool NAT
{ b1 where b1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b1 & b1 <= p ) } is set

len (D | p) 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

Seg p is V34() V41(p) Element of bool NAT
{ b1 where b1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b1 & b1 <= p ) } is 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

dom D is Element of bool NAT
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
{ b1 where b1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b1 & b1 <= p ) } is set

dom (D | p) is Element of bool NAT

rng D is 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
{ b1 where b1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b1 & b1 <= p ) } is set

rng (D | p) is set
D is set

p /. 1 is Element 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
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

len n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT

Seg D is V34() V41(D) Element of bool NAT
{ b1 where b1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b1 & b1 <= D ) } is set

n /. (len n) is Element 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
{ b1 where b1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b1 & b1 <= D + 1 ) } is set

[:NAT,p:] is non empty Relation-like V34() set
bool [:NAT,p:] is non empty V34() set
n . (D + 1) is 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

Seg D is V34() V41(D) Element of bool NAT
{ b1 where b1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b1 & b1 <= D ) } is 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

Seg D is V34() V41(D) Element of bool NAT
{ b1 where b1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b1 & b1 <= D ) } is set

D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
p is set

len n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT

Seg D is V34() V41(D) Element of bool NAT
{ b1 where b1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b1 & b1 <= D ) } is 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
{ b1 where b1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b1 & b1 <= 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

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
{ b1 where b1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b1 & b1 <= len p ) } is set

D is non empty set
p is Element 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

rng d2 is set

p .. d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT

Seg (p .. d2) is V34() V41(p .. d2) Element of bool NAT
{ b1 where b1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b1 & b1 <= p .. d2 ) } is 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
{ b1 where b1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b1 & b1 <= D ) } is 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

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

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

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

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

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

len d2 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT
D is set

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 /. 1 is Element 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

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

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

[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

dom d2 is Element of bool NAT
d2 /. p is Element 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)*> ^ (d2 /^ p) is non empty 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

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

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

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

D is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() set
p is non empty set

Seg D is V34() V41(D) Element of bool NAT
{ b1 where b1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b1 & b1 <= D ) } is set

rng (n | D) is set

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

rng n is set

p .. n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT

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
{ b1 where b1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b1 & b1 <= 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

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

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

[:NAT,p:] is non empty Relation-like V34() set
D is non empty set

len p is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT

(len p) + 0 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT

D is non empty set
p is Element 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

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)})) . 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
{ b1 where b1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b1 & b1 <= 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

Seg D is V34() V41(D) Element of bool NAT
{ b1 where b1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b1 & b1 <= D ) } is 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

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

n is set
n .. p is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT

Seg (n .. p) is V34() V41(n .. p) Element of bool NAT
{ b1 where b1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b1 & b1 <= n .. p ) } is set

D is non empty set
p is Element 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

Seg (p .. n) is V34() V41(p .. n) Element of bool NAT
{ b1 where b1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b1 & b1 <= p .. n ) } is 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

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
{ b1 where b1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b1 & b1 <= n .. d2 ) } is 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

rng n is set

p .. n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT

Seg (p .. n) is V34() V41(p .. n) Element of bool NAT
{ b1 where b1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b1 & b1 <= p .. n ) } is 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

rng n is set

p .. n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT

Seg (p .. n) is V34() V41(p .. n) Element of bool NAT
{ b1 where b1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b1 & b1 <= p .. n ) } is 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

rng n is set
p .. n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT

Seg (p .. n) is V34() V41(p .. n) Element of bool NAT
{ b1 where b1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b1 & b1 <= p .. n ) } is 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
{ b1 where b1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b1 & b1 <= 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

rng n is set

p .. n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT

Seg (p .. n) is V34() V41(p .. n) Element of bool NAT
{ b1 where b1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b1 & b1 <= p .. n ) } is 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

p is Element of D

p .. n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT

Seg (p .. n) is V34() V41(p .. n) Element of bool NAT
{ b1 where b1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b1 & b1 <= p .. n ) } is set

rng (D,n,p) is set
rng n is set
D is non empty set

p is Element of D

p .. n is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT

Seg (p .. n) is V34() V41(p .. n) Element of bool NAT
{ b1 where b1 is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT : ( 1 <= b1 & b1 <= p .. n ) } is set

D is non empty set
n is Element 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

n .. p is ext-real non negative V7() V8() V9() V13() V14() V32() V33() V34() V39() Element of NAT

D is non empty set
p is Element 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

[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) - 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 /. (p .. n) is Element of D
<*(n /. (p .. n))*> is non empty trivial Relation-like NAT -defined D -valued