:: MATRIX16 semantic presentation

REAL is set
NAT is non empty V4() V5() V6() Element of bool REAL

NAT is non empty V4() V5() V6() set

1 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative Element of NAT
2 is non empty V4() V5() V6() V10() V11() V12() integer ext-real positive non negative Element of NAT

RAT is set
INT is set
{} is empty V4() V5() V6() V8() V9() V10() V11() V12() Function-like functional integer ext-real non positive non negative set
0 is empty V4() V5() V6() V8() V9() V10() V11() V12() Function-like functional integer ext-real non positive non negative Element of NAT
K43(1) is V11() V12() integer ext-real non positive Element of REAL
K is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
n is V4() V5() V6() V10() V11() V12() integer ext-real set
n - 1 is V11() V12() integer ext-real set
(n - 1) mod K is V11() V12() integer ext-real set
1 - 1 is V11() V12() integer ext-real set
K - 1 is V11() V12() integer ext-real set
n is V4() V5() V6() V10() V11() V12() integer ext-real set
K is V4() V5() V6() V10() V11() V12() integer ext-real set
Seg K is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= K ) } is set
p is V4() V5() V6() V10() V11() V12() integer ext-real set
p - n is V11() V12() integer ext-real set
(p - n) mod K is V11() V12() integer ext-real set
((p - n) mod K) + 1 is V11() V12() integer ext-real set
1 - K is V11() V12() integer ext-real set
K - 1 is V11() V12() integer ext-real set
- K is V11() V12() integer ext-real set
(- K) + 1 is V11() V12() integer ext-real set
- 1 is V11() V12() integer ext-real non positive set
K + (p - n) is V11() V12() integer ext-real set
K + (- 1) is V11() V12() integer ext-real set
(K - 1) + 1 is V11() V12() integer ext-real set
0 + 1 is non empty V11() V12() integer ext-real positive non negative set
n is V4() V5() V6() V10() V11() V12() integer ext-real set
p is V4() V5() V6() V10() V11() V12() integer ext-real set
[n,p] is set
K is V4() V5() V6() V10() V11() V12() integer ext-real set
Seg K is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= K ) } is set
[:(Seg K),(Seg K):] is set
[p,n] is set
p - n is V11() V12() integer ext-real set
(p - n) mod K is V11() V12() integer ext-real set
((p - n) mod K) + 1 is V11() V12() integer ext-real set

the carrier of K is non empty non trivial set
1_ K is Element of the carrier of K
1. K is V49(K) Element of the carrier of K

(1_ K) * n is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
(1_ K) multfield is Relation-like the carrier of K -defined the carrier of K -valued Function-like V27( the carrier of K, the carrier of K) Element of bool [: the carrier of K, the carrier of K:]
[: the carrier of K, the carrier of K:] is set
bool [: the carrier of K, the carrier of K:] is set
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V27([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[:[: the carrier of K, the carrier of K:], the carrier of K:] is set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is set
id the carrier of K is non empty Relation-like the carrier of K -defined the carrier of K -valued Function-like one-to-one total Element of bool [: the carrier of K, the carrier of K:]
the multF of K [;] ((1_ K),(id the carrier of K)) is Relation-like the carrier of K -defined the carrier of K -valued Function-like V27( the carrier of K, the carrier of K) Element of bool [: the carrier of K, the carrier of K:]
K191( the carrier of K, the carrier of K,n,((1_ K) multfield)) is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
dom n is set
len n is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Seg (len n) is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= len n ) } is set
len ((1_ K) * n) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Seg (len ((1_ K) * n)) is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= len ((1_ K) * n) ) } is set
dom ((1_ K) * n) is set
p is V4() V5() V6() V10() V11() V12() integer ext-real set
((1_ K) * n) . p is set
n . p is set
rng n is set
the multF of K [;] ((1_ K),(id the carrier of K)) is Relation-like Function-like set
dom ( the multF of K [;] ((1_ K),(id the carrier of K))) is set
((1_ K) multfield) . (n . p) is set
(id the carrier of K) . (n . p) is set
the multF of K . ((1_ K),((id the carrier of K) . (n . p))) is set
M1 is Element of the carrier of K
(1_ K) * M1 is Element of the carrier of K
the multF of K . ((1_ K),M1) is Element of the carrier of K

the carrier of K is non empty non trivial set
1_ K is Element of the carrier of K
1. K is V49(K) Element of the carrier of K
- (1_ K) is Element of the carrier of K

