:: 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

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

[:(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

[:(dom p),(Seg (width p)):] is set

c

n + 1 is V11() V12() integer ext-real set

(n + 1) - j is V11() V12() integer ext-real set

c

(n + 1) - i is V11() V12() integer ext-real set

p * (i,j) is Element of the carrier of K

p * (c

Seg n is Element of bool NAT

{ b

[:(Seg n),(Seg n):] is set

[c

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

[:(dom M),(Seg (width M)):] is set

Seg n is Element of bool NAT

{ b

[:(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

[:(dom p),(Seg (width p)):] is set

c

n + 1 is V11() V12() integer ext-real set

(n + 1) - j is V11() V12() integer ext-real set

c

(n + 1) - i is V11() V12() integer ext-real set

p * (i,j) is Element of the carrier of K

p * (c

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

[:(dom (- M)),(Seg (width (- M))):] is set

[c

(- 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

- (M * (c

(- M) * (c

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

[j,c

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

[:(dom i),(Seg (width i)):] is set

c

n + 1 is V11() V12() integer ext-real set

(n + 1) - c

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

i * (c

Seg n is Element of bool NAT

{ b

[:(Seg n),(Seg n):] is set

[c

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

[:(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

[:(dom p),(Seg (width p)):] is set

(M + p) * (j,c

M * (j,c

p * (j,c

(M * (j,c

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

M * (c

(M * (c

the addF of K . ((M * (c

p * (c

(M * (c

the addF of K . ((M * (c

(M + p) * (c

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

[:(dom p),(Seg (width p)):] is set

Seg n is Element of bool NAT

{ b

[:(Seg n),(Seg n):] is set

j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set

c

[j,c

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

[:(dom i),(Seg (width i)):] is set

c

n + 1 is V11() V12() integer ext-real set

(n + 1) - c

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

i * (c

[c

(M * p) * (j,c

p * (j,c

M * (p * (j,c

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

p * (c

M * (p * (c

the multF of K . (M,(p * (c

(M * p) * (c

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

[:(dom M),(Seg (width M)):] is set

Seg n is Element of bool NAT

{ b

[:(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

[:(dom p),(Seg (width p)):] is set

c

n + 1 is V11() V12() integer ext-real set

(n + 1) - j is V11() V12() integer ext-real set

c

(n + 1) - i is V11() V12() integer ext-real set

p * (i,j) is Element of the carrier of K

p * (c

[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

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

[:(dom M),(Seg (width M)):] is set

Seg n is Element of bool NAT

{ b

[:(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

n + 1 is V11() V12() integer ext-real set

(n + 1) - j is V11() V12() integer ext-real set

c

(n + 1) - i is V11() V12() integer ext-real set

M * (i,j) is Element of the carrier of K

M * (c

[c

((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

[:(dom M),(Seg (width M)):] is set

Seg n is Element of bool NAT

{ b

[:(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

n + 1 is V11() V12() integer ext-real set

(n + 1) - j is V11() V12() integer ext-real set

c

(n + 1) - i is V11() V12() integer ext-real set

M * (i,j) is Element of the carrier of K

M * (c

[c

((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

[:(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

(n + 1) - p is V11() V12() integer ext-real set

M * (p,i) is Element of the carrier of K

M * (j,c

- (M * (j,c

Seg n is Element of bool NAT

{ b

[:(Seg n),(Seg n):] is set

[j,c

- (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

Indices c

dom c

width c

Seg (width c

{ b

[:(dom c

c

- (c

(c

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

1_ n is Element of the carrier of n

K142(n) is V49(n) Element of the carrier of n

(1_ n) * (c

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

((1_ n) * (c

the addF of n . (((1_ n) * (c

((1_ n) * (c

the addF of n . (((1_ n) * (c

(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

the multF of n . (((1_ n) + (1_ n)),(c

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

[:(dom M),(Seg (width M)):] is set

Seg n is Element of bool NAT

{ b

[:(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

[:(dom p),(Seg (width p)):] is set

c

n + 1 is V11() V12() integer ext-real set

(n + 1) - j is V11() V12() integer ext-real set

c

(n + 1) - i is V11() V12() integer ext-real set

p * (i,j) is Element of the carrier of K

p * (c

- (p * (c

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

[:(dom (- M)),(Seg (width (- M))):] is set

[c

(- 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

- (M * (c

- (- (M * (c

(- M) * (c

- ((- M) * (c

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

[j,c

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

[:(dom i),(Seg (width i)):] is set

c

n + 1 is V11() V12() integer ext-real set

(n + 1) - c

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

i * (c

- (i * (c

Seg n is Element of bool NAT

{ b

[:(Seg n),(Seg n):] is set

[c

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

[:(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

[:(dom p),(Seg (width p)):] is set

(M + p) * (j,c

M * (j,c

p * (j,c

(M * (j,c

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

M * (c

- (M * (c

(- (M * (c

the addF of K . ((- (M * (c

p * (c

- (p * (c

(- (M * (c

the addF of K . ((- (M * (c

(M * (c

the addF of K . ((M * (c

- ((M * (c

(M + p) * (c

- ((M + p) * (c

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

[:(dom p),(Seg (width p)):] is set

Seg n is Element of bool NAT

{ b

[:(Seg n),(Seg n):] is set

j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set

c

[j,c

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

[:(dom i),(Seg (width i)):] is set

c

n + 1 is V11() V12() integer ext-real set

(n + 1) - c

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

i * (c

- (i * (c

[c

(M * p) * (j,c

p * (j,c

M * (p * (j,c

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

p * (c

- (p * (c

M * (- (p * (c

the multF of K . (M,(- (p * (c

M * (p * (c

the multF of K . (M,(p * (c

- (M * (p * (c

(M * p) * (c

- ((M * p) * (c

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

[:(dom M),(Seg (width M)):] is set

Seg n is Element of bool NAT

{ b

[:(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

[:(dom p),(Seg (width p)):] is set

c

n + 1 is V11() V12() integer ext-real set

(n + 1) - j is V11() V12() integer ext-real set

c

(n + 1) - i is V11() V12() integer ext-real set

p * (i,j) is Element of the carrier of K

p * (c

- (p * (c

[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

- (M * (c

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

[:(dom p),(Seg (width p)):] is set

c

n + 1 is V11() V12() integer ext-real set

(n + 1) - i is V11() V12() integer ext-real set

c

(n + 1) - j is V11() V12() integer ext-real set

p * (i,j) is Element of the carrier of K

p * (c

Seg n is Element of bool NAT

{ b

[:(Seg n),(Seg n):] is set

[c

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

[:(dom M),(Seg (width M)):] is set

Seg n is Element of bool NAT

{ b

[:(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

[:(dom p),(Seg (width p)):] is set

c

n + 1 is V11() V12() integer ext-real set

(n + 1) - i is V11() V12() integer ext-real set

c

(n + 1) - j is V11() V12() integer ext-real set

p * (i,j) is Element of the carrier of K

p * (c

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

[:(dom (- M)),(Seg (width (- M))):] is set

[c

(- 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

- (M * (c

(- M) * (c

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

[j,c

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

[:(dom i),(Seg (width i)):] is set

c

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

i * (j,c

i * (c

Seg n is Element of bool NAT

{ b

[:(Seg n),(Seg n):] is set

[c

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

[:(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

[:(dom p),(Seg (width p)):] is set

(M + p) * (j,c

M * (j,c

p * (j,c

(M * (j,c

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

M * (c

(M * (c

the addF of K . ((M * (c

p * (c

(M * (c

the addF of K . ((M * (c

(M + p) * (c

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

[:(dom p),(Seg (width p)):] is set

Seg n is Element of bool NAT

{ b

[:(Seg n),(Seg n):] is set

j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set

c

[j,c

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

[:(dom i),(Seg (width i)):] is set

c

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

i * (j,c

i * (c

[c

(M * p) * (j,c

p * (j,c

M * (p * (j,c

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

p * (c

M * (p * (c

the multF of K . (M,(p * (c

(M * p) * (c

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

[:(dom M),(Seg (width M)):] is set

Seg n is Element of bool NAT

{ b

[:(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

[:(dom p),(Seg (width p)):] is set

c

n + 1 is V11() V12() integer ext-real set

(n + 1) - i is V11() V12() integer ext-real set

c

(n + 1) - j is V11() V12() integer ext-real set

p * (i,j) is Element of the carrier of K

p * (c

[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

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