:: FINSEQ_2 semantic presentation

REAL is set

bool REAL is non empty 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

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

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

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

{ 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

{ 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

{ 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

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

{ 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

{ 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

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

rng A is set

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 . D is set
rng x is set

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

[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,A] is set
{1,A} is non empty set
{{1,A},{1}} is non empty 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
() \/ () is non empty set
{A} is non empty trivial 1 -element set
() \/ {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

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

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

1 + 1 is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT

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

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

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

1 + 1 is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT

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

dom (A ^ x) is countable Element of bool NAT
D is 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

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) + () is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT
D is 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

A is set

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

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

len A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT

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

i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set
x . i is set
A . i is 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

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

{ 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

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

D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set

{ 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

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

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

{ 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

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

len i 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 e is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT

F2() is non empty set
F1() is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set

len D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of 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()

len A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of 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

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

len A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT

i is Element of F1()

[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

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

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
D is set
bool D is non empty set
A is Element of bool D

rng x is set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set

{ 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

dom x is set
i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of 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

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

{ 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

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

{ 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

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

{ 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

[:(Seg i),A:] is Relation-like set
bool [:(Seg i),A:] is non empty set
dom (i | (Seg i)) is set

rng D is 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 x is set

dom (D (#) x) is set

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

{ 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

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

rng i is set
dom (i (#) x) is set

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

{ 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

len i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT

[:NAT,x:] is Relation-like non empty V46() set
bool [:NAT,x:] is non empty V46() 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

bool [:NAT,A:] is non empty set

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

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

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

[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

dom A is set

A . D is set

[1,(A . D)] is set
{1,(A . D)} is non empty set
{{1,(A . D)},{1}} is non empty 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

[:NAT,i:] is Relation-like non empty V46() set
bool [:NAT,i:] is non empty V46() set
i . 1 is set

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

a . 1 is set
e . D is set
D is 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

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

[:NAT,x:] is Relation-like non empty V46() set
bool [:NAT,x:] is non empty V46() set
i . D is set

[1,(i . D)] is set
{1,(i . D)} is non empty set
{{1,(i . D)},{1}} is non empty set

i . 1 is 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
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

e . 1 is set
D is set
A is 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,A] is set
{1,A} is non empty set
{{1,A},{1}} is non empty 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

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

[1,(e . D)] is set
{1,(e . D)} is non empty set
{{1,(e . D)},{1}} is non empty set

[1,(e . A)] is set
{1,(e . A)} is non empty set
{{1,(e . A)},{1}} is non empty set

i . 2 is set
len i 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
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

a . 2 is set
i . 1 is set
a . 1 is set
D is set
A is set
x is 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,A] is set
{1,A} is non empty set
{{1,A},{1}} is non empty set

1 + 1 is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V46() cardinal countable Element of NAT

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

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

[1,(a . D)] is set
{1,(a . D)} is non empty set
{{1,(a . D)},{1}} is non empty set

[1,(a . A)] is set
{1,(a . A)} is non empty set
{{1,(a . A)},{1}} is non empty set

[1,(a . x)] is set
{1,(a . x)} is non empty set
{{1,(a . x)},{1}} is non empty 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

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

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

{ 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

{ 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

len x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT

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 (i (#) x) is set
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set

{ 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

len A is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of 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

D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set

{ 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

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

rng i is 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 (i (#) A) is set
dom i is set

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

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

rng x is set

D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set

{ 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

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

rng i is set

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

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

D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set

{ 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

{ 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

len i is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT

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

{ 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

len x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of NAT

[:(Seg D),A:] is Relation-like set
bool [:(Seg D),A:] is non empty set
D is non empty set

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

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

{ 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
dom (id (Seg D)) is set
x is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable Element of 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

{ 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
D is V34() V35() V36() V40() V41() ext-real non negative V45() V46() cardinal countable set

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