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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= A + 1 ) } is set
Seg A is V46() A -element countable Element of bool NAT
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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
F2() is non empty set
F1() 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 F1() is V46() F1() -element countable Element of bool NAT
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= F1() ) } is set
A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
D . A is set
F3(A) is Element of F2()
A is Relation-like NAT -defined F2() -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of F2()
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
F3(x) is Element of F2()
F1() is set
<*> F1() is Relation-like non-empty empty-yielding NAT -defined F1() -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 F1()
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 F1() -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of F1()
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 F1() -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of F1()
i is Element of F1()
<*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 F1() -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of F1()
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 F1() -valued Function-like V46() FinSequence-like FinSubsequence-like countable FinSequence of F1()
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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT : ( 1 <= b1 & b1 <= 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