:: MATRIX_2 semantic presentation

REAL is set
NAT is non empty V39() V40() V41() non finite V57() V58() Element of bool REAL

NAT is non empty V39() V40() V41() non finite V57() V58() set
bool NAT is non finite set
bool NAT is non finite set
INT is set
RAT is set

2 is non empty ext-real positive non negative V39() V40() V41() V45() finite V57() Element of NAT
1 is non empty ext-real positive non negative V39() V40() V41() V45() finite V57() Element of NAT
3 is non empty ext-real positive non negative V39() V40() V41() V45() finite V57() Element of NAT

Seg 1 is non empty trivial finite V59(1) Element of bool NAT
{1} is non empty trivial V59(1) set
Seg 2 is non empty finite V59(2) Element of bool NAT
{1,2} is non empty set

id (Seg 1) is Relation-like Seg 1 -defined Seg 1 -valued V6() V8() V9() V13() Function-like one-to-one non empty V22( Seg 1) quasi_total onto bijective Element of bool [:(Seg 1),(Seg 1):]
[:(Seg 1),(Seg 1):] is set
bool [:(Seg 1),(Seg 1):] is set

dom {} is set
rng {} is set
n is ext-real non negative V39() V40() V41() V45() finite V57() set
x is ext-real non negative V39() V40() V41() V45() finite V57() set
x is set

Seg x is finite V59(x) Element of bool NAT

{x} is non empty trivial V59(1) set
[:(Seg x),{x}:] is set
bool [:(Seg x),{x}:] is set

Seg n is finite V59(n) Element of bool NAT
K168((Seg n),(x |-> x)) is Relation-like Seg n -defined {(x |-> x)} -valued Function-like V22( Seg n) quasi_total finite FinSequence-like FinSubsequence-like Element of bool [:(Seg n),{(x |-> x)}:]
{(x |-> x)} is functional non empty trivial V59(1) set
[:(Seg n),{(x |-> x)}:] is set
bool [:(Seg n),{(x |-> x)}:] is set
n is non empty set
x is ext-real non negative V39() V40() V41() V45() finite V57() set
x is ext-real non negative V39() V40() V41() V45() finite V57() set
p is Element of n

Seg x is finite V59(x) Element of bool NAT

{p} is non empty trivial V59(1) set
[:(Seg x),{p}:] is set
bool [:(Seg x),{p}:] is set

Seg x is finite V59(x) Element of bool NAT
K168((Seg x),(x |-> p)) is Relation-like Seg x -defined {(x |-> p)} -valued Function-like V22( Seg x) quasi_total finite FinSequence-like FinSubsequence-like Element of bool [:(Seg x),{(x |-> p)}:]
{(x |-> p)} is functional non empty trivial V59(1) set
[:(Seg x),{(x |-> p)}:] is set
bool [:(Seg x),{(x |-> p)}:] is set

n is ext-real non negative V39() V40() V41() V45() finite V57() set
x is ext-real non negative V39() V40() V41() V45() finite V57() set
[n,x] is set
{n,x} is non empty set
{n} is non empty trivial V59(1) set
{{n,x},{n}} is non empty set
x is ext-real non negative V39() V40() V41() V45() finite V57() set
p is ext-real non negative V39() V40() V41() V45() finite V57() set
p9 is non empty set
q9 is Element of p9

Seg p is finite V59(p) Element of bool NAT

{q9} is non empty trivial V59(1) set
[:(Seg p),{q9}:] is set
bool [:(Seg p),{q9}:] is set

Seg x is finite V59(x) Element of bool NAT
K168((Seg x),(p |-> q9)) is Relation-like Seg x -defined {(p |-> q9)} -valued Function-like V22( Seg x) quasi_total finite FinSequence-like FinSubsequence-like Element of bool [:(Seg x),{(p |-> q9)}:]
{(p |-> q9)} is functional non empty trivial V59(1) set
[:(Seg x),{(p |-> q9)}:] is set
bool [:(Seg x),{(p |-> q9)}:] is set
Indices (p9,x,p,q9) is set
dom (p9,x,p,q9) is Element of bool NAT
width (p9,x,p,q9) is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
Seg (width (p9,x,p,q9)) is finite V59( width (p9,x,p,q9)) Element of bool NAT
[:(dom (p9,x,p,q9)),(Seg (width (p9,x,p,q9))):] is set
(p9,x,p,q9) * (n,x) is Element of p9
len (p9,x,p,q9) is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
Seg (len (p9,x,p,q9)) is finite V59( len (p9,x,p,q9)) Element of bool NAT
r9 is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT

