:: MATRIX16 semantic presentation

REAL is set

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

bool REAL is set

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

bool NAT is set

bool NAT is set

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

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

COMPLEX is set

RAT is set

INT is set

{} is empty V4() V5() V6() V8() V9() V10() V11() V12() Function-like functional integer ext-real non positive non negative set

0 is empty V4() V5() V6() V8() V9() V10() V11() V12() Function-like functional integer ext-real non positive non negative Element of NAT

K43(1) is V11() V12() integer ext-real non positive Element of REAL

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

n is V4() V5() V6() V10() V11() V12() integer ext-real set

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

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

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

K - 1 is V11() V12() integer ext-real set

n is V4() V5() V6() V10() V11() V12() integer ext-real set

K is V4() V5() V6() V10() V11() V12() integer ext-real set

Seg K is Element of bool NAT

{ b

p is V4() V5() V6() V10() V11() V12() integer ext-real set

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

(p - n) mod K is V11() V12() integer ext-real set

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

1 - K is V11() V12() integer ext-real set

K - 1 is V11() V12() integer ext-real set

- K is V11() V12() integer ext-real set

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

- 1 is V11() V12() integer ext-real non positive set

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

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

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

0 + 1 is non empty V11() V12() integer ext-real positive non negative set

n is V4() V5() V6() V10() V11() V12() integer ext-real set

p is V4() V5() V6() V10() V11() V12() integer ext-real set

[n,p] is set

K is V4() V5() V6() V10() V11() V12() integer ext-real set

Seg K is Element of bool NAT

{ b

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

[p,n] is set

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

(p - n) mod K is V11() V12() integer ext-real set

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

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

1_ K is Element of the carrier of K

1. K is V49(K) Element of the carrier of K

n is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K

(1_ K) * n is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K

(1_ K) multfield is Relation-like the carrier of K -defined the carrier of K -valued Function-like V27( the carrier of K, the carrier of K) Element of bool [: the carrier of K, the carrier of K:]

[: the carrier of K, the carrier of K:] is set

bool [: the carrier of K, the carrier of K:] is set

the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V27([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]

[:[: the carrier of K, the carrier of K:], the carrier of K:] is set

bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is set

id the carrier of K is non empty Relation-like the carrier of K -defined the carrier of K -valued Function-like one-to-one total Element of bool [: the carrier of K, the carrier of K:]

the multF of K [;] ((1_ K),(id the carrier of K)) is Relation-like the carrier of K -defined the carrier of K -valued Function-like V27( the carrier of K, the carrier of K) Element of bool [: the carrier of K, the carrier of K:]

K191( the carrier of K, the carrier of K,n,((1_ K) multfield)) is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K

dom n is set

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

Seg (len n) is Element of bool NAT

{ b

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

Seg (len ((1_ K) * n)) is Element of bool NAT

{ b

dom ((1_ K) * n) is set

p is V4() V5() V6() V10() V11() V12() integer ext-real set

((1_ K) * n) . p is set

n . p is set

rng n is set

the multF of K [;] ((1_ K),(id the carrier of K)) is Relation-like Function-like set

dom ( the multF of K [;] ((1_ K),(id the carrier of K))) is set

((1_ K) multfield) . (n . p) is set

(id the carrier of K) . (n . p) is set

the multF of K . ((1_ K),((id the carrier of K) . (n . p))) is set

M1 is Element of the carrier of K

(1_ K) * M1 is Element of the carrier of K

the multF of K . ((1_ K),M1) is Element of the carrier of K

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

1_ K is Element of the carrier of K

1. K is V49(K) Element of the carrier of K

- (1_ K) is Element of the carrier of K

n is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K

(- (1_ K)) * n is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K

(- (1_ K)) multfield is Relation-like the carrier of K -defined the carrier of K -valued Function-like V27( the carrier of K, the carrier of K) Element of bool [: the carrier of K, the carrier of K:]

[: the carrier of K, the carrier of K:] is set

bool [: the carrier of K, the carrier of K:] is set

the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V27([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]

[:[: the carrier of K, the carrier of K:], the carrier of K:] is set

bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is set

id the carrier of K is non empty Relation-like the carrier of K -defined the carrier of K -valued Function-like one-to-one total Element of bool [: the carrier of K, the carrier of K:]

the multF of K [;] ((- (1_ K)),(id the carrier of K)) is Relation-like the carrier of K -defined the carrier of K -valued Function-like V27( the carrier of K, the carrier of K) Element of bool [: the carrier of K, the carrier of K:]

K191( the carrier of K, the carrier of K,n,((- (1_ K)) multfield)) is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K

- n is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K

comp K is Relation-like the carrier of K -defined the carrier of K -valued Function-like V27( the carrier of K, the carrier of K) Element of bool [: the carrier of K, the carrier of K:]

K191( the carrier of K, the carrier of K,n,(comp K)) is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K

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

Seg (len ((- (1_ K)) * n)) is Element of bool NAT

{ b

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

Seg (len n) is Element of bool NAT

{ b

dom ((- (1_ K)) * n) is set

dom n is set

p is V4() V5() V6() V10() V11() V12() integer ext-real set

((- (1_ K)) * n) . p is set

(- n) . p is set

rng n is set

n . p is set

the multF of K [;] ((- (1_ K)),(id the carrier of K)) is Relation-like Function-like set

dom ( the multF of K [;] ((- (1_ K)),(id the carrier of K))) is set

M1 is Element of the carrier of K

(- (1_ K)) * M1 is Element of the carrier of K

the multF of K . ((- (1_ K)),M1) is Element of the carrier of K

((- (1_ K)) * M1) + M1 is Element of the carrier of K

the addF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V27([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]

the addF of K . (((- (1_ K)) * M1),M1) is Element of the carrier of K

(1_ K) * M1 is Element of the carrier of K

the multF of K . ((1_ K),M1) is Element of the carrier of K

((- (1_ K)) * M1) + ((1_ K) * M1) is Element of the carrier of K

the addF of K . (((- (1_ K)) * M1),((1_ K) * M1)) is Element of the carrier of K

(- (1_ K)) + (1_ K) is Element of the carrier of K

the addF of K . ((- (1_ K)),(1_ K)) is Element of the carrier of K

((- (1_ K)) + (1_ K)) * M1 is Element of the carrier of K

the multF of K . (((- (1_ K)) + (1_ K)),M1) is Element of the carrier of K

0. K is V49(K) Element of the carrier of K

(0. K) * M1 is Element of the carrier of K

the multF of K . ((0. K),M1) is Element of the carrier of K

- M1 is Element of the carrier of K

M1 + (- M1) is Element of the carrier of K

the addF of K . (M1,(- M1)) is Element of the carrier of K

((- (1_ K)) * M1) + (M1 + (- M1)) is Element of the carrier of K

the addF of K . (((- (1_ K)) * M1),(M1 + (- M1))) is Element of the carrier of K

(0. K) + (- M1) is Element of the carrier of K

the addF of K . ((0. K),(- M1)) is Element of the carrier of K

((- (1_ K)) * M1) + (0. K) is Element of the carrier of K

the addF of K . (((- (1_ K)) * M1),(0. K)) is Element of the carrier of K

((- (1_ K)) multfield) . (n . p) is set

(id the carrier of K) . (n . p) is set

the multF of K . ((- (1_ K)),((id the carrier of K) . (n . p))) is set

(comp K) . M1 is set

(len n) -tuples_on the carrier of K is non empty functional FinSequence-membered FinSequenceSet of the carrier of K

the carrier of K * is functional FinSequence-membered FinSequenceSet of the carrier of K

{ b

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

dom (- n) is set

Seg (len (- n)) is Element of bool NAT

{ b

K is set

K * is functional FinSequence-membered FinSequenceSet of K

K is set

K * is functional FinSequence-membered FinSequenceSet of K

K is non empty set

K is set

K * is functional FinSequence-membered FinSequenceSet of K

K is set

K * is functional FinSequence-membered FinSequenceSet of K

K is non empty set

K is non empty set

n is Relation-like NAT -defined K -valued Function-like FinSequence-like FinSequence of K

K * is functional FinSequence-membered FinSequenceSet of K

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

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

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

Indices p is set

dom p is Element of bool NAT

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

Seg (width p) is Element of bool NAT

{ b

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

Indices M1 is set

dom M1 is Element of bool NAT

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

Seg (width M1) is Element of bool NAT

{ b

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

p is V4() V5() V6() V10() V11() V12() integer ext-real set

c

[p,c

p * (p,c

M1 * (p,c

c

(c

((c

n . (((c

K is non empty set

n is Relation-like NAT -defined K -valued Function-like FinSequence-like FinSequence of K

K * is functional FinSequence-membered FinSequenceSet of K

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

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

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

Indices p is set

dom p is Element of bool NAT

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

Seg (width p) is Element of bool NAT

{ b

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

Indices M1 is set

dom M1 is Element of bool NAT

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

Seg (width M1) is Element of bool NAT

{ b

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

p is V4() V5() V6() V10() V11() V12() integer ext-real set

c

[p,c

p * (p,c

M1 * (p,c

p - c

(p - c

((p - c

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

0. (K,1,1) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of 1,1, the carrier of K

the carrier of K * is functional FinSequence-membered FinSequenceSet of the carrier of K

1 -tuples_on the carrier of K is non empty functional FinSequence-membered FinSequenceSet of the carrier of K

{ b

0. K is V49(K) Element of the carrier of K

1 |-> (0. K) is Relation-like NAT -defined the carrier of K -valued Function-like V37(1) FinSequence-like Element of 1 -tuples_on the carrier of K

Seg 1 is Element of bool NAT

{ b

(Seg 1) --> (0. K) is Relation-like Seg 1 -defined Seg 1 -defined the carrier of K -valued {(0. K)} -valued Function-like constant total total V27( Seg 1,{(0. K)}) FinSequence-like Element of bool [:(Seg 1),{(0. K)}:]

{(0. K)} is non empty set

[:(Seg 1),{(0. K)}:] is set

bool [:(Seg 1),{(0. K)}:] is set

1 |-> (1 |-> (0. K)) is Relation-like NAT -defined 1 -tuples_on the carrier of K -valued Function-like V37(1) FinSequence-like Function-yielding V105() Element of 1 -tuples_on (1 -tuples_on the carrier of K)

1 -tuples_on (1 -tuples_on the carrier of K) is non empty functional FinSequence-membered FinSequenceSet of 1 -tuples_on the carrier of K

(1 -tuples_on the carrier of K) * is functional FinSequence-membered FinSequenceSet of 1 -tuples_on the carrier of K

{ b

(Seg 1) --> (1 |-> (0. K)) is Relation-like Seg 1 -defined Seg 1 -defined 1 -tuples_on the carrier of K -valued {(1 |-> (0. K))} -valued Function-like constant total total V27( Seg 1,{(1 |-> (0. K))}) FinSequence-like Function-yielding V105() Element of bool [:(Seg 1),{(1 |-> (0. K))}:]

{(1 |-> (0. K))} is non empty functional set

[:(Seg 1),{(1 |-> (0. K))}:] is set

bool [:(Seg 1),{(1 |-> (0. K))}:] is set

0. (K,1) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular Matrix of 1,1, the carrier of K

p is Relation-like NAT -defined the carrier of K -valued Function-like V37(1) FinSequence-like Element of 1 -tuples_on the carrier of K

len (1 |-> (0. K)) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT

Indices (0. (K,1)) is set

dom (0. (K,1)) is Element of bool NAT

width (0. (K,1)) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT

Seg (width (0. (K,1))) is Element of bool NAT

{ b

[:(dom (0. (K,1))),(Seg (width (0. (K,1)))):] is set

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

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

M1 is V4() V5() V6() V10() V11() V12() integer ext-real set

p is V4() V5() V6() V10() V11() V12() integer ext-real set

[M1,p] is set

(0. (K,1)) * (M1,p) is Element of the carrier of K

M1 - p is V11() V12() integer ext-real set

(M1 - p) mod (len p) is V11() V12() integer ext-real set

((M1 - p) mod (len p)) + 1 is V11() V12() integer ext-real set

p . (((M1 - p) mod (len p)) + 1) is set

(M1 - p) mod 1 is V11() V12() integer ext-real set

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

(Seg 1) --> (0. K) is Relation-like Seg 1 -defined Seg 1 -defined the carrier of K -valued Function-like constant total total V27( Seg 1, the carrier of K) FinSequence-like Element of bool [:(Seg 1), the carrier of K:]

[:(Seg 1), the carrier of K:] is set

bool [:(Seg 1), the carrier of K:] is set

((Seg 1) --> (0. K)) . (((M1 - p) mod 1) + 1) is set

M1 is V4() V5() V6() V10() V11() V12() integer ext-real set

p is V4() V5() V6() V10() V11() V12() integer ext-real set

[M1,p] is set

(0. (K,1)) * (M1,p) is Element of the carrier of K

p - M1 is V11() V12() integer ext-real set

(p - M1) mod (len p) is V11() V12() integer ext-real set

((p - M1) mod (len p)) + 1 is V11() V12() integer ext-real set

p . (((p - M1) mod (len p)) + 1) is set

(p - M1) mod 1 is V11() V12() integer ext-real set

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

(Seg 1) --> (0. K) is Relation-like Seg 1 -defined Seg 1 -defined the carrier of K -valued Function-like constant total total V27( Seg 1, the carrier of K) FinSequence-like Element of bool [:(Seg 1), the carrier of K:]

[:(Seg 1), the carrier of K:] is set

bool [:(Seg 1), the carrier of K:] is set

((Seg 1) --> (0. K)) . (((p - M1) mod 1) + 1) is set

len (0. (K,1)) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT

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() integer ext-real Element of NAT

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

the carrier of K * is functional FinSequence-membered FinSequenceSet of the carrier of K

n -tuples_on the carrier of K is non empty functional FinSequence-membered FinSequenceSet of the carrier of K

{ b

0. K is V49(K) Element of the carrier of K

n |-> (0. K) is Relation-like NAT -defined the carrier of K -valued Function-like V37(n) FinSequence-like Element of n -tuples_on the carrier of K

Seg n is Element of bool NAT

{ b

(Seg n) --> (0. K) is Relation-like Seg n -defined Seg n -defined the carrier of K -valued {(0. K)} -valued Function-like constant total total V27( Seg n,{(0. K)}) FinSequence-like Element of bool [:(Seg n),{(0. K)}:]

{(0. K)} is non empty set

[:(Seg n),{(0. K)}:] is set

bool [:(Seg n),{(0. K)}:] is set

n |-> (n |-> (0. K)) is Relation-like NAT -defined n -tuples_on the carrier of K -valued Function-like V37(n) FinSequence-like Function-yielding V105() Element of n -tuples_on (n -tuples_on the carrier of K)

n -tuples_on (n -tuples_on the carrier of K) is non empty functional FinSequence-membered FinSequenceSet of n -tuples_on the carrier of K

(n -tuples_on the carrier of K) * is functional FinSequence-membered FinSequenceSet of n -tuples_on the carrier of K

{ b

(Seg n) --> (n |-> (0. K)) is Relation-like Seg n -defined Seg n -defined n -tuples_on the carrier of K -valued {(n |-> (0. K))} -valued Function-like constant total total V27( Seg n,{(n |-> (0. K))}) FinSequence-like Function-yielding V105() Element of bool [:(Seg n),{(n |-> (0. K))}:]

{(n |-> (0. K))} is non empty functional set

[:(Seg n),{(n |-> (0. K))}:] is set

bool [:(Seg n),{(n |-> (0. K))}:] is set

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

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

len (n |-> (0. K)) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT

Indices (0. (K,n)) is set

dom (0. (K,n)) is Element of bool NAT

width (0. (K,n)) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT

Seg (width (0. (K,n))) is Element of bool NAT

{ b

[:(dom (0. (K,n))),(Seg (width (0. (K,n)))):] is set

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

p is V4() V5() V6() V10() V11() V12() integer ext-real set

c

[p,c

(0. (K,n)) * (p,c

p - c

(p - c

((p - c

(n |-> (0. K)) . (((p - c

(p - c

((p - c

(Seg n) --> (0. K) is Relation-like Seg n -defined Seg n -defined the carrier of K -valued Function-like constant total total V27( Seg n, the carrier of K) FinSequence-like Element of bool [:(Seg n), the carrier of K:]

[:(Seg n), the carrier of K:] is set

bool [:(Seg n), the carrier of K:] is set

((Seg n) --> (0. K)) . (((p - c

p is V4() V5() V6() V10() V11() V12() integer ext-real set

c

[p,c

(0. (K,n)) * (p,c

c

(c

((c

(n |-> (0. K)) . (((c

(c

((c

(Seg n) --> (0. K) is Relation-like Seg n -defined Seg n -defined the carrier of K -valued Function-like constant total total V27( Seg n, the carrier of K) FinSequence-like Element of bool [:(Seg n), the carrier of K:]

[:(Seg n), the carrier of K:] is set

bool [:(Seg n), the carrier of K:] is set

((Seg n) --> (0. K)) . (((c

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() 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() integer ext-real Element of NAT

K is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr

the carrier of K is non empty non trivial set

the carrier of K * is functional FinSequence-membered FinSequenceSet of the carrier of K

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

p is Element of the carrier of K

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

n |-> p is Relation-like NAT -defined the carrier of K -valued Function-like V37(n) FinSequence-like Element of n -tuples_on the carrier of K

n -tuples_on the carrier of K is non empty functional FinSequence-membered FinSequenceSet of the carrier of K

{ b

Seg n is Element of bool NAT

{ b

(Seg n) --> p is Relation-like Seg n -defined Seg n -defined the carrier of K -valued {p} -valued Function-like constant total total V27( Seg n,{p}) FinSequence-like Element of bool [:(Seg n),{p}:]

{p} is non empty set

[:(Seg n),{p}:] is set

bool [:(Seg n),{p}:] is set

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

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

Indices ((n,n) --> p) is set

dom ((n,n) --> p) is Element of bool NAT

Seg (width ((n,n) --> p)) is Element of bool NAT

{ b

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

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

p is V4() V5() V6() V10() V11() V12() integer ext-real set

c

[p,c

((n,n) --> p) * (p,c

c

(c

((c

(n |-> p) . (((c

(c

((c

(Seg n) --> p is Relation-like Seg n -defined Seg n -defined the carrier of K -valued Function-like constant total total V27( Seg n, the carrier of K) FinSequence-like Element of bool [:(Seg n), the carrier of K:]

[:(Seg n), the carrier of K:] is set

bool [:(Seg n), the carrier of K:] is set

((Seg n) --> p) . (((c

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

n |-> p is Relation-like NAT -defined the carrier of K -valued Function-like V37(n) FinSequence-like Element of n -tuples_on the carrier of K

n -tuples_on the carrier of K is non empty functional FinSequence-membered FinSequenceSet of the carrier of K

{ b

Seg n is Element of bool NAT

{ b

(Seg n) --> p is Relation-like Seg n -defined Seg n -defined the carrier of K -valued {p} -valued Function-like constant total total V27( Seg n,{p}) FinSequence-like Element of bool [:(Seg n),{p}:]

{p} is non empty set

[:(Seg n),{p}:] is set

bool [:(Seg n),{p}:] is set

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

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

Indices ((n,n) --> p) is set

dom ((n,n) --> p) is Element of bool NAT

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

Seg (width ((n,n) --> p)) is Element of bool NAT

{ b

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

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

c

c

[c

((n,n) --> p) * (c

c

(c

((c

(n |-> p) . (((c

(c

((c

(Seg n) --> p is Relation-like Seg n -defined Seg n -defined the carrier of K -valued Function-like constant total total V27( Seg n, the carrier of K) FinSequence-like Element of bool [:(Seg n), the carrier of K:]

[:(Seg n), the carrier of K:] is set

bool [:(Seg n), the carrier of K:] is set

((Seg n) --> p) . (((c

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

0. K is V49(K) Element of the carrier of K

(1,1) --> (0. K) is Relation-like NAT -defined the carrier of K * -valued the carrier of K * -valued Function-like FinSequence-like Function-yielding V105() tabular ( the carrier of K) ( the carrier of K) Matrix of 1,1, the carrier of K

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

n is non empty set

n * is functional FinSequence-membered FinSequenceSet of n

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

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

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

M1 is Relation-like NAT -defined n -valued Function-like FinSequence-like FinSequence of n

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

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

Indices (p @) is set

dom (p @) is Element of bool NAT

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

Seg (width (p @)) is Element of bool NAT

{ b

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

p is V4() V5() V6() V10() V11() V12() integer ext-real set

c

[p,c

(p @) * (p,c

p - c

(p - c

((p - c

M1 . (((p - c

Indices p is set

dom p is Element of bool NAT

Seg (width p) is Element of bool NAT

{ b

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

Seg K is Element of bool NAT

{ b

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

[c

p * (c

p is Relation-like NAT -defined n -valued Function-like FinSequence-like FinSequence of n

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

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

n is non empty set

n * is functional FinSequence-membered FinSequenceSet of n

p is Relation-like NAT -defined n -valued Function-like FinSequence-like FinSequence of n

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

Line (M1,1) is Relation-like NAT -defined n -valued Function-like V37( width M1) FinSequence-like Element of (width M1) -tuples_on n

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

(width M1) -tuples_on n is non empty functional FinSequence-membered FinSequenceSet of n

{ b

dom p is set

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

Seg (len p) is Element of bool NAT

{ b

p is V4() V5() V6() V10() V11() V12() integer ext-real set

p . p is set

(Line (M1,1)) . p is set

0 + 1 is non empty V11() V12() integer ext-real positive non negative set

Seg K is Element of bool NAT

{ b

[1,p] is set

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

Indices M1 is set

dom M1 is Element of bool NAT

Seg (width M1) is Element of bool NAT

{ b

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

M1 * (1,p) is Element of n

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

(p - 1) mod (len p) is V11() V12() integer ext-real set

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

p . (((p - 1) mod (len p)) + 1) is set

(p - 1) mod K is V11() V12() integer ext-real set

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

p . (((p - 1) mod K) + 1) is set

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

p . ((p - 1) + 1) is set

len (Line (M1,1)) is V4() V5() V6() V10() V11() V12() integer ext-real Element of NAT

dom (Line (M1,1)) is set

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

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

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

[K,n] is set

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

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

Seg p is Element of bool NAT

{ b

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

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

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

c

c

c

c

c

width c

M3 is Relation-like NAT -defined c

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

Indices c

dom c

Seg (width c

{ b

[:(dom c

1 + 1 is non empty V11() V12() integer ext-real positive non negative set

[M1,p] is set

p - M1 is V11() V12() integer ext-real set

(p - M1) mod (len M3) is V11() V12() integer ext-real set

((p - M1) mod (len M3)) + 1 is V11() V12() integer ext-real set

M3 . (((p - M1) mod (len M3)) + 1) is set

n - K is V11() V12() integer ext-real set

(n - K) mod (len M3) is V11() V12() integer ext-real set

((n - K) mod (len M3)) + 1 is V11() V12() integer ext-real set

M3 . (((n - K) mod (len M3)) + 1) is set

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

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

p is Element of the carrier of n

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

p * M1 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 (p * M1) is set

dom (p * M1) is Element of bool NAT

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

Seg (width (p * M1)) is Element of bool NAT

{ b

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

Seg K is Element of bool NAT

{ b

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

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

p is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n

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

dom p is set

p * p is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n

p multfield is Relation-like the carrier of n -defined the carrier of n -valued Function-like V27( the carrier of n, the carrier of n) Element of bool [: the carrier of n, the carrier of n:]

[: the carrier of n, the carrier of n:] is set

bool [: the carrier of n, the carrier of n:] is set

the multF of n is Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like V27([: the carrier of n, the carrier of n:], the carrier of n) Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]

[:[: the carrier of n, the carrier of n:], the carrier of n:] is set

bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is set

id the carrier of n is non empty Relation-like the carrier of n -defined the carrier of n -valued Function-like one-to-one total Element of bool [: the carrier of n, the carrier of n:]

the multF of n [;] (p,(id the carrier of n)) is Relation-like the carrier of n -defined the carrier of n -valued Function-like V27( the carrier of n, the carrier of n) Element of bool [: the carrier of n, the carrier of n:]

K191( the carrier of n, the carrier of n,p,(p multfield)) is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n

dom (p * p) is set

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

Seg (len (p * p)) is Element of bool NAT

{ b

c

c

[c

(p * M1) * (c

c

(c

((c

(p * p) . (((c

(c

((c

(c

((c

Indices M1 is set

dom M1 is Element of bool NAT

Seg (width M1) is Element of bool NAT

{ b

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

M1 * (c

p * (M1 * (c

the multF of n . (p,(M1 * (c

(p multfield) . (M1 * (c

p . (((c

(p multfield) . (p . (((c

p /. (((c

(p multfield) . (p /. (((c

p * (p /. (((c

the multF of n . (p,(p /. (((c

(p * p) /. (((c

(p * p) . (((c

c

len c

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

n is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr

the carrier of n is non empty non trivial set

the carrier of n * is functional FinSequence-membered FinSequenceSet of the carrier of n

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

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

p + M1 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

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

p is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n

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

Indices M1 is set

dom M1 is Element of bool NAT

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

Seg (width M1) is Element of bool NAT

{ b

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

Seg K is Element of bool NAT

{ b

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

Indices (p + M1) is set

dom (p + M1) is Element of bool NAT

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

Seg (width (p + M1)) is Element of bool NAT

{ b

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

dom p is set

c

len c

Indices p is set

dom p is Element of bool NAT

Seg (width p) is Element of bool NAT

{ b

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

dom c

p + 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

K188( the carrier of n, the carrier of n, the carrier of n, the addF of n,p,c

dom (p + c

len (p + c

Seg (len (p + c

{ b

c

M3 is V4() V5() V6() V10() V11() V12() integer ext-real set

[c

(p + M1) * (c

M3 - c

(M3 - c

((M3 - c

(p + c

p * (c

M1 * (c

(p * (c

the addF of n . ((p * (c

(M3 - c

((M3 - c

c

the addF of n . ((p * (c

p . (((M3 - c

c

the addF of n . ((p . (((M3 - c

c

len c

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

n is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr

the carrier of n is non empty non trivial set

the carrier of n * is functional FinSequence-membered FinSequenceSet of the carrier of n

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

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

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

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

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

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

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

p is Element of the carrier of n

M1 is Element of the carrier of n

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

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

c

M1 * c

(p * p) + (M1 * c

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

n is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr

the carrier of n is non empty non trivial set

the carrier of n * is functional FinSequence-membered FinSequenceSet of the carrier of n

p is Element of the carrier of n

M1 is Element of the carrier of n

p is Element of the carrier of n

c

p * c

c

M1 * c

(p * c

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

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

((p * c

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

n is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr

the carrier of n is non empty non trivial set

the carrier of n * is functional FinSequence-membered FinSequenceSet of the carrier of n

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

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

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

Indices (- p) is set

dom (- p) is Element of bool NAT

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

Seg (width (- p)) is Element of bool NAT

{ b

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

Seg K is Element of bool NAT

{ b

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

M1 is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n

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

(len M1) -tuples_on the carrier of n is non empty functional FinSequence-membered FinSequenceSet of the carrier of n

{ b

- M1 is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n

comp n is Relation-like the carrier of n -defined the carrier of n -valued Function-like V27( the carrier of n, the carrier of n) Element of bool [: the carrier of n, the carrier of n:]

[: the carrier of n, the carrier of n:] is set

bool [: the carrier of n, the carrier of n:] is set

K191( the carrier of n, the carrier of n,M1,(comp n)) is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n

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

Indices p is set

dom p is Element of bool NAT

Seg (width p) is Element of bool NAT

{ b

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

p is V4() V5() V6() V10() V11() V12() integer ext-real set

c

[p,c

(- p) * (p,c

c

(c

((c

(- M1) . (((c

(c

((c

(c

((c

dom M1 is set

p * (p,c

- (p * (p,c

(comp n) . (p * (p,c

M1 . (((c

(comp n) . (M1 . (((c

(- M1) . (((c

p is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n

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

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

n is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr

the carrier of n is non empty non trivial set

the carrier of n * is functional FinSequence-membered FinSequenceSet of the carrier of n

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

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

p - M1 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

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

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

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

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

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

p is Element of the carrier of n

M1 is Element of the carrier of n

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

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

c

M1 * c

(p * p) - (M1 * c

- (M1 * c

(p * p) + (- (M1 * c

- (M1 * c

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

n is non empty non degenerated non trivial right_complementable almost_left_invertible unital V114() V116() V119() V120() V121() right-distributive left-distributive right_unital well-unital V133() left_unital doubleLoopStr

the carrier of n is non empty non trivial set

the carrier of n * is functional FinSequence-membered FinSequenceSet of the carrier of n

p is Element of the carrier of n

M1 is Element of the carrier of n

p is Element of the carrier of n

c

p * c

c

M1 * c

(p * c

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

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

((p * c

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

((p * c

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

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

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

p is Element of the carrier of n

M1 is Element of the carrier of n

p is Element of the carrier of n

c

p * c

c

M1 * c

(p * c

- (M1 * c

(p * c

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

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

((p * c

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

((p * c