(- (1_ K)) * n is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
(- (1_ K)) multfield is Relation-like the carrier of K -defined the carrier of K -valued Function-like V27( the carrier of K, the carrier of K) Element of bool [: the carrier of K, the carrier of K:]
[: the carrier of K, the carrier of K:] is set
bool [: the carrier of K, the carrier of K:] is set
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V27([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[:[: the carrier of K, the carrier of K:], the carrier of K:] is set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is set
id the carrier of K is non empty Relation-like the carrier of K -defined the carrier of K -valued Function-like one-to-one total Element of bool [: the carrier of K, the carrier of K:]
the multF of K [;] ((- (1_ K)),(id the carrier of K)) is Relation-like the carrier of K -defined the carrier of K -valued Function-like V27( the carrier of K, the carrier of K) Element of bool [: the carrier of K, the carrier of K:]
K191( the carrier of K, the carrier of K,n,((- (1_ K)) multfield)) is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K

comp K is Relation-like the carrier of K -defined the carrier of K -valued Function-like V27( the carrier of K, the carrier of K) Element of bool [: the carrier of K, the carrier of K:]
K191( the carrier of K, the carrier of K,n,(comp K)) is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
len ((- (1_ K)) * n) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Seg (len ((- (1_ K)) * n)) is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= len ((- (1_ K)) * n) ) } is set
len n is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Seg (len n) is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= len n ) } is set
dom ((- (1_ K)) * n) is set
dom n is set
p is V4() V5() V6() V10() V11() V12() integer ext-real set
((- (1_ K)) * n) . p is set
(- n) . p is set
rng n is set
n . p is set
the multF of K [;] ((- (1_ K)),(id the carrier of K)) is Relation-like Function-like set
dom ( the multF of K [;] ((- (1_ K)),(id the carrier of K))) is set
M1 is Element of the carrier of K
(- (1_ K)) * M1 is Element of the carrier of K
the multF of K . ((- (1_ K)),M1) is Element of the carrier of K
((- (1_ K)) * M1) + M1 is Element of the carrier of K
the addF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V27([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
the addF of K . (((- (1_ K)) * M1),M1) is Element of the carrier of K
(1_ K) * M1 is Element of the carrier of K
the multF of K . ((1_ K),M1) is Element of the carrier of K
((- (1_ K)) * M1) + ((1_ K) * M1) is Element of the carrier of K
the addF of K . (((- (1_ K)) * M1),((1_ K) * M1)) is Element of the carrier of K
(- (1_ K)) + (1_ K) is Element of the carrier of K
the addF of K . ((- (1_ K)),(1_ K)) is Element of the carrier of K
((- (1_ K)) + (1_ K)) * M1 is Element of the carrier of K
the multF of K . (((- (1_ K)) + (1_ K)),M1) is Element of the carrier of K
0. K is V49(K) Element of the carrier of K
(0. K) * M1 is Element of the carrier of K
the multF of K . ((0. K),M1) is Element of the carrier of K
- M1 is Element of the carrier of K
M1 + (- M1) is Element of the carrier of K
the addF of K . (M1,(- M1)) is Element of the carrier of K
((- (1_ K)) * M1) + (M1 + (- M1)) is Element of the carrier of K
the addF of K . (((- (1_ K)) * M1),(M1 + (- M1))) is Element of the carrier of K
(0. K) + (- M1) is Element of the carrier of K
the addF of K . ((0. K),(- M1)) is Element of the carrier of K
((- (1_ K)) * M1) + (0. K) is Element of the carrier of K
the addF of K . (((- (1_ K)) * M1),(0. K)) is Element of the carrier of K
((- (1_ K)) multfield) . (n . p) is set
(id the carrier of K) . (n . p) is set
the multF of K . ((- (1_ K)),((id the carrier of K) . (n . p))) is set
(comp K) . M1 is set
(len n) -tuples_on the carrier of K is non empty functional FinSequence-membered FinSequenceSet of the carrier of K
the carrier of K * is functional FinSequence-membered FinSequenceSet of the carrier of K
{ b1 where b1 is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like Element of the carrier of K * : len b1 = len n } is set
len (- n) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
dom (- n) is set
Seg (len (- n)) is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= len (- n) ) } is set
K is set

K is set

K is non empty set
K is set

K is set

K is non empty set
K is non empty set

len n is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT

Indices p is set
dom p is Element of bool NAT
width p is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Seg () is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width p ) } is set
[:(dom p),(Seg ()):] is set
Indices M1 is set
dom M1 is Element of bool NAT
width M1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Seg (width M1) is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width M1 ) } is set
[:(dom M1),(Seg (width M1)):] is set
p is V4() V5() V6() V10() V11() V12() integer ext-real set
c6 is V4() V5() V6() V10() V11() V12() integer ext-real set
[p,c6] is set
p * (p,c6) is Element of K
M1 * (p,c6) is Element of K
c6 - p is V11() V12() integer ext-real set
(c6 - p) mod (len n) is V11() V12() integer ext-real set
((c6 - p) mod (len n)) + 1 is V11() V12() integer ext-real set
n . (((c6 - p) mod (len n)) + 1) is set
K is non empty set