{ } is set
Seg r9 is finite V59(r9) Element of bool NAT

[:(Seg r9),{q9}:] is set
bool [:(Seg r9),{q9}:] is set
(r9 |-> q9) . x is set

n is ext-real non negative V39() V40() V41() V45() finite V57() set

the carrier of x is non empty non trivial set
x is Element of the carrier of x
( the carrier of x,n,n,x) is Relation-like NAT -defined the carrier of x * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of n,n, the carrier of x
the carrier of x * is functional non empty FinSequence-membered FinSequenceSet of the carrier of x

Seg n is finite V59(n) Element of bool NAT

{x} is non empty trivial V59(1) set
[:(Seg n),{x}:] is set
bool [:(Seg n),{x}:] is set

K168((Seg n),(n |-> x)) is Relation-like Seg n -defined {(n |-> x)} -valued Function-like V22( Seg n) quasi_total finite FinSequence-like FinSubsequence-like Element of bool [:(Seg n),{(n |-> x)}:]
{(n |-> x)} is functional non empty trivial V59(1) set
[:(Seg n),{(n |-> x)}:] is set
bool [:(Seg n),{(n |-> x)}:] is set
p is Element of the carrier of x
( the carrier of x,n,n,p) is Relation-like NAT -defined the carrier of x * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of n,n, the carrier of x

{p} is non empty trivial V59(1) set
[:(Seg n),{p}:] is set
bool [:(Seg n),{p}:] is set

K168((Seg n),(n |-> p)) is Relation-like Seg n -defined {(n |-> p)} -valued Function-like V22( Seg n) quasi_total finite FinSequence-like FinSubsequence-like Element of bool [:(Seg n),{(n |-> p)}:]
{(n |-> p)} is functional non empty trivial V59(1) set
[:(Seg n),{(n |-> p)}:] is set
bool [:(Seg n),{(n |-> p)}:] is set
( the carrier of x,n,n,x) + ( the carrier of x,n,n,p) is Relation-like NAT -defined the carrier of x * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of n,n, the carrier of x
x + p is Element of the carrier of x
the addF of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like V22([: the carrier of x, the carrier of x:]) quasi_total Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is set
the addF of x . (x,p) is Element of the carrier of x
( the carrier of x,n,n,(x + p)) is Relation-like NAT -defined the carrier of x * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of n,n, the carrier of x

K168((Seg n),(x + p)) is Relation-like Seg n -defined {(x + p)} -valued Function-like V22( Seg n) quasi_total finite FinSequence-like FinSubsequence-like Element of bool [:(Seg n),{(x + p)}:]
{(x + p)} is non empty trivial V59(1) set
[:(Seg n),{(x + p)}:] is set
bool [:(Seg n),{(x + p)}:] is set

K168((Seg n),(n |-> (x + p))) is Relation-like Seg n -defined {(n |-> (x + p))} -valued Function-like V22( Seg n) quasi_total finite FinSequence-like FinSubsequence-like Element of bool [:(Seg n),{(n |-> (x + p))}:]
{(n |-> (x + p))} is functional non empty trivial V59(1) set
[:(Seg n),{(n |-> (x + p))}:] is set
bool [:(Seg n),{(n |-> (x + p))}:] is set
Indices ( the carrier of x,n,n,x) is set
dom ( the carrier of x,n,n,x) is Element of bool NAT
width ( the carrier of x,n,n,x) is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
Seg (width ( the carrier of x,n,n,x)) is finite V59( width ( the carrier of x,n,n,x)) Element of bool NAT
[:(dom ( the carrier of x,n,n,x)),(Seg (width ( the carrier of x,n,n,x))):] is set
Indices ( the carrier of x,n,n,(x + p)) is set
dom ( the carrier of x,n,n,(x + p)) is Element of bool NAT
width ( the carrier of x,n,n,(x + p)) is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
Seg (width ( the carrier of x,n,n,(x + p))) is finite V59( width ( the carrier of x,n,n,(x + p))) Element of bool NAT
[:(dom ( the carrier of x,n,n,(x + p))),(Seg (width ( the carrier of x,n,n,(x + p)))):] is set
Indices ( the carrier of x,n,n,p) is set
dom ( the carrier of x,n,n,p) is Element of bool NAT
width ( the carrier of x,n,n,p) is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
Seg (width ( the carrier of x,n,n,p)) is finite V59( width ( the carrier of x,n,n,p)) Element of bool NAT
[:(dom ( the carrier of x,n,n,p)),(Seg (width ( the carrier of x,n,n,p))):] is set
p9 is ext-real non negative V39() V40() V41() V45() finite V57() set
q9 is ext-real non negative V39() V40() V41() V45() finite V57() set
[p9,q9] is set
{p9,q9} is non empty set
{p9} is non empty trivial V59(1) set
{{p9,q9},{p9}} is non empty set
( the carrier of x,n,n,x) * (p9,q9) is Element of the carrier of x
( the carrier of x,n,n,p) * (p9,q9) is Element of the carrier of x
(( the carrier of x,n,n,x) * (p9,q9)) + (( the carrier of x,n,n,p) * (p9,q9)) is Element of the carrier of x
the addF of x . ((( the carrier of x,n,n,x) * (p9,q9)),(( the carrier of x,n,n,p) * (p9,q9))) is Element of the carrier of x
( the carrier of x,n,n,(x + p)) * (p9,q9) is Element of the carrier of x
n is set
x is set

