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
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width p ) } is set
[:(dom p),(Seg (width p)):] is set
c7 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
c8 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 * (c7,c8) is Element of the carrier of K
Seg n is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
[:(Seg n),(Seg n):] is set
[c7,c8] 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
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width M ) } is set
[:(dom M),(Seg (width M)):] is set
Seg n is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width p ) } is set
[:(dom p),(Seg (width p)):] is set
c7 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
c8 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 * (c7,c8) 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
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width (- M) ) } is set
[:(dom (- M)),(Seg (width (- M))):] is set
[c7,c8] 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 * (c7,c8) is Element of the carrier of K
- (M * (c7,c8)) is Element of the carrier of K
(- M) * (c7,c8) 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
c7 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[j,c7] 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
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width i ) } is set
[:(dom i),(Seg (width i)):] is set
c8 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
n + 1 is V11() V12() integer ext-real set
(n + 1) - c7 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,c7) is Element of the carrier of K
i * (c8,l) is Element of the carrier of K
Seg n is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
[:(Seg n),(Seg n):] is set
[c8,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
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width p ) } is set
[:(dom p),(Seg (width p)):] is set
(M + p) * (j,c7) is Element of the carrier of K
M * (j,c7) is Element of the carrier of K
p * (j,c7) is Element of the carrier of K
(M * (j,c7)) + (p * (j,c7)) 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,c7)),(p * (j,c7))) is Element of the carrier of K
M * (c8,l) is Element of the carrier of K
(M * (c8,l)) + (p * (j,c7)) is Element of the carrier of K
the addF of K . ((M * (c8,l)),(p * (j,c7))) is Element of the carrier of K
p * (c8,l) is Element of the carrier of K
(M * (c8,l)) + (p * (c8,l)) is Element of the carrier of K
the addF of K . ((M * (c8,l)),(p * (c8,l))) is Element of the carrier of K
(M + p) * (c8,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
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width p ) } is set
[:(dom p),(Seg (width p)):] is set
Seg n is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
[:(Seg n),(Seg n):] is set
j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
c7 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[j,c7] 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
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width i ) } is set
[:(dom i),(Seg (width i)):] is set
c8 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
n + 1 is V11() V12() integer ext-real set
(n + 1) - c7 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,c7) is Element of the carrier of K
i * (c8,l) is Element of the carrier of K
[c8,l] is set
(M * p) * (j,c7) is Element of the carrier of K
p * (j,c7) is Element of the carrier of K
M * (p * (j,c7)) 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,c7))) is Element of the carrier of K
p * (c8,l) is Element of the carrier of K
M * (p * (c8,l)) is Element of the carrier of K
the multF of K . (M,(p * (c8,l))) is Element of the carrier of K
(M * p) * (c8,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
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width M ) } is set
[:(dom M),(Seg (width M)):] is set
Seg n is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width p ) } is set
[:(dom p),(Seg (width p)):] is set
c7 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
c8 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 * (c7,c8) 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 * (c8,c7) 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
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width M ) } is set
[:(dom M),(Seg (width M)):] is set
Seg n is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= 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
c7 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
c8 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 * (c7,c8) is Element of the carrier of K
[c7,c8] 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
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width M ) } is set
[:(dom M),(Seg (width M)):] is set
Seg n is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= 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
c7 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
c8 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 * (c7,c8) is Element of the carrier of K
[c7,c8] 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
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= 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
c7 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,c7) is Element of the carrier of K
- (M * (j,c7)) is Element of the carrier of K
Seg n is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
[:(Seg n),(Seg n):] is set
[j,c7] 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
c7 is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of K,K, the carrier of n
Indices c7 is set
dom c7 is Element of bool NAT
width c7 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width c7) is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width c7 ) } is set
[:(dom c7),(Seg (width c7)):] is set
c7 * (M,p) is Element of the carrier of n
- (c7 * (M,p)) is Element of the carrier of n
(c7 * (M,p)) + (c7 * (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 . ((c7 * (M,p)),(c7 * (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) * (c7 * (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),(c7 * (M,p))) is Element of the carrier of n
((1_ n) * (c7 * (M,p))) + (c7 * (M,p)) is Element of the carrier of n
the addF of n . (((1_ n) * (c7 * (M,p))),(c7 * (M,p))) is Element of the carrier of n
((1_ n) * (c7 * (M,p))) + ((1_ n) * (c7 * (M,p))) is Element of the carrier of n
the addF of n . (((1_ n) * (c7 * (M,p))),((1_ n) * (c7 * (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)) * (c7 * (M,p)) is Element of the carrier of n
the multF of n . (((1_ n) + (1_ n)),(c7 * (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
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width M ) } is set
[:(dom M),(Seg (width M)):] is set
Seg n is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width p ) } is set
[:(dom p),(Seg (width p)):] is set
c7 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
c8 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 * (c7,c8) is Element of the carrier of K
- (p * (c7,c8)) 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
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width (- M) ) } is set
[:(dom (- M)),(Seg (width (- M))):] is set
[c7,c8] 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 * (c7,c8) is Element of the carrier of K
- (M * (c7,c8)) is Element of the carrier of K
- (- (M * (c7,c8))) is Element of the carrier of K
(- M) * (c7,c8) is Element of the carrier of K
- ((- M) * (c7,c8)) 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
c7 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[j,c7] 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
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width i ) } is set
[:(dom i),(Seg (width i)):] is set
c8 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
n + 1 is V11() V12() integer ext-real set
(n + 1) - c7 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,c7) is Element of the carrier of K
i * (c8,l) is Element of the carrier of K
- (i * (c8,l)) is Element of the carrier of K
Seg n is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
[:(Seg n),(Seg n):] is set
[c8,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
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width p ) } is set
[:(dom p),(Seg (width p)):] is set
(M + p) * (j,c7) is Element of the carrier of K
M * (j,c7) is Element of the carrier of K
p * (j,c7) is Element of the carrier of K
(M * (j,c7)) + (p * (j,c7)) 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,c7)),(p * (j,c7))) is Element of the carrier of K
M * (c8,l) is Element of the carrier of K
- (M * (c8,l)) is Element of the carrier of K
(- (M * (c8,l))) + (p * (j,c7)) is Element of the carrier of K
the addF of K . ((- (M * (c8,l))),(p * (j,c7))) is Element of the carrier of K
p * (c8,l) is Element of the carrier of K
- (p * (c8,l)) is Element of the carrier of K
(- (M * (c8,l))) + (- (p * (c8,l))) is Element of the carrier of K
the addF of K . ((- (M * (c8,l))),(- (p * (c8,l)))) is Element of the carrier of K
(M * (c8,l)) + (p * (c8,l)) is Element of the carrier of K
the addF of K . ((M * (c8,l)),(p * (c8,l))) is Element of the carrier of K
- ((M * (c8,l)) + (p * (c8,l))) is Element of the carrier of K
(M + p) * (c8,l) is Element of the carrier of K
- ((M + p) * (c8,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
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width p ) } is set
[:(dom p),(Seg (width p)):] is set
Seg n is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
[:(Seg n),(Seg n):] is set
j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
c7 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[j,c7] 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
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width i ) } is set
[:(dom i),(Seg (width i)):] is set
c8 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
n + 1 is V11() V12() integer ext-real set
(n + 1) - c7 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,c7) is Element of the carrier of K
i * (c8,l) is Element of the carrier of K
- (i * (c8,l)) is Element of the carrier of K
[c8,l] is set
(M * p) * (j,c7) is Element of the carrier of K
p * (j,c7) is Element of the carrier of K
M * (p * (j,c7)) 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,c7))) is Element of the carrier of K
p * (c8,l) is Element of the carrier of K
- (p * (c8,l)) is Element of the carrier of K
M * (- (p * (c8,l))) is Element of the carrier of K
the multF of K . (M,(- (p * (c8,l)))) is Element of the carrier of K
M * (p * (c8,l)) is Element of the carrier of K
the multF of K . (M,(p * (c8,l))) is Element of the carrier of K
- (M * (p * (c8,l))) is Element of the carrier of K
(M * p) * (c8,l) is Element of the carrier of K
- ((M * p) * (c8,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
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width M ) } is set
[:(dom M),(Seg (width M)):] is set
Seg n is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width p ) } is set
[:(dom p),(Seg (width p)):] is set
c7 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
c8 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 * (c7,c8) is Element of the carrier of K
- (p * (c7,c8)) 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 * (c8,c7) is Element of the carrier of K
- (M * (c8,c7)) 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
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width p ) } is set
[:(dom p),(Seg (width p)):] is set
c7 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
c8 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 * (c7,c8) is Element of the carrier of K
Seg n is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
[:(Seg n),(Seg n):] is set
[c7,c8] 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
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width M ) } is set
[:(dom M),(Seg (width M)):] is set
Seg n is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width p ) } is set
[:(dom p),(Seg (width p)):] is set
c7 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
c8 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 * (c7,c8) 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
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width (- M) ) } is set
[:(dom (- M)),(Seg (width (- M))):] is set
[c7,c8] 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 * (c7,c8) is Element of the carrier of K
- (M * (c7,c8)) is Element of the carrier of K
(- M) * (c7,c8) 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
c7 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[j,c7] 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
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width i ) } is set
[:(dom i),(Seg (width i)):] is set
c8 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) - c7 is V11() V12() integer ext-real set
i * (j,c7) is Element of the carrier of K
i * (c8,l) is Element of the carrier of K
Seg n is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
[:(Seg n),(Seg n):] is set
[c8,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
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width p ) } is set
[:(dom p),(Seg (width p)):] is set
(M + p) * (j,c7) is Element of the carrier of K
M * (j,c7) is Element of the carrier of K
p * (j,c7) is Element of the carrier of K
(M * (j,c7)) + (p * (j,c7)) 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,c7)),(p * (j,c7))) is Element of the carrier of K
M * (c8,l) is Element of the carrier of K
(M * (c8,l)) + (p * (j,c7)) is Element of the carrier of K
the addF of K . ((M * (c8,l)),(p * (j,c7))) is Element of the carrier of K
p * (c8,l) is Element of the carrier of K
(M * (c8,l)) + (p * (c8,l)) is Element of the carrier of K
the addF of K . ((M * (c8,l)),(p * (c8,l))) is Element of the carrier of K
(M + p) * (c8,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
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width p ) } is set
[:(dom p),(Seg (width p)):] is set
Seg n is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
[:(Seg n),(Seg n):] is set
j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
c7 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[j,c7] 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
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width i ) } is set
[:(dom i),(Seg (width i)):] is set
c8 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) - c7 is V11() V12() integer ext-real set
i * (j,c7) is Element of the carrier of K
i * (c8,l) is Element of the carrier of K
[c8,l] is set
(M * p) * (j,c7) is Element of the carrier of K
p * (j,c7) is Element of the carrier of K
M * (p * (j,c7)) 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,c7))) is Element of the carrier of K
p * (c8,l) is Element of the carrier of K
M * (p * (c8,l)) is Element of the carrier of K
the multF of K . (M,(p * (c8,l))) is Element of the carrier of K
(M * p) * (c8,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
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width M ) } is set
[:(dom M),(Seg (width M)):] is set
Seg n is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width p ) } is set
[:(dom p),(Seg (width p)):] is set
c7 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
c8 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 * (c7,c8) 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 * (c8,c7) 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