len n is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT

Indices p is set
dom p is Element of bool NAT
width p is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Seg () is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width p ) } is set
[:(dom p),(Seg ()):] is set
Indices M1 is set
dom M1 is Element of bool NAT
width M1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Seg (width M1) is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width M1 ) } is set
[:(dom M1),(Seg (width M1)):] is set
p is V4() V5() V6() V10() V11() V12() integer ext-real set
c6 is V4() V5() V6() V10() V11() V12() integer ext-real set
[p,c6] is set
p * (p,c6) is Element of K
M1 * (p,c6) is Element of K
p - c6 is V11() V12() integer ext-real set
(p - c6) mod (len n) is V11() V12() integer ext-real set
((p - c6) mod (len n)) + 1 is V11() V12() integer ext-real set
n . (((p - c6) mod (len n)) + 1) is set

the carrier of K is non empty non trivial set
0. (K,1,1) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of 1,1, the carrier of K
the carrier of K * is functional FinSequence-membered FinSequenceSet of the carrier of K
1 -tuples_on the carrier of K is non empty functional FinSequence-membered FinSequenceSet of the carrier of K
{ b1 where b1 is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like Element of the carrier of K * : len b1 = 1 } is set
0. K is V49(K) Element of the carrier of K
1 |-> (0. K) is Relation-like NAT -defined the carrier of K -valued Function-like V37(1) FinSequence-like Element of 1 -tuples_on the carrier of K
Seg 1 is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set
(Seg 1) --> (0. K) is Relation-like Seg 1 -defined Seg 1 -defined the carrier of K -valued {(0. K)} -valued Function-like constant total total V27( Seg 1,{(0. K)}) FinSequence-like Element of bool [:(Seg 1),{(0. K)}:]
{(0. K)} is non empty set
[:(Seg 1),{(0. K)}:] is set
bool [:(Seg 1),{(0. K)}:] is set
1 |-> (1 |-> (0. K)) is Relation-like NAT -defined 1 -tuples_on the carrier of K -valued Function-like V37(1) FinSequence-like Function-yielding V105() Element of 1 -tuples_on (1 -tuples_on the carrier of K)
1 -tuples_on (1 -tuples_on the carrier of K) is non empty functional FinSequence-membered FinSequenceSet of 1 -tuples_on the carrier of K
(1 -tuples_on the carrier of K) * is functional FinSequence-membered FinSequenceSet of 1 -tuples_on the carrier of K
{ b1 where b1 is Relation-like NAT -defined 1 -tuples_on the carrier of K -valued Function-like FinSequence-like Element of (1 -tuples_on the carrier of K) * : len b1 = 1 } is set
(Seg 1) --> (1 |-> (0. K)) is Relation-like Seg 1 -defined Seg 1 -defined 1 -tuples_on the carrier of K -valued {(1 |-> (0. K))} -valued Function-like constant total total V27( Seg 1,{(1 |-> (0. K))}) FinSequence-like Function-yielding V105() Element of bool [:(Seg 1),{(1 |-> (0. K))}:]
{(1 |-> (0. K))} is non empty functional set
[:(Seg 1),{(1 |-> (0. K))}:] is set
bool [:(Seg 1),{(1 |-> (0. K))}:] is set
0. (K,1) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of 1,1, the carrier of K

len (1 |-> (0. K)) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Indices (0. (K,1)) is set
dom (0. (K,1)) is Element of bool NAT
width (0. (K,1)) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Seg (width (0. (K,1))) is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width (0. (K,1)) ) } is set
[:(dom (0. (K,1))),(Seg (width (0. (K,1)))):] is set
[:(Seg 1),(Seg 1):] is set
len p is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
M1 is V4() V5() V6() V10() V11() V12() integer ext-real set
p is V4() V5() V6() V10() V11() V12() integer ext-real set
[M1,p] is set
(0. (K,1)) * (M1,p) is Element of the carrier of K
M1 - p is V11() V12() integer ext-real set
(M1 - p) mod (len p) is V11() V12() integer ext-real set
((M1 - p) mod (len p)) + 1 is V11() V12() integer ext-real set
p . (((M1 - p) mod (len p)) + 1) is set
(M1 - p) mod 1 is V11() V12() integer ext-real set
((M1 - p) mod 1) + 1 is V11() V12() integer ext-real set
(Seg 1) --> (0. K) is Relation-like Seg 1 -defined Seg 1 -defined the carrier of K -valued Function-like constant total total V27( Seg 1, the carrier of K) FinSequence-like Element of bool [:(Seg 1), the carrier of K:]
[:(Seg 1), the carrier of K:] is set
bool [:(Seg 1), the carrier of K:] is set
((Seg 1) --> (0. K)) . (((M1 - p) mod 1) + 1) is set
M1 is V4() V5() V6() V10() V11() V12() integer ext-real set
p is V4() V5() V6() V10() V11() V12() integer ext-real set
[M1,p] is set
(0. (K,1)) * (M1,p) is Element of the carrier of K
p - M1 is V11() V12() integer ext-real set
(p - M1) mod (len p) is V11() V12() integer ext-real set
((p - M1) mod (len p)) + 1 is V11() V12() integer ext-real set
p . (((p - M1) mod (len p)) + 1) is set
(p - M1) mod 1 is V11() V12() integer ext-real set
((p - M1) mod 1) + 1 is V11() V12() integer ext-real set
(Seg 1) --> (0. K) is Relation-like Seg 1 -defined Seg 1 -defined the carrier of K -valued Function-like constant total total V27( Seg 1, the carrier of K) FinSequence-like Element of bool [:(Seg 1), the carrier of K:]
[:(Seg 1), the carrier of K:] is set
bool [:(Seg 1), the carrier of K:] is set
((Seg 1) --> (0. K)) . (((p - M1) mod 1) + 1) is set
len (0. (K,1)) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT

the carrier of K is non empty non trivial set
n is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
0. (K,n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of n,n, the carrier of K
the carrier of K * is functional FinSequence-membered FinSequenceSet of the carrier of K
n -tuples_on the carrier of K is non empty functional FinSequence-membered FinSequenceSet of the carrier of K
{ b1 where b1 is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like Element of the carrier of K * : len b1 = n } is set
0. K is V49(K) Element of the carrier of K
n |-> (0. K) is Relation-like NAT -defined the carrier of K -valued Function-like V37(n) FinSequence-like Element of n -tuples_on the carrier of K
Seg n is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
(Seg n) --> (0. K) is Relation-like Seg n -defined Seg n -defined the carrier of K -valued {(0. K)} -valued Function-like constant total total V27( Seg n,{(0. K)}) FinSequence-like Element of bool [:(Seg n),{(0. K)}:]
{(0. K)} is non empty set
[:(Seg n),{(0. K)}:] is set
bool [:(Seg n),{(0. K)}:] is set
n |-> (n |-> (0. K)) is Relation-like NAT -defined n -tuples_on the carrier of K -valued Function-like V37(n) FinSequence-like Function-yielding V105() Element of n -tuples_on (n -tuples_on the carrier of K)
n -tuples_on (n -tuples_on the carrier of K) is non empty functional FinSequence-membered FinSequenceSet of n -tuples_on the carrier of K
(n -tuples_on the carrier of K) * is functional FinSequence-membered FinSequenceSet of n -tuples_on the carrier of K
{ b1 where b1 is Relation-like NAT -defined n -tuples_on the carrier of K -valued Function-like FinSequence-like Element of (n -tuples_on the carrier of K) * : len b1 = n } is set
(Seg n) --> (n |-> (0. K)) is Relation-like Seg n -defined Seg n -defined n -tuples_on the carrier of K -valued {(n |-> (0. K))} -valued Function-like constant total total V27( Seg n,{(n |-> (0. K))}) FinSequence-like Function-yielding V105() Element of bool [:(Seg n),{(n |-> (0. K))}:]
{(n |-> (0. K))} is non empty functional set
[:(Seg n),{(n |-> (0. K))}:] is set
bool [:(Seg n),{(n |-> (0. K))}:] is set
len (0. (K,n)) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
0. (K,n,n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of n,n, the carrier of K
len (n |-> (0. K)) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Indices (0. (K,n)) is set
dom (0. (K,n)) is Element of bool NAT
width (0. (K,n)) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Seg (width (0. (K,n))) is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width (0. (K,n)) ) } is set
[:(dom (0. (K,n))),(Seg (width (0. (K,n)))):] is set
[:(Seg n),(Seg n):] is set
p is V4() V5() V6() V10() V11() V12() integer ext-real set
c6 is V4() V5() V6() V10() V11() V12() integer ext-real set
[p,c6] is set
(0. (K,n)) * (p,c6) is Element of the carrier of K
p - c6 is V11() V12() integer ext-real set
(p - c6) mod (len (n |-> (0. K))) is V11() V12() integer ext-real set
((p - c6) mod (len (n |-> (0. K)))) + 1 is V11() V12() integer ext-real set
(n |-> (0. K)) . (((p - c6) mod (len (n |-> (0. K)))) + 1) is set
(p - c6) mod n is V11() V12() integer ext-real set
((p - c6) mod n) + 1 is V11() V12() integer ext-real set
(Seg n) --> (0. K) is Relation-like Seg n -defined Seg n -defined the carrier of K -valued Function-like constant total total V27( Seg n, the carrier of K) FinSequence-like Element of bool [:(Seg n), the carrier of K:]
[:(Seg n), the carrier of K:] is set
bool [:(Seg n), the carrier of K:] is set
((Seg n) --> (0. K)) . (((p - c6) mod (len (n |-> (0. K)))) + 1) is set
p is V4() V5() V6() V10() V11() V12() integer ext-real set
c6 is V4() V5() V6() V10() V11() V12() integer ext-real set
[p,c6] is set
(0. (K,n)) * (p,c6) is Element of the carrier of K
c6 - p is V11() V12() integer ext-real set
(c6 - p) mod (len (n |-> (0. K))) is V11() V12() integer ext-real set
((c6 - p) mod (len (n |-> (0. K)))) + 1 is V11() V12() integer ext-real set
(n |-> (0. K)) . (((c6 - p) mod (len (n |-> (0. K)))) + 1) is set
(c6 - p) mod n is V11() V12() integer ext-real set
((c6 - p) mod n) + 1 is V11() V12() integer ext-real set
(Seg n) --> (0. K) is Relation-like Seg n -defined Seg n -defined the carrier of K -valued Function-like constant total total V27( Seg n, the carrier of K) FinSequence-like Element of bool [:(Seg n), the carrier of K:]
[:(Seg n), the carrier of K:] is set
bool [:(Seg n), the carrier of K:] is set
((Seg n) --> (0. K)) . (((c6 - p) mod n) + 1) is set