x is set
p is set

len <*n,x*> is non empty ext-real positive non negative V39() V40() V41() V45() finite V57() Element of NAT
len <*x,p*> is non empty ext-real positive non negative V39() V40() V41() V45() finite V57() Element of NAT
[:(Seg 2),(Seg 2):] is set
n is set
x is set
x is set
p is set

len (n,x,x,p) is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
width (n,x,x,p) is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
Indices (n,x,x,p) is set
dom (n,x,x,p) is Element of bool NAT
Seg (width (n,x,x,p)) is finite V59( width (n,x,x,p)) Element of bool NAT
[:(dom (n,x,x,p)),(Seg (width (n,x,x,p))):] is set
rng (n,x,x,p) is set
{<*n,x*>,<*x,p*>} is functional non empty set
len <*n,x*> is non empty ext-real positive non negative V39() V40() V41() V45() finite V57() Element of NAT
[1,1] is set
{1,1} is non empty set
{{1,1},{1}} is non empty set
[1,2] is set
{{1,2},{1}} is non empty set
[2,1] is set
{2,1} is non empty set
{2} is non empty trivial V59(1) set
{{2,1},{2}} is non empty set
[2,2] is set
{2,2} is non empty set
{{2,2},{2}} is non empty set
n is set
x is set
x is set
p is set

Indices (n,x,x,p) is set
dom (n,x,x,p) is Element of bool NAT
width (n,x,x,p) is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
Seg (width (n,x,x,p)) is finite V59( width (n,x,x,p)) Element of bool NAT
[:(dom (n,x,x,p)),(Seg (width (n,x,x,p))):] is set
n is non empty set
x is Element of n

{ } is set
n is non empty set
x is ext-real non negative V39() V40() V41() V45() finite V57() set

{ } is set

len x is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
n is non empty set
x is Element of n

{ } is set

Indices (n,1,(n,x)) is set
dom (n,1,(n,x)) is non empty trivial V59(1) Element of bool NAT
width (n,1,(n,x)) is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
Seg (width (n,1,(n,x))) is finite V59( width (n,1,(n,x))) Element of bool NAT
[:(dom (n,1,(n,x))),(Seg (width (n,1,(n,x)))):] is set
(n,1,(n,x)) * (1,1) is Element of n

(n,x) . 1 is set
n is non empty set
x is Element of n
x is Element of n
p is Element of n
p9 is Element of n

n is non empty set
x is Element of n
x is Element of n
p is Element of n
p9 is Element of n

(n,x,x,p,p9) * (1,1) is Element of n
(n,x,x,p,p9) * (1,2) is Element of n
(n,x,x,p,p9) * (2,1) is Element of n
(n,x,x,p,p9) * (2,2) is Element of n

<*x,x*> . 1 is set
<*x,x*> . 2 is set
Indices (n,x,x,p,p9) is set
dom (n,x,x,p,p9) is Element of bool NAT
width (n,x,x,p,p9) is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
Seg (width (n,x,x,p,p9)) is finite V59( width (n,x,x,p,p9)) Element of bool NAT
[:(dom (n,x,x,p,p9)),(Seg (width (n,x,x,p,p9))):] is set
<*p,p9*> . 1 is set
<*p,p9*> . 2 is set

the carrier of x is non empty non trivial set
the carrier of x * is functional non empty FinSequence-membered FinSequenceSet of the carrier of x
n is ext-real non negative V39() V40() V41() V45() finite V57() set

