REAL is set
NAT is non empty V39() V40() V41() non finite V57() V58() Element of bool REAL
bool REAL is set
COMPLEX is set
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
{} is Function-like functional empty ext-real non positive non negative V39() V40() V41() V43() V44() V45() finite V57() V59( {} ) FinSequence-membered 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
0 is Function-like functional empty ext-real non positive non negative V39() V40() V41() V43() V44() V45() finite V57() V59( {} ) FinSequence-membered 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
idseq 1 is Relation-like NAT -defined Function-like constant non empty trivial finite V59(1) FinSequence-like FinSubsequence-like 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
<*1*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V59(1) FinSequence-like FinSubsequence-like FinSequence of NAT
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
x |-> x is Relation-like NAT -defined Function-like finite V59(x) FinSequence-like FinSubsequence-like set
Seg x is finite V59(x) Element of bool NAT
K168((Seg x),x) is Relation-like Seg x -defined {x} -valued Function-like V22( Seg x) quasi_total finite FinSequence-like FinSubsequence-like Element of bool [:(Seg x),{x}:]
{x} is non empty trivial V59(1) set
[:(Seg x),{x}:] is set
bool [:(Seg x),{x}:] is set
n |-> (x |-> x) is Relation-like NAT -defined Function-like finite V59(n) FinSequence-like FinSubsequence-like 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
(x,x,p) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like tabular set
x |-> p is Relation-like NAT -defined Function-like finite V59(x) FinSequence-like FinSubsequence-like set
Seg x is finite V59(x) Element of bool NAT
K168((Seg x),p) is Relation-like Seg x -defined {p} -valued Function-like V22( Seg x) quasi_total finite FinSequence-like FinSubsequence-like Element of bool [:(Seg x),{p}:]
{p} is non empty trivial V59(1) set
[:(Seg x),{p}:] is set
bool [:(Seg x),{p}:] is set
x |-> (x |-> p) is Relation-like NAT -defined Function-like finite V59(x) FinSequence-like FinSubsequence-like 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 functional non empty FinSequence-membered FinSequenceSet of n
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
(p9,x,p,q9) is Relation-like NAT -defined p9 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of x,p,p9
p9 * is functional non empty FinSequence-membered FinSequenceSet of p9
p |-> q9 is Relation-like NAT -defined Function-like finite V59(p) FinSequence-like FinSubsequence-like set
Seg p is finite V59(p) Element of bool NAT
K168((Seg p),q9) is Relation-like Seg p -defined {q9} -valued Function-like V22( Seg p) quasi_total finite FinSequence-like FinSubsequence-like Element of bool [:(Seg p),{q9}:]
{q9} is non empty trivial V59(1) set
[:(Seg p),{q9}:] is set
bool [:(Seg p),{q9}:] is set
x |-> (p |-> q9) is Relation-like NAT -defined Function-like finite V59(x) FinSequence-like FinSubsequence-like 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
r9 |-> q9 is Relation-like NAT -defined p9 -valued Function-like finite V59(r9) FinSequence-like FinSubsequence-like Element of r9 -tuples_on p9
r9 -tuples_on p9 is functional non empty FinSequence-membered FinSequenceSet of p9
{ b1 where b1 is Relation-like NAT -defined p9 -valued Function-like finite FinSequence-like FinSubsequence-like Element of p9 * : len b1 = r9 } is set
Seg r9 is finite V59(r9) Element of bool NAT
K168((Seg r9),q9) is Relation-like Seg r9 -defined {q9} -valued Function-like V22( Seg r9) quasi_total finite FinSequence-like FinSubsequence-like Element of bool [:(Seg r9),{q9}:]
[:(Seg r9),{q9}:] is set
bool [:(Seg r9),{q9}:] is set
(r9 |-> q9) . x is set
(p9,x,p,q9) . n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
n is ext-real non negative V39() V40() V41() V45() finite V57() set
x is non empty non degenerated non trivial right_complementable almost_left_invertible associative commutative V150() V151() V152() well-unital V164() doubleLoopStr
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
n |-> x is Relation-like NAT -defined Function-like finite V59(n) FinSequence-like FinSubsequence-like set
Seg n is finite V59(n) Element of bool NAT
K168((Seg n),x) is Relation-like Seg n -defined {x} -valued Function-like V22( Seg n) quasi_total finite FinSequence-like FinSubsequence-like Element of bool [:(Seg n),{x}:]
{x} is non empty trivial V59(1) set
[:(Seg n),{x}:] is set
bool [:(Seg n),{x}:] is set
n |-> (n |-> x) is Relation-like NAT -defined Function-like finite V59(n) FinSequence-like FinSubsequence-like 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
n |-> p is Relation-like NAT -defined Function-like finite V59(n) FinSequence-like FinSubsequence-like set
K168((Seg n),p) is Relation-like Seg n -defined {p} -valued Function-like V22( Seg n) quasi_total finite FinSequence-like FinSubsequence-like Element of bool [:(Seg n),{p}:]
{p} is non empty trivial V59(1) set
[:(Seg n),{p}:] is set
bool [:(Seg n),{p}:] is set
n |-> (n |-> p) is Relation-like NAT -defined Function-like finite V59(n) FinSequence-like FinSubsequence-like 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
n |-> (x + p) is Relation-like NAT -defined Function-like finite V59(n) FinSequence-like FinSubsequence-like set
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
n |-> (n |-> (x + p)) is Relation-like NAT -defined Function-like finite V59(n) FinSequence-like FinSubsequence-like 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
<*n,x*> is Relation-like NAT -defined Function-like non empty finite V59(2) FinSequence-like FinSubsequence-like set
x is set
p is set
<*x,p*> is Relation-like NAT -defined Function-like non empty finite V59(2) FinSequence-like FinSubsequence-like set
<*<*n,x*>,<*x,p*>*> is Relation-like NAT -defined Function-like non empty finite V59(2) FinSequence-like FinSubsequence-like 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
(n,x,x,p) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like tabular set
<*n,x*> is Relation-like NAT -defined Function-like non empty finite V59(2) FinSequence-like FinSubsequence-like set
<*x,p*> is Relation-like NAT -defined Function-like non empty finite V59(2) FinSequence-like FinSubsequence-like set
<*<*n,x*>,<*x,p*>*> is Relation-like NAT -defined Function-like non empty finite V59(2) FinSequence-like FinSubsequence-like 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
(n,x,x,p) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like tabular set
<*n,x*> is Relation-like NAT -defined Function-like non empty finite V59(2) FinSequence-like FinSubsequence-like set
<*x,p*> is Relation-like NAT -defined Function-like non empty finite V59(2) FinSequence-like FinSubsequence-like set
<*<*n,x*>,<*x,p*>*> is Relation-like NAT -defined Function-like non empty finite V59(2) FinSequence-like FinSubsequence-like 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
<*x*> is Relation-like NAT -defined Function-like constant non empty trivial finite V59(1) FinSequence-like FinSubsequence-like set
1 -tuples_on n is functional non empty FinSequence-membered FinSequenceSet of n
n * is functional non empty FinSequence-membered FinSequenceSet of n
{ b1 where b1 is Relation-like NAT -defined n -valued Function-like finite FinSequence-like FinSubsequence-like Element of n * : len b1 = 1 } is set
n is non empty set
x is ext-real non negative V39() V40() V41() V45() finite V57() set
x -tuples_on n is functional non empty FinSequence-membered FinSequenceSet of n
n * is functional non empty FinSequence-membered FinSequenceSet of n
{ b1 where b1 is Relation-like NAT -defined n -valued Function-like finite FinSequence-like FinSubsequence-like Element of n * : len b1 = x } is set
x is Relation-like NAT -defined n -valued Function-like finite V59(x) FinSequence-like FinSubsequence-like Element of x -tuples_on n
<*x*> is Relation-like NAT -defined Function-like constant non empty trivial finite V59(1) FinSequence-like FinSubsequence-like 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
(n,x) is Relation-like NAT -defined n -valued Function-like constant non empty trivial finite V59(1) FinSequence-like FinSubsequence-like Element of 1 -tuples_on n
1 -tuples_on n is functional non empty FinSequence-membered FinSequenceSet of n
n * is functional non empty FinSequence-membered FinSequenceSet of n
{ b1 where b1 is Relation-like NAT -defined n -valued Function-like finite FinSequence-like FinSubsequence-like Element of n * : len b1 = 1 } is set
(n,1,(n,x)) is Relation-like NAT -defined n * -valued Function-like constant non empty trivial finite V59(1) FinSequence-like FinSubsequence-like tabular Matrix of 1,1,n
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,1,(n,x)) . 1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(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
(x,x,p,p9) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like tabular set
<*x,x*> is Relation-like NAT -defined Function-like non empty finite V59(2) FinSequence-like FinSubsequence-like set
<*p,p9*> is Relation-like NAT -defined Function-like non empty finite V59(2) FinSequence-like FinSubsequence-like set
<*<*x,x*>,<*p,p9*>*> is Relation-like NAT -defined Function-like non empty finite V59(2) FinSequence-like FinSubsequence-like set
n * is functional non empty FinSequence-membered FinSequenceSet 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) is Relation-like NAT -defined n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of 2,2,n
n * is functional non empty FinSequence-membered FinSequenceSet of n
<*x,x*> is Relation-like NAT -defined Function-like non empty finite V59(2) FinSequence-like FinSubsequence-like set
<*p,p9*> is Relation-like NAT -defined Function-like non empty finite V59(2) FinSequence-like FinSubsequence-like set
<*<*x,x*>,<*p,p9*>*> is Relation-like NAT -defined Function-like non empty finite V59(2) FinSequence-like FinSubsequence-like set
(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
(n,x,x,p,p9) . 1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*x,x*> is Relation-like NAT -defined n -valued Function-like non empty finite V59(2) FinSequence-like FinSubsequence-like FinSequence of n
(n,x,x,p,p9) . 2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*p,p9*> is Relation-like NAT -defined n -valued Function-like non empty finite V59(2) FinSequence-like FinSubsequence-like FinSequence 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
x is non empty non degenerated non trivial right_complementable almost_left_invertible associative commutative V150() V151() V152() well-unital V164() doubleLoopStr
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
x is non empty non degenerated non trivial right_complementable almost_left_invertible associative commutative V150() V151() V152() well-unital V164() doubleLoopStr
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
x is Relation-like NAT -defined the carrier of x * -valued Function-like finite FinSequence-like FinSubsequence-like tabular diagonal Matrix of n,n, the carrier of x
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 (width x) is finite V59( width x) Element of bool NAT
[:(dom x),(Seg (width x)):] 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
x is non empty non degenerated non trivial right_complementable almost_left_invertible associative commutative V150() V151() V152() well-unital V164() doubleLoopStr
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
x * is functional non empty FinSequence-membered FinSequenceSet of x
x is Relation-like NAT -defined x * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of x *
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
q9 is Relation-like NAT -defined x -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of x
len q9 is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
q9 is Relation-like NAT -defined x -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of x
len q9 is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
r9 is set
p9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len p9 is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
q9 is set
r9 is Relation-like NAT -defined x -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of x
len r9 is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
j is Relation-like NAT -defined x -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of x
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
x * is functional non empty FinSequence-membered FinSequenceSet of x
p is Relation-like NAT -defined x * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of n,x,x
p9 is ext-real non negative V39() V40() V41() V45() finite V57() set
p . p9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Line (p,p9) is Relation-like NAT -defined x -valued Function-like finite V59( width p) FinSequence-like FinSubsequence-like Element of (width p) -tuples_on x
width p is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
(width p) -tuples_on x is functional non empty FinSequence-membered FinSequenceSet of x
{ b1 where b1 is Relation-like NAT -defined x -valued Function-like finite FinSequence-like FinSubsequence-like Element of x * : len b1 = width p } 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
r9 is Relation-like NAT -defined x -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of x
len r9 is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
Seg (width p) 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 (width p)):] is set
q9 is Relation-like NAT -defined x -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of x
q9 . p9 is set
n is non empty non degenerated non trivial right_complementable almost_left_invertible associative commutative V150() V151() V152() well-unital V164() doubleLoopStr
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 Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence 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
x . x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Line (x,x) is Relation-like NAT -defined the carrier of n -valued Function-like finite V59( width x) FinSequence-like FinSubsequence-like Element of (width x) -tuples_on the carrier of n
width x is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
(width x) -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
p is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of len x, width x, the carrier of n
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
x is non empty non degenerated non trivial right_complementable almost_left_invertible associative commutative V150() V151() V152() well-unital V164() doubleLoopStr
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
x is Relation-like NAT -defined the carrier of x * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence 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 (width x) is finite V59( width x) Element of bool NAT
p is ext-real non negative V39() V40() V41() V45() finite V57() set
x . p is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Line (x,p) is Relation-like NAT -defined the carrier of x -valued Function-like finite V59( width x) FinSequence-like FinSubsequence-like Element of (width x) -tuples_on the carrier of x
(width x) -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
Del ((Line (x,p)),n) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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 (width x) 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
Line (x,r9) is Relation-like NAT -defined the carrier of x -valued Function-like finite V59( width x) FinSequence-like FinSubsequence-like Element of (width x) -tuples_on the carrier of x
(width x) -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
Del ((Line (x,r9)),n) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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
Line (x,r9) is Relation-like NAT -defined the carrier of x -valued Function-like finite V59( width x) FinSequence-like FinSubsequence-like Element of (width x) -tuples_on the carrier of x
(width x) -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
Del ((Line (x,r9)),n) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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
q9 is Relation-like NAT -defined the carrier of x -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of x
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
r9 is Relation-like NAT -defined the carrier of x * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of len x,q9, 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
Line (x,p9) is Relation-like NAT -defined the carrier of x -valued Function-like finite V59( width x) FinSequence-like FinSubsequence-like Element of (width x) -tuples_on the carrier of x
(width x) -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
Del ((Line (x,p9)),n) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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
p9 is Relation-like NAT -defined the carrier of x * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of x *
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
p9 . q9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Line (x,q9) is Relation-like NAT -defined the carrier of x -valued Function-like finite V59( width x) FinSequence-like FinSubsequence-like Element of (width x) -tuples_on the carrier of x
(width x) -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
Del ((Line (x,q9)),n) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Line (p9,q9) is Relation-like NAT -defined the carrier of x -valued Function-like finite V59( width p9) FinSequence-like FinSubsequence-like Element of (width p9) -tuples_on the carrier of x
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
r9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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
p9 . q9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Line (x,q9) is Relation-like NAT -defined the carrier of x -valued Function-like finite V59( width x) FinSequence-like FinSubsequence-like Element of (width x) -tuples_on the carrier of x
(width x) -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
Del ((Line (x,q9)),n) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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
p is Relation-like NAT -defined the carrier of x * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of x *
len p is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
p9 is Relation-like NAT -defined the carrier of x * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of x *
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
p . q9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Line (x,q9) is Relation-like NAT -defined the carrier of x -valued Function-like finite V59( width x) FinSequence-like FinSubsequence-like Element of (width x) -tuples_on the carrier of x
width x is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
(width x) -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
Del ((Line (x,q9)),n) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
p9 . q9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
n is non empty set
n * is functional non empty FinSequence-membered FinSequenceSet of n
x is Relation-like NAT -defined n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of n *
x @ is Relation-like NAT -defined n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of n *
x is Relation-like NAT -defined n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of n *
x @ is Relation-like NAT -defined n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of n *
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 (width x) is finite V59( width x) Element of bool NAT
[:(dom x),(Seg (width x)):] is 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
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
n * is functional non empty FinSequence-membered FinSequenceSet of n
x is Relation-like NAT -defined n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of n *
width x is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
x @ is Relation-like NAT -defined n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of n *
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 (width x) is finite V59( width x) Element of bool NAT
dom x is Element of bool NAT
[:(Seg (width x)),(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 (width x)):] 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 (width x)):] 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
n * is functional non empty FinSequence-membered FinSequenceSet of n
x is Relation-like NAT -defined n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of n *
width x is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
x is Relation-like NAT -defined n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of n *
width x is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
x @ is Relation-like NAT -defined n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of n *
x @ is Relation-like NAT -defined n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of n *
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
n * is functional non empty FinSequence-membered FinSequenceSet of n
x is Relation-like NAT -defined n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of n *
width x is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
x is Relation-like NAT -defined n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of n *
width x is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
x @ is Relation-like NAT -defined n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of n *
x @ is Relation-like NAT -defined n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of n *
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 (width x) is finite V59( width x) Element of bool NAT
[:(dom x),(Seg (width x)):] is 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
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
n * is functional non empty FinSequence-membered FinSequenceSet of n
x is Relation-like NAT -defined n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of n *
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
x @ is Relation-like NAT -defined n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of n *
(x @) @ is Relation-like NAT -defined n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of n *
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 (width x) is finite V59( width x) Element of bool NAT
[:(dom x),(Seg (width x)):] 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
n * is functional non empty FinSequence-membered FinSequenceSet of n
x is Relation-like NAT -defined n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of n *
dom x is Element of bool NAT
x @ is Relation-like NAT -defined n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of n *
x is ext-real non negative V39() V40() V41() V45() finite V57() set
Line (x,x) is Relation-like NAT -defined n -valued Function-like finite V59( width x) FinSequence-like FinSubsequence-like Element of (width x) -tuples_on n
width x is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
(width x) -tuples_on n is functional non empty FinSequence-membered FinSequenceSet of n
{ b1 where b1 is Relation-like NAT -defined n -valued Function-like finite FinSequence-like FinSubsequence-like Element of n * : len b1 = width x } is set
Col ((x @),x) is Relation-like NAT -defined n -valued Function-like finite V59( len (x @)) FinSequence-like FinSubsequence-like Element of (len (x @)) -tuples_on n
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
{ b1 where b1 is Relation-like NAT -defined n -valued Function-like finite FinSequence-like FinSubsequence-like Element of n * : len b1 = len (x @) } 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 (width x) 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 (width x)):] 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
n * is functional non empty FinSequence-membered FinSequenceSet of n
x is Relation-like NAT -defined n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of n *
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
x @ is Relation-like NAT -defined n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of n *
x is ext-real non negative V39() V40() V41() V45() finite V57() set
Line ((x @),x) is Relation-like NAT -defined n -valued Function-like finite V59( width (x @)) FinSequence-like FinSubsequence-like Element of (width (x @)) -tuples_on n
width (x @) is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
(width (x @)) -tuples_on n is functional non empty FinSequence-membered FinSequenceSet of n
{ b1 where b1 is Relation-like NAT -defined n -valued Function-like finite FinSequence-like FinSubsequence-like Element of n * : len b1 = width (x @) } is set
Col (x,x) is Relation-like NAT -defined n -valued Function-like finite V59( len x) FinSequence-like FinSubsequence-like Element of (len x) -tuples_on n
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
{ b1 where b1 is Relation-like NAT -defined n -valued Function-like finite FinSequence-like FinSubsequence-like Element of n * : len b1 = len x } 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
(x @) @ is Relation-like NAT -defined n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of n *
n is non empty set
n * is functional non empty FinSequence-membered FinSequenceSet of n
x is Relation-like NAT -defined n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of n *
dom x is Element of bool NAT
x is ext-real non negative V39() V40() V41() V45() finite V57() set
x . x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Line (x,x) is Relation-like NAT -defined n -valued Function-like finite V59( width x) FinSequence-like FinSubsequence-like Element of (width x) -tuples_on n
width x is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
(width x) -tuples_on n is functional non empty FinSequence-membered FinSequenceSet of n
{ b1 where b1 is Relation-like NAT -defined n -valued Function-like finite FinSequence-like FinSubsequence-like Element of n * : len b1 = width x } is set
rng x is set
len x is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
p is Relation-like NAT -defined n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of n
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 (width x) 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 (width x)):] is set
q9 is Relation-like NAT -defined n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of n
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
n is non empty non degenerated non trivial right_complementable almost_left_invertible associative commutative V150() V151() V152() well-unital V164() doubleLoopStr
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
n is non empty non degenerated non trivial right_complementable almost_left_invertible associative commutative V150() V151() V152() well-unital V164() doubleLoopStr
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
x is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
Del (x,x) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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
n is non empty non degenerated non trivial right_complementable almost_left_invertible associative commutative V150() V151() V152() well-unital V164() doubleLoopStr
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
x is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
Del (x,x) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like tabular set
p is non empty non degenerated non trivial right_complementable almost_left_invertible associative commutative V150() V151() V152() well-unital V164() doubleLoopStr
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
p9 is Relation-like NAT -defined the carrier of p * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of x,x, the carrier of 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 *
(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
p9 is Relation-like Seg p -defined Seg p -valued Function-like one-to-one V22( Seg p) quasi_total onto bijective Element of bool [:(Seg p),(Seg p):]
dom p9 is set
q9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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
p is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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
q9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
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
p9 is Relation-like Seg p -defined Seg p -valued Function-like one-to-one V22( Seg p) quasi_total onto bijective Element of bool [:(Seg p),(Seg p):]
dom p9 is set
q9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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
the Relation-like Seg n -defined Seg n -valued Function-like one-to-one V22( Seg n) quasi_total onto bijective Element of bool [:(Seg n),(Seg n):] is Relation-like Seg n -defined Seg n -valued Function-like one-to-one V22( Seg n) quasi_total onto bijective Element of bool [:(Seg n),(Seg n):]
{ the Relation-like Seg n -defined Seg n -valued Function-like one-to-one V22( Seg n) quasi_total onto bijective Element of bool [:(Seg n),(Seg n):]} 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
the Relation-like Seg (p) -defined Seg (p) -valued Function-like one-to-one V22( Seg (p)) quasi_total onto bijective (p) is Relation-like Seg (p) -defined Seg (p) -valued Function-like one-to-one V22( Seg (p)) quasi_total onto bijective (p)
q9 is Relation-like Seg n -defined Seg n -valued Function-like V22( Seg n) quasi_total Element of bool [:(Seg n),(Seg n):]
dom q9 is set
r9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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
idseq n is Relation-like NAT -defined Function-like finite V59(n) FinSequence-like FinSubsequence-like set
id (Seg n) is Relation-like Seg n -defined Seg n -valued V6() V8() V9() V13() Function-like one-to-one V22( Seg n) quasi_total onto bijective Element of bool [:(Seg n),(Seg n):]
p9 is set
x is non empty 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
p9 is 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
the Relation-like Seg ((n)) -defined Seg ((n)) -valued Function-like one-to-one V22( Seg ((n))) quasi_total onto bijective ((n)) is Relation-like Seg ((n)) -defined Seg ((n)) -valued Function-like one-to-one V22( Seg ((n))) quasi_total onto bijective ((n))
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 Relation-like Seg n -defined Seg n -valued Function-like one-to-one V22( Seg n) quasi_total onto bijective Element of bool [:(Seg n),(Seg n):]
dom x is set
p is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len p is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
(1) is non empty () set
{(idseq 1)} is functional non empty trivial V59(1) set
n is set
x is Relation-like Seg 1 -defined Seg 1 -valued Function-like one-to-one non empty V22( Seg 1) quasi_total onto bijective Element of bool [:(Seg 1),(Seg 1):]
dom x is set
rng x is set
x . 1 is set
x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len x is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
n is 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
x is Relation-like Seg ((n)) -defined Seg ((n)) -valued Function-like one-to-one V22( Seg ((n))) quasi_total onto bijective ((n))
x is Relation-like Seg ((n)) -defined Seg ((n)) -valued Function-like one-to-one V22( Seg ((n))) quasi_total onto bijective ((n))
x * x is Relation-like Seg ((n)) -defined Seg ((n)) -defined Seg ((n)) -valued Seg ((n)) -valued Function-like one-to-one V22( Seg ((n))) quasi_total onto bijective bijective Element of bool [:(Seg ((n))),(Seg ((n))):]
[:(Seg ((n))),(Seg ((n))):] is set
bool [:(Seg ((n))),(Seg ((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
p9 is Relation-like Seg n -defined Seg n -valued Function-like one-to-one V22( Seg n) quasi_total onto bijective Element of bool [:(Seg n),(Seg n):]
p is Relation-like Seg n -defined Seg n -valued Function-like one-to-one V22( Seg n) quasi_total onto bijective Element of bool [:(Seg n),(Seg n):]
p * p9 is Relation-like Seg n -defined Seg n -valued Function-like one-to-one V22( Seg n) quasi_total onto bijective Element of bool [:(Seg n),(Seg n):]
q9 is Relation-like Seg ((n)) -defined Seg ((n)) -valued Function-like one-to-one V22( Seg ((n))) quasi_total onto bijective ((n))
[:(n),(n):] is set
[:[:(n),(n):],(n):] is set
bool [:[:(n),(n):],(n):] is set
x is Relation-like [:(n),(n):] -defined (n) -valued Function-like V22([:(n),(n):]) quasi_total Element of bool [:[:(n),(n):],(n):]
multMagma(# (n),x #) is strict multMagma
the carrier of multMagma(# (n),x #) is set
the multF of multMagma(# (n),x #) is Relation-like [: the carrier of multMagma(# (n),x #), the carrier of multMagma(# (n),x #):] -defined the carrier of multMagma(# (n),x #) -valued Function-like quasi_total Element of bool [:[: the carrier of multMagma(# (n),x #), the carrier of multMagma(# (n),x #):], the carrier of multMagma(# (n),x #):]
[: the carrier of multMagma(# (n),x #), the carrier of multMagma(# (n),x #):] is set
[:[: the carrier of multMagma(# (n),x #), the carrier of multMagma(# (n),x #):], the carrier of multMagma(# (n),x #):] is set
bool [:[: the carrier of multMagma(# (n),x #), the carrier of multMagma(# (n),x #):], the carrier of multMagma(# (n),x #):] is set
x is Relation-like Seg ((n)) -defined Seg ((n)) -valued Function-like one-to-one V22( Seg ((n))) quasi_total onto bijective ((n))
p is Relation-like Seg ((n)) -defined Seg ((n)) -valued Function-like one-to-one V22( Seg ((n))) quasi_total onto bijective ((n))
the multF of multMagma(# (n),x #) . (x,p) is set
p * x is Relation-like Seg ((n)) -defined Seg ((n)) -defined Seg ((n)) -valued Seg ((n)) -valued Function-like one-to-one V22( Seg ((n))) quasi_total onto bijective bijective Element of bool [:(Seg ((n))),(Seg ((n))):]
[:(Seg ((n))),(Seg ((n))):] is set
bool [:(Seg ((n))),(Seg ((n))):] is set
x is strict multMagma
the carrier of x is set
the multF of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like 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
x is strict multMagma
the carrier of x is set
the multF of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like 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
p is Element of the carrier of x
p9 is Element of the carrier of x
the multF of x . (p,p9) is Element of the carrier of x
q9 is Relation-like Seg ((n)) -defined Seg ((n)) -valued Function-like one-to-one V22( Seg ((n))) quasi_total onto bijective ((n))
r9 is Relation-like Seg ((n)) -defined Seg ((n)) -valued Function-like one-to-one V22( Seg ((n))) quasi_total onto bijective ((n))
r9 * q9 is Relation-like Seg ((n)) -defined Seg ((n)) -defined Seg ((n)) -valued Seg ((n)) -valued Function-like one-to-one V22( Seg ((n))) quasi_total onto bijective bijective Element of bool [:(Seg ((n))),(Seg ((n))):]
[:(Seg ((n))),(Seg ((n))):] is set
bool [:(Seg ((n))),(Seg ((n))):] is set
the multF of x . (p,p9) is set
n is ext-real non negative V39() V40() V41() V45() finite V57() set
(n) is strict multMagma
the carrier of (n) is set
(n) is non empty () set
n is ext-real non negative V39() V40() V41() V45() finite V57() set
idseq n is Relation-like NAT -defined Function-like finite V59(n) FinSequence-like FinSubsequence-like set
Seg n is finite V59(n) Element of bool NAT
id (Seg n) is Relation-like Seg n -defined Seg n -valued V6() V8() V9() V13() Function-like one-to-one V22( Seg n) quasi_total onto bijective Element of bool [:(Seg n),(Seg n):]
[:(Seg n),(Seg n):] is set
bool [:(Seg n),(Seg n):] is set
(n) is non empty strict multMagma
the carrier of (n) is non empty set
(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
idseq n is Relation-like NAT -defined Function-like finite V59(n) FinSequence-like FinSubsequence-like set
Seg n is finite V59(n) Element of bool NAT
id (Seg n) is Relation-like Seg n -defined Seg n -valued V6() V8() V9() V13() Function-like one-to-one V22( Seg n) quasi_total onto bijective Element of bool [:(Seg n),(Seg n):]
[:(Seg n),(Seg n):] is set
bool [:(Seg n),(Seg n):] is set
x is Relation-like Seg ((n)) -defined Seg ((n)) -valued Function-like one-to-one V22( Seg ((n))) quasi_total onto bijective ((n))
(idseq n) * x is Relation-like Function-like set
x * (idseq n) is Relation-like Function-like set
rng x is set
dom x is 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
idseq n is Relation-like NAT -defined Function-like finite V59(n) FinSequence-like FinSubsequence-like set
Seg n is finite V59(n) Element of bool NAT
id (Seg n) is Relation-like Seg n -defined Seg n -valued V6() V8() V9() V13() Function-like one-to-one V22( Seg n) quasi_total onto bijective Element of bool [:(Seg n),(Seg n):]
[:(Seg n),(Seg n):] is set
bool [:(Seg n),(Seg n):] is set
x is Relation-like Seg ((n)) -defined Seg ((n)) -valued Function-like one-to-one V22( Seg ((n))) quasi_total onto bijective ((n))
x " is Relation-like Seg ((n)) -defined Seg ((n)) -valued Function-like one-to-one V22( Seg ((n))) quasi_total onto bijective Element of bool [:(Seg ((n))),(Seg ((n))):]
[:(Seg ((n))),(Seg ((n))):] is set
bool [:(Seg ((n))),(Seg ((n))):] is set
x * (x ") is Relation-like Seg ((n)) -defined Seg ((n)) -defined Seg ((n)) -valued Seg ((n)) -valued Function-like one-to-one V22( Seg ((n))) V22( Seg ((n))) quasi_total quasi_total quasi_total onto onto bijective bijective Element of bool [:(Seg ((n))),(Seg ((n))):]
(x ") * x is Relation-like Seg ((n)) -defined Seg ((n)) -defined Seg ((n)) -valued Seg ((n)) -valued Function-like one-to-one V22( Seg ((n))) V22( Seg ((n))) quasi_total quasi_total quasi_total onto onto bijective bijective Element of bool [:(Seg ((n))),(Seg ((n))):]
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
(n) is non empty strict multMagma
the carrier of (n) is non empty set
x is Relation-like Seg ((n)) -defined Seg ((n)) -valued Function-like one-to-one V22( Seg ((n))) quasi_total onto bijective ((n))
x " is Relation-like Seg ((n)) -defined Seg ((n)) -valued Function-like one-to-one V22( Seg ((n))) quasi_total onto bijective Element of bool [:(Seg ((n))),(Seg ((n))):]
[:(Seg ((n))),(Seg ((n))):] is set
bool [:(Seg ((n))),(Seg ((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
x is Relation-like Seg n -defined Seg n -valued Function-like one-to-one V22( Seg n) quasi_total onto bijective Element of bool [:(Seg n),(Seg n):]
x " is Relation-like Seg n -defined Seg n -valued Function-like one-to-one V22( Seg n) quasi_total onto bijective Element of bool [:(Seg n),(Seg n):]
n is ext-real non negative V39() V40() V41() V45() finite V57() set
(n) is non empty strict multMagma
the carrier of (n) is non empty set
idseq n is Relation-like NAT -defined Function-like finite V59(n) FinSequence-like FinSubsequence-like set
Seg n is finite V59(n) Element of bool NAT
id (Seg n) is Relation-like Seg n -defined Seg n -valued V6() V8() V9() V13() Function-like one-to-one V22( Seg n) quasi_total onto bijective Element of bool [:(Seg n),(Seg n):]
[:(Seg n),(Seg n):] is set
bool [:(Seg n),(Seg n):] is set
x is Element of the carrier of (n)
(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
p is Element of the carrier of (n)
p9 is Relation-like Seg ((n)) -defined Seg ((n)) -valued Function-like one-to-one V22( Seg ((n))) quasi_total onto bijective ((n))
q9 is Relation-like Seg n -defined Seg n -valued Function-like one-to-one V22( Seg n) quasi_total onto bijective Element of bool [:(Seg n),(Seg n):]
q9 " is Relation-like Seg n -defined Seg n -valued Function-like one-to-one V22( Seg n) quasi_total onto bijective Element of bool [:(Seg n),(Seg n):]
r9 is Relation-like Seg ((n)) -defined Seg ((n)) -valued Function-like one-to-one V22( Seg ((n))) quasi_total onto bijective ((n))
p9 is Element of the carrier of (n)
p * p9 is Element of the carrier of (n)
the multF of (n) is Relation-like [: the carrier of (n), the carrier of (n):] -defined the carrier of (n) -valued Function-like V22([: the carrier of (n), the carrier of (n):]) quasi_total Element of bool [:[: the carrier of (n), the carrier of (n):], the carrier of (n):]
[: the carrier of (n), the carrier of (n):] is set
[:[: the carrier of (n), the carrier of (n):], the carrier of (n):] is set
bool [:[: the carrier of (n), the carrier of (n):], the carrier of (n):] is set
the multF of (n) . (p,p9) is Element of the carrier of (n)
p9 * p is Element of the carrier of (n)
the multF of (n) . (p9,p) is Element of the carrier of (n)
p9 * r9 is Relation-like Seg ((n)) -defined Seg ((n)) -defined Seg ((n)) -valued Seg ((n)) -valued Function-like one-to-one V22( Seg ((n))) quasi_total onto bijective bijective Element of bool [:(Seg ((n))),(Seg ((n))):]
[:(Seg ((n))),(Seg ((n))):] is set
bool [:(Seg ((n))),(Seg ((n))):] is set
r9 * p9 is Relation-like Seg ((n)) -defined Seg ((n)) -defined Seg ((n)) -valued Seg ((n)) -valued Function-like one-to-one V22( Seg ((n))) quasi_total onto bijective bijective Element of bool [:(Seg ((n))),(Seg ((n))):]
p is Element of the carrier of (n)
p * x is Element of the carrier of (n)
the multF of (n) is Relation-like [: the carrier of (n), the carrier of (n):] -defined the carrier of (n) -valued Function-like V22([: the carrier of (n), the carrier of (n):]) quasi_total Element of bool [:[: the carrier of (n), the carrier of (n):], the carrier of (n):]
[: the carrier of (n), the carrier of (n):] is set
[:[: the carrier of (n), the carrier of (n):], the carrier of (n):] is set
bool [:[: the carrier of (n), the carrier of (n):], the carrier of (n):] is set
the multF of (n) . (p,x) is Element of the carrier of (n)
x * p is Element of the carrier of (n)
the multF of (n) . (x,p) is Element of the carrier of (n)
x is Relation-like Seg ((n)) -defined Seg ((n)) -valued Function-like one-to-one V22( Seg ((n))) quasi_total onto bijective ((n))
p9 is Relation-like Seg ((n)) -defined Seg ((n)) -valued Function-like one-to-one V22( Seg ((n))) quasi_total onto bijective ((n))
p9 * x is Relation-like Seg ((n)) -defined Seg ((n)) -defined Seg ((n)) -valued Seg ((n)) -valued Function-like one-to-one V22( Seg ((n))) quasi_total onto bijective bijective Element of bool [:(Seg ((n))),(Seg ((n))):]
[:(Seg ((n))),(Seg ((n))):] is set
bool [:(Seg ((n))),(Seg ((n))):] is set
x * p9 is Relation-like Seg ((n)) -defined Seg ((n)) -defined Seg ((n)) -valued Seg ((n)) -valued Function-like one-to-one V22( Seg ((n))) quasi_total onto bijective bijective Element of bool [:(Seg ((n))),(Seg ((n))):]
p is Element of the carrier of (n)
p * x is Element of the carrier of (n)
the multF of (n) is Relation-like [: the carrier of (n), the carrier of (n):] -defined the carrier of (n) -valued Function-like V22([: the carrier of (n), the carrier of (n):]) quasi_total Element of bool [:[: the carrier of (n), the carrier of (n):], the carrier of (n):]
[: the carrier of (n), the carrier of (n):] is set
[:[: the carrier of (n), the carrier of (n):], the carrier of (n):] is set
bool [:[: the carrier of (n), the carrier of (n):], the carrier of (n):] is set
the multF of (n) . (p,x) is Element of the carrier of (n)
p9 is Element of the carrier of (n)
x * p9 is Element of the carrier of (n)
the multF of (n) . (x,p9) is Element of the carrier of (n)
q9 is Element of the carrier of (n)
x is Element of the carrier of (n)
x is Element of the carrier of (n)
x * x is Element of the carrier of (n)
the multF of (n) is Relation-like [: the carrier of (n), the carrier of (n):] -defined the carrier of (n) -valued Function-like V22([: the carrier of (n), the carrier of (n):]) quasi_total Element of bool [:[: the carrier of (n), the carrier of (n):], the carrier of (n):]
[: the carrier of (n), the carrier of (n):] is set
[:[: the carrier of (n), the carrier of (n):], the carrier of (n):] is set
bool [:[: the carrier of (n), the carrier of (n):], the carrier of (n):] is set
the multF of (n) . (x,x) is Element of the carrier of (n)
p is Element of the carrier of (n)
(x * x) * p is Element of the carrier of (n)
the multF of (n) . ((x * x),p) is Element of the carrier of (n)
x * p is Element of the carrier of (n)
the multF of (n) . (x,p) is Element of the carrier of (n)
x * (x * p) is Element of the carrier of (n)
the multF of (n) . (x,(x * p)) is Element of the carrier of (n)
(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
p9 is Relation-like Seg ((n)) -defined Seg ((n)) -valued Function-like one-to-one V22( Seg ((n))) quasi_total onto bijective ((n))
q9 is Relation-like Seg ((n)) -defined Seg ((n)) -valued Function-like one-to-one V22( Seg ((n))) quasi_total onto bijective ((n))
q9 * p9 is Relation-like Seg ((n)) -defined Seg ((n)) -defined Seg ((n)) -valued Seg ((n)) -valued Function-like one-to-one V22( Seg ((n))) quasi_total onto bijective bijective Element of bool [:(Seg ((n))),(Seg ((n))):]
[:(Seg ((n))),(Seg ((n))):] is set
bool [:(Seg ((n))),(Seg ((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
r9 is Relation-like Seg ((n)) -defined Seg ((n)) -valued Function-like one-to-one V22( Seg ((n))) quasi_total onto bijective ((n))
r9 * q9 is Relation-like Seg ((n)) -defined Seg ((n)) -defined Seg ((n)) -valued Seg ((n)) -valued Function-like one-to-one V22( Seg ((n))) quasi_total onto bijective bijective Element of bool [:(Seg ((n))),(Seg ((n))):]
p9 is Relation-like Seg n -defined Seg n -valued Function-like one-to-one V22( Seg n) quasi_total onto bijective Element of bool [:(Seg n),(Seg n):]
q9 is Relation-like Seg n -defined Seg n -valued Function-like one-to-one V22( Seg n) quasi_total onto bijective Element of bool [:(Seg n),(Seg n):]
q9 * p9 is Relation-like Seg n -defined Seg n -valued Function-like one-to-one V22( Seg n) quasi_total onto bijective Element of bool [:(Seg n),(Seg n):]
r9 is Relation-like Seg n -defined Seg n -valued Function-like one-to-one V22( Seg n) quasi_total onto bijective Element of bool [:(Seg n),(Seg n):]
r9 * q9 is Relation-like Seg n -defined Seg n -valued Function-like one-to-one V22( Seg n) quasi_total onto bijective Element of bool [:(Seg n),(Seg n):]
the multF of (n) . ((q9 * p9),r9) is set
r9 * (q9 * p9) is Relation-like Seg ((n)) -defined Seg ((n)) -defined Seg ((n)) -valued Seg ((n)) -valued Function-like one-to-one V22( Seg ((n))) V22( Seg ((n))) quasi_total quasi_total quasi_total onto onto bijective bijective Element of bool [:(Seg ((n))),(Seg ((n))):]
(r9 * q9) * p9 is Relation-like Seg ((n)) -defined Seg ((n)) -defined Seg ((n)) -valued Seg ((n)) -valued Function-like one-to-one V22( Seg ((n))) V22( Seg ((n))) quasi_total quasi_total quasi_total onto onto bijective bijective Element of bool [:(Seg ((n))),(Seg ((n))):]
the multF of (n) . (p9,(r9 * q9)) is set
x is Element of the carrier of (n)
n is ext-real non negative V39() V40() V41() V45() finite V57() set
idseq n is Relation-like NAT -defined Function-like finite V59(n) FinSequence-like FinSubsequence-like set
Seg n is finite V59(n) Element of bool NAT
id (Seg n) is Relation-like Seg n -defined Seg n -valued V6() V8() V9() V13() Function-like one-to-one V22( Seg n) quasi_total onto bijective Element of bool [:(Seg n),(Seg n):]
[:(Seg n),(Seg n):] is set
bool [:(Seg n),(Seg n):] is set
(n) is non empty strict unital Group-like associative multMagma
1_ (n) is non being_of_order_0 Element of the carrier of (n)
the carrier of (n) is non empty 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
x is Element of the carrier of (n)
p is Element of the carrier of (n)
p * x is Element of the carrier of (n)
the multF of (n) is Relation-like [: the carrier of (n), the carrier of (n):] -defined the carrier of (n) -valued Function-like V22([: the carrier of (n), the carrier of (n):]) quasi_total associative V63( the carrier of (n)) Element of bool [:[: the carrier of (n), the carrier of (n):], the carrier of (n):]
[: the carrier of (n), the carrier of (n):] is set
[:[: the carrier of (n), the carrier of (n):], the carrier of (n):] is set
bool [:[: the carrier of (n), the carrier of (n):], the carrier of (n):] is set
the multF of (n) . (p,x) is Element of the carrier of (n)
x * p is Element of the carrier of (n)
the multF of (n) . (x,p) is Element of the carrier of (n)
x is Relation-like Seg ((n)) -defined Seg ((n)) -valued Function-like one-to-one V22( Seg ((n))) quasi_total onto bijective ((n))
p9 is Relation-like Seg ((n)) -defined Seg ((n)) -valued Function-like one-to-one V22( Seg ((n))) quasi_total onto bijective ((n))
p9 * x is Relation-like Seg ((n)) -defined Seg ((n)) -defined Seg ((n)) -valued Seg ((n)) -valued Function-like one-to-one V22( Seg ((n))) quasi_total onto bijective bijective Element of bool [:(Seg ((n))),(Seg ((n))):]
[:(Seg ((n))),(Seg ((n))):] is set
bool [:(Seg ((n))),(Seg ((n))):] is set
x * p9 is Relation-like Seg ((n)) -defined Seg ((n)) -defined Seg ((n)) -valued Seg ((n)) -valued Function-like one-to-one V22( Seg ((n))) quasi_total onto bijective bijective Element of bool [:(Seg ((n))),(Seg ((n))):]
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
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
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
n is ext-real non negative V39() V40() V41() V45() finite V57() set
Seg n is finite V59(n) Element of bool NAT
id (Seg n) is Relation-like Seg n -defined Seg n -valued V6() V8() V9() V13() Function-like one-to-one V22( Seg n) quasi_total onto bijective Element of bool [:(Seg n),(Seg n):]
[:(Seg n),(Seg n):] is set
bool [:(Seg n),(Seg n):] is set
(n) is non empty strict unital Group-like associative multMagma
the carrier of (n) is non empty set
<*> the carrier of (n) is Relation-like NAT -defined the carrier of (n) -valued Function-like one-to-one constant functional empty ext-real non positive non negative V39() V40() V41() V43() V44() V45() finite V57() V59( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of the carrier of (n)
2 * 0 is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
(2 * 0) + 0 is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
len (<*> the carrier of (n)) is Function-like functional empty ext-real non positive non negative V39() V40() V41() V43() V44() V45() finite V57() V59( {} ) FinSequence-membered Element of NAT
(len (<*> the carrier of (n))) mod 2 is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
Product (<*> the carrier of (n)) is Element of the carrier of (n)
1_ (n) is non being_of_order_0 Element of the carrier of (n)
idseq n is Relation-like NAT -defined Function-like finite V59(n) FinSequence-like FinSubsequence-like set
dom (<*> the carrier of (n)) is Function-like functional empty ext-real non positive non negative V39() V40() V41() V43() V44() V45() finite V57() V59( {} ) FinSequence-membered Element of bool NAT
(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
x is ext-real non negative V39() V40() V41() V45() finite V57() set
(<*> the carrier of (n)) . x is set
n is non empty non degenerated non trivial right_complementable almost_left_invertible associative commutative V150() V151() V152() well-unital V164() doubleLoopStr
the carrier of n is non empty non trivial set
x is ext-real non negative V39() V40() V41() V45() finite V57() set
(x) is non empty () set
((x)) is ext-real non negative V39() V40() V41() V45() finite V57() Element of NAT
Seg ((x)) is finite V59(((x))) Element of bool NAT
p is Relation-like Seg ((x)) -defined Seg ((x)) -valued Function-like one-to-one V22( Seg ((x))) quasi_total onto bijective ((x))
x is Element of the carrier of n
- x is Element of the carrier of n
n is set
Fin n is preBoolean set
n is ext-real non negative V39() V40() V41() V45() finite V57() set
(n) is non empty () set
Seg n is finite V59(n) Element of bool NAT
Funcs ((Seg n),(Seg n)) is functional non empty set
x is set
[:(Seg n),(Seg n):] is set
bool [:(Seg n),(Seg n):] is set