len p is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT

len p is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT

the carrier of K is non empty non trivial set
the carrier of K * is functional FinSequence-membered FinSequenceSet of the carrier of K
n is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
p is Element of the carrier of K
(n,n) --> p is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of n,n, the carrier of K

n -tuples_on the carrier of K is non empty functional FinSequence-membered FinSequenceSet of the carrier of K
{ b1 where b1 is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like Element of the carrier of K * : len b1 = n } is set
Seg n is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= n ) } is set

{p} is non empty set
[:(Seg n),{p}:] is set
bool [:(Seg n),{p}:] is set
width ((n,n) --> p) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
len (n |-> p) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Indices ((n,n) --> p) is set
dom ((n,n) --> p) is Element of bool NAT
Seg (width ((n,n) --> p)) is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width ((n,n) --> p) ) } is set
[:(dom ((n,n) --> p)),(Seg (width ((n,n) --> p))):] is set
[:(Seg n),(Seg n):] is set
p is V4() V5() V6() V10() V11() V12() integer ext-real set
c6 is V4() V5() V6() V10() V11() V12() integer ext-real set
[p,c6] is set
((n,n) --> p) * (p,c6) is Element of the carrier of K
c6 - p is V11() V12() integer ext-real set
(c6 - p) mod (len (n |-> p)) is V11() V12() integer ext-real set
((c6 - p) mod (len (n |-> p))) + 1 is V11() V12() integer ext-real set
(n |-> p) . (((c6 - p) mod (len (n |-> p))) + 1) is set
(c6 - p) mod n is V11() V12() integer ext-real set
((c6 - p) mod n) + 1 is V11() V12() integer ext-real set
(Seg n) --> p is Relation-like Seg n -defined Seg n -defined the carrier of K -valued Function-like constant total total V27( Seg n, the carrier of K) FinSequence-like Element of bool [:(Seg n), the carrier of K:]
[:(Seg n), the carrier of K:] is set
bool [:(Seg n), the carrier of K:] is set
((Seg n) --> p) . (((c6 - p) mod (len (n |-> p))) + 1) is set

n -tuples_on the carrier of K is non empty functional FinSequence-membered FinSequenceSet of the carrier of K
{ b1 where b1 is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like Element of the carrier of K * : len b1 = n } is set
Seg n is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= n ) } is set

{p} is non empty set
[:(Seg n),{p}:] is set
bool [:(Seg n),{p}:] is set
len ((n,n) --> p) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
len (n |-> p) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Indices ((n,n) --> p) is set
dom ((n,n) --> p) is Element of bool NAT
width ((n,n) --> p) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Seg (width ((n,n) --> p)) is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width ((n,n) --> p) ) } is set
[:(dom ((n,n) --> p)),(Seg (width ((n,n) --> p))):] is set
[:(Seg n),(Seg n):] is set
c6 is V4() V5() V6() V10() V11() V12() integer ext-real set
c7 is V4() V5() V6() V10() V11() V12() integer ext-real set
[c6,c7] is set
((n,n) --> p) * (c6,c7) is Element of the carrier of K
c6 - c7 is V11() V12() integer ext-real set
(c6 - c7) mod (len (n |-> p)) is V11() V12() integer ext-real set
((c6 - c7) mod (len (n |-> p))) + 1 is V11() V12() integer ext-real set
(n |-> p) . (((c6 - c7) mod (len (n |-> p))) + 1) is set
(c6 - c7) mod n is V11() V12() integer ext-real set
((c6 - c7) mod n) + 1 is V11() V12() integer ext-real set
(Seg n) --> p is Relation-like Seg n -defined Seg n -defined the carrier of K -valued Function-like constant total total V27( Seg n, the carrier of K) FinSequence-like Element of bool [:(Seg n), the carrier of K:]
[:(Seg n), the carrier of K:] is set
bool [:(Seg n), the carrier of K:] is set
((Seg n) --> p) . (((c6 - c7) mod (len (n |-> p))) + 1) is set