the carrier of x is non empty non trivial set
the carrier of x * is functional non empty FinSequence-membered FinSequenceSet of the carrier of x
n is ext-real non negative V39() V40() V41() V45() finite V57() set

Indices x is set
dom x is Element of bool NAT
width x is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
Seg () is finite V59( width x) Element of bool NAT
[:(dom x),(Seg ()):] is set
0. x is V76(x) Element of the carrier of x
the ZeroF of x is Element of the carrier of x
p is ext-real non negative V39() V40() V41() V45() finite V57() set
p9 is ext-real non negative V39() V40() V41() V45() finite V57() set
[p,p9] is set
{p,p9} is non empty set
{p} is non empty trivial V59(1) set
{{p,p9},{p}} is non empty set
x * (p,p9) is Element of the carrier of x
p is ext-real non negative V39() V40() V41() V45() finite V57() set
p9 is ext-real non negative V39() V40() V41() V45() finite V57() set
[p,p9] is set
{p,p9} is non empty set
{p} is non empty trivial V59(1) set
{{p,p9},{p}} is non empty set
x * (p,p9) is Element of the carrier of x

the carrier of x is non empty non trivial set
the carrier of x * is functional non empty FinSequence-membered FinSequenceSet of the carrier of x
n is ext-real non negative V39() V40() V41() V45() finite V57() set
the Relation-like NAT -defined the carrier of x * -valued Function-like finite FinSequence-like FinSubsequence-like tabular diagonal (n,x) (n,x) Matrix of n,n, the carrier of x is Relation-like NAT -defined the carrier of x * -valued Function-like finite FinSequence-like FinSubsequence-like tabular diagonal (n,x) (n,x) Matrix of n,n, the carrier of x
n is ext-real non negative V39() V40() V41() V45() finite V57() set
x is non empty set

len x is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
width x is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
rng x is set
p9 is ext-real non negative V39() V40() V41() V45() finite V57() set

len q9 is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT

len q9 is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
r9 is set

len p9 is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
q9 is set

len r9 is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT

len j is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
rng x is set
n is ext-real non negative V39() V40() V41() V45() finite V57() set
Seg n is finite V59(n) Element of bool NAT
x is ext-real non negative V39() V40() V41() V45() finite V57() set
x is non empty set

p9 is ext-real non negative V39() V40() V41() V45() finite V57() set

width p is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT

{ } is set
len p is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
dom p is Element of bool NAT
Seg (len p) is finite V59( len p) Element of bool NAT
rng p is set
q9 is ext-real non negative V39() V40() V41() V45() finite V57() set

len r9 is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
Seg () is finite V59( width p) Element of bool NAT
p9 is ext-real non negative V39() V40() V41() V45() finite V57() set
r9 . p9 is set
p * (p9,p9) is Element of x
[p9,p9] is set
{p9,p9} is non empty set
{p9} is non empty trivial V59(1) set
{{p9,p9},{p9}} is non empty set
Seg x is finite V59(x) Element of bool NAT
[:(Seg n),(Seg x):] is set
Indices p is set
[:(dom p),(Seg ()):] is set

q9 . p9 is set

the carrier of n is non empty non trivial set
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n

dom x is Element of bool NAT
x is ext-real non negative V39() V40() V41() V45() finite V57() set

width x is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
() -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b1 where b1 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of n * : len b1 = width x } is set
len x is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT

len p is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
Seg (len p) is finite V59( len p) Element of bool NAT

the carrier of x is non empty non trivial set
the carrier of x * is functional non empty FinSequence-membered FinSequenceSet of the carrier of x

len x is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
dom x is Element of bool NAT
n is ext-real non negative V39() V40() V41() V45() finite V57() set
width x is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
Seg () is finite V59( width x) Element of bool NAT
p is ext-real non negative V39() V40() V41() V45() finite V57() set

() -tuples_on the carrier of x is functional non empty FinSequence-membered FinSequenceSet of the carrier of x
{ b1 where b1 is Relation-like NAT -defined the carrier of x -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of x * : len b1 = width x } is set

len (Line (x,p)) is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
dom (Line (x,p)) is V59( width x) Element of bool NAT
width x is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
Seg () is finite V59( width x) Element of bool NAT
Seg (len x) is finite V59( len x) Element of bool NAT
p9 is ext-real non negative V39() V40() V41() V45() finite V57() set
p9 + 1 is non empty ext-real positive non negative V39() V40() V41() V45() finite V57() Element of NAT
q9 is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
r9 is ext-real non negative V39() V40() V41() V45() finite V57() set

