:: FINSEQ_2 semantic presentation

REAL is set
NAT is non empty V34() V35() V36() V46() cardinal limit_cardinal countable denumerable Element of bool REAL
bool REAL is non empty set
{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty Function-yielding V33() V34() V35() V36() V38() V39() V40() V41() ext-real non positive non negative V45() V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable set
1 is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
{{},1} is non empty set
COMPLEX is set
NAT is non empty V34() V35() V36() V46() cardinal limit_cardinal countable denumerable set
bool NAT is non empty V46() set
bool NAT is non empty V46() set
RAT is set
INT is set
2 is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
3 is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty Function-yielding V33() V34() V35() V36() V38() V39() V40() V41() ext-real non positive non negative V45() V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable Element of NAT
Seg 1 is non empty trivial V46() 1 -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= 1 ) } is set
card {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty Function-yielding V33() V34() V35() V36() V38() V39() V40() V41() ext-real non positive non negative V45() V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
min (D,A) is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
max (x,i) is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
Seg D is V46() D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
Seg A is V46() A -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= A ) } is set
x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
min (A,x) is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
Seg x is V46() x -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= x ) } is set
(Seg A) /\ (Seg x) is countable Element of bool NAT
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
D - A is V41() ext-real V45() set
max (0,(D - A)) is V41() ext-real V45() set
D - D is V41() ext-real V45() set
A - D is V41() ext-real V45() set
- (A - D) is V41() ext-real V45() set
- 0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty Function-yielding V33() V34() V35() V36() V38() V39() V40() V41() ext-real non positive non negative V45() V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
A - D is V41() ext-real V45() set
max (0,(A - D)) is V41() ext-real V45() set
D - D is V41() ext-real V45() set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
D - A is V41() ext-real V45() set
max (0,(D - A)) is V41() ext-real V45() set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
min (0,D) is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
min (A,0) is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
max (0,x) is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
max (i,0) is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
A + 1 is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
Seg (A + 1) is non empty V46() A + 1 -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= A + 1 ) } is set
Seg A is V46() A -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= A ) } is set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
Seg A is V46() A -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= A ) } is set
x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
A + x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
Seg (A + x) is V46() A + x -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= A + x ) } is set
D is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
len D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
dom D is countable Element of bool NAT
A is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
len A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
Seg (len D) is V46() len D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= len D ) } is set
dom A is countable Element of bool NAT
D is set
A is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
rng A is set
dom A is countable Element of bool NAT
x is set
A . x is set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
A is set
x is Relation-like NAT -defined A -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of A
dom x is countable Element of bool NAT
x . D is set
rng x is set
D is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
dom D is countable Element of bool NAT
A is set
x is set
rng D is set
i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
D . i is set
D is set
A is set
<*D,A*> is Relation-like NAT -defined Function-like non empty V46() 2 -element FinSequence-like FinSubsequence-like countable set
<*D*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,D] is set
{1,D} is non empty set
{1} is non empty trivial 1 -element set
{{1,D},{1}} is non empty set
{[1,D]} is Relation-like Function-like constant non empty trivial 1 -element set
<*A*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,A] is set
{1,A} is non empty set
{{1,A},{1}} is non empty set
{[1,A]} is Relation-like Function-like constant non empty trivial 1 -element set
<*D*> ^ <*A*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
1 + 1 is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
rng <*D,A*> is non empty set
{D,A} is non empty set
rng <*D*> is non empty trivial 1 -element set
rng <*A*> is non empty trivial 1 -element set
(rng <*D*>) \/ (rng <*A*>) is non empty set
{A} is non empty trivial 1 -element set
(rng <*D*>) \/ {A} is non empty set
{D} is non empty trivial 1 -element set
{D} \/ {A} is non empty set
D is non empty set
A is Element of D
x is Element of D
<*A,x*> is Relation-like NAT -defined Function-like non empty V46() 2 -element FinSequence-like FinSubsequence-like countable set
<*A*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,A] is set
{1,A} is non empty set
{1} is non empty trivial 1 -element set
{{1,A},{1}} is non empty set
{[1,A]} is Relation-like Function-like constant non empty trivial 1 -element set
<*x*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,x] is set
{1,x} is non empty set
{{1,x},{1}} is non empty set
{[1,x]} is Relation-like Function-like constant non empty trivial 1 -element set
<*A*> ^ <*x*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
1 + 1 is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
rng <*A,x*> is non empty set
{A,x} is non empty Element of bool D
bool D is non empty set
D is set
A is set
x is set
<*D,A,x*> is Relation-like NAT -defined Function-like non empty V46() 3 -element FinSequence-like FinSubsequence-like countable set
<*D*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,D] is set
{1,D} is non empty set
{1} is non empty trivial 1 -element set
{{1,D},{1}} is non empty set
{[1,D]} is Relation-like Function-like constant non empty trivial 1 -element set
<*A*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,A] is set
{1,A} is non empty set
{{1,A},{1}} is non empty set
{[1,A]} is Relation-like Function-like constant non empty trivial 1 -element set
<*D*> ^ <*A*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
1 + 1 is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
<*x*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,x] is set
{1,x} is non empty set
{{1,x},{1}} is non empty set
{[1,x]} is Relation-like Function-like constant non empty trivial 1 -element set
(<*D*> ^ <*A*>) ^ <*x*> is Relation-like NAT -defined Function-like non empty V46() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like countable set
(1 + 1) + 1 is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
rng <*D,A,x*> is non empty set
{D,A,x} is non empty set
<*A,x*> is Relation-like NAT -defined Function-like non empty V46() 2 -element FinSequence-like FinSubsequence-like countable set
<*A*> ^ <*x*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
<*D*> ^ <*A,x*> is Relation-like NAT -defined Function-like non empty V46() 1 + 2 -element FinSequence-like FinSubsequence-like countable set
1 + 2 is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
rng (<*D*> ^ <*A,x*>) is non empty set
rng <*D*> is non empty trivial 1 -element set
rng <*A,x*> is non empty set
(rng <*D*>) \/ (rng <*A,x*>) is non empty set
{D} is non empty trivial 1 -element set
{D} \/ (rng <*A,x*>) is non empty set
{A,x} is non empty set
{D} \/ {A,x} is non empty set
D is non empty set
A is Element of D
x is Element of D
i is Element of D
<*A,x,i*> is Relation-like NAT -defined Function-like non empty V46() 3 -element FinSequence-like FinSubsequence-like countable set
<*A*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,A] is set
{1,A} is non empty set
{1} is non empty trivial 1 -element set
{{1,A},{1}} is non empty set
{[1,A]} is Relation-like Function-like constant non empty trivial 1 -element set
<*x*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,x] is set
{1,x} is non empty set
{{1,x},{1}} is non empty set
{[1,x]} is Relation-like Function-like constant non empty trivial 1 -element set
<*A*> ^ <*x*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
1 + 1 is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
<*i*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,i] is set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
(<*A*> ^ <*x*>) ^ <*i*> is Relation-like NAT -defined Function-like non empty V46() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like countable set
(1 + 1) + 1 is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
rng <*A,x,i*> is non empty set
{A,x,i} is non empty Element of bool D
bool D is non empty set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
A is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
dom A is countable Element of bool NAT
x is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
A ^ x is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
dom (A ^ x) is countable Element of bool NAT
D is set
<*D*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,D] is set
{1,D} is non empty set
{1} is non empty trivial 1 -element set
{{1,D},{1}} is non empty set
{[1,D]} is Relation-like Function-like constant non empty trivial 1 -element set
A is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
A ^ <*D*> is Relation-like NAT -defined Function-like non empty V46() FinSequence-like FinSubsequence-like countable set
len (A ^ <*D*>) is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
len A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
(len A) + 1 is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
len <*D*> is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
(len A) + (len <*D*>) is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
D is set
<*D*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,D] is set
{1,D} is non empty set
{1} is non empty trivial 1 -element set
{{1,D},{1}} is non empty set
{[1,D]} is Relation-like Function-like constant non empty trivial 1 -element set
A is set
<*A*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,A] is set
{1,A} is non empty set
{{1,A},{1}} is non empty set
{[1,A]} is Relation-like Function-like constant non empty trivial 1 -element set
x is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
x ^ <*D*> is Relation-like NAT -defined Function-like non empty V46() FinSequence-like FinSubsequence-like countable set
i is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
i ^ <*A*> is Relation-like NAT -defined Function-like non empty V46() FinSequence-like FinSubsequence-like countable set
len x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
(len x) + 1 is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
(x ^ <*D*>) . ((len x) + 1) is set
len i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
(len i) + 1 is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
(i ^ <*A*>) . ((len i) + 1) is set
len (x ^ <*D*>) is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
len (i ^ <*A*>) is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
A is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
len A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
D + 1 is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
D is set
A is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of D
len A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
x is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
i is set
<*i*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,i] is set
{1,i} is non empty set
{1} is non empty trivial 1 -element set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
x ^ <*i*> is Relation-like NAT -defined Function-like non empty V46() FinSequence-like FinSubsequence-like countable set
dom x is countable Element of bool NAT
i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
x . i is set
A . i is set
dom A is countable Element of bool NAT
Seg (len A) is V46() len A -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= len A ) } is set
dom A is countable Element of bool NAT
len x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
(len x) + 1 is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
A . (len A) is set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
Seg D is V46() D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
A is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
x is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
x | (Seg D) is Relation-like NAT -defined Seg D -defined NAT -defined Function-like FinSubsequence-like set
len x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
Seg (len x) is V46() len x -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= len x ) } is set
dom x is countable Element of bool NAT
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
Seg D is V46() D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
A is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
len A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
x is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
x | (Seg D) is Relation-like NAT -defined Seg D -defined NAT -defined Function-like FinSubsequence-like set
len x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
min (D,(len x)) is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
D + A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
x is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
len x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
Seg i is V46() i -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= i ) } is set
x | (Seg i) is Relation-like NAT -defined Seg i -defined NAT -defined Function-like FinSubsequence-like set
i is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
e is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
i ^ e is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
len i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
len e is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
len (i ^ e) is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
D + (len e) is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
D + A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
x is non empty set
i is Relation-like NAT -defined x -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of x
len i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
i is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
len i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
e is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
len e is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
i ^ e is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
F₂() is non empty set
F₁() is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
D is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
len D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
dom D is countable Element of bool NAT
Seg F₁() is V46() F₁() -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= F₁() ) } is set
A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
D . A is set
F₃(A) is Element of F₂()
A is Relation-like NAT -defined F₂() -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of F₂()
len A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
dom A is countable Element of bool NAT
x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
A . x is set
F₃(x) is Element of F₂()
F₁() is set
<*> F₁() is Relation-like non-empty empty-yielding NAT -defined F₁() -valued Function-like one-to-one constant functional empty Function-yielding V33() V34() V35() V36() V38() V39() V40() V41() ext-real non positive non negative V45() V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable FinSequence of F₁()
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
D + 1 is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
A is Relation-like NAT -defined F₁() -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of F₁()
len A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
x is Relation-like NAT -defined F₁() -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of F₁()
i is Element of F₁()
<*i*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,i] is set
{1,i} is non empty set
{1} is non empty trivial 1 -element set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
x ^ <*i*> is Relation-like NAT -defined Function-like non empty V46() FinSequence-like FinSubsequence-like countable set
len x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
(len x) + 1 is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
D is Relation-like NAT -defined F₁() -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of F₁()
len D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
A is Relation-like NAT -defined F₁() -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of F₁()
len A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
D is set
bool D is non empty set
A is Element of bool D
x is Relation-like NAT -defined A -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of A
rng x is set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
Seg D is V46() D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
A is non empty set
[:(Seg D),A:] is Relation-like set
bool [:(Seg D),A:] is non empty set
x is Relation-like Seg D -defined A -valued Function-like total quasi_total Element of bool [:(Seg D),A:]
dom x is set
i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
Seg i is V46() i -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= i ) } is set
rng x is set
D is non empty set
A is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of D
dom A is countable Element of bool NAT
[:(dom A),D:] is Relation-like set
bool [:(dom A),D:] is non empty set
rng A is set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
Seg D is V46() D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
A is non empty set
[:NAT,A:] is Relation-like non empty V46() set
bool [:NAT,A:] is non empty V46() set
x is Relation-like NAT -defined A -valued Function-like non empty total quasi_total Element of bool [:NAT,A:]
x | (Seg D) is Relation-like NAT -defined Seg D -defined NAT -defined A -valued Function-like Element of bool [:NAT,A:]
[:(Seg D),A:] is Relation-like set
bool [:(Seg D),A:] is non empty set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
Seg D is V46() D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
A is non empty set
[:NAT,A:] is Relation-like non empty V46() set
bool [:NAT,A:] is non empty V46() set
x is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
len x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
i is Relation-like NAT -defined A -valued Function-like non empty total quasi_total Element of bool [:NAT,A:]
i | (Seg D) is Relation-like NAT -defined Seg D -defined NAT -defined A -valued Function-like Element of bool [:NAT,A:]
i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
Seg i is V46() i -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= i ) } is set
i | (Seg i) is Relation-like NAT -defined Seg i -defined NAT -defined A -valued Function-like Element of bool [:NAT,A:]
[:(Seg i),A:] is Relation-like set
bool [:(Seg i),A:] is non empty set
dom (i | (Seg i)) is set
D is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
rng D is set
len D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
A is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
len A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
x is Relation-like Function-like set
dom x is set
D (#) x is Relation-like NAT -defined Function-like set
dom (D (#) x) is set
dom D is countable Element of bool NAT
Seg (len D) is V46() len D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= len D ) } is set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
Seg D is V46() D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
A is non empty set
x is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
len x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
i is Relation-like NAT -defined A -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of A
i (#) x is Relation-like NAT -defined Function-like set
Seg (len x) is V46() len x -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= len x ) } is set
dom x is countable Element of bool NAT
rng i is set
dom (i (#) x) is set
dom i is countable Element of bool NAT
len i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
Seg (len i) is V46() len i -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= len i ) } is set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
Seg D is V46() D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
A is non empty set
x is non empty set
i is Relation-like NAT -defined x -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of x
len i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
i is Relation-like NAT -defined A -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of A
i * i is Relation-like NAT -defined x -valued Function-like Element of bool [:NAT,x:]
[:NAT,x:] is Relation-like non empty V46() set
bool [:NAT,x:] is non empty V46() set
e is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
rng e is set
rng i is set
D is set
A is set
[:D,A:] is Relation-like set
bool [:D,A:] is non empty set
x is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of D
i is Relation-like D -defined A -valued Function-like quasi_total Element of bool [:D,A:]
i * x is Relation-like NAT -defined A -valued Function-like Element of bool [:NAT,A:]
[:NAT,A:] is Relation-like set
bool [:NAT,A:] is non empty set
<*> A is Relation-like non-empty empty-yielding NAT -defined A -valued Function-like one-to-one constant functional empty Function-yielding V33() V34() V35() V36() V38() V39() V40() V41() ext-real non positive non negative V45() V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable FinSequence of A
rng x is set
rng (i * x) is set
dom i is set
D is set
A is non empty set
[:D,A:] is Relation-like set
bool [:D,A:] is non empty set
x is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
len x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
i is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of D
len i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
i is Relation-like D -defined A -valued Function-like total quasi_total Element of bool [:D,A:]
i * i is Relation-like NAT -defined A -valued Function-like Element of bool [:NAT,A:]
[:NAT,A:] is Relation-like non empty V46() set
bool [:NAT,A:] is non empty V46() set
dom i is set
rng i is set
D is set
<*D*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,D] is set
{1,D} is non empty set
{1} is non empty trivial 1 -element set
{{1,D},{1}} is non empty set
{[1,D]} is Relation-like Function-like constant non empty trivial 1 -element set
A is Relation-like Function-like set
dom A is set
<*D*> (#) A is Relation-like NAT -defined Function-like set
A . D is set
<*(A . D)*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,(A . D)] is set
{1,(A . D)} is non empty set
{{1,(A . D)},{1}} is non empty set
{[1,(A . D)]} is Relation-like Function-like constant non empty trivial 1 -element set
rng A is set
rng <*D*> is non empty trivial 1 -element set
{D} is non empty trivial 1 -element set
x is non empty set
i is non empty set
[:x,i:] is Relation-like non empty set
bool [:x,i:] is non empty set
i is Relation-like NAT -defined x -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of x
e is Relation-like x -defined i -valued Function-like non empty total quasi_total Element of bool [:x,i:]
e * i is Relation-like NAT -defined i -valued Function-like Element of bool [:NAT,i:]
[:NAT,i:] is Relation-like non empty V46() set
bool [:NAT,i:] is non empty V46() set
i . 1 is set
a is Relation-like NAT -defined i -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of i
len a is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
len i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
Seg (len a) is V46() len a -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= len a ) } is set
dom a is countable Element of bool NAT
a . 1 is set
e . D is set
D is set
<*D*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,D] is set
{1,D} is non empty set
{1} is non empty trivial 1 -element set
{{1,D},{1}} is non empty set
{[1,D]} is Relation-like Function-like constant non empty trivial 1 -element set
A is non empty set
x is non empty set
[:A,x:] is Relation-like non empty set
bool [:A,x:] is non empty set
i is Relation-like NAT -defined A -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of A
i is Relation-like A -defined x -valued Function-like non empty total quasi_total Element of bool [:A,x:]
i * i is Relation-like NAT -defined x -valued Function-like Element of bool [:NAT,x:]
[:NAT,x:] is Relation-like non empty V46() set
bool [:NAT,x:] is non empty V46() set
i . D is set
<*(i . D)*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,(i . D)] is set
{1,(i . D)} is non empty set
{{1,(i . D)},{1}} is non empty set
{[1,(i . D)]} is Relation-like Function-like constant non empty trivial 1 -element set
i . 1 is set
len i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
e is Relation-like NAT -defined x -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of x
len e is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
Seg (len e) is V46() len e -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= len e ) } is set
dom e is countable Element of bool NAT
e . 1 is set
D is set
A is set
<*D,A*> is Relation-like NAT -defined Function-like non empty V46() 2 -element FinSequence-like FinSubsequence-like countable set
<*D*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,D] is set
{1,D} is non empty set
{1} is non empty trivial 1 -element set
{{1,D},{1}} is non empty set
{[1,D]} is Relation-like Function-like constant non empty trivial 1 -element set
<*A*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,A] is set
{1,A} is non empty set
{{1,A},{1}} is non empty set
{[1,A]} is Relation-like Function-like constant non empty trivial 1 -element set
<*D*> ^ <*A*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
1 + 1 is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
x is non empty set
i is non empty set
[:x,i:] is Relation-like non empty set
bool [:x,i:] is non empty set
i is Relation-like NAT -defined x -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of x
e is Relation-like x -defined i -valued Function-like non empty total quasi_total Element of bool [:x,i:]
e * i is Relation-like NAT -defined i -valued Function-like Element of bool [:NAT,i:]
[:NAT,i:] is Relation-like non empty V46() set
bool [:NAT,i:] is non empty V46() set
e . D is set
e . A is set
<*(e . D),(e . A)*> is Relation-like NAT -defined Function-like non empty V46() 2 -element FinSequence-like FinSubsequence-like countable set
<*(e . D)*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,(e . D)] is set
{1,(e . D)} is non empty set
{{1,(e . D)},{1}} is non empty set
{[1,(e . D)]} is Relation-like Function-like constant non empty trivial 1 -element set
<*(e . A)*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,(e . A)] is set
{1,(e . A)} is non empty set
{{1,(e . A)},{1}} is non empty set
{[1,(e . A)]} is Relation-like Function-like constant non empty trivial 1 -element set
<*(e . D)*> ^ <*(e . A)*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
i . 2 is set
len i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
a is Relation-like NAT -defined i -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of i
len a is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
Seg (len a) is V46() len a -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= len a ) } is set
dom a is countable Element of bool NAT
a . 2 is set
i . 1 is set
a . 1 is set
D is set
A is set
x is set
<*D,A,x*> is Relation-like NAT -defined Function-like non empty V46() 3 -element FinSequence-like FinSubsequence-like countable set
<*D*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,D] is set
{1,D} is non empty set
{1} is non empty trivial 1 -element set
{{1,D},{1}} is non empty set
{[1,D]} is Relation-like Function-like constant non empty trivial 1 -element set
<*A*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,A] is set
{1,A} is non empty set
{{1,A},{1}} is non empty set
{[1,A]} is Relation-like Function-like constant non empty trivial 1 -element set
<*D*> ^ <*A*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
1 + 1 is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
<*x*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,x] is set
{1,x} is non empty set
{{1,x},{1}} is non empty set
{[1,x]} is Relation-like Function-like constant non empty trivial 1 -element set
(<*D*> ^ <*A*>) ^ <*x*> is Relation-like NAT -defined Function-like non empty V46() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like countable set
(1 + 1) + 1 is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
i is non empty set
i is non empty set
[:i,i:] is Relation-like non empty set
bool [:i,i:] is non empty set
e is Relation-like NAT -defined i -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of i
a is Relation-like i -defined i -valued Function-like non empty total quasi_total Element of bool [:i,i:]
a * e is Relation-like NAT -defined i -valued Function-like Element of bool [:NAT,i:]
[:NAT,i:] is Relation-like non empty V46() set
bool [:NAT,i:] is non empty V46() set
a . D is set
a . A is set
a . x is set
<*(a . D),(a . A),(a . x)*> is Relation-like NAT -defined Function-like non empty V46() 3 -element FinSequence-like FinSubsequence-like countable set
<*(a . D)*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,(a . D)] is set
{1,(a . D)} is non empty set
{{1,(a . D)},{1}} is non empty set
{[1,(a . D)]} is Relation-like Function-like constant non empty trivial 1 -element set
<*(a . A)*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,(a . A)] is set
{1,(a . A)} is non empty set
{{1,(a . A)},{1}} is non empty set
{[1,(a . A)]} is Relation-like Function-like constant non empty trivial 1 -element set
<*(a . D)*> ^ <*(a . A)*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
<*(a . x)*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,(a . x)] is set
{1,(a . x)} is non empty set
{{1,(a . x)},{1}} is non empty set
{[1,(a . x)]} is Relation-like Function-like constant non empty trivial 1 -element set
(<*(a . D)*> ^ <*(a . A)*>) ^ <*(a . x)*> is Relation-like NAT -defined Function-like non empty V46() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like countable set
e . 2 is set
len e is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
b is Relation-like NAT -defined i -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of i
len b is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
Seg (len b) is V46() len b -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= len b ) } is set
dom b is countable Element of bool NAT
b . 2 is set
e . 3 is set
e . 1 is set
b . 3 is set
b . 1 is set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
Seg D is V46() D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
Seg A is V46() A -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= A ) } is set
[:(Seg D),(Seg A):] is Relation-like set
bool [:(Seg D),(Seg A):] is non empty set
x is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
len x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
i is Relation-like Seg D -defined Seg A -valued Function-like quasi_total Element of bool [:(Seg D),(Seg A):]
i (#) x is Relation-like Seg D -defined Function-like set
dom i is set
rng i is set
Seg (len x) is V46() len x -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= len x ) } is set
dom x is countable Element of bool NAT
dom (i (#) x) is set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
Seg D is V46() D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
[:(Seg D),(Seg D):] is Relation-like set
bool [:(Seg D),(Seg D):] is non empty set
A is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
len A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
x is Relation-like Seg D -defined Seg D -valued Function-like total quasi_total Element of bool [:(Seg D),(Seg D):]
x (#) A is Relation-like Seg D -defined Function-like set
D is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
dom D is countable Element of bool NAT
[:(dom D),(dom D):] is Relation-like set
bool [:(dom D),(dom D):] is non empty set
len D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
Seg (len D) is V46() len D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= len D ) } is set
A is Relation-like dom D -defined dom D -valued Function-like total quasi_total Element of bool [:(dom D),(dom D):]
A (#) D is Relation-like dom D -defined Function-like set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
Seg D is V46() D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
[:(Seg D),(Seg D):] is Relation-like set
bool [:(Seg D),(Seg D):] is non empty set
A is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
len A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
x is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
len x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
i is Relation-like Seg D -defined Seg D -valued Function-like total quasi_total Element of bool [:(Seg D),(Seg D):]
rng i is set
i (#) A is Relation-like Seg D -defined Function-like set
Seg (len A) is V46() len A -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= len A ) } is set
dom A is countable Element of bool NAT
dom (i (#) A) is set
dom i is set
D is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
dom D is countable Element of bool NAT
[:(dom D),(dom D):] is Relation-like set
bool [:(dom D),(dom D):] is non empty set
len D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
A is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
len A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
Seg (len D) is V46() len D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= len D ) } is set
x is Relation-like dom D -defined dom D -valued Function-like total quasi_total Element of bool [:(dom D),(dom D):]
rng x is set
x (#) D is Relation-like dom D -defined Function-like set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
Seg D is V46() D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
[:(Seg D),(Seg D):] is Relation-like set
bool [:(Seg D),(Seg D):] is non empty set
A is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
len A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
x is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
len x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
i is Relation-like Seg D -defined Seg D -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(Seg D),(Seg D):]
i (#) A is Relation-like Seg D -defined Function-like set
rng i is set
D is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
dom D is countable Element of bool NAT
[:(dom D),(dom D):] is Relation-like set
bool [:(dom D),(dom D):] is non empty set
len D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
A is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
len A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
Seg (len D) is V46() len D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= len D ) } is set
x is Relation-like dom D -defined dom D -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(dom D),(dom D):]
x (#) D is Relation-like dom D -defined Function-like set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
Seg D is V46() D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
Seg A is V46() A -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= A ) } is set
[:(Seg D),(Seg A):] is Relation-like set
bool [:(Seg D),(Seg A):] is non empty set
x is non empty set
i is Relation-like NAT -defined x -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of x
len i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
i is Relation-like Seg D -defined Seg A -valued Function-like quasi_total Element of bool [:(Seg D),(Seg A):]
i * i is Relation-like Seg D -defined x -valued Function-like Element of bool [:(Seg D),x:]
[:(Seg D),x:] is Relation-like set
bool [:(Seg D),x:] is non empty set
rng i is set
rng (i * i) is set
A is non empty set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
Seg D is V46() D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
[:(Seg D),(Seg D):] is Relation-like set
bool [:(Seg D),(Seg D):] is non empty set
x is Relation-like NAT -defined A -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of A
len x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
i is Relation-like Seg D -defined Seg D -valued Function-like total quasi_total Element of bool [:(Seg D),(Seg D):]
x * i is Relation-like Seg D -defined A -valued Function-like Element of bool [:(Seg D),A:]
[:(Seg D),A:] is Relation-like set
bool [:(Seg D),A:] is non empty set
D is non empty set
A is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of D
dom A is countable Element of bool NAT
[:(dom A),(dom A):] is Relation-like set
bool [:(dom A),(dom A):] is non empty set
len A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
Seg (len A) is V46() len A -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= len A ) } is set
x is Relation-like dom A -defined dom A -valued Function-like total quasi_total Element of bool [:(dom A),(dom A):]
A * x is Relation-like dom A -defined D -valued Function-like Element of bool [:(dom A),D:]
[:(dom A),D:] is Relation-like set
bool [:(dom A),D:] is non empty set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
Seg D is V46() D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
id (Seg D) is Relation-like Seg D -defined Seg D -valued V6() V8() V9() V13() Function-like one-to-one total quasi_total onto bijective Element of bool [:(Seg D),(Seg D):]
[:(Seg D),(Seg D):] is Relation-like set
bool [:(Seg D),(Seg D):] is non empty set
dom (id (Seg D)) is set
x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
Seg x is V46() x -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= x ) } is set
rng (id (Seg D)) is set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
Seg D is V46() D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
id (Seg D) is Relation-like Seg D -defined Seg D -valued V6() V8() V9() V13() Function-like one-to-one total quasi_total onto bijective Element of bool [:(Seg D),(Seg D):]
[:(Seg D),(Seg D):] is Relation-like set
bool [:(Seg D),(Seg D):] is non empty set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
(D) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
Seg D is V46() D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
id (Seg D) is Relation-like Seg D -defined Seg D -valued V6() V8() V9() V13() Function-like one-to-one total quasi_total onto bijective Element of bool [:(Seg D),(Seg D):]
[:(Seg D),(Seg D):] is Relation-like set
bool [:(Seg D),(Seg D):] is non empty set
dom (D) is countable Element of bool NAT
len (D) is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
(0) is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty Function-yielding V33() V34() V35() V36() V38() V39() V40() V41() ext-real non positive non negative V45() V46() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable set
Seg 0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty proper Function-yielding V33() V34() V35() V36() V38() V39() V40() V41() ext-real non positive non negative V45() V46() cardinal 0 -element {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= 0 ) } is set
id (Seg 0) is Relation-like non-empty empty-yielding Seg 0 -defined Seg 0 -valued V6() V8() V9() V13() Function-like one-to-one constant functional empty total quasi_total onto bijective Function-yielding V33() V34() V35() V36() V38() V39() V40() V41() ext-real non positive non negative V45() V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable Element of bool [:(Seg 0),(Seg 0):]
[:(Seg 0),(Seg 0):] is Relation-like set
bool [:(Seg 0),(Seg 0):] is non empty set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
Seg D is V46() D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
(D) is Relation-like NAT -defined Function-like V46() D -element FinSequence-like FinSubsequence-like countable set
id (Seg D) is Relation-like Seg D -defined Seg D -valued V6() V8() V9() V13() Function-like one-to-one total quasi_total onto bijective Element of bool [:(Seg D),(Seg D):]
[:(Seg D),(Seg D):] is Relation-like set
bool [:(Seg D),(Seg D):] is non empty set
A is Element of Seg D
(D) . A is set
dom (D) is D -element countable Element of bool NAT
(1) is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
id (Seg 1) is Relation-like Seg 1 -defined Seg 1 -valued V6() V8() V9() V13() Function-like one-to-one non empty total quasi_total onto bijective Element of bool [:(Seg 1),(Seg 1):]
[:(Seg 1),(Seg 1):] is Relation-like non empty set
bool [:(Seg 1),(Seg 1):] is non empty set
<*1*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable FinSequence of NAT
[1,1] is set
{1,1} is non empty set
{1} is non empty trivial 1 -element set
{{1,1},{1}} is non empty set
{[1,1]} is Relation-like Function-like constant non empty trivial 1 -element set
len (1) is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
(1) . 1 is set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
D + 1 is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
((D + 1)) is Relation-like NAT -defined Function-like V46() D + 1 -element FinSequence-like FinSubsequence-like countable set
Seg (D + 1) is non empty V46() D + 1 -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D + 1 ) } is set
id (Seg (D + 1)) is Relation-like Seg (D + 1) -defined Seg (D + 1) -valued V6() V8() V9() V13() Function-like one-to-one non empty total quasi_total onto bijective Element of bool [:(Seg (D + 1)),(Seg (D + 1)):]
[:(Seg (D + 1)),(Seg (D + 1)):] is Relation-like non empty set
bool [:(Seg (D + 1)),(Seg (D + 1)):] is non empty set
(D) is Relation-like NAT -defined Function-like V46() D -element FinSequence-like FinSubsequence-like countable set
Seg D is V46() D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
id (Seg D) is Relation-like Seg D -defined Seg D -valued V6() V8() V9() V13() Function-like one-to-one total quasi_total onto bijective Element of bool [:(Seg D),(Seg D):]
[:(Seg D),(Seg D):] is Relation-like set
bool [:(Seg D),(Seg D):] is non empty set
<*(D + 1)*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable FinSequence of NAT
[1,(D + 1)] is set
{1,(D + 1)} is non empty set
{{1,(D + 1)},{1}} is non empty set
{[1,(D + 1)]} is Relation-like Function-like constant non empty trivial 1 -element set
(D) ^ <*(D + 1)*> is Relation-like NAT -defined Function-like non empty V46() D + 1 -element FinSequence-like FinSubsequence-like countable set
x is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
i is set
<*i*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,i] is set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
x ^ <*i*> is Relation-like NAT -defined Function-like non empty V46() FinSequence-like FinSubsequence-like countable set
len ((D + 1)) is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
len x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
(len x) + 1 is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
dom x is countable Element of bool NAT
Seg (len x) is V46() len x -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= len x ) } is set
i is set
x . i is set
e is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
((D + 1)) . e is set
x . e is set
((D + 1)) . (D + 1) is set
(2) is Relation-like NAT -defined Function-like V46() 2 -element FinSequence-like FinSubsequence-like countable set
Seg 2 is non empty V46() 2 -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= 2 ) } is set
id (Seg 2) is Relation-like Seg 2 -defined Seg 2 -valued V6() V8() V9() V13() Function-like one-to-one non empty total quasi_total onto bijective Element of bool [:(Seg 2),(Seg 2):]
[:(Seg 2),(Seg 2):] is Relation-like non empty set
bool [:(Seg 2),(Seg 2):] is non empty set
<*1,2*> is Relation-like NAT -defined Function-like non empty V46() 2 -element FinSequence-like FinSubsequence-like countable set
<*1*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
<*2*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,2] is set
{1,2} is non empty set
{{1,2},{1}} is non empty set
{[1,2]} is Relation-like Function-like constant non empty trivial 1 -element set
<*1*> ^ <*2*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
1 + 1 is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
(3) is Relation-like NAT -defined Function-like V46() 3 -element FinSequence-like FinSubsequence-like countable set
Seg 3 is non empty V46() 3 -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= 3 ) } is set
id (Seg 3) is Relation-like Seg 3 -defined Seg 3 -valued V6() V8() V9() V13() Function-like one-to-one non empty total quasi_total onto bijective Element of bool [:(Seg 3),(Seg 3):]
[:(Seg 3),(Seg 3):] is Relation-like non empty set
bool [:(Seg 3),(Seg 3):] is non empty set
<*1,2,3*> is Relation-like NAT -defined Function-like non empty V46() 3 -element FinSequence-like FinSubsequence-like countable set
<*3*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,3] is set
{1,3} is non empty set
{{1,3},{1}} is non empty set
{[1,3]} is Relation-like Function-like constant non empty trivial 1 -element set
(<*1*> ^ <*2*>) ^ <*3*> is Relation-like NAT -defined Function-like non empty V46() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like countable set
(1 + 1) + 1 is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
(D) is Relation-like NAT -defined Function-like V46() D -element FinSequence-like FinSubsequence-like countable set
Seg D is V46() D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
id (Seg D) is Relation-like Seg D -defined Seg D -valued V6() V8() V9() V13() Function-like one-to-one total quasi_total onto bijective Element of bool [:(Seg D),(Seg D):]
[:(Seg D),(Seg D):] is Relation-like set
bool [:(Seg D),(Seg D):] is non empty set
A is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
len A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
(D) (#) A is Relation-like NAT -defined Function-like set
dom A is countable Element of bool NAT
Seg (len A) is V46() len A -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= len A ) } is set
x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
Seg x is V46() x -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= x ) } is set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
(D) is Relation-like NAT -defined Function-like V46() D -element FinSequence-like FinSubsequence-like countable set
Seg D is V46() D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
id (Seg D) is Relation-like Seg D -defined Seg D -valued V6() V8() V9() V13() Function-like one-to-one total quasi_total onto bijective Element of bool [:(Seg D),(Seg D):]
[:(Seg D),(Seg D):] is Relation-like set
bool [:(Seg D),(Seg D):] is non empty set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
Seg D is V46() D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
A is set
(Seg D) --> A is Relation-like Seg D -defined {A} -valued Function-like constant total quasi_total Element of bool [:(Seg D),{A}:]
{A} is non empty trivial 1 -element set
[:(Seg D),{A}:] is Relation-like set
bool [:(Seg D),{A}:] is non empty set
dom ((Seg D) --> A) is set
i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
Seg i is V46() i -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= i ) } is set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
Seg D is V46() D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
A is set
(Seg D) --> A is Relation-like Seg D -defined {A} -valued Function-like constant total quasi_total Element of bool [:(Seg D),{A}:]
{A} is non empty trivial 1 -element set
[:(Seg D),{A}:] is Relation-like set
bool [:(Seg D),{A}:] is non empty set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
Seg D is V46() D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
A is set
(Seg D) --> A is Relation-like Seg D -defined Seg D -defined {A} -valued Function-like constant total total quasi_total V46() FinSequence-like FinSubsequence-like countable Element of bool [:(Seg D),{A}:]
{A} is non empty trivial 1 -element set
[:(Seg D),{A}:] is Relation-like set
bool [:(Seg D),{A}:] is non empty set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
A is set
(D,A) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
Seg D is V46() D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
(Seg D) --> A is Relation-like Seg D -defined Seg D -defined {A} -valued Function-like constant total total quasi_total V46() FinSequence-like FinSubsequence-like countable Element of bool [:(Seg D),{A}:]
{A} is non empty trivial 1 -element set
[:(Seg D),{A}:] is Relation-like set
bool [:(Seg D),{A}:] is non empty set
dom (D,A) is countable Element of bool NAT
len (D,A) is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
x is set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
Seg D is V46() D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
A is set
(D,A) is Relation-like NAT -defined Function-like V46() D -element FinSequence-like FinSubsequence-like countable set
(Seg D) --> A is Relation-like Seg D -defined Seg D -defined {A} -valued Function-like constant total total quasi_total V46() FinSequence-like FinSubsequence-like countable Element of bool [:(Seg D),{A}:]
{A} is non empty trivial 1 -element set
[:(Seg D),{A}:] is Relation-like set
bool [:(Seg D),{A}:] is non empty set
(D,A) . x is set
D is set
(0,D) is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty Function-yielding V33() V34() V35() V36() V38() V39() V40() V41() ext-real non positive non negative V45() V46() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable set
(Seg 0) --> D is Relation-like non-empty empty-yielding Seg 0 -defined Seg 0 -defined {D} -valued Function-like one-to-one constant functional empty total total quasi_total Function-yielding V33() V34() V35() V36() V38() V39() V40() V41() ext-real non positive non negative V45() V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable Element of bool [:(Seg 0),{D}:]
{D} is non empty trivial 1 -element set
[:(Seg 0),{D}:] is Relation-like set
bool [:(Seg 0),{D}:] is non empty set
D is set
(1,D) is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
(Seg 1) --> D is Relation-like Seg 1 -defined Seg 1 -defined {D} -valued Function-like constant non empty total total quasi_total V46() FinSequence-like FinSubsequence-like countable Element of bool [:(Seg 1),{D}:]
{D} is non empty trivial 1 -element set
[:(Seg 1),{D}:] is Relation-like non empty set
bool [:(Seg 1),{D}:] is non empty set
<*D*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,D] is set
{1,D} is non empty set
{{1,D},{1}} is non empty set
{[1,D]} is Relation-like Function-like constant non empty trivial 1 -element set
len (1,D) is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
(1,D) . 1 is set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
D + 1 is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
A is set
((D + 1),A) is Relation-like NAT -defined Function-like V46() D + 1 -element FinSequence-like FinSubsequence-like countable set
Seg (D + 1) is non empty V46() D + 1 -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D + 1 ) } is set
(Seg (D + 1)) --> A is Relation-like Seg (D + 1) -defined Seg (D + 1) -defined {A} -valued Function-like constant non empty total total quasi_total V46() FinSequence-like FinSubsequence-like countable Element of bool [:(Seg (D + 1)),{A}:]
{A} is non empty trivial 1 -element set
[:(Seg (D + 1)),{A}:] is Relation-like non empty set
bool [:(Seg (D + 1)),{A}:] is non empty set
(D,A) is Relation-like NAT -defined Function-like V46() D -element FinSequence-like FinSubsequence-like countable set
Seg D is V46() D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
(Seg D) --> A is Relation-like Seg D -defined Seg D -defined {A} -valued Function-like constant total total quasi_total V46() FinSequence-like FinSubsequence-like countable Element of bool [:(Seg D),{A}:]
[:(Seg D),{A}:] is Relation-like set
bool [:(Seg D),{A}:] is non empty set
<*A*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,A] is set
{1,A} is non empty set
{{1,A},{1}} is non empty set
{[1,A]} is Relation-like Function-like constant non empty trivial 1 -element set
(D,A) ^ <*A*> is Relation-like NAT -defined Function-like non empty V46() D + 1 -element FinSequence-like FinSubsequence-like countable set
i is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
i is set
<*i*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,i] is set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
i ^ <*i*> is Relation-like NAT -defined Function-like non empty V46() FinSequence-like FinSubsequence-like countable set
len ((D + 1),A) is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
len i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
(len i) + 1 is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
rng i is set
rng ((D + 1),A) is set
dom i is countable Element of bool NAT
Seg (len i) is V46() len i -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= len i ) } is set
i . D is set
((D + 1),A) . (D + 1) is set
D is set
(2,D) is Relation-like NAT -defined Function-like V46() 2 -element FinSequence-like FinSubsequence-like countable set
(Seg 2) --> D is Relation-like Seg 2 -defined Seg 2 -defined {D} -valued Function-like constant non empty total total quasi_total V46() FinSequence-like FinSubsequence-like countable Element of bool [:(Seg 2),{D}:]
{D} is non empty trivial 1 -element set
[:(Seg 2),{D}:] is Relation-like non empty set
bool [:(Seg 2),{D}:] is non empty set
<*D,D*> is Relation-like NAT -defined Function-like non empty V46() 2 -element FinSequence-like FinSubsequence-like countable set
<*D*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,D] is set
{1,D} is non empty set
{{1,D},{1}} is non empty set
{[1,D]} is Relation-like Function-like constant non empty trivial 1 -element set
<*D*> ^ <*D*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
1 + 1 is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
((1 + 1),D) is Relation-like NAT -defined Function-like V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
Seg (1 + 1) is non empty V46() 1 + 1 -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= 1 + 1 ) } is set
(Seg (1 + 1)) --> D is Relation-like Seg (1 + 1) -defined Seg (1 + 1) -defined {D} -valued Function-like constant non empty total total quasi_total V46() FinSequence-like FinSubsequence-like countable Element of bool [:(Seg (1 + 1)),{D}:]
[:(Seg (1 + 1)),{D}:] is Relation-like non empty set
bool [:(Seg (1 + 1)),{D}:] is non empty set
(1,D) is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
(Seg 1) --> D is Relation-like Seg 1 -defined Seg 1 -defined {D} -valued Function-like constant non empty total total quasi_total V46() FinSequence-like FinSubsequence-like countable Element of bool [:(Seg 1),{D}:]
[:(Seg 1),{D}:] is Relation-like non empty set
bool [:(Seg 1),{D}:] is non empty set
(1,D) ^ <*D*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
D is set
(3,D) is Relation-like NAT -defined Function-like V46() 3 -element FinSequence-like FinSubsequence-like countable set
(Seg 3) --> D is Relation-like Seg 3 -defined Seg 3 -defined {D} -valued Function-like constant non empty total total quasi_total V46() FinSequence-like FinSubsequence-like countable Element of bool [:(Seg 3),{D}:]
{D} is non empty trivial 1 -element set
[:(Seg 3),{D}:] is Relation-like non empty set
bool [:(Seg 3),{D}:] is non empty set
<*D,D,D*> is Relation-like NAT -defined Function-like non empty V46() 3 -element FinSequence-like FinSubsequence-like countable set
<*D*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,D] is set
{1,D} is non empty set
{{1,D},{1}} is non empty set
{[1,D]} is Relation-like Function-like constant non empty trivial 1 -element set
<*D*> ^ <*D*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
(<*D*> ^ <*D*>) ^ <*D*> is Relation-like NAT -defined Function-like non empty V46() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like countable set
2 + 1 is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
((2 + 1),D) is Relation-like NAT -defined Function-like V46() 2 + 1 -element FinSequence-like FinSubsequence-like countable set
Seg (2 + 1) is non empty V46() 2 + 1 -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= 2 + 1 ) } is set
(Seg (2 + 1)) --> D is Relation-like Seg (2 + 1) -defined Seg (2 + 1) -defined {D} -valued Function-like constant non empty total total quasi_total V46() FinSequence-like FinSubsequence-like countable Element of bool [:(Seg (2 + 1)),{D}:]
[:(Seg (2 + 1)),{D}:] is Relation-like non empty set
bool [:(Seg (2 + 1)),{D}:] is non empty set
(2,D) is Relation-like NAT -defined Function-like V46() 2 -element FinSequence-like FinSubsequence-like countable set
(Seg 2) --> D is Relation-like Seg 2 -defined Seg 2 -defined {D} -valued Function-like constant non empty total total quasi_total V46() FinSequence-like FinSubsequence-like countable Element of bool [:(Seg 2),{D}:]
[:(Seg 2),{D}:] is Relation-like non empty set
bool [:(Seg 2),{D}:] is non empty set
(2,D) ^ <*D*> is Relation-like NAT -defined Function-like non empty V46() 2 + 1 -element FinSequence-like FinSubsequence-like countable set
2 + 1 is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
<*D,D*> is Relation-like NAT -defined Function-like non empty V46() 2 -element FinSequence-like FinSubsequence-like countable set
<*D,D*> ^ <*D*> is Relation-like NAT -defined Function-like non empty V46() 2 + 1 -element FinSequence-like FinSubsequence-like countable set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
A is non empty set
x is Element of A
(D,x) is Relation-like NAT -defined Function-like V46() D -element FinSequence-like FinSubsequence-like countable set
Seg D is V46() D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
(Seg D) --> x is Relation-like Seg D -defined Seg D -defined A -valued {x} -valued Function-like constant total total quasi_total V46() FinSequence-like FinSubsequence-like countable Element of bool [:(Seg D),{x}:]
{x} is non empty trivial 1 -element set
[:(Seg D),{x}:] is Relation-like set
bool [:(Seg D),{x}:] is non empty set
rng (D,x) is set
{x} is non empty trivial 1 -element Element of bool A
bool A is non empty set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
Seg D is V46() D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
A is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
rng A is set
len A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
x is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
rng x is set
[:(rng A),(rng x):] is Relation-like set
len x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
min ((len A),(len x)) is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
i is Relation-like Function-like set
dom i is set
i .: (A,x) is Relation-like Function-like set
<:A,x:> is Relation-like Function-like set
<:A,x:> (#) i is Relation-like Function-like set
dom (i .: (A,x)) is set
rng <:A,x:> is set
dom <:A,x:> is set
dom A is countable Element of bool NAT
dom x is countable Element of bool NAT
(dom A) /\ (dom x) is countable Element of bool NAT
Seg (len A) is V46() len A -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= len A ) } is set
Seg (len x) is V46() len x -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= len x ) } is set
D is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
rng D is set
A is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
rng A is set
[:(rng D),(rng A):] is Relation-like set
x is Relation-like Function-like set
dom x is set
x .: (D,A) is Relation-like Function-like set
<:D,A:> is Relation-like Function-like set
<:D,A:> (#) x is Relation-like Function-like set
len D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
len A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
min ((len D),(len A)) is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
dom (x .: (D,A)) is set
i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
Seg i is V46() i -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= i ) } is set
D is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
rng D is set
len D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
A is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
rng A is set
[:(rng D),(rng A):] is Relation-like set
len A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
min ((len D),(len A)) is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
x is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
len x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
i is Relation-like Function-like set
dom i is set
i .: (D,A) is Relation-like Function-like set
<:D,A:> is Relation-like Function-like set
<:D,A:> (#) i is Relation-like Function-like set
dom (i .: (D,A)) is set
i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
Seg i is V46() i -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= i ) } is set
D is set
{D} is non empty trivial 1 -element set
A is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
rng A is set
[:{D},(rng A):] is Relation-like set
dom A is countable Element of bool NAT
x is Relation-like Function-like set
dom x is set
x [;] (D,A) is Relation-like Function-like set
dom A is set
(dom A) --> D is Relation-like dom A -defined Function-like constant total set
[:(dom A),{D}:] is Relation-like set
<:((dom A) --> D),A:> is Relation-like Function-like set
<:((dom A) --> D),A:> (#) x is Relation-like Function-like set
dom (x [;] (D,A)) is set
(dom A) --> D is Relation-like dom A -defined {D} -valued Function-like constant total quasi_total Element of bool [:(dom A),{D}:]
[:(dom A),{D}:] is Relation-like set
bool [:(dom A),{D}:] is non empty set
dom ((dom A) --> D) is set
<:((dom A) --> D),A:> is Relation-like Function-like set
dom <:((dom A) --> D),A:> is set
rng ((dom A) --> D) is trivial set
rng <:((dom A) --> D),A:> is set
[:(rng ((dom A) --> D)),(rng A):] is Relation-like set
D is set
{D} is non empty trivial 1 -element set
A is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
rng A is set
[:{D},(rng A):] is Relation-like set
x is Relation-like Function-like set
dom x is set
x [;] (D,A) is Relation-like Function-like set
dom A is set
(dom A) --> D is Relation-like dom A -defined Function-like constant total set
[:(dom A),{D}:] is Relation-like set
<:((dom A) --> D),A:> is Relation-like Function-like set
<:((dom A) --> D),A:> (#) x is Relation-like Function-like set
dom (x [;] (D,A)) is set
dom A is countable Element of bool NAT
len A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
Seg (len A) is V46() len A -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= len A ) } is set
D is set
{D} is non empty trivial 1 -element set
A is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
rng A is set
[:{D},(rng A):] is Relation-like set
len A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
x is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
len x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
i is Relation-like Function-like set
dom i is set
i [;] (D,A) is Relation-like Function-like set
dom A is set
(dom A) --> D is Relation-like dom A -defined Function-like constant total set
[:(dom A),{D}:] is Relation-like set
<:((dom A) --> D),A:> is Relation-like Function-like set
<:((dom A) --> D),A:> (#) i is Relation-like Function-like set
dom (i [;] (D,A)) is set
dom A is countable Element of bool NAT
Seg (len A) is V46() len A -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= len A ) } is set
D is set
{D} is non empty trivial 1 -element set
A is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
rng A is set
[:(rng A),{D}:] is Relation-like set
dom A is countable Element of bool NAT
x is Relation-like Function-like set
dom x is set
x [:] (A,D) is Relation-like Function-like set
dom A is set
(dom A) --> D is Relation-like dom A -defined Function-like constant total set
[:(dom A),{D}:] is Relation-like set
<:A,((dom A) --> D):> is Relation-like Function-like set
<:A,((dom A) --> D):> (#) x is Relation-like Function-like set
dom (x [:] (A,D)) is set
(dom A) --> D is Relation-like dom A -defined {D} -valued Function-like constant total quasi_total Element of bool [:(dom A),{D}:]
[:(dom A),{D}:] is Relation-like set
bool [:(dom A),{D}:] is non empty set
dom ((dom A) --> D) is set
<:A,((dom A) --> D):> is Relation-like Function-like set
dom <:A,((dom A) --> D):> is set
rng ((dom A) --> D) is trivial set
rng <:A,((dom A) --> D):> is set
[:(rng A),(rng ((dom A) --> D)):] is Relation-like set
D is set
{D} is non empty trivial 1 -element set
A is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
rng A is set
[:(rng A),{D}:] is Relation-like set
x is Relation-like Function-like set
dom x is set
x [:] (A,D) is Relation-like Function-like set
dom A is set
(dom A) --> D is Relation-like dom A -defined Function-like constant total set
[:(dom A),{D}:] is Relation-like set
<:A,((dom A) --> D):> is Relation-like Function-like set
<:A,((dom A) --> D):> (#) x is Relation-like Function-like set
dom (x [:] (A,D)) is set
dom A is countable Element of bool NAT
len A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
Seg (len A) is V46() len A -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= len A ) } is set
D is set
{D} is non empty trivial 1 -element set
A is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
rng A is set
[:(rng A),{D}:] is Relation-like set
len A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
x is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
len x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
i is Relation-like Function-like set
dom i is set
i [:] (A,D) is Relation-like Function-like set
dom A is set
(dom A) --> D is Relation-like dom A -defined Function-like constant total set
[:(dom A),{D}:] is Relation-like set
<:A,((dom A) --> D):> is Relation-like Function-like set
<:A,((dom A) --> D):> (#) i is Relation-like Function-like set
dom (i [:] (A,D)) is set
dom A is countable Element of bool NAT
Seg (len A) is V46() len A -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= len A ) } is set
D is non empty set
A is non empty set
[:D,A:] is Relation-like non empty set
x is non empty set
[:[:D,A:],x:] is Relation-like non empty set
bool [:[:D,A:],x:] is non empty set
i is Relation-like [:D,A:] -defined x -valued Function-like non empty total quasi_total Element of bool [:[:D,A:],x:]
i is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of D
e is Relation-like NAT -defined A -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of A
i .: (i,e) is Relation-like Function-like set
<:i,e:> is Relation-like Function-like set
<:i,e:> (#) i is Relation-like x -valued Function-like set
rng (i .: (i,e)) is set
rng i is non empty set
rng i is set
rng e is set
[:(rng i),(rng e):] is Relation-like set
dom i is Relation-like non empty set
D is non empty set
A is non empty set
[:D,A:] is Relation-like non empty set
x is non empty set
[:[:D,A:],x:] is Relation-like non empty set
bool [:[:D,A:],x:] is non empty set
i is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
len i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
i is Relation-like [:D,A:] -defined x -valued Function-like non empty total quasi_total Element of bool [:[:D,A:],x:]
e is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of D
len e is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
a is Relation-like NAT -defined A -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of A
i .: (e,a) is Relation-like Function-like set
<:e,a:> is Relation-like Function-like set
<:e,a:> (#) i is Relation-like x -valued Function-like set
len a is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
min ((len e),(len a)) is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
rng e is set
rng a is set
[:(rng e),(rng a):] is Relation-like set
dom i is Relation-like non empty set
D is non empty set
A is non empty set
[:D,A:] is Relation-like non empty set
x is non empty set
[:[:D,A:],x:] is Relation-like non empty set
bool [:[:D,A:],x:] is non empty set
i is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
len i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
i is Relation-like [:D,A:] -defined x -valued Function-like non empty total quasi_total Element of bool [:[:D,A:],x:]
e is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of D
len e is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
a is Relation-like NAT -defined A -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of A
len a is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
i .: (e,a) is Relation-like Function-like set
<:e,a:> is Relation-like Function-like set
<:e,a:> (#) i is Relation-like x -valued Function-like set
min ((len e),(len a)) is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
D is non empty set
<*> D is Relation-like non-empty empty-yielding NAT -defined D -valued Function-like one-to-one constant functional empty proper Function-yielding V33() V34() V35() V36() V38() V39() V40() V41() ext-real non positive non negative V45() V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable FinSequence of D
[:NAT,D:] is Relation-like non empty V46() set
A is non empty set
[:D,A:] is Relation-like non empty set
<*> A is Relation-like non-empty empty-yielding NAT -defined A -valued Function-like one-to-one constant functional empty proper Function-yielding V33() V34() V35() V36() V38() V39() V40() V41() ext-real non positive non negative V45() V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable FinSequence of A
[:NAT,A:] is Relation-like non empty V46() set
x is non empty set
[:[:D,A:],x:] is Relation-like non empty set
bool [:[:D,A:],x:] is non empty set
<*> x is Relation-like non-empty empty-yielding NAT -defined x -valued Function-like one-to-one constant functional empty proper Function-yielding V33() V34() V35() V36() V38() V39() V40() V41() ext-real non positive non negative V45() V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable FinSequence of x
[:NAT,x:] is Relation-like non empty V46() set
i is Relation-like [:D,A:] -defined x -valued Function-like non empty total quasi_total Element of bool [:[:D,A:],x:]
i is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of D
i .: (i,(<*> A)) is Relation-like Function-like set
<:i,(<*> A):> is Relation-like Function-like set
<:i,(<*> A):> (#) i is Relation-like x -valued Function-like set
e is Relation-like NAT -defined A -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of A
i .: ((<*> D),e) is Relation-like Function-like set
<:(<*> D),e:> is Relation-like Function-like set
<:(<*> D),e:> (#) i is Relation-like x -valued Function-like set
len (<*> D) is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty Function-yielding V33() V34() V35() V36() V38() V39() V40() V41() ext-real non positive non negative V45() V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable Element of NAT
a is Relation-like NAT -defined x -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of x
len a is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
len e is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
min (0,(len e)) is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
b is Relation-like NAT -defined x -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of x
len b is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
len i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
min ((len i),0) is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
D is non empty set
A is non empty set
[:D,A:] is Relation-like non empty set
x is non empty set
[:[:D,A:],x:] is Relation-like non empty set
bool [:[:D,A:],x:] is non empty set
i is Element of D
<*i*> is Relation-like NAT -defined D -valued Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable FinSequence of D
[1,i] is set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
i is Element of A
<*i*> is Relation-like NAT -defined A -valued Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable FinSequence of A
[1,i] is set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
e is Relation-like [:D,A:] -defined x -valued Function-like non empty total quasi_total Element of bool [:[:D,A:],x:]
e . (i,i) is Element of x
<*(e . (i,i))*> is Relation-like NAT -defined x -valued Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable FinSequence of x
[1,(e . (i,i))] is set
{1,(e . (i,i))} is non empty set
{{1,(e . (i,i))},{1}} is non empty set
{[1,(e . (i,i))]} is Relation-like Function-like constant non empty trivial 1 -element set
a is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of D
b is Relation-like NAT -defined A -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of A
e .: (a,b) is Relation-like Function-like set
<:a,b:> is Relation-like Function-like set
<:a,b:> (#) e is Relation-like x -valued Function-like set
a . 1 is set
b . 1 is set
len a is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
len b is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
c is Relation-like NAT -defined x -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of x
len c is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
Seg (len c) is V46() len c -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= len c ) } is set
dom c is countable Element of bool NAT
c . 1 is set
D is non empty set
A is non empty set
[:D,A:] is Relation-like non empty set
x is non empty set
[:[:D,A:],x:] is Relation-like non empty set
bool [:[:D,A:],x:] is non empty set
i is Element of D
i is Element of D
<*i,i*> is Relation-like NAT -defined Function-like non empty V46() 2 -element FinSequence-like FinSubsequence-like countable set
<*i*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,i] is set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
<*i*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,i] is set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
<*i*> ^ <*i*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
e is Element of A
a is Element of A
<*e,a*> is Relation-like NAT -defined Function-like non empty V46() 2 -element FinSequence-like FinSubsequence-like countable set
<*e*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,e] is set
{1,e} is non empty set
{{1,e},{1}} is non empty set
{[1,e]} is Relation-like Function-like constant non empty trivial 1 -element set
<*a*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,a] is set
{1,a} is non empty set
{{1,a},{1}} is non empty set
{[1,a]} is Relation-like Function-like constant non empty trivial 1 -element set
<*e*> ^ <*a*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
b is Relation-like [:D,A:] -defined x -valued Function-like non empty total quasi_total Element of bool [:[:D,A:],x:]
b . (i,e) is Element of x
b . (i,a) is Element of x
<*(b . (i,e)),(b . (i,a))*> is Relation-like NAT -defined Function-like non empty V46() 2 -element FinSequence-like FinSubsequence-like countable set
<*(b . (i,e))*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,(b . (i,e))] is set
{1,(b . (i,e))} is non empty set
{{1,(b . (i,e))},{1}} is non empty set
{[1,(b . (i,e))]} is Relation-like Function-like constant non empty trivial 1 -element set
<*(b . (i,a))*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,(b . (i,a))] is set
{1,(b . (i,a))} is non empty set
{{1,(b . (i,a))},{1}} is non empty set
{[1,(b . (i,a))]} is Relation-like Function-like constant non empty trivial 1 -element set
<*(b . (i,e))*> ^ <*(b . (i,a))*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
c is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of D
r is Relation-like NAT -defined A -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of A
b .: (c,r) is Relation-like Function-like set
<:c,r:> is Relation-like Function-like set
<:c,r:> (#) b is Relation-like x -valued Function-like set
c . 2 is set
r . 2 is set
len c is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
len r is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
p is Relation-like NAT -defined x -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of x
len p is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
Seg (len p) is V46() len p -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= len p ) } is set
dom p is countable Element of bool NAT
p . 2 is set
c . 1 is set
r . 1 is set
p . 1 is set
D is non empty set
A is non empty set
[:D,A:] is Relation-like non empty set
x is non empty set
[:[:D,A:],x:] is Relation-like non empty set
bool [:[:D,A:],x:] is non empty set
i is Element of D
i is Element of D
e is Element of D
<*i,i,e*> is Relation-like NAT -defined Function-like non empty V46() 3 -element FinSequence-like FinSubsequence-like countable set
<*i*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,i] is set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
<*i*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,i] is set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
<*i*> ^ <*i*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
<*e*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,e] is set
{1,e} is non empty set
{{1,e},{1}} is non empty set
{[1,e]} is Relation-like Function-like constant non empty trivial 1 -element set
(<*i*> ^ <*i*>) ^ <*e*> is Relation-like NAT -defined Function-like non empty V46() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like countable set
a is Element of A
b is Element of A
c is Element of A
<*a,b,c*> is Relation-like NAT -defined Function-like non empty V46() 3 -element FinSequence-like FinSubsequence-like countable set
<*a*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,a] is set
{1,a} is non empty set
{{1,a},{1}} is non empty set
{[1,a]} is Relation-like Function-like constant non empty trivial 1 -element set
<*b*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,b] is set
{1,b} is non empty set
{{1,b},{1}} is non empty set
{[1,b]} is Relation-like Function-like constant non empty trivial 1 -element set
<*a*> ^ <*b*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
<*c*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,c] is set
{1,c} is non empty set
{{1,c},{1}} is non empty set
{[1,c]} is Relation-like Function-like constant non empty trivial 1 -element set
(<*a*> ^ <*b*>) ^ <*c*> is Relation-like NAT -defined Function-like non empty V46() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like countable set
r is Relation-like [:D,A:] -defined x -valued Function-like non empty total quasi_total Element of bool [:[:D,A:],x:]
r . (i,a) is Element of x
r . (i,b) is Element of x
r . (e,c) is Element of x
<*(r . (i,a)),(r . (i,b)),(r . (e,c))*> is Relation-like NAT -defined Function-like non empty V46() 3 -element FinSequence-like FinSubsequence-like countable set
<*(r . (i,a))*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,(r . (i,a))] is set
{1,(r . (i,a))} is non empty set
{{1,(r . (i,a))},{1}} is non empty set
{[1,(r . (i,a))]} is Relation-like Function-like constant non empty trivial 1 -element set
<*(r . (i,b))*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,(r . (i,b))] is set
{1,(r . (i,b))} is non empty set
{{1,(r . (i,b))},{1}} is non empty set
{[1,(r . (i,b))]} is Relation-like Function-like constant non empty trivial 1 -element set
<*(r . (i,a))*> ^ <*(r . (i,b))*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
<*(r . (e,c))*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,(r . (e,c))] is set
{1,(r . (e,c))} is non empty set
{{1,(r . (e,c))},{1}} is non empty set
{[1,(r . (e,c))]} is Relation-like Function-like constant non empty trivial 1 -element set
(<*(r . (i,a))*> ^ <*(r . (i,b))*>) ^ <*(r . (e,c))*> is Relation-like NAT -defined Function-like non empty V46() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like countable set
p is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of D
q is Relation-like NAT -defined A -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of A
r .: (p,q) is Relation-like Function-like set
<:p,q:> is Relation-like Function-like set
<:p,q:> (#) r is Relation-like x -valued Function-like set
p . 2 is set
q . 2 is set
len p is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
len q is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
r is Relation-like NAT -defined x -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of x
len r is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
Seg (len r) is V46() len r -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= len r ) } is set
dom r is countable Element of bool NAT
r . 2 is set
p . 3 is set
q . 3 is set
p . 1 is set
q . 1 is set
r . 3 is set
r . 1 is set
D is non empty set
A is non empty set
[:D,A:] is Relation-like non empty set
x is non empty set
[:[:D,A:],x:] is Relation-like non empty set
bool [:[:D,A:],x:] is non empty set
i is Element of D
i is Relation-like [:D,A:] -defined x -valued Function-like non empty total quasi_total Element of bool [:[:D,A:],x:]
e is Relation-like NAT -defined A -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of A
i [;] (i,e) is Relation-like Function-like set
dom e is set
(dom e) --> i is Relation-like dom e -defined D -valued Function-like constant total set
{i} is non empty trivial 1 -element set
[:(dom e),{i}:] is Relation-like set
<:((dom e) --> i),e:> is Relation-like Function-like set
<:((dom e) --> i),e:> (#) i is Relation-like x -valued Function-like set
rng (i [;] (i,e)) is set
rng i is non empty set
rng e is set
{i} is non empty trivial 1 -element Element of bool D
bool D is non empty set
[:{i},(rng e):] is Relation-like set
dom i is Relation-like non empty set
D is non empty set
A is non empty set
[:D,A:] is Relation-like non empty set
x is non empty set
[:[:D,A:],x:] is Relation-like non empty set
bool [:[:D,A:],x:] is non empty set
i is Element of D
i is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
len i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
e is Relation-like [:D,A:] -defined x -valued Function-like non empty total quasi_total Element of bool [:[:D,A:],x:]
a is Relation-like NAT -defined A -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of A
e [;] (i,a) is Relation-like Function-like set
dom a is set
(dom a) --> i is Relation-like dom a -defined D -valued Function-like constant total set
{i} is non empty trivial 1 -element set
[:(dom a),{i}:] is Relation-like set
<:((dom a) --> i),a:> is Relation-like Function-like set
<:((dom a) --> i),a:> (#) e is Relation-like x -valued Function-like set
len a is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
rng a is set
{i} is non empty trivial 1 -element Element of bool D
bool D is non empty set
[:{i},(rng a):] is Relation-like set
dom e is Relation-like non empty set
D is non empty set
A is non empty set
[:D,A:] is Relation-like non empty set
<*> A is Relation-like non-empty empty-yielding NAT -defined A -valued Function-like one-to-one constant functional empty proper Function-yielding V33() V34() V35() V36() V38() V39() V40() V41() ext-real non positive non negative V45() V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable FinSequence of A
[:NAT,A:] is Relation-like non empty V46() set
x is non empty set
[:[:D,A:],x:] is Relation-like non empty set
bool [:[:D,A:],x:] is non empty set
<*> x is Relation-like non-empty empty-yielding NAT -defined x -valued Function-like one-to-one constant functional empty proper Function-yielding V33() V34() V35() V36() V38() V39() V40() V41() ext-real non positive non negative V45() V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable FinSequence of x
[:NAT,x:] is Relation-like non empty V46() set
i is Element of D
i is Relation-like [:D,A:] -defined x -valued Function-like non empty total quasi_total Element of bool [:[:D,A:],x:]
i [;] (i,(<*> A)) is Relation-like Function-like set
dom (<*> A) is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty Function-yielding V33() V34() V35() V36() V38() V39() V40() V41() ext-real non positive non negative V45() V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable set
(dom (<*> A)) --> i is Relation-like non-empty empty-yielding dom (<*> A) -defined D -valued Function-like one-to-one constant functional empty total Function-yielding V33() V34() V35() V36() V38() V39() V40() V41() ext-real non positive non negative V45() V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable set
{i} is non empty trivial 1 -element set
[:(dom (<*> A)),{i}:] is Relation-like set
<:((dom (<*> A)) --> i),(<*> A):> is Relation-like Function-like set
<:((dom (<*> A)) --> i),(<*> A):> (#) i is Relation-like x -valued Function-like set
len (<*> A) is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty Function-yielding V33() V34() V35() V36() V38() V39() V40() V41() ext-real non positive non negative V45() V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable Element of NAT
e is Relation-like NAT -defined x -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of x
len e is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
D is non empty set
A is non empty set
[:D,A:] is Relation-like non empty set
x is non empty set
[:[:D,A:],x:] is Relation-like non empty set
bool [:[:D,A:],x:] is non empty set
i is Element of D
i is Element of A
<*i*> is Relation-like NAT -defined A -valued Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable FinSequence of A
[1,i] is set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
e is Relation-like [:D,A:] -defined x -valued Function-like non empty total quasi_total Element of bool [:[:D,A:],x:]
e . (i,i) is Element of x
<*(e . (i,i))*> is Relation-like NAT -defined x -valued Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable FinSequence of x
[1,(e . (i,i))] is set
{1,(e . (i,i))} is non empty set
{{1,(e . (i,i))},{1}} is non empty set
{[1,(e . (i,i))]} is Relation-like Function-like constant non empty trivial 1 -element set
a is Relation-like NAT -defined A -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of A
e [;] (i,a) is Relation-like Function-like set
dom a is set
(dom a) --> i is Relation-like dom a -defined D -valued Function-like constant total set
{i} is non empty trivial 1 -element set
[:(dom a),{i}:] is Relation-like set
<:((dom a) --> i),a:> is Relation-like Function-like set
<:((dom a) --> i),a:> (#) e is Relation-like x -valued Function-like set
a . 1 is set
len a is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
b is Relation-like NAT -defined x -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of x
len b is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
Seg (len b) is V46() len b -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= len b ) } is set
dom b is countable Element of bool NAT
b . 1 is set
D is non empty set
A is non empty set
[:D,A:] is Relation-like non empty set
x is non empty set
[:[:D,A:],x:] is Relation-like non empty set
bool [:[:D,A:],x:] is non empty set
i is Element of D
i is Element of A
e is Element of A
<*i,e*> is Relation-like NAT -defined Function-like non empty V46() 2 -element FinSequence-like FinSubsequence-like countable set
<*i*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,i] is set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
<*e*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,e] is set
{1,e} is non empty set
{{1,e},{1}} is non empty set
{[1,e]} is Relation-like Function-like constant non empty trivial 1 -element set
<*i*> ^ <*e*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
a is Relation-like [:D,A:] -defined x -valued Function-like non empty total quasi_total Element of bool [:[:D,A:],x:]
a . (i,i) is Element of x
a . (i,e) is Element of x
<*(a . (i,i)),(a . (i,e))*> is Relation-like NAT -defined Function-like non empty V46() 2 -element FinSequence-like FinSubsequence-like countable set
<*(a . (i,i))*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,(a . (i,i))] is set
{1,(a . (i,i))} is non empty set
{{1,(a . (i,i))},{1}} is non empty set
{[1,(a . (i,i))]} is Relation-like Function-like constant non empty trivial 1 -element set
<*(a . (i,e))*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,(a . (i,e))] is set
{1,(a . (i,e))} is non empty set
{{1,(a . (i,e))},{1}} is non empty set
{[1,(a . (i,e))]} is Relation-like Function-like constant non empty trivial 1 -element set
<*(a . (i,i))*> ^ <*(a . (i,e))*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
b is Relation-like NAT -defined A -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of A
a [;] (i,b) is Relation-like Function-like set
dom b is set
(dom b) --> i is Relation-like dom b -defined D -valued Function-like constant total set
{i} is non empty trivial 1 -element set
[:(dom b),{i}:] is Relation-like set
<:((dom b) --> i),b:> is Relation-like Function-like set
<:((dom b) --> i),b:> (#) a is Relation-like x -valued Function-like set
b . 2 is set
len b is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
c is Relation-like NAT -defined x -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of x
len c is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
Seg (len c) is V46() len c -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= len c ) } is set
dom c is countable Element of bool NAT
c . 2 is set
b . 1 is set
c . 1 is set
D is non empty set
A is non empty set
[:D,A:] is Relation-like non empty set
x is non empty set
[:[:D,A:],x:] is Relation-like non empty set
bool [:[:D,A:],x:] is non empty set
i is Element of D
i is Element of A
e is Element of A
a is Element of A
<*i,e,a*> is Relation-like NAT -defined Function-like non empty V46() 3 -element FinSequence-like FinSubsequence-like countable set
<*i*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,i] is set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
<*e*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,e] is set
{1,e} is non empty set
{{1,e},{1}} is non empty set
{[1,e]} is Relation-like Function-like constant non empty trivial 1 -element set
<*i*> ^ <*e*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
<*a*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,a] is set
{1,a} is non empty set
{{1,a},{1}} is non empty set
{[1,a]} is Relation-like Function-like constant non empty trivial 1 -element set
(<*i*> ^ <*e*>) ^ <*a*> is Relation-like NAT -defined Function-like non empty V46() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like countable set
b is Relation-like [:D,A:] -defined x -valued Function-like non empty total quasi_total Element of bool [:[:D,A:],x:]
b . (i,i) is Element of x
b . (i,e) is Element of x
b . (i,a) is Element of x
<*(b . (i,i)),(b . (i,e)),(b . (i,a))*> is Relation-like NAT -defined Function-like non empty V46() 3 -element FinSequence-like FinSubsequence-like countable set
<*(b . (i,i))*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,(b . (i,i))] is set
{1,(b . (i,i))} is non empty set
{{1,(b . (i,i))},{1}} is non empty set
{[1,(b . (i,i))]} is Relation-like Function-like constant non empty trivial 1 -element set
<*(b . (i,e))*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,(b . (i,e))] is set
{1,(b . (i,e))} is non empty set
{{1,(b . (i,e))},{1}} is non empty set
{[1,(b . (i,e))]} is Relation-like Function-like constant non empty trivial 1 -element set
<*(b . (i,i))*> ^ <*(b . (i,e))*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
<*(b . (i,a))*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,(b . (i,a))] is set
{1,(b . (i,a))} is non empty set
{{1,(b . (i,a))},{1}} is non empty set
{[1,(b . (i,a))]} is Relation-like Function-like constant non empty trivial 1 -element set
(<*(b . (i,i))*> ^ <*(b . (i,e))*>) ^ <*(b . (i,a))*> is Relation-like NAT -defined Function-like non empty V46() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like countable set
c is Relation-like NAT -defined A -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of A
b [;] (i,c) is Relation-like Function-like set
dom c is set
(dom c) --> i is Relation-like dom c -defined D -valued Function-like constant total set
{i} is non empty trivial 1 -element set
[:(dom c),{i}:] is Relation-like set
<:((dom c) --> i),c:> is Relation-like Function-like set
<:((dom c) --> i),c:> (#) b is Relation-like x -valued Function-like set
c . 2 is set
len c is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
r is Relation-like NAT -defined x -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of x
len r is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
Seg (len r) is V46() len r -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= len r ) } is set
dom r is countable Element of bool NAT
r . 2 is set
c . 3 is set
c . 1 is set
r . 3 is set
r . 1 is set
D is non empty set
A is non empty set
[:D,A:] is Relation-like non empty set
x is non empty set
[:[:D,A:],x:] is Relation-like non empty set
bool [:[:D,A:],x:] is non empty set
i is Element of A
i is Relation-like [:D,A:] -defined x -valued Function-like non empty total quasi_total Element of bool [:[:D,A:],x:]
e is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of D
i [:] (e,i) is Relation-like Function-like set
dom e is set
(dom e) --> i is Relation-like dom e -defined A -valued Function-like constant total set
{i} is non empty trivial 1 -element set
[:(dom e),{i}:] is Relation-like set
<:e,((dom e) --> i):> is Relation-like Function-like set
<:e,((dom e) --> i):> (#) i is Relation-like x -valued Function-like set
rng (i [:] (e,i)) is set
rng i is non empty set
rng e is set
{i} is non empty trivial 1 -element Element of bool A
bool A is non empty set
[:(rng e),{i}:] is Relation-like set
dom i is Relation-like non empty set
D is non empty set
A is non empty set
[:D,A:] is Relation-like non empty set
x is non empty set
[:[:D,A:],x:] is Relation-like non empty set
bool [:[:D,A:],x:] is non empty set
i is Element of A
i is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
len i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
e is Relation-like [:D,A:] -defined x -valued Function-like non empty total quasi_total Element of bool [:[:D,A:],x:]
a is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of D
e [:] (a,i) is Relation-like Function-like set
dom a is set
(dom a) --> i is Relation-like dom a -defined A -valued Function-like constant total set
{i} is non empty trivial 1 -element set
[:(dom a),{i}:] is Relation-like set
<:a,((dom a) --> i):> is Relation-like Function-like set
<:a,((dom a) --> i):> (#) e is Relation-like x -valued Function-like set
len a is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
rng a is set
{i} is non empty trivial 1 -element Element of bool A
bool A is non empty set
[:(rng a),{i}:] is Relation-like set
dom e is Relation-like non empty set
D is non empty set
<*> D is Relation-like non-empty empty-yielding NAT -defined D -valued Function-like one-to-one constant functional empty proper Function-yielding V33() V34() V35() V36() V38() V39() V40() V41() ext-real non positive non negative V45() V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable FinSequence of D
[:NAT,D:] is Relation-like non empty V46() set
A is non empty set
[:D,A:] is Relation-like non empty set
x is non empty set
[:[:D,A:],x:] is Relation-like non empty set
bool [:[:D,A:],x:] is non empty set
<*> x is Relation-like non-empty empty-yielding NAT -defined x -valued Function-like one-to-one constant functional empty proper Function-yielding V33() V34() V35() V36() V38() V39() V40() V41() ext-real non positive non negative V45() V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable FinSequence of x
[:NAT,x:] is Relation-like non empty V46() set
i is Element of A
i is Relation-like [:D,A:] -defined x -valued Function-like non empty total quasi_total Element of bool [:[:D,A:],x:]
i [:] ((<*> D),i) is Relation-like Function-like set
dom (<*> D) is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty Function-yielding V33() V34() V35() V36() V38() V39() V40() V41() ext-real non positive non negative V45() V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable set
(dom (<*> D)) --> i is Relation-like non-empty empty-yielding dom (<*> D) -defined A -valued Function-like one-to-one constant functional empty total Function-yielding V33() V34() V35() V36() V38() V39() V40() V41() ext-real non positive non negative V45() V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable set
{i} is non empty trivial 1 -element set
[:(dom (<*> D)),{i}:] is Relation-like set
<:(<*> D),((dom (<*> D)) --> i):> is Relation-like Function-like set
<:(<*> D),((dom (<*> D)) --> i):> (#) i is Relation-like x -valued Function-like set
len (<*> D) is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty Function-yielding V33() V34() V35() V36() V38() V39() V40() V41() ext-real non positive non negative V45() V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable Element of NAT
e is Relation-like NAT -defined x -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of x
len e is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
D is non empty set
A is non empty set
[:D,A:] is Relation-like non empty set
x is non empty set
[:[:D,A:],x:] is Relation-like non empty set
bool [:[:D,A:],x:] is non empty set
i is Element of D
<*i*> is Relation-like NAT -defined D -valued Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable FinSequence of D
[1,i] is set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
i is Element of A
e is Relation-like [:D,A:] -defined x -valued Function-like non empty total quasi_total Element of bool [:[:D,A:],x:]
e . (i,i) is Element of x
<*(e . (i,i))*> is Relation-like NAT -defined x -valued Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable FinSequence of x
[1,(e . (i,i))] is set
{1,(e . (i,i))} is non empty set
{{1,(e . (i,i))},{1}} is non empty set
{[1,(e . (i,i))]} is Relation-like Function-like constant non empty trivial 1 -element set
a is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of D
e [:] (a,i) is Relation-like Function-like set
dom a is set
(dom a) --> i is Relation-like dom a -defined A -valued Function-like constant total set
{i} is non empty trivial 1 -element set
[:(dom a),{i}:] is Relation-like set
<:a,((dom a) --> i):> is Relation-like Function-like set
<:a,((dom a) --> i):> (#) e is Relation-like x -valued Function-like set
a . 1 is set
len a is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
b is Relation-like NAT -defined x -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of x
len b is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
Seg (len b) is V46() len b -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= len b ) } is set
dom b is countable Element of bool NAT
b . 1 is set
D is non empty set
A is non empty set
[:D,A:] is Relation-like non empty set
x is non empty set
[:[:D,A:],x:] is Relation-like non empty set
bool [:[:D,A:],x:] is non empty set
i is Element of D
i is Element of D
<*i,i*> is Relation-like NAT -defined Function-like non empty V46() 2 -element FinSequence-like FinSubsequence-like countable set
<*i*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,i] is set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
<*i*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,i] is set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
<*i*> ^ <*i*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
e is Element of A
a is Relation-like [:D,A:] -defined x -valued Function-like non empty total quasi_total Element of bool [:[:D,A:],x:]
a . (i,e) is Element of x
a . (i,e) is Element of x
<*(a . (i,e)),(a . (i,e))*> is Relation-like NAT -defined Function-like non empty V46() 2 -element FinSequence-like FinSubsequence-like countable set
<*(a . (i,e))*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,(a . (i,e))] is set
{1,(a . (i,e))} is non empty set
{{1,(a . (i,e))},{1}} is non empty set
{[1,(a . (i,e))]} is Relation-like Function-like constant non empty trivial 1 -element set
<*(a . (i,e))*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,(a . (i,e))] is set
{1,(a . (i,e))} is non empty set
{{1,(a . (i,e))},{1}} is non empty set
{[1,(a . (i,e))]} is Relation-like Function-like constant non empty trivial 1 -element set
<*(a . (i,e))*> ^ <*(a . (i,e))*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
b is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of D
a [:] (b,e) is Relation-like Function-like set
dom b is set
(dom b) --> e is Relation-like dom b -defined A -valued Function-like constant total set
{e} is non empty trivial 1 -element set
[:(dom b),{e}:] is Relation-like set
<:b,((dom b) --> e):> is Relation-like Function-like set
<:b,((dom b) --> e):> (#) a is Relation-like x -valued Function-like set
b . 2 is set
len b is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
c is Relation-like NAT -defined x -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of x
len c is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
Seg (len c) is V46() len c -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= len c ) } is set
dom c is countable Element of bool NAT
c . 2 is set
b . 1 is set
c . 1 is set
D is non empty set
A is non empty set
[:D,A:] is Relation-like non empty set
x is non empty set
[:[:D,A:],x:] is Relation-like non empty set
bool [:[:D,A:],x:] is non empty set
i is Element of D
i is Element of D
e is Element of D
<*i,i,e*> is Relation-like NAT -defined Function-like non empty V46() 3 -element FinSequence-like FinSubsequence-like countable set
<*i*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,i] is set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
<*i*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,i] is set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
<*i*> ^ <*i*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
<*e*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,e] is set
{1,e} is non empty set
{{1,e},{1}} is non empty set
{[1,e]} is Relation-like Function-like constant non empty trivial 1 -element set
(<*i*> ^ <*i*>) ^ <*e*> is Relation-like NAT -defined Function-like non empty V46() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like countable set
a is Element of A
b is Relation-like [:D,A:] -defined x -valued Function-like non empty total quasi_total Element of bool [:[:D,A:],x:]
b . (i,a) is Element of x
b . (i,a) is Element of x
b . (e,a) is Element of x
<*(b . (i,a)),(b . (i,a)),(b . (e,a))*> is Relation-like NAT -defined Function-like non empty V46() 3 -element FinSequence-like FinSubsequence-like countable set
<*(b . (i,a))*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,(b . (i,a))] is set
{1,(b . (i,a))} is non empty set
{{1,(b . (i,a))},{1}} is non empty set
{[1,(b . (i,a))]} is Relation-like Function-like constant non empty trivial 1 -element set
<*(b . (i,a))*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,(b . (i,a))] is set
{1,(b . (i,a))} is non empty set
{{1,(b . (i,a))},{1}} is non empty set
{[1,(b . (i,a))]} is Relation-like Function-like constant non empty trivial 1 -element set
<*(b . (i,a))*> ^ <*(b . (i,a))*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
<*(b . (e,a))*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,(b . (e,a))] is set
{1,(b . (e,a))} is non empty set
{{1,(b . (e,a))},{1}} is non empty set
{[1,(b . (e,a))]} is Relation-like Function-like constant non empty trivial 1 -element set
(<*(b . (i,a))*> ^ <*(b . (i,a))*>) ^ <*(b . (e,a))*> is Relation-like NAT -defined Function-like non empty V46() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like countable set
c is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of D
b [:] (c,a) is Relation-like Function-like set
dom c is set
(dom c) --> a is Relation-like dom c -defined A -valued Function-like constant total set
{a} is non empty trivial 1 -element set
[:(dom c),{a}:] is Relation-like set
<:c,((dom c) --> a):> is Relation-like Function-like set
<:c,((dom c) --> a):> (#) b is Relation-like x -valued Function-like set
c . 2 is set
len c is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
r is Relation-like NAT -defined x -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of x
len r is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
Seg (len r) is V46() len r -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= len r ) } is set
dom r is countable Element of bool NAT
r . 2 is set
c . 3 is set
c . 1 is set
r . 3 is set
r . 1 is set
D is set
D * is functional non empty FinSequence-membered set
A is set
D is set
A is (D)
x is Element of A
<*> D is Relation-like non-empty empty-yielding NAT -defined D -valued Function-like one-to-one constant functional empty Function-yielding V33() V34() V35() V36() V38() V39() V40() V41() ext-real non positive non negative V45() V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable FinSequence of D
x is Element of A
D is set
[:NAT,D:] is Relation-like set
bool [:NAT,D:] is non empty set
<*> D is Relation-like non-empty empty-yielding NAT -defined D -valued Function-like one-to-one constant functional empty Function-yielding V33() V34() V35() V36() V38() V39() V40() V41() ext-real non positive non negative V45() V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable FinSequence of D
{(<*> D)} is functional non empty trivial 1 -element with_common_domain Element of bool (bool [:NAT,D:])
bool (bool [:NAT,D:]) is non empty set
A is set
D is set
D * is functional non empty FinSequence-membered set
A is set
D is set
D * is functional non empty FinSequence-membered set
D is set
(D) is functional non empty FinSequence-membered (D)
A is (D)
x is set
D is non empty set
bool D is non empty set
A is Element of bool D
x is (A)
i is set
i is Relation-like NAT -defined A -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of A
rng i is set
A is non empty set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
the Element of A is Element of A
(D, the Element of A) is Relation-like NAT -defined Function-like V46() D -element FinSequence-like FinSubsequence-like countable set
Seg D is V46() D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
(Seg D) --> the Element of A is Relation-like Seg D -defined Seg D -defined A -valued { the Element of A} -valued Function-like constant total total quasi_total V46() FinSequence-like FinSubsequence-like countable Element of bool [:(Seg D),{ the Element of A}:]
{ the Element of A} is non empty trivial 1 -element set
[:(Seg D),{ the Element of A}:] is Relation-like set
bool [:(Seg D),{ the Element of A}:] is non empty set
[:NAT,A:] is Relation-like non empty V46() set
bool [:NAT,A:] is non empty V46() set
A is set
(A) is functional non empty FinSequence-membered (A)
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
{ b₁ where b₁ is Relation-like NAT -defined A -valued Function-like V46() FinSequence-like FinSubsequence-like countable (A,(A)) : len b₁ = D } is set
x is set
i is Relation-like NAT -defined A -valued Function-like V46() FinSequence-like FinSubsequence-like countable (A,(A))
len i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
A is non empty set
(D,A) is (A)
(A) is functional non empty FinSequence-membered (A)
{ b₁ where b₁ is Relation-like NAT -defined A -valued Function-like V46() FinSequence-like FinSubsequence-like countable (A,(A)) : len b₁ = D } is set
the Element of A is Element of A
(D, the Element of A) is Relation-like NAT -defined Function-like V46() D -element FinSequence-like FinSubsequence-like countable set
Seg D is V46() D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
(Seg D) --> the Element of A is Relation-like Seg D -defined Seg D -defined A -valued { the Element of A} -valued Function-like constant total total quasi_total V46() FinSequence-like FinSubsequence-like countable Element of bool [:(Seg D),{ the Element of A}:]
{ the Element of A} is non empty trivial 1 -element set
[:(Seg D),{ the Element of A}:] is Relation-like set
bool [:(Seg D),{ the Element of A}:] is non empty set
i is Relation-like NAT -defined A -valued Function-like V46() FinSequence-like FinSubsequence-like countable (A,(A))
len i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
D is non empty set
A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
(A,D) is non empty (D)
(D) is functional non empty FinSequence-membered (D)
{ b₁ where b₁ is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable (D,(D)) : len b₁ = A } is set
x is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable (D,(A,D))
len x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
i is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable (D,(D))
len i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
D is set
A is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of D
len A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
((len A),D) is (D)
(D) is functional non empty FinSequence-membered (D)
{ b₁ where b₁ is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable (D,(D)) : len b₁ = len A } is set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
Seg D is V46() D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
A is set
(D,A) is (A)
(A) is functional non empty FinSequence-membered (A)
{ b₁ where b₁ is Relation-like NAT -defined A -valued Function-like V46() FinSequence-like FinSubsequence-like countable (A,(A)) : len b₁ = D } is set
Funcs ((Seg D),A) is functional set
i is set
i is Relation-like NAT -defined A -valued Function-like V46() FinSequence-like FinSubsequence-like countable (A,(A))
len i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
rng i is set
dom i is countable Element of bool NAT
x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
Seg x is V46() x -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= x ) } is set
i is Relation-like Function-like set
dom i is set
rng i is set
e is Relation-like NAT -defined A -valued Function-like V46() FinSequence-like FinSubsequence-like countable (A,(A))
len e is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
D is set
(0,D) is (D)
(D) is functional non empty FinSequence-membered (D)
{ b₁ where b₁ is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable (D,(D)) : len b₁ = 0 } is set
[:NAT,D:] is Relation-like set
bool [:NAT,D:] is non empty set
<*> D is Relation-like non-empty empty-yielding NAT -defined D -valued Function-like one-to-one constant functional empty Function-yielding V33() V34() V35() V36() V38() V39() V40() V41() ext-real non positive non negative V45() V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable FinSequence of D
{(<*> D)} is functional non empty trivial 1 -element with_common_domain Element of bool (bool [:NAT,D:])
bool (bool [:NAT,D:]) is non empty set
A is set
x is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable (D,(D))
len x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
len (<*> D) is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty Function-yielding V33() V34() V35() V36() V38() V39() V40() V41() ext-real non positive non negative V45() V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable Element of NAT
A is non empty set
[:NAT,A:] is Relation-like non empty V46() set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
e is non empty set
[:NAT,e:] is Relation-like non empty V46() set
i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
x is Relation-like non-empty empty-yielding NAT -defined A -valued Function-like one-to-one constant functional empty proper Function-yielding V33() V34() V35() V36() V38() V39() V40() V41() ext-real non positive non negative V45() V46() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable FinSequence of A
i is Relation-like NAT -defined A -valued Function-like V46() D -element FinSequence-like FinSubsequence-like countable FinSequence of A
x ^ i is Relation-like NAT -defined A -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of A
b is Relation-like NAT -defined e -valued Function-like V46() i -element FinSequence-like FinSubsequence-like countable FinSequence of e
a is Relation-like non-empty empty-yielding NAT -defined e -valued Function-like one-to-one constant functional empty proper Function-yielding V33() V34() V35() V36() V38() V39() V40() V41() ext-real non positive non negative V45() V46() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable FinSequence of e
b ^ a is Relation-like NAT -defined e -valued Function-like V46() i + 0 -element FinSequence-like FinSubsequence-like countable FinSequence of e
i + 0 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
D is non empty set
(1,D) is non empty (D)
(D) is functional non empty FinSequence-membered (D)
{ b₁ where b₁ is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable (D,(D)) : len b₁ = 1 } is set
{ <*b₁*> where b₁ is Element of D : verum } is set
A is set
x is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable (D,(D))
len x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
dom x is countable Element of bool NAT
x . 1 is set
i is Element of D
<*i*> is Relation-like NAT -defined D -valued Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable FinSequence of D
[1,i] is set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
x is Element of D
<*x*> is Relation-like NAT -defined D -valued Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable FinSequence of D
[1,x] is set
{1,x} is non empty set
{{1,x},{1}} is non empty set
{[1,x]} is Relation-like Function-like constant non empty trivial 1 -element set
len <*x*> is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
A is non empty set
(D,A) is non empty (A)
(A) is functional non empty FinSequence-membered (A)
{ b₁ where b₁ is Relation-like NAT -defined A -valued Function-like V46() FinSequence-like FinSubsequence-like countable (A,(A)) : len b₁ = D } is set
x is Relation-like NAT -defined A -valued Function-like V46() D -element FinSequence-like FinSubsequence-like countable FinSequence of A
len x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
D is non empty set
A is Relation-like NAT -defined D -valued Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable FinSequence of D
(1,D) is non empty (D)
(D) is functional non empty FinSequence-membered (D)
{ b₁ where b₁ is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable (D,(D)) : len b₁ = 1 } is set
{ <*b₁*> where b₁ is Element of D : verum } is set
D is non empty set
(1,D) is non empty (D)
(D) is functional non empty FinSequence-membered (D)
{ b₁ where b₁ is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable (D,(D)) : len b₁ = 1 } is set
A is Element of D
<*A*> is Relation-like NAT -defined D -valued Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable FinSequence of D
[1,A] is set
{1,A} is non empty set
{{1,A},{1}} is non empty set
{[1,A]} is Relation-like Function-like constant non empty trivial 1 -element set
{ <*b₁*> where b₁ is Element of D : verum } is set
D is non empty set
(2,D) is non empty (D)
(D) is functional non empty FinSequence-membered (D)
{ b₁ where b₁ is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable (D,(D)) : len b₁ = 2 } is set
{ <*b₁,b₂*> where b₁, b₂ is Element of D : verum } is set
A is set
x is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable (D,(D))
len x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
dom x is countable Element of bool NAT
x . 1 is set
x . 2 is set
i is Element of D
i is Element of D
<*i,i*> is Relation-like NAT -defined Function-like non empty V46() 2 -element FinSequence-like FinSubsequence-like countable set
<*i*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,i] is set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
<*i*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,i] is set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
<*i*> ^ <*i*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
x is Element of D
i is Element of D
<*x,i*> is Relation-like NAT -defined Function-like non empty V46() 2 -element FinSequence-like FinSubsequence-like countable set
<*x*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,x] is set
{1,x} is non empty set
{{1,x},{1}} is non empty set
{[1,x]} is Relation-like Function-like constant non empty trivial 1 -element set
<*i*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,i] is set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
<*x*> ^ <*i*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
len <*x,i*> is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
D is non empty set
A is Relation-like NAT -defined D -valued Function-like V46() 2 -element FinSequence-like FinSubsequence-like countable FinSequence of D
(D) is functional non empty FinSequence-membered (D)
len A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
(2,D) is non empty (D)
{ b₁ where b₁ is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable (D,(D)) : len b₁ = 2 } is set
{ <*b₁,b₂*> where b₁, b₂ is Element of D : verum } is set
D is non empty set
(2,D) is non empty (D)
(D) is functional non empty FinSequence-membered (D)
{ b₁ where b₁ is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable (D,(D)) : len b₁ = 2 } is set
A is Element of D
x is Element of D
<*A,x*> is Relation-like NAT -defined Function-like non empty V46() 2 -element FinSequence-like FinSubsequence-like countable set
<*A*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,A] is set
{1,A} is non empty set
{{1,A},{1}} is non empty set
{[1,A]} is Relation-like Function-like constant non empty trivial 1 -element set
<*x*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,x] is set
{1,x} is non empty set
{{1,x},{1}} is non empty set
{[1,x]} is Relation-like Function-like constant non empty trivial 1 -element set
<*A*> ^ <*x*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
{ <*b₁,b₂*> where b₁, b₂ is Element of D : verum } is set
D is non empty set
(3,D) is non empty (D)
(D) is functional non empty FinSequence-membered (D)
{ b₁ where b₁ is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable (D,(D)) : len b₁ = 3 } is set
{ <*b₁,b₂,b₃*> where b₁, b₂, b₃ is Element of D : verum } is set
A is set
x is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable (D,(D))
len x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
dom x is countable Element of bool NAT
x . 1 is set
x . 2 is set
x . 3 is set
i is Element of D
i is Element of D
e is Element of D
<*i,i,e*> is Relation-like NAT -defined Function-like non empty V46() 3 -element FinSequence-like FinSubsequence-like countable set
<*i*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,i] is set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
<*i*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,i] is set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
<*i*> ^ <*i*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
<*e*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,e] is set
{1,e} is non empty set
{{1,e},{1}} is non empty set
{[1,e]} is Relation-like Function-like constant non empty trivial 1 -element set
(<*i*> ^ <*i*>) ^ <*e*> is Relation-like NAT -defined Function-like non empty V46() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like countable set
x is Element of D
i is Element of D
i is Element of D
<*x,i,i*> is Relation-like NAT -defined Function-like non empty V46() 3 -element FinSequence-like FinSubsequence-like countable set
<*x*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,x] is set
{1,x} is non empty set
{{1,x},{1}} is non empty set
{[1,x]} is Relation-like Function-like constant non empty trivial 1 -element set
<*i*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,i] is set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
<*x*> ^ <*i*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
<*i*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,i] is set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
(<*x*> ^ <*i*>) ^ <*i*> is Relation-like NAT -defined Function-like non empty V46() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like countable set
len <*x,i,i*> is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
D is non empty set
A is Relation-like NAT -defined D -valued Function-like V46() 3 -element FinSequence-like FinSubsequence-like countable FinSequence of D
(D) is functional non empty FinSequence-membered (D)
len A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
(3,D) is non empty (D)
{ b₁ where b₁ is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable (D,(D)) : len b₁ = 3 } is set
{ <*b₁,b₂,b₃*> where b₁, b₂, b₃ is Element of D : verum } is set
D is non empty set
(3,D) is non empty (D)
(D) is functional non empty FinSequence-membered (D)
{ b₁ where b₁ is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable (D,(D)) : len b₁ = 3 } is set
A is Element of D
x is Element of D
i is Element of D
<*A,x,i*> is Relation-like NAT -defined Function-like non empty V46() 3 -element FinSequence-like FinSubsequence-like countable set
<*A*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,A] is set
{1,A} is non empty set
{{1,A},{1}} is non empty set
{[1,A]} is Relation-like Function-like constant non empty trivial 1 -element set
<*x*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,x] is set
{1,x} is non empty set
{{1,x},{1}} is non empty set
{[1,x]} is Relation-like Function-like constant non empty trivial 1 -element set
<*A*> ^ <*x*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
<*i*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,i] is set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
(<*A*> ^ <*x*>) ^ <*i*> is Relation-like NAT -defined Function-like non empty V46() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like countable set
{ <*b₁,b₂,b₃*> where b₁, b₂, b₃ is Element of D : verum } is set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
D + A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
x is non empty set
((D + A),x) is non empty (x)
(x) is functional non empty FinSequence-membered (x)
{ b₁ where b₁ is Relation-like NAT -defined x -valued Function-like V46() FinSequence-like FinSubsequence-like countable (x,(x)) : len b₁ = D + A } is set
{ (b₁ ^ b₂) where b₁ is Relation-like NAT -defined x -valued Function-like V46() D -element FinSequence-like FinSubsequence-like countable FinSequence of x, b₂ is Relation-like NAT -defined x -valued Function-like V46() A -element FinSequence-like FinSubsequence-like countable FinSequence of x : verum } is set
i is set
e is Relation-like NAT -defined x -valued Function-like V46() FinSequence-like FinSubsequence-like countable (x,(x))
len e is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
a is Relation-like NAT -defined x -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of x
len a is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
b is Relation-like NAT -defined x -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of x
len b is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
a ^ b is Relation-like NAT -defined x -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of x
e is Relation-like NAT -defined x -valued Function-like V46() D -element FinSequence-like FinSubsequence-like countable FinSequence of x
a is Relation-like NAT -defined x -valued Function-like V46() A -element FinSequence-like FinSubsequence-like countable FinSequence of x
e ^ a is Relation-like NAT -defined x -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of x
len e is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
len a is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
len (e ^ a) is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
D + A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
x is non empty set
(D,x) is non empty (x)
(x) is functional non empty FinSequence-membered (x)
{ b₁ where b₁ is Relation-like NAT -defined x -valued Function-like V46() FinSequence-like FinSubsequence-like countable (x,(x)) : len b₁ = D } is set
(A,x) is non empty (x)
{ b₁ where b₁ is Relation-like NAT -defined x -valued Function-like V46() FinSequence-like FinSubsequence-like countable (x,(x)) : len b₁ = A } is set
i is Relation-like NAT -defined x -valued Function-like V46() D + A -element FinSequence-like FinSubsequence-like countable FinSequence of x
len i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
((D + A),x) is non empty (x)
{ b₁ where b₁ is Relation-like NAT -defined x -valued Function-like V46() FinSequence-like FinSubsequence-like countable (x,(x)) : len b₁ = D + A } is set
{ (b₁ ^ b₂) where b₁ is Relation-like NAT -defined x -valued Function-like V46() D -element FinSequence-like FinSubsequence-like countable FinSequence of x, b₂ is Relation-like NAT -defined x -valued Function-like V46() A -element FinSequence-like FinSubsequence-like countable FinSequence of x : verum } is set
i is Relation-like NAT -defined x -valued Function-like V46() D -element FinSequence-like FinSubsequence-like countable FinSequence of x
e is Relation-like NAT -defined x -valued Function-like V46() A -element FinSequence-like FinSubsequence-like countable FinSequence of x
i ^ e is Relation-like NAT -defined x -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of x
a is Relation-like NAT -defined x -valued Function-like V46() D -element FinSequence-like FinSubsequence-like countable (x,(D,x))
b is Relation-like NAT -defined x -valued Function-like V46() A -element FinSequence-like FinSubsequence-like countable (x,(A,x))
a ^ b is Relation-like NAT -defined x -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of x
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
D + A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
x is non empty set
i is Relation-like NAT -defined x -valued Function-like V46() D -element FinSequence-like FinSubsequence-like countable FinSequence of x
i is Relation-like NAT -defined x -valued Function-like V46() A -element FinSequence-like FinSubsequence-like countable FinSequence of x
i ^ i is Relation-like NAT -defined x -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of x
{ (b₁ ^ b₂) where b₁ is Relation-like NAT -defined x -valued Function-like V46() D -element FinSequence-like FinSubsequence-like countable FinSequence of x, b₂ is Relation-like NAT -defined x -valued Function-like V46() A -element FinSequence-like FinSubsequence-like countable FinSequence of x : verum } is set
((D + A),x) is non empty (x)
(x) is functional non empty FinSequence-membered (x)
{ b₁ where b₁ is Relation-like NAT -defined x -valued Function-like V46() FinSequence-like FinSubsequence-like countable (x,(x)) : len b₁ = D + A } is set
D is non empty set
(D) is functional non empty FinSequence-membered (D)
{ (b₁,D) where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : verum } is set
union { (b₁,D) where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : verum } is set
A is set
x is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of D
len x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
((len x),D) is non empty (D)
{ b₁ where b₁ is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable (D,(D)) : len b₁ = len x } is set
x is set
i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
(i,D) is non empty (D)
{ b₁ where b₁ is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable (D,(D)) : len b₁ = i } is set
i is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable (D,(D))
len i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
A is non empty set
bool A is non empty set
(D,A) is non empty (A)
(A) is functional non empty FinSequence-membered (A)
{ b₁ where b₁ is Relation-like NAT -defined A -valued Function-like V46() FinSequence-like FinSubsequence-like countable (A,(A)) : len b₁ = D } is set
x is non empty Element of bool A
i is Relation-like NAT -defined x -valued Function-like V46() D -element FinSequence-like FinSubsequence-like countable FinSequence of x
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
A is set
x is set
(D,x) is (x)
(x) is functional non empty FinSequence-membered (x)
{ b₁ where b₁ is Relation-like NAT -defined x -valued Function-like V46() FinSequence-like FinSubsequence-like countable (x,(x)) : len b₁ = D } is set
i is Relation-like NAT -defined x -valued Function-like V46() FinSequence-like FinSubsequence-like countable (x,(x))
len i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
x is set
(A,x) is (x)
(x) is functional non empty FinSequence-membered (x)
{ b₁ where b₁ is Relation-like NAT -defined x -valued Function-like V46() FinSequence-like FinSubsequence-like countable (x,(x)) : len b₁ = A } is set
i is non empty set
(D,i) is non empty (i)
(i) is functional non empty FinSequence-membered (i)
{ b₁ where b₁ is Relation-like NAT -defined i -valued Function-like V46() FinSequence-like FinSubsequence-like countable (i,(i)) : len b₁ = D } is set
the Element of i is Element of i
(D, the Element of i) is Relation-like NAT -defined Function-like V46() D -element FinSequence-like FinSubsequence-like countable set
Seg D is V46() D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
(Seg D) --> the Element of i is Relation-like Seg D -defined Seg D -defined i -valued { the Element of i} -valued Function-like constant total total quasi_total V46() FinSequence-like FinSubsequence-like countable Element of bool [:(Seg D),{ the Element of i}:]
{ the Element of i} is non empty trivial 1 -element set
[:(Seg D),{ the Element of i}:] is Relation-like set
bool [:(Seg D),{ the Element of i}:] is non empty set
len (D, the Element of i) is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
(D) is Relation-like NAT -defined Function-like V46() D -element FinSequence-like FinSubsequence-like countable set
Seg D is V46() D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
id (Seg D) is Relation-like Seg D -defined Seg D -valued V6() V8() V9() V13() Function-like one-to-one total quasi_total onto bijective Element of bool [:(Seg D),(Seg D):]
[:(Seg D),(Seg D):] is Relation-like set
bool [:(Seg D),(Seg D):] is non empty set
(D,NAT) is non empty ( NAT )
(NAT) is functional non empty FinSequence-membered ( NAT )
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like V46() FinSequence-like FinSubsequence-like countable ( NAT ,(NAT)) : len b₁ = D } is set
len (D) is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
A is non empty set
(D,A) is non empty (A)
(A) is functional non empty FinSequence-membered (A)
{ b₁ where b₁ is Relation-like NAT -defined A -valued Function-like V46() FinSequence-like FinSubsequence-like countable (A,(A)) : len b₁ = D } is set
x is Element of A
(D,x) is Relation-like NAT -defined Function-like V46() D -element FinSequence-like FinSubsequence-like countable set
Seg D is V46() D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
(Seg D) --> x is Relation-like Seg D -defined Seg D -defined A -valued {x} -valued Function-like constant total total quasi_total V46() FinSequence-like FinSubsequence-like countable Element of bool [:(Seg D),{x}:]
{x} is non empty trivial 1 -element set
[:(Seg D),{x}:] is Relation-like set
bool [:(Seg D),{x}:] is non empty set
len (D,x) is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
A is non empty set
x is non empty set
[:A,x:] is Relation-like non empty set
bool [:A,x:] is non empty set
(D,x) is non empty (x)
(x) is functional non empty FinSequence-membered (x)
{ b₁ where b₁ is Relation-like NAT -defined x -valued Function-like V46() FinSequence-like FinSubsequence-like countable (x,(x)) : len b₁ = D } is set
i is Relation-like NAT -defined A -valued Function-like V46() D -element FinSequence-like FinSubsequence-like countable FinSequence of A
i is Relation-like A -defined x -valued Function-like non empty total quasi_total Element of bool [:A,x:]
i * i is Relation-like NAT -defined x -valued Function-like Element of bool [:NAT,x:]
[:NAT,x:] is Relation-like non empty V46() set
bool [:NAT,x:] is non empty V46() set
len i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
e is Relation-like NAT -defined x -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of x
len e is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
Seg D is V46() D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
[:(Seg D),(Seg D):] is Relation-like set
bool [:(Seg D),(Seg D):] is non empty set
A is non empty set
(D,A) is non empty (A)
(A) is functional non empty FinSequence-membered (A)
{ b₁ where b₁ is Relation-like NAT -defined A -valued Function-like V46() FinSequence-like FinSubsequence-like countable (A,(A)) : len b₁ = D } is set
x is Relation-like NAT -defined A -valued Function-like V46() D -element FinSequence-like FinSubsequence-like countable FinSequence of A
i is Relation-like Seg D -defined Seg D -valued Function-like total quasi_total Element of bool [:(Seg D),(Seg D):]
rng i is set
x * i is Relation-like Seg D -defined A -valued Function-like Element of bool [:(Seg D),A:]
[:(Seg D),A:] is Relation-like set
bool [:(Seg D),A:] is non empty set
len x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
dom x is D -element countable Element of bool NAT
i is Relation-like NAT -defined A -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of A
len i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
Seg D is V46() D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
[:(Seg D),(Seg D):] is Relation-like set
bool [:(Seg D),(Seg D):] is non empty set
A is non empty set
x is Relation-like NAT -defined A -valued Function-like V46() D -element FinSequence-like FinSubsequence-like countable FinSequence of A
i is Relation-like Seg D -defined Seg D -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(Seg D),(Seg D):]
x * i is Relation-like Seg D -defined A -valued Function-like Element of bool [:(Seg D),A:]
[:(Seg D),A:] is Relation-like set
bool [:(Seg D),A:] is non empty set
rng i is set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
D + 1 is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
A is non empty set
x is Relation-like NAT -defined A -valued Function-like V46() D -element FinSequence-like FinSubsequence-like countable FinSequence of A
i is Element of A
<*i*> is Relation-like NAT -defined A -valued Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable FinSequence of A
[1,i] is set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
x ^ <*i*> is Relation-like NAT -defined A -valued Function-like non empty V46() D + 1 -element FinSequence-like FinSubsequence-like countable FinSequence of A
(x ^ <*i*>) . (D + 1) is set
len x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
D + 1 is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
A is non empty set
(D,A) is non empty (A)
(A) is functional non empty FinSequence-membered (A)
{ b₁ where b₁ is Relation-like NAT -defined A -valued Function-like V46() FinSequence-like FinSubsequence-like countable (A,(A)) : len b₁ = D } is set
x is Relation-like NAT -defined A -valued Function-like V46() D + 1 -element FinSequence-like FinSubsequence-like countable FinSequence of A
(1,A) is non empty (A)
{ b₁ where b₁ is Relation-like NAT -defined A -valued Function-like V46() FinSequence-like FinSubsequence-like countable (A,(A)) : len b₁ = 1 } is set
i is Relation-like NAT -defined A -valued Function-like V46() D -element FinSequence-like FinSubsequence-like countable (A,(D,A))
i is Relation-like NAT -defined A -valued Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable (A,(1,A))
i ^ i is Relation-like NAT -defined A -valued Function-like non empty V46() D + 1 -element FinSequence-like FinSubsequence-like countable FinSequence of A
e is Element of A
<*e*> is Relation-like NAT -defined A -valued Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable FinSequence of A
[1,e] is set
{1,e} is non empty set
{{1,e},{1}} is non empty set
{[1,e]} is Relation-like Function-like constant non empty trivial 1 -element set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
(D) is Relation-like NAT -defined Function-like V46() D -element FinSequence-like FinSubsequence-like countable set
Seg D is V46() D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
id (Seg D) is Relation-like Seg D -defined Seg D -valued V6() V8() V9() V13() Function-like one-to-one total quasi_total onto bijective Element of bool [:(Seg D),(Seg D):]
[:(Seg D),(Seg D):] is Relation-like set
bool [:(Seg D),(Seg D):] is non empty set
A is non empty set
x is Relation-like NAT -defined A -valued Function-like V46() D -element FinSequence-like FinSubsequence-like countable FinSequence of A
(D) (#) x is Relation-like NAT -defined A -valued Function-like set
len x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
Seg D is V46() D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
A is non empty set
x is Relation-like NAT -defined A -valued Function-like V46() D -element FinSequence-like FinSubsequence-like countable FinSequence of A
i is Relation-like NAT -defined A -valued Function-like V46() D -element FinSequence-like FinSubsequence-like countable FinSequence of A
len i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
dom i is D -element countable Element of bool NAT
len x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
dom x is D -element countable Element of bool NAT
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
A is non empty set
x is non empty set
[:A,x:] is Relation-like non empty set
i is non empty set
[:[:A,x:],i:] is Relation-like non empty set
bool [:[:A,x:],i:] is non empty set
(D,i) is non empty (i)
(i) is functional non empty FinSequence-membered (i)
{ b₁ where b₁ is Relation-like NAT -defined i -valued Function-like V46() FinSequence-like FinSubsequence-like countable (i,(i)) : len b₁ = D } is set
i is Relation-like [:A,x:] -defined i -valued Function-like non empty total quasi_total Element of bool [:[:A,x:],i:]
e is Relation-like NAT -defined A -valued Function-like V46() D -element FinSequence-like FinSubsequence-like countable FinSequence of A
a is Relation-like NAT -defined x -valued Function-like V46() D -element FinSequence-like FinSubsequence-like countable FinSequence of x
i .: (e,a) is Relation-like Function-like set
<:e,a:> is Relation-like Function-like set
<:e,a:> (#) i is Relation-like i -valued Function-like set
len e is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
len a is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
b is Relation-like NAT -defined i -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of i
len b is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
A is non empty set
x is non empty set
[:A,x:] is Relation-like non empty set
i is non empty set
[:[:A,x:],i:] is Relation-like non empty set
bool [:[:A,x:],i:] is non empty set
(D,i) is non empty (i)
(i) is functional non empty FinSequence-membered (i)
{ b₁ where b₁ is Relation-like NAT -defined i -valued Function-like V46() FinSequence-like FinSubsequence-like countable (i,(i)) : len b₁ = D } is set
i is Element of A
e is Relation-like [:A,x:] -defined i -valued Function-like non empty total quasi_total Element of bool [:[:A,x:],i:]
a is Relation-like NAT -defined x -valued Function-like V46() D -element FinSequence-like FinSubsequence-like countable FinSequence of x
e [;] (i,a) is Relation-like Function-like set
dom a is D -element set
(dom a) --> i is Relation-like dom a -defined A -valued Function-like constant total set
{i} is non empty trivial 1 -element set
[:(dom a),{i}:] is Relation-like set
<:((dom a) --> i),a:> is Relation-like Function-like set
<:((dom a) --> i),a:> (#) e is Relation-like i -valued Function-like set
len a is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
b is Relation-like NAT -defined i -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of i
len b is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
A is non empty set
x is non empty set
[:A,x:] is Relation-like non empty set
i is non empty set
[:[:A,x:],i:] is Relation-like non empty set
bool [:[:A,x:],i:] is non empty set
(D,i) is non empty (i)
(i) is functional non empty FinSequence-membered (i)
{ b₁ where b₁ is Relation-like NAT -defined i -valued Function-like V46() FinSequence-like FinSubsequence-like countable (i,(i)) : len b₁ = D } is set
i is Element of x
e is Relation-like [:A,x:] -defined i -valued Function-like non empty total quasi_total Element of bool [:[:A,x:],i:]
a is Relation-like NAT -defined A -valued Function-like V46() D -element FinSequence-like FinSubsequence-like countable FinSequence of A
e [:] (a,i) is Relation-like Function-like set
dom a is D -element set
(dom a) --> i is Relation-like dom a -defined x -valued Function-like constant total set
{i} is non empty trivial 1 -element set
[:(dom a),{i}:] is Relation-like set
<:a,((dom a) --> i):> is Relation-like Function-like set
<:a,((dom a) --> i):> (#) e is Relation-like i -valued Function-like set
len a is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
b is Relation-like NAT -defined i -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of i
len b is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
D + A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
x is set
((D + A),x) is Relation-like NAT -defined Function-like V46() D + A -element FinSequence-like FinSubsequence-like countable set
Seg (D + A) is V46() D + A -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D + A ) } is set
(Seg (D + A)) --> x is Relation-like Seg (D + A) -defined Seg (D + A) -defined {x} -valued Function-like constant total total quasi_total V46() FinSequence-like FinSubsequence-like countable Element of bool [:(Seg (D + A)),{x}:]
{x} is non empty trivial 1 -element set
[:(Seg (D + A)),{x}:] is Relation-like set
bool [:(Seg (D + A)),{x}:] is non empty set
(D,x) is Relation-like NAT -defined Function-like V46() D -element FinSequence-like FinSubsequence-like countable set
Seg D is V46() D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
(Seg D) --> x is Relation-like Seg D -defined Seg D -defined {x} -valued Function-like constant total total quasi_total V46() FinSequence-like FinSubsequence-like countable Element of bool [:(Seg D),{x}:]
[:(Seg D),{x}:] is Relation-like set
bool [:(Seg D),{x}:] is non empty set
(A,x) is Relation-like NAT -defined Function-like V46() A -element FinSequence-like FinSubsequence-like countable set
Seg A is V46() A -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= A ) } is set
(Seg A) --> x is Relation-like Seg A -defined Seg A -defined {x} -valued Function-like constant total total quasi_total V46() FinSequence-like FinSubsequence-like countable Element of bool [:(Seg A),{x}:]
[:(Seg A),{x}:] is Relation-like set
bool [:(Seg A),{x}:] is non empty set
(D,x) ^ (A,x) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
D + i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
((D + i),x) is Relation-like NAT -defined Function-like V46() D + i -element FinSequence-like FinSubsequence-like countable set
Seg (D + i) is V46() D + i -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D + i ) } is set
(Seg (D + i)) --> x is Relation-like Seg (D + i) -defined Seg (D + i) -defined {x} -valued Function-like constant total total quasi_total V46() FinSequence-like FinSubsequence-like countable Element of bool [:(Seg (D + i)),{x}:]
[:(Seg (D + i)),{x}:] is Relation-like set
bool [:(Seg (D + i)),{x}:] is non empty set
(i,x) is Relation-like NAT -defined Function-like V46() i -element FinSequence-like FinSubsequence-like countable set
Seg i is V46() i -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= i ) } is set
(Seg i) --> x is Relation-like Seg i -defined Seg i -defined {x} -valued Function-like constant total total quasi_total V46() FinSequence-like FinSubsequence-like countable Element of bool [:(Seg i),{x}:]
[:(Seg i),{x}:] is Relation-like set
bool [:(Seg i),{x}:] is non empty set
(D,x) ^ (i,x) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
i + 1 is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
D + (i + 1) is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable set
((D + (i + 1)),x) is Relation-like NAT -defined Function-like V46() D + (i + 1) -element FinSequence-like FinSubsequence-like countable set
Seg (D + (i + 1)) is non empty V46() D + (i + 1) -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D + (i + 1) ) } is set
(Seg (D + (i + 1))) --> x is Relation-like Seg (D + (i + 1)) -defined Seg (D + (i + 1)) -defined {x} -valued Function-like constant non empty total total quasi_total V46() FinSequence-like FinSubsequence-like countable Element of bool [:(Seg (D + (i + 1))),{x}:]
[:(Seg (D + (i + 1))),{x}:] is Relation-like non empty set
bool [:(Seg (D + (i + 1))),{x}:] is non empty set
((i + 1),x) is Relation-like NAT -defined Function-like V46() i + 1 -element FinSequence-like FinSubsequence-like countable set
Seg (i + 1) is non empty V46() i + 1 -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= i + 1 ) } is set
(Seg (i + 1)) --> x is Relation-like Seg (i + 1) -defined Seg (i + 1) -defined {x} -valued Function-like constant non empty total total quasi_total V46() FinSequence-like FinSubsequence-like countable Element of bool [:(Seg (i + 1)),{x}:]
[:(Seg (i + 1)),{x}:] is Relation-like non empty set
bool [:(Seg (i + 1)),{x}:] is non empty set
(D,x) ^ ((i + 1),x) is Relation-like NAT -defined Function-like V46() D + (i + 1) -element FinSequence-like FinSubsequence-like countable set
D + (i + 1) is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
((D + (i + 1)),x) is Relation-like NAT -defined Function-like V46() D + (i + 1) -element FinSequence-like FinSubsequence-like countable set
Seg (D + (i + 1)) is non empty V46() D + (i + 1) -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D + (i + 1) ) } is set
(Seg (D + (i + 1))) --> x is Relation-like Seg (D + (i + 1)) -defined Seg (D + (i + 1)) -defined {x} -valued Function-like constant non empty total total quasi_total V46() FinSequence-like FinSubsequence-like countable Element of bool [:(Seg (D + (i + 1))),{x}:]
[:(Seg (D + (i + 1))),{x}:] is Relation-like non empty set
bool [:(Seg (D + (i + 1))),{x}:] is non empty set
(D + i) + 1 is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
(((D + i) + 1),x) is Relation-like NAT -defined Function-like V46() (D + i) + 1 -element FinSequence-like FinSubsequence-like countable set
Seg ((D + i) + 1) is non empty V46() (D + i) + 1 -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= (D + i) + 1 ) } is set
(Seg ((D + i) + 1)) --> x is Relation-like Seg ((D + i) + 1) -defined Seg ((D + i) + 1) -defined {x} -valued Function-like constant non empty total total quasi_total V46() FinSequence-like FinSubsequence-like countable Element of bool [:(Seg ((D + i) + 1)),{x}:]
[:(Seg ((D + i) + 1)),{x}:] is Relation-like non empty set
bool [:(Seg ((D + i) + 1)),{x}:] is non empty set
<*x*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,x] is set
{1,x} is non empty set
{{1,x},{1}} is non empty set
{[1,x]} is Relation-like Function-like constant non empty trivial 1 -element set
((D + i),x) ^ <*x*> is Relation-like NAT -defined Function-like non empty V46() (D + i) + 1 -element FinSequence-like FinSubsequence-like countable set
(i,x) ^ <*x*> is Relation-like NAT -defined Function-like non empty V46() i + 1 -element FinSequence-like FinSubsequence-like countable set
(D,x) ^ ((i,x) ^ <*x*>) is Relation-like NAT -defined Function-like non empty V46() D + (i + 1) -element FinSequence-like FinSubsequence-like countable set
D + 0 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
((D + 0),x) is Relation-like NAT -defined Function-like V46() D + 0 -element FinSequence-like FinSubsequence-like countable set
Seg (D + 0) is V46() D + 0 -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D + 0 ) } is set
(Seg (D + 0)) --> x is Relation-like Seg (D + 0) -defined Seg (D + 0) -defined {x} -valued Function-like constant total total quasi_total V46() FinSequence-like FinSubsequence-like countable Element of bool [:(Seg (D + 0)),{x}:]
[:(Seg (D + 0)),{x}:] is Relation-like set
bool [:(Seg (D + 0)),{x}:] is non empty set
(D,x) ^ {} is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
(0,x) is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty Function-yielding V33() V34() V35() V36() V38() V39() V40() V41() ext-real non positive non negative V45() V46() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable set
(Seg 0) --> x is Relation-like non-empty empty-yielding Seg 0 -defined Seg 0 -defined {x} -valued Function-like one-to-one constant functional empty total total quasi_total Function-yielding V33() V34() V35() V36() V38() V39() V40() V41() ext-real non positive non negative V45() V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable Element of bool [:(Seg 0),{x}:]
[:(Seg 0),{x}:] is Relation-like set
bool [:(Seg 0),{x}:] is non empty set
(D,x) ^ (0,x) is Relation-like NAT -defined Function-like V46() D + 0 -element FinSequence-like FinSubsequence-like countable set
D + 0 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
((D + 0),x) is Relation-like NAT -defined Function-like V46() D + 0 -element FinSequence-like FinSubsequence-like countable set
Seg (D + 0) is V46() D + 0 -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D + 0 ) } is set
(Seg (D + 0)) --> x is Relation-like Seg (D + 0) -defined Seg (D + 0) -defined {x} -valued Function-like constant total total quasi_total V46() FinSequence-like FinSubsequence-like countable Element of bool [:(Seg (D + 0)),{x}:]
[:(Seg (D + 0)),{x}:] is Relation-like set
bool [:(Seg (D + 0)),{x}:] is non empty set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
Seg D is V46() D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
A is non empty set
x is Relation-like NAT -defined A -valued Function-like V46() D -element FinSequence-like FinSubsequence-like countable FinSequence of A
dom x is D -element countable Element of bool NAT
len x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
D is Relation-like Function-like set
dom D is set
A is set
x is set
<*A,x*> is Relation-like NAT -defined Function-like non empty V46() 2 -element FinSequence-like FinSubsequence-like countable set
<*A*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,A] is set
{1,A} is non empty set
{{1,A},{1}} is non empty set
{[1,A]} is Relation-like Function-like constant non empty trivial 1 -element set
<*x*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,x] is set
{1,x} is non empty set
{{1,x},{1}} is non empty set
{[1,x]} is Relation-like Function-like constant non empty trivial 1 -element set
<*A*> ^ <*x*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
<*A,x*> (#) D is Relation-like NAT -defined Function-like set
D . A is set
D . x is set
<*(D . A),(D . x)*> is Relation-like NAT -defined Function-like non empty V46() 2 -element FinSequence-like FinSubsequence-like countable set
<*(D . A)*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,(D . A)] is set
{1,(D . A)} is non empty set
{{1,(D . A)},{1}} is non empty set
{[1,(D . A)]} is Relation-like Function-like constant non empty trivial 1 -element set
<*(D . x)*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,(D . x)] is set
{1,(D . x)} is non empty set
{{1,(D . x)},{1}} is non empty set
{[1,(D . x)]} is Relation-like Function-like constant non empty trivial 1 -element set
<*(D . A)*> ^ <*(D . x)*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
rng D is set
rng <*A,x*> is non empty set
{A,x} is non empty set
i is non empty set
i is non empty set
[:i,i:] is Relation-like non empty set
bool [:i,i:] is non empty set
e is Relation-like NAT -defined i -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of i
a is Relation-like i -defined i -valued Function-like non empty total quasi_total Element of bool [:i,i:]
a * e is Relation-like NAT -defined i -valued Function-like Element of bool [:NAT,i:]
[:NAT,i:] is Relation-like non empty V46() set
bool [:NAT,i:] is non empty V46() set
D is Relation-like Function-like set
dom D is set
A is set
x is set
i is set
<*A,x,i*> is Relation-like NAT -defined Function-like non empty V46() 3 -element FinSequence-like FinSubsequence-like countable set
<*A*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,A] is set
{1,A} is non empty set
{{1,A},{1}} is non empty set
{[1,A]} is Relation-like Function-like constant non empty trivial 1 -element set
<*x*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,x] is set
{1,x} is non empty set
{{1,x},{1}} is non empty set
{[1,x]} is Relation-like Function-like constant non empty trivial 1 -element set
<*A*> ^ <*x*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
<*i*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,i] is set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
(<*A*> ^ <*x*>) ^ <*i*> is Relation-like NAT -defined Function-like non empty V46() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like countable set
<*A,x,i*> (#) D is Relation-like NAT -defined Function-like set
D . A is set
D . x is set
D . i is set
<*(D . A),(D . x),(D . i)*> is Relation-like NAT -defined Function-like non empty V46() 3 -element FinSequence-like FinSubsequence-like countable set
<*(D . A)*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,(D . A)] is set
{1,(D . A)} is non empty set
{{1,(D . A)},{1}} is non empty set
{[1,(D . A)]} is Relation-like Function-like constant non empty trivial 1 -element set
<*(D . x)*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,(D . x)] is set
{1,(D . x)} is non empty set
{{1,(D . x)},{1}} is non empty set
{[1,(D . x)]} is Relation-like Function-like constant non empty trivial 1 -element set
<*(D . A)*> ^ <*(D . x)*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
<*(D . i)*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,(D . i)] is set
{1,(D . i)} is non empty set
{{1,(D . i)},{1}} is non empty set
{[1,(D . i)]} is Relation-like Function-like constant non empty trivial 1 -element set
(<*(D . A)*> ^ <*(D . x)*>) ^ <*(D . i)*> is Relation-like NAT -defined Function-like non empty V46() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like countable set
rng D is set
rng <*A,x,i*> is non empty set
{A,x,i} is non empty set
{A,x} is non empty set
{i} is non empty trivial 1 -element set
{A,x} \/ {i} is non empty set
i is non empty set
e is non empty set
[:i,e:] is Relation-like non empty set
bool [:i,e:] is non empty set
a is Relation-like NAT -defined i -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of i
b is Relation-like i -defined e -valued Function-like non empty total quasi_total Element of bool [:i,e:]
b * a is Relation-like NAT -defined e -valued Function-like Element of bool [:NAT,e:]
[:NAT,e:] is Relation-like non empty V46() set
bool [:NAT,e:] is non empty V46() set
D is set
A is set
<*D,A*> is Relation-like NAT -defined Function-like non empty V46() 2 -element FinSequence-like FinSubsequence-like countable set
<*D*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,D] is set
{1,D} is non empty set
{{1,D},{1}} is non empty set
{[1,D]} is Relation-like Function-like constant non empty trivial 1 -element set
<*A*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,A] is set
{1,A} is non empty set
{{1,A},{1}} is non empty set
{[1,A]} is Relation-like Function-like constant non empty trivial 1 -element set
<*D*> ^ <*A*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
rng <*D,A*> is non empty set
{D,A} is non empty set
D is set
A is set
x is set
<*D,A,x*> is Relation-like NAT -defined Function-like non empty V46() 3 -element FinSequence-like FinSubsequence-like countable set
<*D*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,D] is set
{1,D} is non empty set
{{1,D},{1}} is non empty set
{[1,D]} is Relation-like Function-like constant non empty trivial 1 -element set
<*A*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,A] is set
{1,A} is non empty set
{{1,A},{1}} is non empty set
{[1,A]} is Relation-like Function-like constant non empty trivial 1 -element set
<*D*> ^ <*A*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
<*x*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,x] is set
{1,x} is non empty set
{{1,x},{1}} is non empty set
{[1,x]} is Relation-like Function-like constant non empty trivial 1 -element set
(<*D*> ^ <*A*>) ^ <*x*> is Relation-like NAT -defined Function-like non empty V46() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like countable set
rng <*D,A,x*> is non empty set
{D,A,x} is non empty set
D is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
x is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
A is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
len D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
len A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
dom D is countable Element of bool NAT
i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
Seg i is V46() i -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= i ) } is set
dom A is countable Element of bool NAT
i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
D . i is set
x . i is set
A . i is set
D is non empty set
A is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of D
x is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of D
i is Element of D
<*i*> is Relation-like NAT -defined D -valued Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable FinSequence of D
[1,i] is set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
x ^ <*i*> is Relation-like NAT -defined D -valued Function-like non empty V46() FinSequence-like FinSubsequence-like countable FinSequence of D
<*> D is Relation-like non-empty empty-yielding NAT -defined D -valued Function-like one-to-one constant functional empty proper Function-yielding V33() V34() V35() V36() V38() V39() V40() V41() ext-real non positive non negative V45() V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable FinSequence of D
[:NAT,D:] is Relation-like non empty V46() set
i is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of D
e is Element of D
<*e*> is Relation-like NAT -defined D -valued Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable FinSequence of D
[1,e] is set
{1,e} is non empty set
{{1,e},{1}} is non empty set
{[1,e]} is Relation-like Function-like constant non empty trivial 1 -element set
<*e*> ^ i is Relation-like NAT -defined D -valued Function-like non empty V46() FinSequence-like FinSubsequence-like countable FinSequence of D
e is Element of D
<*e*> is Relation-like NAT -defined D -valued Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable FinSequence of D
[1,e] is set
{1,e} is non empty set
{{1,e},{1}} is non empty set
{[1,e]} is Relation-like Function-like constant non empty trivial 1 -element set
i is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of D
<*e*> ^ i is Relation-like NAT -defined D -valued Function-like non empty V46() FinSequence-like FinSubsequence-like countable FinSequence of D
e is Element of D
<*e*> is Relation-like NAT -defined D -valued Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable FinSequence of D
[1,e] is set
{1,e} is non empty set
{{1,e},{1}} is non empty set
{[1,e]} is Relation-like Function-like constant non empty trivial 1 -element set
i is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of D
<*e*> ^ i is Relation-like NAT -defined D -valued Function-like non empty V46() FinSequence-like FinSubsequence-like countable FinSequence of D
i ^ <*i*> is Relation-like NAT -defined D -valued Function-like non empty V46() FinSequence-like FinSubsequence-like countable FinSequence of D
<*e*> ^ (i ^ <*i*>) is Relation-like NAT -defined D -valued Function-like non empty V46() FinSequence-like FinSubsequence-like countable FinSequence of D
<*> D is Relation-like non-empty empty-yielding NAT -defined D -valued Function-like one-to-one constant functional empty proper Function-yielding V33() V34() V35() V36() V38() V39() V40() V41() ext-real non positive non negative V45() V46() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable FinSequence of D
[:NAT,D:] is Relation-like non empty V46() set
D is set
A is (D)
x is set
D is non empty set
A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
x is Element of D
(A,x) is Relation-like NAT -defined Function-like V46() A -element FinSequence-like FinSubsequence-like countable set
Seg A is V46() A -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= A ) } is set
(Seg A) --> x is Relation-like Seg A -defined Seg A -defined D -valued {x} -valued Function-like constant total total quasi_total V46() FinSequence-like FinSubsequence-like countable Element of bool [:(Seg A),{x}:]
{x} is non empty trivial 1 -element set
[:(Seg A),{x}:] is Relation-like set
bool [:(Seg A),{x}:] is non empty set
(A,D) is functional non empty (D)
(D) is functional non empty FinSequence-membered (D)
{ b₁ where b₁ is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable (D,(D)) : len b₁ = A } is set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
A is non empty set
(D,A) is functional non empty (A)
(A) is functional non empty FinSequence-membered (A)
{ b₁ where b₁ is Relation-like NAT -defined A -valued Function-like V46() FinSequence-like FinSubsequence-like countable (A,(A)) : len b₁ = D } is set
x is set
i is Relation-like NAT -defined A -valued Function-like V46() FinSequence-like FinSubsequence-like countable (A,(A))
len i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
D is set
A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
(A,D) is functional (D)
(D) is functional non empty FinSequence-membered (D)
{ b₁ where b₁ is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable (D,(D)) : len b₁ = A } is set
x is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable set
len x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
rng x is set
i is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable (D,(D))
len i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
D is set
A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
(A,D) is functional (D)
(D) is functional non empty FinSequence-membered (D)
{ b₁ where b₁ is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable (D,(D)) : len b₁ = A } is set
x is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of D
len x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
rng x is set
D is set
(D) is functional non empty FinSequence-membered (D)
A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
(A,D) is functional (D)
{ b₁ where b₁ is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable (D,(D)) : len b₁ = A } is set
x is set
A is set
D is set
(1,D) is functional (D)
(D) is functional non empty FinSequence-membered (D)
{ b₁ where b₁ is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable (D,(D)) : len b₁ = 1 } is set
x is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable (D,(D))
len x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
x . 1 is set
i is set
<*i*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,i] is set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
rng <*i*> is non empty trivial 1 -element set
{i} is non empty trivial 1 -element set
rng x is set
x is set
<*x*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,x] is set
{1,x} is non empty set
{{1,x},{1}} is non empty set
{[1,x]} is Relation-like Function-like constant non empty trivial 1 -element set
i is non empty set
i is Element of i
<*i*> is Relation-like NAT -defined i -valued Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable FinSequence of i
[1,i] is set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
(1,i) is functional non empty (i)
(i) is functional non empty FinSequence-membered (i)
{ b₁ where b₁ is Relation-like NAT -defined i -valued Function-like V46() FinSequence-like FinSubsequence-like countable (i,(i)) : len b₁ = 1 } is set
A is set
<*A*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,A] is set
{1,A} is non empty set
{{1,A},{1}} is non empty set
{[1,A]} is Relation-like Function-like constant non empty trivial 1 -element set
D is set
(1,D) is functional (D)
(D) is functional non empty FinSequence-membered (D)
{ b₁ where b₁ is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable (D,(D)) : len b₁ = 1 } is set
<*A*> . 1 is set
x is set
<*x*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,x] is set
{1,x} is non empty set
{{1,x},{1}} is non empty set
{[1,x]} is Relation-like Function-like constant non empty trivial 1 -element set
A is set
D is set
(2,D) is functional (D)
(D) is functional non empty FinSequence-membered (D)
{ b₁ where b₁ is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable (D,(D)) : len b₁ = 2 } is set
x is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable (D,(D))
len x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
x . 1 is set
x . 2 is set
i is set
i is set
<*i,i*> is Relation-like NAT -defined Function-like non empty V46() 2 -element FinSequence-like FinSubsequence-like countable set
<*i*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,i] is set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
<*i*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,i] is set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
<*i*> ^ <*i*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
rng <*i,i*> is non empty set
{i,i} is non empty set
rng x is set
x is set
i is set
<*x,i*> is Relation-like NAT -defined Function-like non empty V46() 2 -element FinSequence-like FinSubsequence-like countable set
<*x*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,x] is set
{1,x} is non empty set
{{1,x},{1}} is non empty set
{[1,x]} is Relation-like Function-like constant non empty trivial 1 -element set
<*i*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,i] is set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
<*x*> ^ <*i*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
i is non empty set
e is Element of i
a is Element of i
<*e,a*> is Relation-like NAT -defined Function-like non empty V46() 2 -element FinSequence-like FinSubsequence-like countable set
<*e*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,e] is set
{1,e} is non empty set
{{1,e},{1}} is non empty set
{[1,e]} is Relation-like Function-like constant non empty trivial 1 -element set
<*a*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,a] is set
{1,a} is non empty set
{{1,a},{1}} is non empty set
{[1,a]} is Relation-like Function-like constant non empty trivial 1 -element set
<*e*> ^ <*a*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
(2,i) is functional non empty (i)
(i) is functional non empty FinSequence-membered (i)
{ b₁ where b₁ is Relation-like NAT -defined i -valued Function-like V46() FinSequence-like FinSubsequence-like countable (i,(i)) : len b₁ = 2 } is set
A is set
x is set
<*A,x*> is Relation-like NAT -defined Function-like non empty V46() 2 -element FinSequence-like FinSubsequence-like countable set
<*A*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,A] is set
{1,A} is non empty set
{{1,A},{1}} is non empty set
{[1,A]} is Relation-like Function-like constant non empty trivial 1 -element set
<*x*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,x] is set
{1,x} is non empty set
{{1,x},{1}} is non empty set
{[1,x]} is Relation-like Function-like constant non empty trivial 1 -element set
<*A*> ^ <*x*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
D is set
(2,D) is functional (D)
(D) is functional non empty FinSequence-membered (D)
{ b₁ where b₁ is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable (D,(D)) : len b₁ = 2 } is set
<*A,x*> . 1 is set
<*A,x*> . 2 is set
i is set
i is set
<*i,i*> is Relation-like NAT -defined Function-like non empty V46() 2 -element FinSequence-like FinSubsequence-like countable set
<*i*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,i] is set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
<*i*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,i] is set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
<*i*> ^ <*i*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
A is set
D is set
(3,D) is functional (D)
(D) is functional non empty FinSequence-membered (D)
{ b₁ where b₁ is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable (D,(D)) : len b₁ = 3 } is set
x is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable (D,(D))
len x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
x . 1 is set
x . 2 is set
x . 3 is set
i is set
i is set
e is set
<*i,i,e*> is Relation-like NAT -defined Function-like non empty V46() 3 -element FinSequence-like FinSubsequence-like countable set
<*i*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,i] is set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
<*i*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,i] is set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
<*i*> ^ <*i*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
<*e*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,e] is set
{1,e} is non empty set
{{1,e},{1}} is non empty set
{[1,e]} is Relation-like Function-like constant non empty trivial 1 -element set
(<*i*> ^ <*i*>) ^ <*e*> is Relation-like NAT -defined Function-like non empty V46() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like countable set
rng <*i,i,e*> is non empty set
{i,i,e} is non empty set
rng x is set
x is set
i is set
i is set
<*x,i,i*> is Relation-like NAT -defined Function-like non empty V46() 3 -element FinSequence-like FinSubsequence-like countable set
<*x*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,x] is set
{1,x} is non empty set
{{1,x},{1}} is non empty set
{[1,x]} is Relation-like Function-like constant non empty trivial 1 -element set
<*i*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,i] is set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
<*x*> ^ <*i*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
<*i*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,i] is set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
(<*x*> ^ <*i*>) ^ <*i*> is Relation-like NAT -defined Function-like non empty V46() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like countable set
e is non empty set
a is Element of e
b is Element of e
c is Element of e
<*a,b,c*> is Relation-like NAT -defined Function-like non empty V46() 3 -element FinSequence-like FinSubsequence-like countable set
<*a*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,a] is set
{1,a} is non empty set
{{1,a},{1}} is non empty set
{[1,a]} is Relation-like Function-like constant non empty trivial 1 -element set
<*b*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,b] is set
{1,b} is non empty set
{{1,b},{1}} is non empty set
{[1,b]} is Relation-like Function-like constant non empty trivial 1 -element set
<*a*> ^ <*b*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
<*c*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,c] is set
{1,c} is non empty set
{{1,c},{1}} is non empty set
{[1,c]} is Relation-like Function-like constant non empty trivial 1 -element set
(<*a*> ^ <*b*>) ^ <*c*> is Relation-like NAT -defined Function-like non empty V46() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like countable set
(3,e) is functional non empty (e)
(e) is functional non empty FinSequence-membered (e)
{ b₁ where b₁ is Relation-like NAT -defined e -valued Function-like V46() FinSequence-like FinSubsequence-like countable (e,(e)) : len b₁ = 3 } is set
A is set
x is set
i is set
<*A,x,i*> is Relation-like NAT -defined Function-like non empty V46() 3 -element FinSequence-like FinSubsequence-like countable set
<*A*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,A] is set
{1,A} is non empty set
{{1,A},{1}} is non empty set
{[1,A]} is Relation-like Function-like constant non empty trivial 1 -element set
<*x*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,x] is set
{1,x} is non empty set
{{1,x},{1}} is non empty set
{[1,x]} is Relation-like Function-like constant non empty trivial 1 -element set
<*A*> ^ <*x*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
<*i*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,i] is set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
(<*A*> ^ <*x*>) ^ <*i*> is Relation-like NAT -defined Function-like non empty V46() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like countable set
D is set
(3,D) is functional (D)
(D) is functional non empty FinSequence-membered (D)
{ b₁ where b₁ is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable (D,(D)) : len b₁ = 3 } is set
<*A,x,i*> . 3 is set
<*A,x,i*> . 1 is set
<*A,x,i*> . 2 is set
i is set
e is set
a is set
<*i,e,a*> is Relation-like NAT -defined Function-like non empty V46() 3 -element FinSequence-like FinSubsequence-like countable set
<*i*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,i] is set
{1,i} is non empty set
{{1,i},{1}} is non empty set
{[1,i]} is Relation-like Function-like constant non empty trivial 1 -element set
<*e*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,e] is set
{1,e} is non empty set
{{1,e},{1}} is non empty set
{[1,e]} is Relation-like Function-like constant non empty trivial 1 -element set
<*i*> ^ <*e*> is Relation-like NAT -defined Function-like non empty V46() 1 + 1 -element FinSequence-like FinSubsequence-like countable set
<*a*> is Relation-like NAT -defined Function-like constant non empty trivial V46() 1 -element FinSequence-like FinSubsequence-like countable set
[1,a] is set
{1,a} is non empty set
{{1,a},{1}} is non empty set
{[1,a]} is Relation-like Function-like constant non empty trivial 1 -element set
(<*i*> ^ <*e*>) ^ <*a*> is Relation-like NAT -defined Function-like non empty V46() (1 + 1) + 1 -element FinSequence-like FinSubsequence-like countable set
A is set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
x is set
(D,x) is functional (x)
(x) is functional non empty FinSequence-membered (x)
{ b₁ where b₁ is Relation-like NAT -defined x -valued Function-like V46() FinSequence-like FinSubsequence-like countable (x,(x)) : len b₁ = D } is set
D is non empty set
(D) is functional non empty FinSequence-membered (D)
A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
(A,D) is functional non empty (D)
{ b₁ where b₁ is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable (D,(D)) : len b₁ = A } is set
{ b₁ where b₁ is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable (D,(D)) : S₁[b₁] } is set
D is set
A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
(A,D) is Relation-like NAT -defined Function-like V46() A -element FinSequence-like FinSubsequence-like countable set
Seg A is V46() A -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= A ) } is set
(Seg A) --> D is Relation-like Seg A -defined Seg A -defined {D} -valued Function-like constant total total quasi_total V46() FinSequence-like FinSubsequence-like countable Element of bool [:(Seg A),{D}:]
{D} is non empty trivial 1 -element set
[:(Seg A),{D}:] is Relation-like set
bool [:(Seg A),{D}:] is non empty set
x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
(x,D) is Relation-like NAT -defined Function-like V46() x -element FinSequence-like FinSubsequence-like countable set
Seg x is V46() x -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= x ) } is set
(Seg x) --> D is Relation-like Seg x -defined Seg x -defined {D} -valued Function-like constant total total quasi_total V46() FinSequence-like FinSubsequence-like countable Element of bool [:(Seg x),{D}:]
[:(Seg x),{D}:] is Relation-like set
bool [:(Seg x),{D}:] is non empty set
len (A,D) is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
D is set
(D) is functional non empty FinSequence-membered (D)
A is Relation-like D -defined Function-like total set
x is set
i is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable (D,(D))
i (#) A is Relation-like NAT -defined Function-like set
product (i (#) A) is functional with_common_domain product-like set
i is set
x is Relation-like (D) -defined Function-like non empty total set
i is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable (D,(D))
x . i is set
i (#) A is Relation-like NAT -defined Function-like set
product (i (#) A) is functional with_common_domain product-like set
i is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable (D,(D))
i (#) A is Relation-like NAT -defined Function-like set
product (i (#) A) is functional with_common_domain product-like set
x is Relation-like (D) -defined Function-like non empty total set
i is Relation-like (D) -defined Function-like non empty total set
i is set
x . i is set
e is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable (D,(D))
e (#) A is Relation-like NAT -defined Function-like set
product (e (#) A) is functional with_common_domain product-like set
i . i is set
D is set
A is Relation-like non-empty D -defined Function-like total set
(D,A) is Relation-like (D) -defined Function-like non empty total set
(D) is functional non empty FinSequence-membered (D)
x is set
(D,A) . x is set
i is Relation-like NAT -defined D -valued Function-like V46() FinSequence-like FinSubsequence-like countable (D,(D))
i (#) A is Relation-like non-empty NAT -defined Function-like set
product (i (#) A) is functional non empty with_common_domain product-like set
D is set
{D} is non empty trivial 1 -element set
({D}) is functional non empty FinSequence-membered ({D})
[:NAT,({D}):] is Relation-like non empty V46() set
bool [:NAT,({D}):] is non empty V46() set
A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
(A,D) is Relation-like NAT -defined Function-like V46() A -element FinSequence-like FinSubsequence-like countable set
Seg A is V46() A -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= A ) } is set
(Seg A) --> D is Relation-like Seg A -defined Seg A -defined {D} -valued Function-like constant total total quasi_total V46() FinSequence-like FinSubsequence-like countable Element of bool [:(Seg A),{D}:]
[:(Seg A),{D}:] is Relation-like set
bool [:(Seg A),{D}:] is non empty set
x is Relation-like NAT -defined {D} -valued Function-like V46() FinSequence-like FinSubsequence-like countable ({D},({D}))
A is Relation-like NAT -defined ({D}) -valued Function-like non empty total quasi_total Function-yielding V33() Element of bool [:NAT,({D}):]
A is Relation-like NAT -defined ({D}) -valued Function-like non empty total quasi_total Function-yielding V33() Element of bool [:NAT,({D}):]
x is Relation-like NAT -defined ({D}) -valued Function-like non empty total quasi_total Function-yielding V33() Element of bool [:NAT,({D}):]
i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
A . i is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable Element of ({D})
(i,D) is Relation-like NAT -defined Function-like V46() i -element FinSequence-like FinSubsequence-like countable set
Seg i is V46() i -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= i ) } is set
(Seg i) --> D is Relation-like Seg i -defined Seg i -defined {D} -valued Function-like constant total total quasi_total V46() FinSequence-like FinSubsequence-like countable Element of bool [:(Seg i),{D}:]
[:(Seg i),{D}:] is Relation-like set
bool [:(Seg i),{D}:] is non empty set
x . i is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable Element of ({D})
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
A is set
(D,A) is Relation-like NAT -defined Function-like V46() D -element FinSequence-like FinSubsequence-like countable set
Seg D is V46() D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
(Seg D) --> A is Relation-like Seg D -defined Seg D -defined {A} -valued Function-like constant total total quasi_total V46() FinSequence-like FinSubsequence-like countable Element of bool [:(Seg D),{A}:]
{A} is non empty trivial 1 -element set
[:(Seg D),{A}:] is Relation-like set
bool [:(Seg D),{A}:] is non empty set
x is set
A .--> x is Relation-like {A} -defined Function-like one-to-one set
{A} --> x is Relation-like {A} -defined {x} -valued Function-like constant non empty total quasi_total Element of bool [:{A},{x}:]
{x} is non empty trivial 1 -element set
[:{A},{x}:] is Relation-like non empty set
bool [:{A},{x}:] is non empty set
(D,A) (#) (A .--> x) is Relation-like NAT -defined Function-like set
(D,x) is Relation-like NAT -defined Function-like V46() D -element FinSequence-like FinSubsequence-like countable set
(Seg D) --> x is Relation-like Seg D -defined Seg D -defined {x} -valued Function-like constant total total quasi_total V46() FinSequence-like FinSubsequence-like countable Element of bool [:(Seg D),{x}:]
[:(Seg D),{x}:] is Relation-like set
bool [:(Seg D),{x}:] is non empty set
i is set
dom (D,x) is D -element countable Element of bool NAT
dom (D,A) is D -element countable Element of bool NAT
dom (A .--> x) is set
(D,A) . i is set
i is set
(D,x) . i is set
(A .--> x) . A is set
(D,A) . i is set
(A .--> x) . ((D,A) . i) is set
D is non empty set
A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
Seg A is V46() A -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= A ) } is set
Funcs ((Seg A),D) is functional non empty FUNCTION_DOMAIN of Seg A,D
x is set
{x} is non empty trivial 1 -element set
x .--> D is Relation-like {x} -defined Function-like one-to-one set
{x} --> D is Relation-like non-empty non empty-yielding {x} -defined {D} -valued Function-like constant non empty total quasi_total Element of bool [:{x},{D}:]
{D} is non empty trivial 1 -element set
[:{x},{D}:] is Relation-like non empty set
bool [:{x},{D}:] is non empty set
(x) is Relation-like NAT -defined ({x}) -valued Function-like non empty total quasi_total Function-yielding V33() Element of bool [:NAT,({x}):]
({x}) is functional non empty FinSequence-membered ({x})
[:NAT,({x}):] is Relation-like non empty V46() set
bool [:NAT,({x}):] is non empty V46() set
i is Relation-like {x} -defined Function-like non empty total set
({x},i) is Relation-like ({x}) -defined Function-like non empty total set
(x) (#) ({x},i) is Relation-like NAT -defined Function-like non empty total set
((x) (#) ({x},i)) . A is set
(A,x) is Relation-like NAT -defined Function-like V46() A -element FinSequence-like FinSubsequence-like countable set
(Seg A) --> x is Relation-like Seg A -defined Seg A -defined {x} -valued Function-like constant total total quasi_total V46() FinSequence-like FinSubsequence-like countable Element of bool [:(Seg A),{x}:]
[:(Seg A),{x}:] is Relation-like set
bool [:(Seg A),{x}:] is non empty set
dom (x) is non empty set
(x) . A is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like countable Element of ({x})
({x},i) . ((x) . A) is set
({x},i) . (A,x) is set
(A,x) (#) (x .--> D) is Relation-like NAT -defined Function-like set
product ((A,x) (#) (x .--> D)) is functional with_common_domain product-like set
(A,D) is Relation-like NAT -defined Function-like V46() A -element FinSequence-like FinSubsequence-like countable set
(Seg A) --> D is Relation-like non-empty Seg A -defined Seg A -defined {D} -valued Function-like constant total total quasi_total V46() FinSequence-like FinSubsequence-like countable Element of bool [:(Seg A),{D}:]
[:(Seg A),{D}:] is Relation-like set
bool [:(Seg A),{D}:] is non empty set
product (A,D) is functional with_common_domain product-like set
D is Relation-like NAT -defined Function-like non empty total set
A is Relation-like NAT -defined Function-like set
dom A is set
x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
Shift (A,x) is Relation-like Function-like set
i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
x + i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT
D . (x + i) is set
A . i is set
dom (Shift (A,x)) is set
(Shift (A,x)) . (x + i) is set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
(NAT,D,0) is Relation-like NAT -defined NAT -valued Function-like V46() D -element FinSequence-like FinSubsequence-like countable ( NAT ,(D,NAT))
(D,NAT) is functional non empty ( NAT )
(NAT) is functional non empty FinSequence-membered ( NAT )
{ b₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like V46() FinSequence-like FinSubsequence-like countable ( NAT ,(NAT)) : len b₁ = D } is set
Seg D is V46() D -element countable Element of bool NAT
{ b₁ where b₁ is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b₁ & b₁ <= D ) } is set
(Seg D) --> 0 is Relation-like Seg D -defined Seg D -defined NAT -valued {0} -valued Function-like constant total total quasi_total Function-yielding V33() V46() FinSequence-like FinSubsequence-like Cardinal-yielding countable Element of bool [:(Seg D),{0}:]
{0} is functional non empty trivial 1 -element with_common_domain set
[:(Seg D),{0}:] is Relation-like set
bool [:(Seg D),{0}:] is non empty set
A is set
dom (NAT,D,0) is D -element set
(NAT,D,0) . A is set
dom (NAT,D,0) is D -element countable Element of bool NAT
D is set
A is functional (D)
x is set