the carrier of K is non empty non trivial set
the carrier of K * is functional FinSequence-membered FinSequenceSet of the carrier of K
0. K is V49(K) Element of the carrier of K
(1,1) --> (0. K) is Relation-like NAT -defined the carrier of K * -valued the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular ( the carrier of K) ( the carrier of K) Matrix of 1,1, the carrier of K
K is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
n is non empty set

width p is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT

len M1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
len (p @) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Indices (p @) is set
dom (p @) is Element of bool NAT
width (p @) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Seg (width (p @)) is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width (p @) ) } is set
[:(dom (p @)),(Seg (width (p @))):] is set
p is V4() V5() V6() V10() V11() V12() integer ext-real set
c6 is V4() V5() V6() V10() V11() V12() integer ext-real set
[p,c6] is set
(p @) * (p,c6) is Element of n
p - c6 is V11() V12() integer ext-real set
(p - c6) mod (len M1) is V11() V12() integer ext-real set
((p - c6) mod (len M1)) + 1 is V11() V12() integer ext-real set
M1 . (((p - c6) mod (len M1)) + 1) is set
Indices p is set
dom p is Element of bool NAT
Seg () is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width p ) } is set
[:(dom p),(Seg ()):] is set
Seg K is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= K ) } is set
[:(Seg K),(Seg K):] is set
[c6,p] is set
p * (c6,p) is Element of n

len p is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
K is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
n is non empty set

width M1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(width M1) -tuples_on n is non empty functional FinSequence-membered FinSequenceSet of n
{ b1 where b1 is Relation-like NAT -defined n -valued Function-like FinSequence-like Element of n * : len b1 = width M1 } is set
dom p is set
len p is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Seg (len p) is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= len p ) } is set
p is V4() V5() V6() V10() V11() V12() integer ext-real set
p . p is set
(Line (M1,1)) . p is set
0 + 1 is non empty V11() V12() integer ext-real positive non negative set
Seg K is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= K ) } is set
[1,p] is set
[:(Seg K),(Seg K):] is set
Indices M1 is set
dom M1 is Element of bool NAT
Seg (width M1) is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width M1 ) } is set
[:(dom M1),(Seg (width M1)):] is set
M1 * (1,p) is Element of n
p - 1 is V11() V12() integer ext-real set
(p - 1) mod (len p) is V11() V12() integer ext-real set
((p - 1) mod (len p)) + 1 is V11() V12() integer ext-real set
p . (((p - 1) mod (len p)) + 1) is set
(p - 1) mod K is V11() V12() integer ext-real set
((p - 1) mod K) + 1 is V11() V12() integer ext-real set
p . (((p - 1) mod K) + 1) is set
(p - 1) + 1 is V11() V12() integer ext-real set
p . ((p - 1) + 1) is set
len (Line (M1,1)) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
dom (Line (M1,1)) is set
K is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
K + 1 is V11() V12() integer ext-real set
n is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
[K,n] is set
n + 1 is V11() V12() integer ext-real set
p is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Seg p is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= p ) } is set
[:(Seg p),(Seg p):] is set
M1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
p is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
c6 is non empty set

c7 * (K,n) is Element of c6
c7 * (M1,p) is Element of c6
width c7 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT

len M3 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Indices c7 is set
dom c7 is Element of bool NAT
Seg (width c7) is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width c7 ) } is set
[:(dom c7),(Seg (width c7)):] is set
1 + 1 is non empty V11() V12() integer ext-real positive non negative set
[M1,p] is set
p - M1 is V11() V12() integer ext-real set
(p - M1) mod (len M3) is V11() V12() integer ext-real set
((p - M1) mod (len M3)) + 1 is V11() V12() integer ext-real set
M3 . (((p - M1) mod (len M3)) + 1) is set
n - K is V11() V12() integer ext-real set
(n - K) mod (len M3) is V11() V12() integer ext-real set
((n - K) mod (len M3)) + 1 is V11() V12() integer ext-real set
M3 . (((n - K) mod (len M3)) + 1) is set
K is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT

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