() -tuples_on the carrier of x is functional non empty FinSequence-membered FinSequenceSet of the carrier of x
{ b1 where b1 is Relation-like NAT -defined the carrier of x -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of x * : len b1 = width x } is set

len (Del ((Line (x,r9)),n)) is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
len (Line (x,r9)) is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
dom (Line (x,r9)) is V59( width x) Element of bool NAT
p9 is ext-real non negative V39() V40() V41() V45() finite V57() set
p9 + 1 is non empty ext-real positive non negative V39() V40() V41() V45() finite V57() Element of NAT
Seg (len x) is finite V59( len x) Element of bool NAT
Seg q9 is finite V59(q9) Element of bool NAT
[:(Seg (len x)),(Seg q9):] is set
r9 is ext-real non negative V39() V40() V41() V45() finite V57() set

() -tuples_on the carrier of x is functional non empty FinSequence-membered FinSequenceSet of the carrier of x
{ b1 where b1 is Relation-like NAT -defined the carrier of x -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of x * : len b1 = width x } is set

p9 is ext-real non negative V39() V40() V41() V45() finite V57() set
[r9,p9] is set
{r9,p9} is non empty set
{r9} is non empty trivial V59(1) set
{{r9,p9},{r9}} is non empty set
(Del ((Line (x,r9)),n)) . p9 is set

len q9 is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
dom q9 is Element of bool NAT
Seg (len q9) is finite V59( len q9) Element of bool NAT
q9 . p9 is set
r9 is Element of the carrier of x

Indices r9 is set
dom r9 is Element of bool NAT
width r9 is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
Seg (width r9) is finite V59( width r9) Element of bool NAT
[:(dom r9),(Seg (width r9)):] is set
[:(dom x),(Seg q9):] is set
p9 is ext-real non negative V39() V40() V41() V45() finite V57() set

() -tuples_on the carrier of x is functional non empty FinSequence-membered FinSequenceSet of the carrier of x
{ b1 where b1 is Relation-like NAT -defined the carrier of x -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of x * : len b1 = width x } is set

q9 is ext-real non negative V39() V40() V41() V45() finite V57() set
r9 * (p9,q9) is Element of the carrier of x
(Del ((Line (x,p9)),n)) . q9 is set
[p9,q9] is set
{p9,q9} is non empty set
{p9} is non empty trivial V59(1) set
{{p9,q9},{p9}} is non empty set

len p9 is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
q9 is ext-real non negative V39() V40() V41() V45() finite V57() set

() -tuples_on the carrier of x is functional non empty FinSequence-membered FinSequenceSet of the carrier of x
{ b1 where b1 is Relation-like NAT -defined the carrier of x -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of x * : len b1 = width x } is set

width p9 is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
(width p9) -tuples_on the carrier of x is functional non empty FinSequence-membered FinSequenceSet of the carrier of x
{ b1 where b1 is Relation-like NAT -defined the carrier of x -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of x * : len b1 = width p9 } is set

len r9 is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
dom r9 is Element of bool NAT
j is ext-real non negative V39() V40() V41() V45() finite V57() set
(Line (p9,q9)) . j is set
p9 * (q9,j) is Element of the carrier of x
r9 . j is set
(Del ((Line (x,q9)),n)) . j is set
len (Del ((Line (x,q9)),n)) is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
q9 is ext-real non negative V39() V40() V41() V45() finite V57() set

() -tuples_on the carrier of x is functional non empty FinSequence-membered FinSequenceSet of the carrier of x
{ b1 where b1 is Relation-like NAT -defined the carrier of x -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of x * : len b1 = width x } is set

width x is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
Seg () is finite V59( width x) Element of bool NAT

len p is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT

len p9 is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
dom p is Element of bool NAT
q9 is ext-real non negative V39() V40() V41() V45() finite V57() set

width x is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
() -tuples_on the carrier of x is functional non empty FinSequence-membered FinSequenceSet of the carrier of x
{ b1 where b1 is Relation-like NAT -defined the carrier of x -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of x * : len b1 = width x } is set

n is non empty set

