:: MATRIX17 semantic presentation

REAL is set
NAT is non empty V4() V5() V6() V30() V35() V36() Element of bool REAL
bool REAL is set
NAT is non empty V4() V5() V6() V30() V35() V36() set
bool NAT is V30() set
bool NAT is V30() set
1 is non empty V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real positive non negative Element of NAT
2 is non empty V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real positive non negative Element of NAT
COMPLEX is set
RAT is set
INT is set
{} is empty V4() V5() V6() V8() V9() V10() V11() V12() Function-like functional V30() V35() V37( {} ) integer ext-real non positive non negative set
[:COMPLEX,COMPLEX:] is set
bool [:COMPLEX,COMPLEX:] is set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is set
[:REAL,REAL:] is set
bool [:REAL,REAL:] is set
[:[:REAL,REAL:],REAL:] is set
bool [:[:REAL,REAL:],REAL:] is set
[:RAT,RAT:] is set
bool [:RAT,RAT:] is set
[:[:RAT,RAT:],RAT:] is set
bool [:[:RAT,RAT:],RAT:] is set
[:INT,INT:] is set
bool [:INT,INT:] is set
[:[:INT,INT:],INT:] is set
bool [:[:INT,INT:],INT:] is set
[:NAT,NAT:] is V30() set
[:[:NAT,NAT:],NAT:] is V30() set
bool [:[:NAT,NAT:],NAT:] is V30() set
0 is empty V4() V5() V6() V8() V9() V10() V11() V12() Function-like functional V30() V35() V37( {} ) integer ext-real non positive non negative Element of NAT
K is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
n is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
Seg n is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
n + 1 is V11() V12() integer ext-real set
(n + 1) - K is V11() V12() integer ext-real set
K + 1 is V11() V12() integer ext-real set
(K + 1) - K is V11() V12() integer ext-real set
K + n is V11() V12() integer ext-real set
(K + n) - K is V11() V12() integer ext-real set
K is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
M is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[K,M] is set
n is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
Seg n is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
[:(Seg n),(Seg n):] is set
n + 1 is V11() V12() integer ext-real set
(n + 1) - M is V11() V12() integer ext-real set
(n + 1) - K is V11() V12() integer ext-real set
n is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
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() V30() V35() integer ext-real set
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
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() V30() V35() integer ext-real set
M is Element of the carrier of K
(n,n) --> M 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
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
i is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[i,j] is set
Indices p is set
dom p is Element of bool NAT
width p is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width p) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width p ) } is set
[:(dom p),(Seg (width p)):] is set
c₇ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
n + 1 is V11() V12() integer ext-real set
(n + 1) - j is V11() V12() integer ext-real set
c₈ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
(n + 1) - i is V11() V12() integer ext-real set
p * (i,j) is Element of the carrier of K
p * (c₇,c₈) is Element of the carrier of K
Seg n is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
[:(Seg n),(Seg n):] is set
[c₇,c₈] is set
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
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() V30() V35() integer ext-real set
0. K is V49(K) Element of the carrier of K
(n,n) --> (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 (K,n) Matrix of n,n, the carrier of K
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
n is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real 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
M is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular (K,n) Matrix of n,n, the carrier of K
- M 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
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
Indices M is set
dom M is Element of bool NAT
width M is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width M) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width M ) } is set
[:(dom M),(Seg (width M)):] is set
Seg n is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
[:(Seg n),(Seg n):] is set
i is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[i,j] is set
Indices p is set
dom p is Element of bool NAT
width p is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width p) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width p ) } is set
[:(dom p),(Seg (width p)):] is set
c₇ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
n + 1 is V11() V12() integer ext-real set
(n + 1) - j is V11() V12() integer ext-real set
c₈ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
(n + 1) - i is V11() V12() integer ext-real set
p * (i,j) is Element of the carrier of K
p * (c₇,c₈) is Element of the carrier of K
Indices (- M) is set
dom (- M) is Element of bool NAT
width (- M) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width (- M)) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width (- M) ) } is set
[:(dom (- M)),(Seg (width (- M))):] is set
[c₇,c₈] is set
(- M) * (i,j) is Element of the carrier of K
M * (i,j) is Element of the carrier of K
- (M * (i,j)) is Element of the carrier of K
M * (c₇,c₈) is Element of the carrier of K
- (M * (c₇,c₈)) is Element of the carrier of K
(- M) * (c₇,c₈) is Element of the carrier of K
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
n is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real 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
M is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular (K,n) Matrix of n,n, the carrier of K
p is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular (K,n) Matrix of n,n, the carrier of K
M + 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
i 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
j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
c₇ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[j,c₇] is set
Indices i is set
dom i is Element of bool NAT
width i is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width i) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width i ) } is set
[:(dom i),(Seg (width i)):] is set
c₈ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
n + 1 is V11() V12() integer ext-real set
(n + 1) - c₇ is V11() V12() integer ext-real set
l is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
(n + 1) - j is V11() V12() integer ext-real set
i * (j,c₇) is Element of the carrier of K
i * (c₈,l) is Element of the carrier of K
Seg n is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
[:(Seg n),(Seg n):] is set
[c₈,l] is set
Indices M is set
dom M is Element of bool NAT
width M is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width M) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width M ) } is set
[:(dom M),(Seg (width M)):] is set
Indices p is set
dom p is Element of bool NAT
width p is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width p) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width p ) } is set
[:(dom p),(Seg (width p)):] is set
(M + p) * (j,c₇) is Element of the carrier of K
M * (j,c₇) is Element of the carrier of K
p * (j,c₇) is Element of the carrier of K
(M * (j,c₇)) + (p * (j,c₇)) 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 carrier of K, the carrier of K:] is set
[:[: 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
the addF of K . ((M * (j,c₇)),(p * (j,c₇))) is Element of the carrier of K
M * (c₈,l) is Element of the carrier of K
(M * (c₈,l)) + (p * (j,c₇)) is Element of the carrier of K
the addF of K . ((M * (c₈,l)),(p * (j,c₇))) is Element of the carrier of K
p * (c₈,l) is Element of the carrier of K
(M * (c₈,l)) + (p * (c₈,l)) is Element of the carrier of K
the addF of K . ((M * (c₈,l)),(p * (c₈,l))) is Element of the carrier of K
(M + p) * (c₈,l) is Element of the carrier of K
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
the carrier of K is non empty non trivial set
n is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
the carrier of K * is functional FinSequence-membered FinSequenceSet of the carrier of K
p is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular (K,n) Matrix of n,n, the carrier of K
M is Element of the carrier of K
M * 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
i 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
Indices p is set
dom p is Element of bool NAT
width p is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width p) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width p ) } is set
[:(dom p),(Seg (width p)):] is set
Seg n is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
[:(Seg n),(Seg n):] is set
j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
c₇ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[j,c₇] is set
Indices i is set
dom i is Element of bool NAT
width i is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width i) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width i ) } is set
[:(dom i),(Seg (width i)):] is set
c₈ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
n + 1 is V11() V12() integer ext-real set
(n + 1) - c₇ is V11() V12() integer ext-real set
l is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
(n + 1) - j is V11() V12() integer ext-real set
i * (j,c₇) is Element of the carrier of K
i * (c₈,l) is Element of the carrier of K
[c₈,l] is set
(M * p) * (j,c₇) is Element of the carrier of K
p * (j,c₇) is Element of the carrier of K
M * (p * (j,c₇)) is Element of the carrier of K
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:] is set
[:[: 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
the multF of K . (M,(p * (j,c₇))) is Element of the carrier of K
p * (c₈,l) is Element of the carrier of K
M * (p * (c₈,l)) is Element of the carrier of K
the multF of K . (M,(p * (c₈,l))) is Element of the carrier of K
(M * p) * (c₈,l) is Element of the carrier of K
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
n is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real 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
M is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular (K,n) Matrix of n,n, the carrier of K
p is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular (K,n) Matrix of n,n, the carrier of K
M - 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
- p is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular FinSequence of the carrier of K *
M + (- p) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular FinSequence of the carrier of K *
- p is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular (K,n) Matrix of n,n, the carrier of K
M + (- p) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular (K,n) Matrix of n,n, the carrier of K
i 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
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
n is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real 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
M is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular (K,n) Matrix of n,n, the carrier of K
M @ 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
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
Indices M is set
dom M is Element of bool NAT
width M is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width M) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width M ) } is set
[:(dom M),(Seg (width M)):] is set
Seg n is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
[:(Seg n),(Seg n):] is set
i is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[i,j] is set
Indices p is set
dom p is Element of bool NAT
width p is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width p) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width p ) } is set
[:(dom p),(Seg (width p)):] is set
c₇ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
n + 1 is V11() V12() integer ext-real set
(n + 1) - j is V11() V12() integer ext-real set
c₈ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
(n + 1) - i is V11() V12() integer ext-real set
p * (i,j) is Element of the carrier of K
p * (c₇,c₈) is Element of the carrier of K
[j,i] is set
[((n + 1) - i),((n + 1) - j)] is set
[((n + 1) - j),((n + 1) - i)] is set
M * (j,i) is Element of the carrier of K
M * (c₈,c₇) is Element of the carrier of K
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
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() V30() V35() integer ext-real set
M 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
width M is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
p is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
len p is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Indices M is set
dom M is Element of bool NAT
Seg (width M) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width M ) } is set
[:(dom M),(Seg (width M)):] is set
Seg n is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
[:(Seg n),(Seg n):] is set
i is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[i,j] is set
c₇ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
n + 1 is V11() V12() integer ext-real set
(n + 1) - j is V11() V12() integer ext-real set
c₈ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
(n + 1) - i is V11() V12() integer ext-real set
M * (i,j) is Element of the carrier of K
M * (c₇,c₈) is Element of the carrier of K
[c₇,c₈] is set
((n + 1) - i) - ((n + 1) - j) is V11() V12() integer ext-real set
(((n + 1) - i) - ((n + 1) - j)) mod (len p) is V11() V12() integer ext-real set
((((n + 1) - i) - ((n + 1) - j)) mod (len p)) + 1 is V11() V12() integer ext-real set
p . (((((n + 1) - i) - ((n + 1) - j)) mod (len p)) + 1) is set
j - i is V11() V12() integer ext-real set
(j - i) mod (len p) is V11() V12() integer ext-real set
((j - i) mod (len p)) + 1 is V11() V12() integer ext-real set
p . (((j - i) mod (len p)) + 1) is set
M 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 M is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
p is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
len p is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Indices M is set
dom M is Element of bool NAT
width M is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width M) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width M ) } is set
[:(dom M),(Seg (width M)):] is set
Seg n is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
[:(Seg n),(Seg n):] is set
i is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[i,j] is set
c₇ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
n + 1 is V11() V12() integer ext-real set
(n + 1) - j is V11() V12() integer ext-real set
c₈ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
(n + 1) - i is V11() V12() integer ext-real set
M * (i,j) is Element of the carrier of K
M * (c₇,c₈) is Element of the carrier of K
[c₇,c₈] is set
((n + 1) - j) - ((n + 1) - i) is V11() V12() integer ext-real set
(((n + 1) - j) - ((n + 1) - i)) mod n is V11() V12() integer ext-real set
((((n + 1) - j) - ((n + 1) - i)) mod n) + 1 is V11() V12() integer ext-real set
p . (((((n + 1) - j) - ((n + 1) - i)) mod n) + 1) is set
i - j is V11() V12() integer ext-real set
(i - j) mod n is V11() V12() integer ext-real set
((i - j) mod n) + 1 is V11() V12() integer ext-real set
p . (((i - j) mod n) + 1) is set
n is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
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() V30() V35() integer ext-real set
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
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() V30() V35() integer ext-real set
0. K is V49(K) Element of the carrier of K
(n,n) --> (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 (K,n) Matrix of n,n, the carrier of K
M is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular (K,n) Matrix of n,n, the carrier of K
p is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
i is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[p,i] is set
Indices M is set
dom M is Element of bool NAT
width M is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width M) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width M ) } is set
[:(dom M),(Seg (width M)):] is set
j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
n + 1 is V11() V12() integer ext-real set
(n + 1) - i is V11() V12() integer ext-real set
c₇ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
(n + 1) - p is V11() V12() integer ext-real set
M * (p,i) is Element of the carrier of K
M * (j,c₇) is Element of the carrier of K
- (M * (j,c₇)) is Element of the carrier of K
Seg n is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
[:(Seg n),(Seg n):] is set
[j,c₇] is set
- (0. K) is Element of the carrier of K
n is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital Fanoian doubleLoopStr
the carrier of n is non empty non trivial set
the carrier of n * is functional FinSequence-membered FinSequenceSet of the carrier of n
0. n is V49(n) Element of the carrier of n
K is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
M is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
p is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[M,p] is set
M + p is V11() V12() integer ext-real set
K + 1 is V11() V12() integer ext-real set
i is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
(K + 1) - p is V11() V12() integer ext-real set
j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
(K + 1) - M is V11() V12() integer ext-real set
c₇ 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
Indices c₇ is set
dom c₇ is Element of bool NAT
width c₇ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width c₇) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width c₇ ) } is set
[:(dom c₇),(Seg (width c₇)):] is set
c₇ * (M,p) is Element of the carrier of n
- (c₇ * (M,p)) is Element of the carrier of n
(c₇ * (M,p)) + (c₇ * (M,p)) is Element of the carrier of n
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
the addF of n . ((c₇ * (M,p)),(c₇ * (M,p))) is Element of the carrier of n
1_ n is Element of the carrier of n
K142(n) is V49(n) Element of the carrier of n
(1_ n) * (c₇ * (M,p)) 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 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 multF of n . ((1_ n),(c₇ * (M,p))) is Element of the carrier of n
((1_ n) * (c₇ * (M,p))) + (c₇ * (M,p)) is Element of the carrier of n
the addF of n . (((1_ n) * (c₇ * (M,p))),(c₇ * (M,p))) is Element of the carrier of n
((1_ n) * (c₇ * (M,p))) + ((1_ n) * (c₇ * (M,p))) is Element of the carrier of n
the addF of n . (((1_ n) * (c₇ * (M,p))),((1_ n) * (c₇ * (M,p)))) is Element of the carrier of n
(1_ n) + (1_ n) is Element of the carrier of n
the addF of n . ((1_ n),(1_ n)) is Element of the carrier of n
((1_ n) + (1_ n)) * (c₇ * (M,p)) is Element of the carrier of n
the multF of n . (((1_ n) + (1_ n)),(c₇ * (M,p))) is Element of the carrier of n
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
n is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real 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
M is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular (K,n) Matrix of n,n, the carrier of K
- M 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
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
Indices M is set
dom M is Element of bool NAT
width M is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width M) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width M ) } is set
[:(dom M),(Seg (width M)):] is set
Seg n is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
[:(Seg n),(Seg n):] is set
i is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[i,j] is set
Indices p is set
dom p is Element of bool NAT
width p is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width p) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width p ) } is set
[:(dom p),(Seg (width p)):] is set
c₇ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
n + 1 is V11() V12() integer ext-real set
(n + 1) - j is V11() V12() integer ext-real set
c₈ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
(n + 1) - i is V11() V12() integer ext-real set
p * (i,j) is Element of the carrier of K
p * (c₇,c₈) is Element of the carrier of K
- (p * (c₇,c₈)) is Element of the carrier of K
Indices (- M) is set
dom (- M) is Element of bool NAT
width (- M) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width (- M)) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width (- M) ) } is set
[:(dom (- M)),(Seg (width (- M))):] is set
[c₇,c₈] is set
(- M) * (i,j) is Element of the carrier of K
M * (i,j) is Element of the carrier of K
- (M * (i,j)) is Element of the carrier of K
M * (c₇,c₈) is Element of the carrier of K
- (M * (c₇,c₈)) is Element of the carrier of K
- (- (M * (c₇,c₈))) is Element of the carrier of K
(- M) * (c₇,c₈) is Element of the carrier of K
- ((- M) * (c₇,c₈)) is Element of the carrier of K
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
n is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real 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
M is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular (K,n) Matrix of n,n, the carrier of K
p is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular (K,n) Matrix of n,n, the carrier of K
M + 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
i 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
j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
c₇ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[j,c₇] is set
Indices i is set
dom i is Element of bool NAT
width i is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width i) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width i ) } is set
[:(dom i),(Seg (width i)):] is set
c₈ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
n + 1 is V11() V12() integer ext-real set
(n + 1) - c₇ is V11() V12() integer ext-real set
l is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
(n + 1) - j is V11() V12() integer ext-real set
i * (j,c₇) is Element of the carrier of K
i * (c₈,l) is Element of the carrier of K
- (i * (c₈,l)) is Element of the carrier of K
Seg n is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
[:(Seg n),(Seg n):] is set
[c₈,l] is set
Indices M is set
dom M is Element of bool NAT
width M is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width M) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width M ) } is set
[:(dom M),(Seg (width M)):] is set
Indices p is set
dom p is Element of bool NAT
width p is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width p) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width p ) } is set
[:(dom p),(Seg (width p)):] is set
(M + p) * (j,c₇) is Element of the carrier of K
M * (j,c₇) is Element of the carrier of K
p * (j,c₇) is Element of the carrier of K
(M * (j,c₇)) + (p * (j,c₇)) 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 carrier of K, the carrier of K:] is set
[:[: 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
the addF of K . ((M * (j,c₇)),(p * (j,c₇))) is Element of the carrier of K
M * (c₈,l) is Element of the carrier of K
- (M * (c₈,l)) is Element of the carrier of K
(- (M * (c₈,l))) + (p * (j,c₇)) is Element of the carrier of K
the addF of K . ((- (M * (c₈,l))),(p * (j,c₇))) is Element of the carrier of K
p * (c₈,l) is Element of the carrier of K
- (p * (c₈,l)) is Element of the carrier of K
(- (M * (c₈,l))) + (- (p * (c₈,l))) is Element of the carrier of K
the addF of K . ((- (M * (c₈,l))),(- (p * (c₈,l)))) is Element of the carrier of K
(M * (c₈,l)) + (p * (c₈,l)) is Element of the carrier of K
the addF of K . ((M * (c₈,l)),(p * (c₈,l))) is Element of the carrier of K
- ((M * (c₈,l)) + (p * (c₈,l))) is Element of the carrier of K
(M + p) * (c₈,l) is Element of the carrier of K
- ((M + p) * (c₈,l)) is Element of the carrier of K
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
the carrier of K is non empty non trivial set
n is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
the carrier of K * is functional FinSequence-membered FinSequenceSet of the carrier of K
p is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular (K,n) Matrix of n,n, the carrier of K
M is Element of the carrier of K
M * 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
i 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
Indices p is set
dom p is Element of bool NAT
width p is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width p) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width p ) } is set
[:(dom p),(Seg (width p)):] is set
Seg n is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
[:(Seg n),(Seg n):] is set
j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
c₇ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[j,c₇] is set
Indices i is set
dom i is Element of bool NAT
width i is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width i) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width i ) } is set
[:(dom i),(Seg (width i)):] is set
c₈ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
n + 1 is V11() V12() integer ext-real set
(n + 1) - c₇ is V11() V12() integer ext-real set
l is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
(n + 1) - j is V11() V12() integer ext-real set
i * (j,c₇) is Element of the carrier of K
i * (c₈,l) is Element of the carrier of K
- (i * (c₈,l)) is Element of the carrier of K
[c₈,l] is set
(M * p) * (j,c₇) is Element of the carrier of K
p * (j,c₇) is Element of the carrier of K
M * (p * (j,c₇)) is Element of the carrier of K
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:] is set
[:[: 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
the multF of K . (M,(p * (j,c₇))) is Element of the carrier of K
p * (c₈,l) is Element of the carrier of K
- (p * (c₈,l)) is Element of the carrier of K
M * (- (p * (c₈,l))) is Element of the carrier of K
the multF of K . (M,(- (p * (c₈,l)))) is Element of the carrier of K
M * (p * (c₈,l)) is Element of the carrier of K
the multF of K . (M,(p * (c₈,l))) is Element of the carrier of K
- (M * (p * (c₈,l))) is Element of the carrier of K
(M * p) * (c₈,l) is Element of the carrier of K
- ((M * p) * (c₈,l)) is Element of the carrier of K
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
n is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real 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
M is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular (K,n) Matrix of n,n, the carrier of K
p is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular (K,n) Matrix of n,n, the carrier of K
M - 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
- p is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular FinSequence of the carrier of K *
M + (- p) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular FinSequence of the carrier of K *
- p is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular (K,n) Matrix of n,n, the carrier of K
M + (- p) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular (K,n) Matrix of n,n, the carrier of K
i 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
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
n is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real 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
M is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular (K,n) Matrix of n,n, the carrier of K
M @ 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
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
Indices M is set
dom M is Element of bool NAT
width M is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width M) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width M ) } is set
[:(dom M),(Seg (width M)):] is set
Seg n is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
[:(Seg n),(Seg n):] is set
i is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[i,j] is set
Indices p is set
dom p is Element of bool NAT
width p is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width p) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width p ) } is set
[:(dom p),(Seg (width p)):] is set
c₇ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
n + 1 is V11() V12() integer ext-real set
(n + 1) - j is V11() V12() integer ext-real set
c₈ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
(n + 1) - i is V11() V12() integer ext-real set
p * (i,j) is Element of the carrier of K
p * (c₇,c₈) is Element of the carrier of K
- (p * (c₇,c₈)) is Element of the carrier of K
[j,i] is set
[((n + 1) - i),((n + 1) - j)] is set
[((n + 1) - j),((n + 1) - i)] is set
M * (j,i) is Element of the carrier of K
M * (c₈,c₇) is Element of the carrier of K
- (M * (c₈,c₇)) is Element of the carrier of K
n is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
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() V30() V35() integer ext-real set
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
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() V30() V35() integer ext-real set
M is Element of the carrier of K
(n,n) --> M is Relation-like NAT -defined the carrier of K * -valued the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular (K,n) Matrix of n,n, the carrier of K
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
i is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[i,j] is set
Indices p is set
dom p is Element of bool NAT
width p is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width p) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width p ) } is set
[:(dom p),(Seg (width p)):] is set
c₇ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
n + 1 is V11() V12() integer ext-real set
(n + 1) - i is V11() V12() integer ext-real set
c₈ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
(n + 1) - j is V11() V12() integer ext-real set
p * (i,j) is Element of the carrier of K
p * (c₇,c₈) is Element of the carrier of K
Seg n is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
[:(Seg n),(Seg n):] is set
[c₇,c₈] is set
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
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() V30() V35() integer ext-real set
0. K is V49(K) Element of the carrier of K
(n,n) --> (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 (K,n) (K,n) Matrix of n,n, the carrier of K
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
n is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real 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
M is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular (K,n) Matrix of n,n, the carrier of K
- M 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
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
Indices M is set
dom M is Element of bool NAT
width M is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width M) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width M ) } is set
[:(dom M),(Seg (width M)):] is set
Seg n is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
[:(Seg n),(Seg n):] is set
i is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[i,j] is set
Indices p is set
dom p is Element of bool NAT
width p is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width p) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width p ) } is set
[:(dom p),(Seg (width p)):] is set
c₇ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
n + 1 is V11() V12() integer ext-real set
(n + 1) - i is V11() V12() integer ext-real set
c₈ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
(n + 1) - j is V11() V12() integer ext-real set
p * (i,j) is Element of the carrier of K
p * (c₇,c₈) is Element of the carrier of K
Indices (- M) is set
dom (- M) is Element of bool NAT
width (- M) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width (- M)) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width (- M) ) } is set
[:(dom (- M)),(Seg (width (- M))):] is set
[c₇,c₈] is set
(- M) * (i,j) is Element of the carrier of K
M * (i,j) is Element of the carrier of K
- (M * (i,j)) is Element of the carrier of K
M * (c₇,c₈) is Element of the carrier of K
- (M * (c₇,c₈)) is Element of the carrier of K
(- M) * (c₇,c₈) is Element of the carrier of K
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
n is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real 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
M is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular (K,n) Matrix of n,n, the carrier of K
p is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular (K,n) Matrix of n,n, the carrier of K
M + 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
i 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
j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
c₇ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[j,c₇] is set
Indices i is set
dom i is Element of bool NAT
width i is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width i) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width i ) } is set
[:(dom i),(Seg (width i)):] is set
c₈ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
n + 1 is V11() V12() integer ext-real set
(n + 1) - j is V11() V12() integer ext-real set
l is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
(n + 1) - c₇ is V11() V12() integer ext-real set
i * (j,c₇) is Element of the carrier of K
i * (c₈,l) is Element of the carrier of K
Seg n is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
[:(Seg n),(Seg n):] is set
[c₈,l] is set
Indices M is set
dom M is Element of bool NAT
width M is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width M) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width M ) } is set
[:(dom M),(Seg (width M)):] is set
Indices p is set
dom p is Element of bool NAT
width p is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width p) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width p ) } is set
[:(dom p),(Seg (width p)):] is set
(M + p) * (j,c₇) is Element of the carrier of K
M * (j,c₇) is Element of the carrier of K
p * (j,c₇) is Element of the carrier of K
(M * (j,c₇)) + (p * (j,c₇)) 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 carrier of K, the carrier of K:] is set
[:[: 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
the addF of K . ((M * (j,c₇)),(p * (j,c₇))) is Element of the carrier of K
M * (c₈,l) is Element of the carrier of K
(M * (c₈,l)) + (p * (j,c₇)) is Element of the carrier of K
the addF of K . ((M * (c₈,l)),(p * (j,c₇))) is Element of the carrier of K
p * (c₈,l) is Element of the carrier of K
(M * (c₈,l)) + (p * (c₈,l)) is Element of the carrier of K
the addF of K . ((M * (c₈,l)),(p * (c₈,l))) is Element of the carrier of K
(M + p) * (c₈,l) is Element of the carrier of K
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
the carrier of K is non empty non trivial set
n is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
the carrier of K * is functional FinSequence-membered FinSequenceSet of the carrier of K
p is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular (K,n) Matrix of n,n, the carrier of K
M is Element of the carrier of K
M * 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
i 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
Indices p is set
dom p is Element of bool NAT
width p is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width p) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width p ) } is set
[:(dom p),(Seg (width p)):] is set
Seg n is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
[:(Seg n),(Seg n):] is set
j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
c₇ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[j,c₇] is set
Indices i is set
dom i is Element of bool NAT
width i is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width i) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width i ) } is set
[:(dom i),(Seg (width i)):] is set
c₈ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
n + 1 is V11() V12() integer ext-real set
(n + 1) - j is V11() V12() integer ext-real set
l is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
(n + 1) - c₇ is V11() V12() integer ext-real set
i * (j,c₇) is Element of the carrier of K
i * (c₈,l) is Element of the carrier of K
[c₈,l] is set
(M * p) * (j,c₇) is Element of the carrier of K
p * (j,c₇) is Element of the carrier of K
M * (p * (j,c₇)) is Element of the carrier of K
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:] is set
[:[: 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
the multF of K . (M,(p * (j,c₇))) is Element of the carrier of K
p * (c₈,l) is Element of the carrier of K
M * (p * (c₈,l)) is Element of the carrier of K
the multF of K . (M,(p * (c₈,l))) is Element of the carrier of K
(M * p) * (c₈,l) is Element of the carrier of K
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
n is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real 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
M is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular (K,n) Matrix of n,n, the carrier of K
p is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular (K,n) Matrix of n,n, the carrier of K
M - 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
- p is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular FinSequence of the carrier of K *
M + (- p) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular FinSequence of the carrier of K *
- p is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular (K,n) Matrix of n,n, the carrier of K
M + (- p) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular (K,n) Matrix of n,n, the carrier of K
i 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
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
n is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real 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
M is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular (K,n) Matrix of n,n, the carrier of K
M @ 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
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
Indices M is set
dom M is Element of bool NAT
width M is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width M) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width M ) } is set
[:(dom M),(Seg (width M)):] is set
Seg n is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
[:(Seg n),(Seg n):] is set
i is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[i,j] is set
Indices p is set
dom p is Element of bool NAT
width p is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width p) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width p ) } is set
[:(dom p),(Seg (width p)):] is set
c₇ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
n + 1 is V11() V12() integer ext-real set
(n + 1) - i is V11() V12() integer ext-real set
c₈ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
(n + 1) - j is V11() V12() integer ext-real set
p * (i,j) is Element of the carrier of K
p * (c₇,c₈) is Element of the carrier of K
[j,i] is set
[((n + 1) - i),((n + 1) - j)] is set
[((n + 1) - j),((n + 1) - i)] is set
M * (j,i) is Element of the carrier of K
M * (c₈,c₇) is Element of the carrier of K
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
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() V30() V35() integer ext-real set
M 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
Indices M is set
dom M is Element of bool NAT
width M is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width M) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width M ) } is set
[:(dom M),(Seg (width M)):] is set
Seg n is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
[:(Seg n),(Seg n):] is set
p is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
i is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[p,i] is set
j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
n + 1 is V11() V12() integer ext-real set
(n + 1) - p is V11() V12() integer ext-real set
c₇ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
(n + 1) - i is V11() V12() integer ext-real set
M * (p,i) is Element of the carrier of K
M * (j,c₇) is Element of the carrier of K
[j,c₇] is set
[c₇,j] is set
M * (c₇,j) is Element of the carrier of K
M @ 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
(M @) * (j,c₇) is Element of the carrier of K
K is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
n is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
Seg n is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
M is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
K + M is V11() V12() integer ext-real set
n + 1 is V11() V12() integer ext-real set
(K + M) - 1 is V11() V12() integer ext-real set
((K + M) - 1) mod n is V11() V12() integer ext-real set
1 + 1 is non empty V11() V12() integer ext-real positive non negative set
(1 + 1) - 1 is V11() V12() integer ext-real set
(n + 1) - 1 is V11() V12() integer ext-real set
(K + M) - n is V11() V12() integer ext-real set
(n + 1) - n is V11() V12() integer ext-real set
((K + M) - n) - 1 is V11() V12() integer ext-real set
1 - 1 is V11() V12() integer ext-real set
0 + 1 is non empty V11() V12() integer ext-real positive non negative set
n + n is V11() V12() integer ext-real set
(n + n) - n is V11() V12() integer ext-real set
n - 1 is V11() V12() integer ext-real set
(((K + M) - n) - 1) mod n is V11() V12() integer ext-real set
((K + M) - 1) - n is V11() V12() integer ext-real set
(((K + M) - 1) - n) + n is V11() V12() integer ext-real set
((((K + M) - 1) - n) + n) mod n is V11() V12() integer ext-real set
(((K + M) - 1) - n) mod n is V11() V12() integer ext-real set
n mod n is V11() V12() integer ext-real set
((((K + M) - 1) - n) mod n) + (n mod n) is V11() V12() integer ext-real set
(((((K + M) - 1) - n) mod n) + (n mod n)) mod n is V11() V12() integer ext-real set
(((K + M) - 1) - n) + 0 is V11() V12() integer ext-real set
((((K + M) - 1) - n) + 0) mod n is V11() V12() integer ext-real set
K is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
M is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[K,M] is set
n is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
Seg n is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
[:(Seg n),(Seg n):] is set
K + M is V11() V12() integer ext-real set
n + 1 is V11() V12() integer ext-real set
(K + M) - 1 is V11() V12() integer ext-real set
((K + M) - 1) mod n is V11() V12() integer ext-real set
n is set
n * is functional FinSequence-membered FinSequenceSet of n
n is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
the carrier of K is non empty non trivial set
M is Element of the carrier of K
(n,n) --> M is Relation-like NAT -defined the carrier of K * -valued the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular (K,n) (K,n) Matrix of n,n, the carrier of K
the carrier of K * is functional FinSequence-membered FinSequenceSet of the carrier of K
n |-> M 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
n -tuples_on the carrier of K is non empty functional FinSequence-membered FinSequenceSet of the carrier of K
{ b₁ where b₁ is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like Element of the carrier of K * : len b₁ = n } is set
Seg n is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
(Seg n) --> M is Relation-like Seg n -defined Seg n -defined the carrier of K -valued {M} -valued Function-like constant total total V27( Seg n,{M}) FinSequence-like Element of bool [:(Seg n),{M}:]
{M} is non empty trivial V37(1) set
[:(Seg n),{M}:] is set
bool [:(Seg n),{M}:] is set
width ((n,n) --> M) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
len (n |-> M) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Indices ((n,n) --> M) is set
dom ((n,n) --> M) is Element of bool NAT
Seg (width ((n,n) --> M)) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width ((n,n) --> M) ) } is set
[:(dom ((n,n) --> M)),(Seg (width ((n,n) --> M))):] is set
(len (n |-> M)) + 1 is V11() V12() integer ext-real set
(n |-> M) . (len (n |-> M)) is set
[:(Seg n),(Seg n):] is set
j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
c₇ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[j,c₇] is set
j + c₇ is V11() V12() integer ext-real set
((n,n) --> M) * (j,c₇) is Element of the carrier of K
(j + c₇) - 1 is V11() V12() integer ext-real set
((j + c₇) - 1) mod (len (n |-> M)) is V11() V12() integer ext-real set
(n |-> M) . (((j + c₇) - 1) mod (len (n |-> M))) is set
(Seg n) --> M 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) --> M) . (((j + c₇) - 1) mod (len (n |-> M))) is set
j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
c₇ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[j,c₇] is set
j + c₇ is V11() V12() integer ext-real set
((n,n) --> M) * (j,c₇) is Element of the carrier of K
1 + 1 is non empty V11() V12() integer ext-real positive non negative set
(1 + 1) - 1 is V11() V12() integer ext-real set
((len (n |-> M)) + 1) - 1 is V11() V12() integer ext-real set
Seg (len (n |-> M)) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= len (n |-> M) ) } is set
(Seg n) --> M 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) --> M) . (len (n |-> M)) is set
n is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
the carrier of K is non empty non trivial set
the carrier of K * is functional FinSequence-membered FinSequenceSet of the carrier of K
M is Element of the carrier of K
p is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
M * p is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
M 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 [;] (M,(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,p,(M multfield)) is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
i 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
M * i 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 p is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
width i is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Indices (M * i) is set
dom (M * i) is Element of bool NAT
width (M * i) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width (M * i)) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width (M * i) ) } is set
[:(dom (M * i)),(Seg (width (M * i))):] is set
Seg n is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
[:(Seg n),(Seg n):] is set
dom p is set
dom (M * p) is set
len (M * p) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (len (M * p)) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= len (M * p) ) } is set
(len (M * p)) + 1 is V11() V12() integer ext-real set
j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
c₇ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[j,c₇] is set
j + c₇ is V11() V12() integer ext-real set
(M * i) * (j,c₇) is Element of the carrier of K
(j + c₇) - 1 is V11() V12() integer ext-real set
((j + c₇) - 1) mod (len (M * p)) is V11() V12() integer ext-real set
(M * p) . (((j + c₇) - 1) mod (len (M * p))) is set
((j + c₇) - 1) mod n is V11() V12() integer ext-real set
Indices i is set
dom i is Element of bool NAT
Seg (width i) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width i ) } is set
[:(dom i),(Seg (width i)):] is set
i * (j,c₇) is Element of the carrier of K
M * (i * (j,c₇)) is Element of the carrier of K
the multF of K . (M,(i * (j,c₇))) is Element of the carrier of K
(M multfield) . (i * (j,c₇)) is set
((j + c₇) - 1) mod (len p) is V11() V12() integer ext-real set
p . (((j + c₇) - 1) mod (len p)) is set
(M multfield) . (p . (((j + c₇) - 1) mod (len p))) is set
p /. (((j + c₇) - 1) mod (len p)) is Element of the carrier of K
(M multfield) . (p /. (((j + c₇) - 1) mod (len p))) is set
M * (p /. (((j + c₇) - 1) mod (len p))) is Element of the carrier of K
the multF of K . (M,(p /. (((j + c₇) - 1) mod (len p)))) is Element of the carrier of K
(M * p) /. (((j + c₇) - 1) mod (len p)) is Element of the carrier of K
(M * p) . (((j + c₇) - 1) mod (len p)) is set
(M * p) . (len (M * p)) is set
j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
c₇ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[j,c₇] is set
j + c₇ is V11() V12() integer ext-real set
(M * i) * (j,c₇) is Element of the carrier of K
1 + 1 is non empty V11() V12() integer ext-real positive non negative set
(1 + 1) - 1 is V11() V12() integer ext-real set
((len (M * p)) + 1) - 1 is V11() V12() integer ext-real set
Indices i is set
dom i is Element of bool NAT
Seg (width i) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width i ) } is set
[:(dom i),(Seg (width i)):] is set
i * (j,c₇) is Element of the carrier of K
M * (i * (j,c₇)) is Element of the carrier of K
the multF of K . (M,(i * (j,c₇))) is Element of the carrier of K
(M multfield) . (i * (j,c₇)) is set
p . (len p) is set
(M multfield) . (p . (len p)) is set
p /. (len p) is Element of the carrier of K
(M multfield) . (p /. (len p)) is set
M * (p /. (len p)) is Element of the carrier of K
the multF of K . (M,(p /. (len p))) is Element of the carrier of K
(M * p) /. (len p) is Element of the carrier of K
(M * p) . (len p) is set
n is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
the carrier of K is non empty non trivial set
the carrier of K * is functional FinSequence-membered FinSequenceSet of the carrier of K
M is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
- M 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:]
[: the carrier of K, the carrier of K:] is set
bool [: the carrier of K, the carrier of K:] is set
K191( the carrier of K, the carrier of K,M,(comp K)) is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
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
- 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
len M is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
width p is V4() V5() V6() V10() V11() V12() V30() V35() 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() V30() V35() integer ext-real Element of NAT
Seg (width (- p)) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width (- p) ) } is set
[:(dom (- p)),(Seg (width (- p))):] is set
Seg n is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
[:(Seg n),(Seg n):] is set
(len M) -tuples_on the carrier of K is non empty functional FinSequence-membered FinSequenceSet of the carrier of K
{ b₁ where b₁ is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like Element of the carrier of K * : len b₁ = len M } is set
len (- M) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Indices p is set
dom p is Element of bool NAT
Seg (width p) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width p ) } is set
[:(dom p),(Seg (width p)):] is set
(len M) + 1 is V11() V12() integer ext-real set
i is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[i,j] is set
i + j is V11() V12() integer ext-real set
(- p) * (i,j) is Element of the carrier of K
(i + j) - 1 is V11() V12() integer ext-real set
((i + j) - 1) mod (len (- M)) is V11() V12() integer ext-real set
(- M) . (((i + j) - 1) mod (len (- M))) is set
((i + j) - 1) mod n is V11() V12() integer ext-real set
((i + j) - 1) mod (len M) is V11() V12() integer ext-real set
dom M is set
p * (i,j) is Element of the carrier of K
- (p * (i,j)) is Element of the carrier of K
(comp K) . (p * (i,j)) is set
M . (((i + j) - 1) mod (len M)) is set
(comp K) . (M . (((i + j) - 1) mod (len M))) is set
(- M) . (((i + j) - 1) mod (len M)) is set
(- M) . (len (- M)) is set
i is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[i,j] is set
i + j is V11() V12() integer ext-real set
(- p) * (i,j) is Element of the carrier of K
1 + 1 is non empty V11() V12() integer ext-real positive non negative set
(1 + 1) - 1 is V11() V12() integer ext-real set
((len M) + 1) - 1 is V11() V12() integer ext-real set
Seg (len M) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= len M ) } is set
dom M is set
p * (i,j) is Element of the carrier of K
- (p * (i,j)) is Element of the carrier of K
(comp K) . (p * (i,j)) is set
M . (len M) is set
(comp K) . (M . (len M)) is set
(- M) . (len M) is set
n is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
the carrier of K is non empty non trivial set
the carrier of K * is functional FinSequence-membered FinSequenceSet of the carrier of K
M is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
p is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
M + p is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence 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 carrier of K, the carrier of K:] is set
[:[: 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
K188( the carrier of K, the carrier of K, the carrier of K, the addF of K,M,p) is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
i 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
j 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
i + j 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 M is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
width i is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Indices j is set
dom j is Element of bool NAT
width j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width j) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width j ) } is set
[:(dom j),(Seg (width j)):] is set
Seg n is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
[:(Seg n),(Seg n):] is set
Indices (i + j) is set
dom (i + j) is Element of bool NAT
width (i + j) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width (i + j)) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width (i + j) ) } is set
[:(dom (i + j)),(Seg (width (i + j))):] is set
dom M is set
len p is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Indices i is set
dom i is Element of bool NAT
Seg (width i) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width i ) } is set
[:(dom i),(Seg (width i)):] is set
dom p is set
dom (M + p) is set
len (M + p) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (len (M + p)) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= len (M + p) ) } is set
(len (M + p)) + 1 is V11() V12() integer ext-real set
c₇ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
c₈ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[c₇,c₈] is set
c₇ + c₈ is V11() V12() integer ext-real set
(i + j) * (c₇,c₈) is Element of the carrier of K
(c₇ + c₈) - 1 is V11() V12() integer ext-real set
((c₇ + c₈) - 1) mod (len (M + p)) is V11() V12() integer ext-real set
(M + p) . (((c₇ + c₈) - 1) mod (len (M + p))) is set
i * (c₇,c₈) is Element of the carrier of K
j * (c₇,c₈) is Element of the carrier of K
(i * (c₇,c₈)) + (j * (c₇,c₈)) is Element of the carrier of K
the addF of K . ((i * (c₇,c₈)),(j * (c₇,c₈))) is Element of the carrier of K
p . (((c₇ + c₈) - 1) mod (len (M + p))) is set
the addF of K . ((i * (c₇,c₈)),(p . (((c₇ + c₈) - 1) mod (len (M + p))))) is set
M . (((c₇ + c₈) - 1) mod (len (M + p))) is set
the addF of K . ((M . (((c₇ + c₈) - 1) mod (len (M + p)))),(p . (((c₇ + c₈) - 1) mod (len (M + p))))) is set
(M + p) . (len (M + p)) is set
c₇ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
c₈ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[c₇,c₈] is set
c₇ + c₈ is V11() V12() integer ext-real set
(i + j) * (c₇,c₈) is Element of the carrier of K
1 + 1 is non empty V11() V12() integer ext-real positive non negative set
(1 + 1) - 1 is V11() V12() integer ext-real set
((len (M + p)) + 1) - 1 is V11() V12() integer ext-real set
i * (c₇,c₈) is Element of the carrier of K
j * (c₇,c₈) is Element of the carrier of K
(i * (c₇,c₈)) + (j * (c₇,c₈)) is Element of the carrier of K
the addF of K . ((i * (c₇,c₈)),(j * (c₇,c₈))) is Element of the carrier of K
p . (len (M + p)) is set
the addF of K . ((i * (c₇,c₈)),(p . (len (M + p)))) is set
M . (len (M + p)) is set
the addF of K . ((M . (len (M + p))),(p . (len (M + p)))) is set
n is set
n * is functional FinSequence-membered FinSequenceSet of n
n is non empty set
n is non empty set
K is Relation-like NAT -defined n -valued Function-like FinSequence-like FinSequence of n
n * is functional FinSequence-membered FinSequenceSet of n
len K is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
M is Relation-like NAT -defined n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of len K, len K,n
p is Relation-like NAT -defined n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of len K, len K,n
Indices M is set
dom M is Element of bool NAT
width M is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width M) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width M ) } is set
[:(dom M),(Seg (width M)):] is set
Indices p is set
dom p is Element of bool NAT
width p is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width p) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width p ) } is set
[:(dom p),(Seg (width p)):] is set
i is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[i,j] is set
M * (i,j) is Element of n
p * (i,j) is Element of n
i + j is V11() V12() integer ext-real set
(len K) + 1 is V11() V12() integer ext-real set
(i + j) - 1 is V11() V12() integer ext-real set
((i + j) - 1) mod (len K) is V11() V12() integer ext-real set
K . (((i + j) - 1) mod (len K)) is set
i + j is V11() V12() integer ext-real set
(len K) + 1 is V11() V12() integer ext-real set
K . (len K) is set
i + j is V11() V12() integer ext-real set
(len K) + 1 is V11() V12() integer ext-real set
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
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() V30() V35() integer ext-real set
M is Element of the carrier of K
(n,n) --> M is Relation-like NAT -defined the carrier of K * -valued the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular (K,n) (K,n) Matrix of n,n, the carrier of K
n |-> M 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
n -tuples_on the carrier of K is non empty functional FinSequence-membered FinSequenceSet of the carrier of K
{ b₁ where b₁ is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like Element of the carrier of K * : len b₁ = n } is set
Seg n is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
(Seg n) --> M is Relation-like Seg n -defined Seg n -defined the carrier of K -valued {M} -valued Function-like constant total total V27( Seg n,{M}) FinSequence-like Element of bool [:(Seg n),{M}:]
{M} is non empty trivial V37(1) set
[:(Seg n),{M}:] is set
bool [:(Seg n),{M}:] is set
width ((n,n) --> M) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
len (n |-> M) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
i 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
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
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() V30() V35() integer ext-real set
0. K is V49(K) Element of the carrier of K
(n,n) --> (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 (K,n) (K,n) ( the carrier of K) Matrix of n,n, the carrier of K
n is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
K is non empty set
K * is functional FinSequence-membered FinSequenceSet of K
M is Relation-like NAT -defined K * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of n,n,K
M @ is Relation-like NAT -defined K * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of n,n,K
p is Relation-like NAT -defined K -valued Function-like FinSequence-like FinSequence of K
len p is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
width M is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
len M is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
width (M @) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Indices (M @) is set
dom (M @) is Element of bool NAT
Seg (width (M @)) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width (M @) ) } is set
[:(dom (M @)),(Seg (width (M @))):] is set
(len p) + 1 is V11() V12() integer ext-real set
i is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[i,j] is set
i + j is V11() V12() integer ext-real set
(M @) * (i,j) is Element of K
(i + j) - 1 is V11() V12() integer ext-real set
((i + j) - 1) mod (len p) is V11() V12() integer ext-real set
p . (((i + j) - 1) mod (len p)) is set
Indices M is set
dom M is Element of bool NAT
Seg (width M) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width M ) } is set
[:(dom M),(Seg (width M)):] is set
Seg n is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
[:(Seg n),(Seg n):] is set
[j,i] is set
M * (j,i) is Element of K
p . (len p) is set
i is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[i,j] is set
i + j is V11() V12() integer ext-real set
(M @) * (i,j) is Element of K
Indices M is set
dom M is Element of bool NAT
Seg (width M) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width M ) } is set
[:(dom M),(Seg (width M)):] is set
Seg n is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
[:(Seg n),(Seg n):] is set
[j,i] is set
M * (j,i) is Element of K
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
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() V30() V35() integer ext-real set
p is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular ( the carrier of K) Matrix of n,n, the carrier of K
M is Element of the carrier of K
M * 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
width p is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
i is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
len i is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
width (M * p) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
M * i is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
M 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 [;] (M,(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,i,(M multfield)) is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
len (M * i) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
j 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
c₇ is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
len c₇ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
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() V30() V35() integer ext-real set
M is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular ( the carrier of K) Matrix of n,n, the carrier of K
p is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular ( the carrier of K) Matrix of n,n, the carrier of K
M + 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
i 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
width M is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
j is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
len j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
dom j is set
Seg n is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
width p is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
c₇ is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
len c₇ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
dom c₇ is set
j + c₇ is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence 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 carrier of K, the carrier of K:] is set
[:[: 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
K188( the carrier of K, the carrier of K, the carrier of K, the addF of K,j,c₇) is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
dom (j + c₇) is set
len (j + c₇) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
width (M + p) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
c₈ is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
len c₈ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
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() V30() V35() integer ext-real set
M is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular ( the carrier of K) Matrix of n,n, the carrier of K
- M 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
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
width M is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
i is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
len i is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
(len i) -tuples_on the carrier of K is non empty functional FinSequence-membered FinSequenceSet of the carrier of K
{ b₁ where b₁ is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like Element of the carrier of K * : len b₁ = len i } is set
- i 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:]
[: the carrier of K, the carrier of K:] is set
bool [: the carrier of K, the carrier of K:] is set
K191( the carrier of K, the carrier of K,i,(comp K)) is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
width (- M) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
len (- i) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
j is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
len j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
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() V30() V35() integer ext-real set
M is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular ( the carrier of K) Matrix of n,n, the carrier of K
p is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular ( the carrier of K) Matrix of n,n, the carrier of K
M - 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
- p is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular FinSequence of the carrier of K *
M + (- p) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular FinSequence of the carrier of K *
- p is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular ( the carrier of K) Matrix of n,n, the carrier of K
M + (- p) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular ( the carrier of K) Matrix of n,n, the carrier of K
i 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 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
K is non empty set
K * is functional FinSequence-membered FinSequenceSet of K
M is Relation-like NAT -defined K * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of n,n,K
M @ is Relation-like NAT -defined K * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of n,n,K
width M is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
p is Relation-like NAT -defined K -valued Function-like FinSequence-like FinSequence of K
len p is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
len M is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
width (M @) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
i is Relation-like NAT -defined K -valued Function-like FinSequence-like FinSequence of K
len i is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
n is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
the carrier of n is non empty non trivial set
K is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n
- K is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n
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,K,(comp n)) is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n
len K is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
the carrier of n * is functional FinSequence-membered FinSequenceSet of the carrier of n
p is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of len K, len K, the carrier of n
(len K) -tuples_on the carrier of n is non empty functional FinSequence-membered FinSequenceSet of the carrier of n
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like Element of the carrier of n * : len b₁ = len K } is set
len (- K) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
- p is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of len K, len K, the carrier of n
i is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of len (- K), len (- K), the carrier of n
n is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
the carrier of n is non empty non trivial set
K is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n
- K is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n
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,K,(comp n)) is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n
( the carrier of n,(- K)) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of len (- K), len (- K), the carrier of n
the carrier of n * is functional FinSequence-membered FinSequenceSet of the carrier of n
len (- K) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
len K is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
( the carrier of n,K) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of len K, len K, the carrier of n
- ( the carrier of n,K) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of len K, len K, the carrier of n
len ( the carrier of n,K) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
width ( the carrier of n,K) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Indices ( the carrier of n,K) is set
dom ( the carrier of n,K) is Element of bool NAT
Seg (width ( the carrier of n,K)) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width ( the carrier of n,K) ) } is set
[:(dom ( the carrier of n,K)),(Seg (width ( the carrier of n,K))):] is set
Seg (len K) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= len K ) } is set
[:(Seg (len K)),(Seg (len K)):] is set
(len K) -tuples_on the carrier of n is non empty functional FinSequence-membered FinSequenceSet of the carrier of n
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like Element of the carrier of n * : len b₁ = len K } is set
p is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
i is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[p,i] is set
( the carrier of n,(- K)) * (p,i) is Element of the carrier of n
( the carrier of n,K) * (p,i) is Element of the carrier of n
- (( the carrier of n,K) * (p,i)) is Element of the carrier of n
p + i is V11() V12() integer ext-real set
(len K) + 1 is V11() V12() integer ext-real set
(p + i) - 1 is V11() V12() integer ext-real set
((p + i) - 1) mod (len K) is V11() V12() integer ext-real set
dom K is set
Indices ( the carrier of n,(- K)) is set
dom ( the carrier of n,(- K)) is Element of bool NAT
width ( the carrier of n,(- K)) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width ( the carrier of n,(- K))) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width ( the carrier of n,(- K)) ) } is set
[:(dom ( the carrier of n,(- K))),(Seg (width ( the carrier of n,(- K)))):] is set
((p + i) - 1) mod (len (- K)) is V11() V12() integer ext-real set
(- K) . (((p + i) - 1) mod (len (- K))) is set
K . (((p + i) - 1) mod (len K)) is set
(comp n) . (K . (((p + i) - 1) mod (len K))) is set
(comp n) . (( the carrier of n,K) * (p,i)) is set
p + i is V11() V12() integer ext-real set
(len K) + 1 is V11() V12() integer ext-real set
1 + 1 is non empty V11() V12() integer ext-real positive non negative set
(1 + 1) - 1 is V11() V12() integer ext-real set
((len K) + 1) - 1 is V11() V12() integer ext-real set
dom K is set
Indices ( the carrier of n,(- K)) is set
dom ( the carrier of n,(- K)) is Element of bool NAT
width ( the carrier of n,(- K)) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width ( the carrier of n,(- K))) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width ( the carrier of n,(- K)) ) } is set
[:(dom ( the carrier of n,(- K))),(Seg (width ( the carrier of n,(- K)))):] is set
(- K) . (len (- K)) is set
K . (len K) is set
(comp n) . (K . (len K)) is set
(comp n) . (( the carrier of n,K) * (p,i)) is set
p + i is V11() V12() integer ext-real set
(len K) + 1 is V11() V12() integer ext-real set
len ( the carrier of n,(- K)) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
width ( the carrier of n,(- K)) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
n is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
the carrier of n is non empty non trivial set
K is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n
len K is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
M is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n
len M is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
K + M is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n
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,K,M) is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n
the carrier of n * is functional FinSequence-membered FinSequenceSet of the carrier of n
i is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of len K, len K, the carrier of n
dom K is set
Seg (len K) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= len K ) } is set
dom M is set
dom (K + M) is set
len (K + M) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
j is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of len K, len K, the carrier of n
j + i is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of len K, len K, the carrier of n
width (j + i) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
c₇ is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of len (K + M), len (K + M), the carrier of n
width c₇ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
n is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
the carrier of n is non empty non trivial set
K is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n
len K is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
( the carrier of n,K) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of len K, len K, the carrier of n
the carrier of n * is functional FinSequence-membered FinSequenceSet of the carrier of n
M is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n
len M is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
K + M is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n
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,K,M) is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n
( the carrier of n,(K + M)) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of len (K + M), len (K + M), the carrier of n
len (K + M) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
( the carrier of n,M) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of len M, len M, the carrier of n
( the carrier of n,K) + ( the carrier of n,M) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular FinSequence of the carrier of n *
Indices ( the carrier of n,K) is set
dom ( the carrier of n,K) is Element of bool NAT
width ( the carrier of n,K) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width ( the carrier of n,K)) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width ( the carrier of n,K) ) } is set
[:(dom ( the carrier of n,K)),(Seg (width ( the carrier of n,K))):] is set
Indices ( the carrier of n,M) is set
dom ( the carrier of n,M) is Element of bool NAT
width ( the carrier of n,M) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width ( the carrier of n,M)) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width ( the carrier of n,M) ) } is set
[:(dom ( the carrier of n,M)),(Seg (width ( the carrier of n,M))):] is set
dom K is set
Seg (len K) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= len K ) } is set
dom (K + M) is set
Seg (len (K + M)) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= len (K + M) ) } is set
[:(Seg (len K)),(Seg (len K)):] is set
dom M is set
Indices ( the carrier of n,(K + M)) is set
dom ( the carrier of n,(K + M)) is Element of bool NAT
width ( the carrier of n,(K + M)) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width ( the carrier of n,(K + M))) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width ( the carrier of n,(K + M)) ) } is set
[:(dom ( the carrier of n,(K + M))),(Seg (width ( the carrier of n,(K + M)))):] is set
i is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[i,j] is set
( the carrier of n,(K + M)) * (i,j) is Element of the carrier of n
( the carrier of n,K) * (i,j) is Element of the carrier of n
( the carrier of n,M) * (i,j) is Element of the carrier of n
(( the carrier of n,K) * (i,j)) + (( the carrier of n,M) * (i,j)) is Element of the carrier of n
the addF of n . ((( the carrier of n,K) * (i,j)),(( the carrier of n,M) * (i,j))) is Element of the carrier of n
i + j is V11() V12() integer ext-real set
(len (K + M)) + 1 is V11() V12() integer ext-real set
(i + j) - 1 is V11() V12() integer ext-real set
((i + j) - 1) mod (len K) is V11() V12() integer ext-real set
((i + j) - 1) mod (len (K + M)) is V11() V12() integer ext-real set
(K + M) . (((i + j) - 1) mod (len (K + M))) is set
K . (((i + j) - 1) mod (len (K + M))) is set
M . (((i + j) - 1) mod (len (K + M))) is set
the addF of n . ((K . (((i + j) - 1) mod (len (K + M)))),(M . (((i + j) - 1) mod (len (K + M))))) is set
((i + j) - 1) mod (len M) is V11() V12() integer ext-real set
M . (((i + j) - 1) mod (len M)) is set
the addF of n . ((( the carrier of n,K) * (i,j)),(M . (((i + j) - 1) mod (len M)))) is set
i + j is V11() V12() integer ext-real set
(len (K + M)) + 1 is V11() V12() integer ext-real set
1 + 1 is non empty V11() V12() integer ext-real positive non negative set
(1 + 1) - 1 is V11() V12() integer ext-real set
((len (K + M)) + 1) - 1 is V11() V12() integer ext-real set
(K + M) . (len (K + M)) is set
K . (len (K + M)) is set
M . (len (K + M)) is set
the addF of n . ((K . (len (K + M))),(M . (len (K + M)))) is set
M . (len M) is set
the addF of n . ((( the carrier of n,K) * (i,j)),(M . (len M))) is set
i + j is V11() V12() integer ext-real set
(len (K + M)) + 1 is V11() V12() integer ext-real set
len ( the carrier of n,K) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
len ( the carrier of n,(K + M)) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
n is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
the carrier of n is non empty non trivial set
K is Element of the carrier of n
M is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n
K * M is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n
K 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 [;] (K,(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,M,(K multfield)) is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n
len M is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
len (K * M) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
the carrier of n * is functional FinSequence-membered FinSequenceSet of the carrier of n
i is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of len M, len M, the carrier of n
K * i is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of len M, len M, the carrier of n
j is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of len (K * M), len (K * M), the carrier of n
n is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
the carrier of n is non empty non trivial set
K is Element of the carrier of n
M is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n
K * M is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n
K 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 [;] (K,(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,M,(K multfield)) is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n
( the carrier of n,(K * M)) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of len (K * M), len (K * M), the carrier of n
the carrier of n * is functional FinSequence-membered FinSequenceSet of the carrier of n
len (K * M) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
len M is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
( the carrier of n,M) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of len M, len M, the carrier of n
K * ( the carrier of n,M) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of len M, len M, the carrier of n
Indices ( the carrier of n,M) is set
dom ( the carrier of n,M) is Element of bool NAT
width ( the carrier of n,M) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width ( the carrier of n,M)) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width ( the carrier of n,M) ) } is set
[:(dom ( the carrier of n,M)),(Seg (width ( the carrier of n,M))):] is set
Seg (len M) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= len M ) } is set
[:(Seg (len M)),(Seg (len M)):] is set
i is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[i,j] is set
( the carrier of n,(K * M)) * (i,j) is Element of the carrier of n
( the carrier of n,M) * (i,j) is Element of the carrier of n
K * (( the carrier of n,M) * (i,j)) is Element of the carrier of n
the multF of n . (K,(( the carrier of n,M) * (i,j))) is Element of the carrier of n
dom (K * M) is set
Seg (len (K * M)) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= len (K * M) ) } is set
i + j is V11() V12() integer ext-real set
(len M) + 1 is V11() V12() integer ext-real set
(i + j) - 1 is V11() V12() integer ext-real set
((i + j) - 1) mod (len M) is V11() V12() integer ext-real set
dom M is set
Indices ( the carrier of n,(K * M)) is set
dom ( the carrier of n,(K * M)) is Element of bool NAT
width ( the carrier of n,(K * M)) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width ( the carrier of n,(K * M))) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width ( the carrier of n,(K * M)) ) } is set
[:(dom ( the carrier of n,(K * M))),(Seg (width ( the carrier of n,(K * M)))):] is set
((i + j) - 1) mod (len (K * M)) is V11() V12() integer ext-real set
(K * M) . (((i + j) - 1) mod (len (K * M))) is set
(K * M) /. (((i + j) - 1) mod (len M)) is Element of the carrier of n
M /. (((i + j) - 1) mod (len M)) is Element of the carrier of n
K * (M /. (((i + j) - 1) mod (len M))) is Element of the carrier of n
the multF of n . (K,(M /. (((i + j) - 1) mod (len M)))) is Element of the carrier of n
(K multfield) . (M /. (((i + j) - 1) mod (len M))) is set
M . (((i + j) - 1) mod (len M)) is set
(K multfield) . (M . (((i + j) - 1) mod (len M))) is set
(K multfield) . (( the carrier of n,M) * (i,j)) is set
i + j is V11() V12() integer ext-real set
(len M) + 1 is V11() V12() integer ext-real set
Indices ( the carrier of n,(K * M)) is set
dom ( the carrier of n,(K * M)) is Element of bool NAT
width ( the carrier of n,(K * M)) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width ( the carrier of n,(K * M))) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width ( the carrier of n,(K * M)) ) } is set
[:(dom ( the carrier of n,(K * M))),(Seg (width ( the carrier of n,(K * M)))):] is set
1 + 1 is non empty V11() V12() integer ext-real positive non negative set
(1 + 1) - 1 is V11() V12() integer ext-real set
((len M) + 1) - 1 is V11() V12() integer ext-real set
dom M is set
(K * M) . (len (K * M)) is set
(K * M) /. (len M) is Element of the carrier of n
M /. (len M) is Element of the carrier of n
K * (M /. (len M)) is Element of the carrier of n
the multF of n . (K,(M /. (len M))) is Element of the carrier of n
(K multfield) . (M /. (len M)) is set
M . (len M) is set
(K multfield) . (M . (len M)) is set
(K multfield) . (( the carrier of n,M) * (i,j)) is set
i + j is V11() V12() integer ext-real set
(len M) + 1 is V11() V12() integer ext-real set
len ( the carrier of n,M) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
len ( the carrier of n,(K * M)) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
width ( the carrier of n,(K * M)) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
n is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
the carrier of n is non empty non trivial set
K is Element of the carrier of n
M is Element of the carrier of n
K + M is Element of the carrier of n
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
the addF of n . (K,M) is Element of 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
len p is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
( the carrier of n,p) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of len p, len p, the carrier of n
the carrier of n * is functional FinSequence-membered FinSequenceSet of the carrier of n
K * ( the carrier of n,p) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of len p, len p, the carrier of n
M * ( the carrier of n,p) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of len p, len p, the carrier of n
(K * ( the carrier of n,p)) + (M * ( the carrier of n,p)) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of len p, len p, the carrier of n
(K + M) * p is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n
(K + M) 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:]
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:]
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 [;] ((K + M),(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,((K + M) multfield)) is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n
( the carrier of n,((K + M) * p)) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of len ((K + M) * p), len ((K + M) * p), the carrier of n
len ((K + M) * p) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
M * p is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n
M 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 multF of n [;] (M,(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,(M multfield)) is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n
len (M * p) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
(len p) -tuples_on the carrier of n is non empty functional FinSequence-membered FinSequenceSet of the carrier of n
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like Element of the carrier of n * : len b₁ = len p } is set
K * p is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n
K 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 multF of n [;] (K,(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,(K multfield)) is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n
( the carrier of n,(K * p)) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of len (K * p), len (K * p), the carrier of n
len (K * p) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
( the carrier of n,(M * p)) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of len (M * p), len (M * p), the carrier of n
(K * p) + (M * p) is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n
K188( the carrier of n, the carrier of n, the carrier of n, the addF of n,(K * p),(M * p)) is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n
( the carrier of n,((K * p) + (M * p))) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of len ((K * p) + (M * p)), len ((K * p) + (M * p)), the carrier of n
len ((K * p) + (M * p)) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
n is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
the carrier of n is non empty non trivial set
K is Element of the carrier of n
M is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n
len M is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
( the carrier of n,M) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of len M, len M, the carrier of n
the carrier of n * is functional FinSequence-membered FinSequenceSet of the carrier of n
K * ( the carrier of n,M) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of len M, len M, 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
len p is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
( the carrier of n,p) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of len p, len p, the carrier of n
K * ( the carrier of n,p) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of len p, len p, the carrier of n
(K * ( the carrier of n,M)) + (K * ( the carrier of n,p)) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular FinSequence of the carrier of n *
M + p is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n
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,M,p) is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n
K * (M + p) is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n
K 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:]
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:]
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 [;] (K,(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,(M + p),(K multfield)) is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n
( the carrier of n,(K * (M + p))) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of len (K * (M + p)), len (K * (M + p)), the carrier of n
len (K * (M + p)) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
len ( the carrier of n,M) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
width ( the carrier of n,M) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
len ( the carrier of n,p) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
width ( the carrier of n,p) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
( the carrier of n,M) + ( the carrier of n,p) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular FinSequence of the carrier of n *
K * (( the carrier of n,M) + ( the carrier of n,p)) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular FinSequence of the carrier of n *
len (M + p) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
( the carrier of n,(M + p)) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of len (M + p), len (M + p), the carrier of n
K * ( the carrier of n,(M + p)) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of len (M + p), len (M + p), the carrier of n
n is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
the carrier of n is non empty non trivial set
K is Element of the carrier of n
M is Element of 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
len p is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
( the carrier of n,p) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of len p, len p, the carrier of n
the carrier of n * is functional FinSequence-membered FinSequenceSet of the carrier of n
K * ( the carrier of n,p) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of len p, len p, the carrier of n
K * p is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n
K 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 [;] (K,(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,(K multfield)) is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n
i is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n
len i is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
( the carrier of n,i) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of len i, len i, the carrier of n
M * ( the carrier of n,i) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of len i, len i, the carrier of n
(K * ( the carrier of n,p)) + (M * ( the carrier of n,i)) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular FinSequence of the carrier of n *
M * i is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n
M 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 multF of n [;] (M,(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,i,(M multfield)) is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n
(K * p) + (M * i) is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n
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:]
K188( the carrier of n, the carrier of n, the carrier of n, the addF of n,(K * p),(M * i)) is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n
( the carrier of n,((K * p) + (M * i))) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of len ((K * p) + (M * i)), len ((K * p) + (M * i)), the carrier of n
len ((K * p) + (M * i)) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
len (M * i) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
( the carrier of n,(K * p)) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of len (K * p), len (K * p), the carrier of n
len (K * p) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
( the carrier of n,(K * p)) + (M * ( the carrier of n,i)) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular FinSequence of the carrier of n *
( the carrier of n,(M * i)) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of len (M * i), len (M * i), the carrier of n
( the carrier of n,(K * p)) + ( the carrier of n,(M * i)) is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular FinSequence of the carrier of n *
n is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
the carrier of K is non empty non trivial set
the carrier of K * is functional FinSequence-membered FinSequenceSet of the carrier of K
M 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
M @ 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
width M is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
p is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
len p is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Indices M is set
dom M is Element of bool NAT
Seg (width M) is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= width M ) } is set
[:(dom M),(Seg (width M)):] is set
Seg n is Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
[:(Seg n),(Seg n):] is set
len M is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
len (M @) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
width (M @) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
i is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[i,j] is set
(M @) * (i,j) is Element of the carrier of K
M * (i,j) is Element of the carrier of K
i + j is V11() V12() integer ext-real set
(len p) + 1 is V11() V12() integer ext-real set
[j,i] is set
M * (j,i) is Element of the carrier of K
(i + j) - 1 is V11() V12() integer ext-real set
((i + j) - 1) mod (len p) is V11() V12() integer ext-real set
p . (((i + j) - 1) mod (len p)) is set
i + j is V11() V12() integer ext-real set
(len p) + 1 is V11() V12() integer ext-real set
[j,i] is set
M * (j,i) is Element of the carrier of K
p . (len p) is set
i + j is V11() V12() integer ext-real set
(len p) + 1 is V11() V12() integer ext-real set
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr
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() V30() V35() integer ext-real set
M 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
M @ 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