Indices (p * M1) is set
dom (p * M1) is Element of bool NAT
width (p * M1) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Seg (width (p * M1)) is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width (p * M1) ) } is set
[:(dom (p * M1)),(Seg (width (p * M1))):] is set
Seg K is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= K ) } is set
[:(Seg K),(Seg K):] is set
width M1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT

len p is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
dom p is set

p multfield is Relation-like the carrier of n -defined the carrier of n -valued Function-like V27( the carrier of n, the carrier of n) Element of bool [: the carrier of n, the carrier of n:]
[: the carrier of n, the carrier of n:] is set
bool [: the carrier of n, the carrier of n:] is set
the multF of n is Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like V27([: the carrier of n, the carrier of n:], 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:], the carrier of n:] is set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is set
id the carrier of n is non empty Relation-like the carrier of n -defined the carrier of n -valued Function-like one-to-one total Element of bool [: the carrier of n, the carrier of n:]
the multF of n [;] (p,(id the carrier of n)) is Relation-like the carrier of n -defined the carrier of n -valued Function-like V27( the carrier of n, the carrier of n) Element of bool [: the carrier of n, the carrier of n:]
K191( the carrier of n, the carrier of n,p,()) is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n
dom (p * p) is set
len (p * p) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Seg (len (p * p)) is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= len (p * p) ) } is set
c6 is V4() V5() V6() V10() V11() V12() integer ext-real set
c7 is V4() V5() V6() V10() V11() V12() integer ext-real set
[c6,c7] is set
(p * M1) * (c6,c7) is Element of the carrier of n
c7 - c6 is V11() V12() integer ext-real set
(c7 - c6) mod (len (p * p)) is V11() V12() integer ext-real set
((c7 - c6) mod (len (p * p))) + 1 is V11() V12() integer ext-real set
(p * p) . (((c7 - c6) mod (len (p * p))) + 1) is set
(c7 - c6) mod K is V11() V12() integer ext-real set
((c7 - c6) mod K) + 1 is V11() V12() integer ext-real set
(c7 - c6) mod (len p) is V11() V12() integer ext-real set
((c7 - c6) mod (len p)) + 1 is V11() V12() integer ext-real set
Indices M1 is set
dom M1 is Element of bool NAT
Seg (width M1) is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width M1 ) } is set
[:(dom M1),(Seg (width M1)):] is set
M1 * (c6,c7) is Element of the carrier of n
p * (M1 * (c6,c7)) is Element of the carrier of n
the multF of n . (p,(M1 * (c6,c7))) is Element of the carrier of n
() . (M1 * (c6,c7)) is set
p . (((c7 - c6) mod (len p)) + 1) is set
() . (p . (((c7 - c6) mod (len p)) + 1)) is set
p /. (((c7 - c6) mod (len p)) + 1) is Element of the carrier of n
() . (p /. (((c7 - c6) mod (len p)) + 1)) is set
p * (p /. (((c7 - c6) mod (len p)) + 1)) is Element of the carrier of n
the multF of n . (p,(p /. (((c7 - c6) mod (len p)) + 1))) is Element of the carrier of n
(p * p) /. (((c7 - c6) mod (len p)) + 1) is Element of the carrier of n
(p * p) . (((c7 - c6) mod (len p)) + 1) is set

len c6 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
K is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT

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

width p is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT

len p is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Indices M1 is set
dom M1 is Element of bool NAT
width M1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Seg (width M1) is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width M1 ) } is set
[:(dom M1),(Seg (width M1)):] is set
Seg K is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= K ) } is set
[:(Seg K),(Seg K):] is set
Indices (p + M1) is set
dom (p + M1) is Element of bool NAT
width (p + M1) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Seg (width (p + M1)) is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width (p + M1) ) } is set
[:(dom (p + M1)),(Seg (width (p + M1))):] is set
dom p is set

len c6 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Indices p is set
dom p is Element of bool NAT
Seg () is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width p ) } is set
[:(dom p),(Seg ()):] is set
dom c6 is set