len x is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
len x is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
len (x @) is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
width x is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
width x is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
Indices x is set
dom x is Element of bool NAT
Seg () is finite V59( width x) Element of bool NAT
[:(dom x),(Seg ()):] is set
Indices x is set
dom x is Element of bool NAT
Seg () is finite V59( width x) Element of bool NAT
[:(dom x),(Seg ()):] is set
p is ext-real non negative V39() V40() V41() V45() finite V57() set
p9 is ext-real non negative V39() V40() V41() V45() finite V57() set
[p,p9] is set
{p,p9} is non empty set
{p} is non empty trivial V59(1) set
{{p,p9},{p}} is non empty set
x * (p,p9) is Element of n
x * (p,p9) is Element of n
Seg (len x) is finite V59( len x) Element of bool NAT
(x @) * (p9,p) is Element of n
n is non empty set

width x is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT

len (x @) is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
width (x @) is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
len x is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
dom (x @) is Element of bool NAT
Seg (width (x @)) is finite V59( width (x @)) Element of bool NAT
[:(dom (x @)),(Seg (width (x @))):] is set
Seg () is finite V59( width x) Element of bool NAT
dom x is Element of bool NAT
[:(Seg ()),(dom x):] is set
x is set
p is set
[x,p] is set
{x,p} is non empty set
{x} is non empty trivial V59(1) set
{{x,p},{x}} is non empty set
p9 is ext-real non negative V39() V40() V41() V45() finite V57() set
q9 is ext-real non negative V39() V40() V41() V45() finite V57() set
[p9,q9] is set
{p9,q9} is non empty set
{p9} is non empty trivial V59(1) set
{{p9,q9},{p9}} is non empty set
Indices (x @) is set
[q9,p9] is set
{q9,p9} is non empty set
{q9} is non empty trivial V59(1) set
{{q9,p9},{q9}} is non empty set
Indices x is set
[:(dom x),(Seg ()):] is set
q9 is ext-real non negative V39() V40() V41() V45() finite V57() set
p9 is ext-real non negative V39() V40() V41() V45() finite V57() set
[q9,p9] is set
{q9,p9} is non empty set
{q9} is non empty trivial V59(1) set
{{q9,p9},{q9}} is non empty set
Indices x is set
[:(dom x),(Seg ()):] is set
[p9,q9] is set
{p9,q9} is non empty set
{p9} is non empty trivial V59(1) set
{{p9,q9},{p9}} is non empty set
Indices (x @) is set
Seg (len x) is finite V59( len x) Element of bool NAT
n is non empty set

width x is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT

width x is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT

width (x @) is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
len x is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
width (x @) is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
len x is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
n is non empty set

width x is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT

width x is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT

len x is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
width (x @) is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
len x is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
Indices x is set
dom x is Element of bool NAT
Seg () is finite V59( width x) Element of bool NAT
[:(dom x),(Seg ()):] is set
Indices x is set
dom x is Element of bool NAT
Seg () is finite V59( width x) Element of bool NAT
[:(dom x),(Seg ()):] is set
p is ext-real non negative V39() V40() V41() V45() finite V57() set
p9 is ext-real non negative V39() V40() V41() V45() finite V57() set
[p,p9] is set
{p,p9} is non empty set
{p} is non empty trivial V59(1) set
{{p,p9},{p}} is non empty set
x * (p,p9) is Element of n
x * (p,p9) is Element of n
Seg (len x) is finite V59( len x) Element of bool NAT
(x @) * (p9,p) is Element of n
n is non empty set

len x is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
width x is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT

width (x @) is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
len ((x @) @) is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
len (x @) is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
dom x is Element of bool NAT
Seg (len x) is finite V59( len x) Element of bool NAT
dom ((x @) @) is Element of bool NAT
Seg (len ((x @) @)) is finite V59( len ((x @) @)) Element of bool NAT
Indices ((x @) @) is set
width ((x @) @) is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
Seg (width ((x @) @)) is finite V59( width ((x @) @)) Element of bool NAT
[:(dom ((x @) @)),(Seg (width ((x @) @))):] is set
Indices x is set
Seg () is finite V59( width x) Element of bool NAT
[:(dom x),(Seg ()):] is set
p is ext-real non negative V39() V40() V41() V45() finite V57() set
p9 is ext-real non negative V39() V40() V41() V45() finite V57() set
[p,p9] is set
{p,p9} is non empty set
{p} is non empty trivial V59(1) set
{{p,p9},{p}} is non empty set
((x @) @) * (p,p9) is Element of n
x * (p,p9) is Element of n
[p9,p] is set
{p9,p} is non empty set
{p9} is non empty trivial V59(1) set
{{p9,p},{p9}} is non empty set
Indices (x @) is set
dom (x @) is Element of bool NAT
Seg (width (x @)) is finite V59( width (x @)) Element of bool NAT
[:(dom (x @)),(Seg (width (x @))):] is set
(x @) * (p9,p) is Element of n
n is non empty set