the addF of n is Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like V27([: the carrier of n, the carrier of n:], 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
K188( the carrier of n, the carrier of n, the carrier of n, the addF of n,p,c6) is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n
dom (p + c6) is set
len (p + c6) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Seg (len (p + c6)) is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= len (p + c6) ) } is set
c7 is V4() V5() V6() V10() V11() V12() integer ext-real set
M3 is V4() V5() V6() V10() V11() V12() integer ext-real set
[c7,M3] is set
(p + M1) * (c7,M3) is Element of the carrier of n
M3 - c7 is V11() V12() integer ext-real set
(M3 - c7) mod (len (p + c6)) is V11() V12() integer ext-real set
((M3 - c7) mod (len (p + c6))) + 1 is V11() V12() integer ext-real set
(p + c6) . (((M3 - c7) mod (len (p + c6))) + 1) is set
p * (c7,M3) is Element of the carrier of n
M1 * (c7,M3) is Element of the carrier of n
(p * (c7,M3)) + (M1 * (c7,M3)) is Element of the carrier of n
the addF of n . ((p * (c7,M3)),(M1 * (c7,M3))) is Element of the carrier of n
(M3 - c7) mod (len c6) is V11() V12() integer ext-real set
((M3 - c7) mod (len c6)) + 1 is V11() V12() integer ext-real set
c6 . (((M3 - c7) mod (len c6)) + 1) is set
the addF of n . ((p * (c7,M3)),(c6 . (((M3 - c7) mod (len c6)) + 1))) is set
p . (((M3 - c7) mod (len (p + c6))) + 1) is set
c6 . (((M3 - c7) mod (len (p + c6))) + 1) is set
the addF of n . ((p . (((M3 - c7) mod (len (p + c6))) + 1)),(c6 . (((M3 - c7) mod (len (p + c6))) + 1))) is set

len c7 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
K is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT

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

(p + M1) + p is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of K,K, the carrier of n
K is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT

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

(p * p) + (M1 * c6) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of K,K, the carrier of n
K is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT

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

(p * c6) + (M1 * c7) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of K,K, the carrier of n

((p * c6) + (M1 * c7)) + (p * M3) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of K,K, the carrier of n
K is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT

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

width p is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Indices (- p) is set
dom (- p) is Element of bool NAT
width (- p) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Seg (width (- p)) is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width (- p) ) } is set
[:(dom (- p)),(Seg (width (- p))):] is set
Seg K is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= K ) } is set
[:(Seg K),(Seg K):] is set

len M1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
(len M1) -tuples_on the carrier of n is non empty functional FinSequence-membered FinSequenceSet of the carrier of n
{ b1 where b1 is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like Element of the carrier of n * : len b1 = len M1 } is set

comp n is Relation-like the carrier of n -defined the carrier of n -valued Function-like V27( the carrier of n, the carrier of n) Element of bool [: the carrier of n, the carrier of n:]
[: the carrier of n, the carrier of n:] is set
bool [: the carrier of n, the carrier of n:] is set
K191( the carrier of n, the carrier of n,M1,(comp n)) is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n
len (- M1) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
Indices p is set
dom p is Element of bool NAT
Seg () is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width p ) } is set
[:(dom p),(Seg ()):] is set
p is V4() V5() V6() V10() V11() V12() integer ext-real set
c6 is V4() V5() V6() V10() V11() V12() integer ext-real set
[p,c6] is set
(- p) * (p,c6) is Element of the carrier of n
c6 - p is V11() V12() integer ext-real set
(c6 - p) mod (len (- M1)) is V11() V12() integer ext-real set
((c6 - p) mod (len (- M1))) + 1 is V11() V12() integer ext-real set
(- M1) . (((c6 - p) mod (len (- M1))) + 1) is set
(c6 - p) mod K is V11() V12() integer ext-real set
((c6 - p) mod K) + 1 is V11() V12() integer ext-real set
(c6 - p) mod (len M1) is V11() V12() integer ext-real set
((c6 - p) mod (len M1)) + 1 is V11() V12() integer ext-real set
dom M1 is set
p * (p,c6) is Element of the carrier of n
- (p * (p,c6)) is Element of the carrier of n
(comp n) . (p * (p,c6)) is set
M1 . (((c6 - p) mod (len M1)) + 1) is set
(comp n) . (M1 . (((c6 - p) mod (len M1)) + 1)) is set
(- M1) . (((c6 - p) mod (len M1)) + 1) is set

len p is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT
K is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT

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

K is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT

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

(p * p) - (M1 * c6) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of K,K, the carrier of n

(p * p) + (- (M1 * c6)) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular FinSequence of the carrier of n *
- (M1 * c6) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of K,K, the carrier of n
K is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT

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

(p * c6) + (M1 * c7) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of K,K, the carrier of n

((p * c6) + (M1 * c7)) - (p * M3) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of K,K, the carrier of n

((p * c6) + (M1 * c7)) + (- (p * M3)) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular FinSequence of the carrier of n *
- (p * M3) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of K,K, the carrier of n
K is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT

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

(p * c6) - (M1 * c7) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of K,K, the carrier of n

(p * c6) + (- (M1 * c7)) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular FinSequence of the carrier of n *

((p * c6) - (M1 * c7)) - (p * M3) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of K,K, the carrier of n

((p * c6) - (M1 * c7)) + (