dom x is Element of bool NAT

x is ext-real non negative V39() V40() V41() V45() finite V57() set

width x is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT

{ } is set

len (x @) is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
(len (x @)) -tuples_on n is functional non empty FinSequence-membered FinSequenceSet of n
{ } is set
len (Col ((x @),x)) is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
dom (Col ((x @),x)) is V59( len (x @)) Element of bool NAT
Seg () is finite V59( width x) Element of bool NAT
dom (x @) is Element of bool NAT
Seg (len (x @)) is finite V59( len (x @)) Element of bool NAT
p is ext-real non negative V39() V40() V41() V45() finite V57() set
(Line (x,x)) . p is set
x * (x,p) is Element of n
[x,p] is set
{x,p} is non empty set
{x} is non empty trivial V59(1) set
{{x,p},{x}} is non empty set
Indices x is set
[:(dom x),(Seg ()):] is set
(x @) * (p,x) is Element of n
(Col ((x @),x)) . p is set
len (Line (x,x)) is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
n is non empty set

width x is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
Seg () is finite V59( width x) Element of bool NAT

x is ext-real non negative V39() V40() V41() V45() finite V57() set

width (x @) is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT

{ } is set

len x is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT

{ } is set
len (x @) is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
Seg (len (x @)) is finite V59( len (x @)) Element of bool NAT
dom (x @) is Element of bool NAT
Seg (len x) is finite V59( len x) Element of bool NAT

n is non empty set

dom x is Element of bool NAT
x is ext-real non negative V39() V40() V41() V45() finite V57() set

width x is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT

{ } is set
rng x is set
len x is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT

len p is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
len (Line (x,x)) is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
dom (Line (x,x)) is V59( width x) Element of bool NAT
Seg () is finite V59( width x) Element of bool NAT
p9 is ext-real non negative V39() V40() V41() V45() finite V57() set
x * (x,p9) is Element of n
p . p9 is set
[x,p9] is set
{x,p9} is non empty set
{x} is non empty trivial V59(1) set
{{x,p9},{x}} is non empty set
Indices x is set
[:(dom x),(Seg ()):] is set

q9 . p9 is set
p9 is ext-real non negative V39() V40() V41() V45() finite V57() set
(Line (x,x)) . p9 is set
x * (x,p9) is Element of n
p . p9 is set

the carrier of n is non empty non trivial set
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n

the carrier of n is non empty non trivial set
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
x is ext-real non negative V39() V40() V41() V45() finite V57() set

rng x is set
p is ext-real non negative V39() V40() V41() V45() finite V57() set
rng (Del (x,x)) is set
p9 is set

the carrier of n is non empty non trivial set
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
x is ext-real non negative V39() V40() V41() V45() finite V57() set

the carrier of p is non empty non trivial set
the carrier of p * is functional non empty FinSequence-membered FinSequenceSet of the carrier of p
x is ext-real non negative V39() V40() V41() V45() finite V57() set
x is ext-real non negative V39() V40() V41() V45() finite V57() set
n is ext-real non negative V39() V40() V41() V45() finite V57() set

(x,p,(p,n,p9)) is Relation-like NAT -defined the carrier of p * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of p *
the ext-real non negative V39() V40() V41() V45() finite V57() set is ext-real non negative V39() V40() V41() V45() finite V57() set
Seg the ext-real non negative V39() V40() V41() V45() finite V57() set is finite V59( the ext-real non negative V39() V40() V41() V45() finite V57() set ) Element of bool NAT
[:(Seg the ext-real non negative V39() V40() V41() V45() finite V57() set ),(Seg the ext-real non negative V39() V40() V41() V45() finite V57() set ):] is set
bool [:(Seg the ext-real non negative V39() V40() V41() V45() finite V57() set ),(Seg the ext-real non negative V39() V40() V41() V45() finite V57() set ):] is set
the Relation-like Seg the ext-real non negative V39() V40() V41() V45() finite V57() set -defined Seg the ext-real non negative V39() V40() V41() V45() finite V57() set -valued Function-like one-to-one V22( Seg the ext-real non negative V39() V40() V41() V45() finite V57() set ) quasi_total onto bijective Element of bool [:(Seg the ext-real non negative V39() V40() V41() V45() finite V57() set ),(Seg the ext-real non negative V39() V40() V41() V45() finite V57() set ):] is Relation-like Seg the ext-real non negative V39() V40() V41() V45() finite V57() set -defined Seg the ext-real non negative V39() V40() V41() V45() finite V57() set -valued Function-like one-to-one V22( Seg the ext-real non negative V39() V40() V41() V45() finite V57() set ) quasi_total onto bijective Element of bool [:(Seg the ext-real non negative V39() V40() V41() V45() finite V57() set ),(Seg the ext-real non negative V39() V40() V41() V45() finite V57() set ):]
{ the Relation-like Seg the ext-real non negative V39() V40() V41() V45() finite V57() set -defined Seg the ext-real non negative V39() V40() V41() V45() finite V57() set -valued Function-like one-to-one V22( Seg the ext-real non negative V39() V40() V41() V45() finite V57() set ) quasi_total onto bijective Element of bool [:(Seg the ext-real non negative V39() V40() V41() V45() finite V57() set ),(Seg the ext-real non negative V39() V40() V41() V45() finite V57() set ):]} is functional non empty trivial V59(1) set
x is functional non empty trivial V59(1) set
p is set
n is non empty () set
the Element of n is Element of n
x is ext-real non negative V39() V40() V41() V45() finite V57() set
Seg x is finite V59(x) Element of bool NAT
[:(Seg x),(Seg x):] is set
bool [:(Seg x),(Seg x):] is set
p is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
Seg p is finite V59(p) Element of bool NAT
[:(Seg p),(Seg p):] is set
bool [:(Seg p),(Seg p):] is set

dom p9 is set

len q9 is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
x is ext-real non negative V39() V40() V41() V45() finite V57() set
x is ext-real non negative V39() V40() V41() V45() finite V57() set

len p is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
p9 is ext-real non negative V39() V40() V41() V45() finite V57() set
Seg p9 is finite V59(p9) Element of bool NAT
[:(Seg p9),(Seg p9):] is set
bool [:(Seg p9),(Seg p9):] is set
dom p is Element of bool NAT

len q9 is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
dom q9 is Element of bool NAT
n is non empty () set
(n) is ext-real non negative V39() V40() V41() V45() finite V57() set
n is non empty () set
(n) is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
Seg (n) is finite V59((n)) Element of bool NAT
[:(Seg (n)),(Seg (n)):] is set
bool [:(Seg (n)),(Seg (n)):] is set
x is Element of n
x is ext-real non negative V39() V40() V41() V45() finite V57() set
Seg x is finite V59(x) Element of bool NAT
[:(Seg x),(Seg x):] is set
bool [:(Seg x),(Seg x):] is set
p is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
Seg p is finite V59(p) Element of bool NAT
[:(Seg p),(Seg p):] is set
bool [:(Seg p),(Seg p):] is set

dom p9 is set

len q9 is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
n is ext-real non negative V39() V40() V41() V45() finite V57() set
Seg n is finite V59(n) Element of bool NAT
[:(Seg n),(Seg n):] is set
bool [:(Seg n),(Seg n):] is set

{} is functional non empty trivial V59(1) set
p9 is set
p is ext-real non negative V39() V40() V41() V45() finite V57() set
Seg p is finite V59(p) Element of bool NAT
[:(Seg p),(Seg p):] is set
bool [:(Seg p),(Seg p):] is set
p9 is ext-real non negative V39() V40() V41() V45() finite V57() set
Seg p9 is finite V59(p9) Element of bool NAT
[:(Seg p9),(Seg p9):] is set
bool [:(Seg p9),(Seg p9):] is set
p is non empty () set
(p) is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
Seg (p) is finite V59((p)) Element of bool NAT

dom q9 is set

len r9 is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
n is ext-real non negative V39() V40() V41() V45() finite V57() set
Seg n is finite V59(n) Element of bool NAT
[:(Seg n),(Seg n):] is set
bool [:(Seg n),(Seg n):] is set
Funcs ((Seg n),(Seg n)) is functional non empty set
x is set
x is set
x is set
x is set
p is set
p is set
n is ext-real non negative V39() V40() V41() V45() finite V57() set
(n) is set
Seg n is finite V59(n) Element of bool NAT
[:(Seg n),(Seg n):] is set
bool [:(Seg n),(Seg n):] is set
Funcs ((Seg n),(Seg n)) is functional non empty set
x is set