:: MATRIX17 semantic presentation

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

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

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

is V30() set
is V30() set

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

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

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

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 () is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width p ) } is set
[:(dom p),(Seg ()):] is set
c7 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
n + 1 is V11() V12() integer ext-real set
(n + 1) - j is V11() V12() integer ext-real set
c8 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
(n + 1) - i is V11() V12() integer ext-real set
p * (i,j) is Element of the carrier of K
p * (c7,c8) is Element of the carrier of K
Seg n is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
[:(Seg n),(Seg n):] is set
[c7,c8] is set

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

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

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 () is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width M ) } is set
[:(dom M),(Seg ()):] is set
Seg n is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
[:(Seg n),(Seg n):] is set
i is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[i,j] is set
Indices p is set
dom p is Element of bool NAT
width p is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg () is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width p ) } is set
[:(dom p),(Seg ()):] is set
c7 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
n + 1 is V11() V12() integer ext-real set
(n + 1) - j is V11() V12() integer ext-real set
c8 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
(n + 1) - i is V11() V12() integer ext-real set
p * (i,j) is Element of the carrier of K
p * (c7,c8) is Element of the carrier of K
Indices (- M) is set
dom (- M) is Element of bool NAT
width (- M) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width (- M)) is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width (- M) ) } is set
[:(dom (- M)),(Seg (width (- M))):] is set
[c7,c8] is set
(- M) * (i,j) is Element of the carrier of K
M * (i,j) is Element of the carrier of K
- (M * (i,j)) is Element of the carrier of K
M * (c7,c8) is Element of the carrier of K
- (M * (c7,c8)) is Element of the carrier of K
(- M) * (c7,c8) is Element of the carrier of K

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

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

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

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

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

- 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

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

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 () is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width M ) } is set
[:(dom M),(Seg ()):] is set
Seg n is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
[:(Seg n),(Seg n):] is set
i is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[i,j] is set
Indices p is set
dom p is Element of bool NAT
width p is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg () is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width p ) } is set
[:(dom p),(Seg ()):] is set
c7 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
n + 1 is V11() V12() integer ext-real set
(n + 1) - j is V11() V12() integer ext-real set
c8 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
(n + 1) - i is V11() V12() integer ext-real set
p * (i,j) is Element of the carrier of K
p * (c7,c8) is Element of the carrier of K
[j,i] is set
[((n + 1) - i),((n + 1) - j)] is set
[((n + 1) - j),((n + 1) - i)] is set
M * (j,i) is Element of the carrier of K
M * (c8,c7) is Element of the carrier of K

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

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

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 () is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width M ) } is set
[:(dom M),(Seg ()):] is set
Seg n is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
[:(Seg n),(Seg n):] is set
i is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[i,j] is set
c7 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
n + 1 is V11() V12() integer ext-real set
(n + 1) - j is V11() V12() integer ext-real set
c8 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
(n + 1) - i is V11() V12() integer ext-real set
M * (i,j) is Element of the carrier of K
M * (c7,c8) is Element of the carrier of K
[c7,c8] is set
((n + 1) - i) - ((n + 1) - j) is V11() V12() integer ext-real set
(((n + 1) - i) - ((n + 1) - j)) mod (len p) is V11() V12() integer ext-real set
((((n + 1) - i) - ((n + 1) - j)) mod (len p)) + 1 is V11() V12() integer ext-real set
p . (((((n + 1) - i) - ((n + 1) - j)) mod (len p)) + 1) is set
j - i is V11() V12() integer ext-real set
(j - i) mod (len p) is V11() V12() integer ext-real set
((j - i) mod (len p)) + 1 is V11() V12() integer ext-real set
p . (((j - i) mod (len p)) + 1) is set

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

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 () is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width M ) } is set
[:(dom M),(Seg ()):] is set
Seg n is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
[:(Seg n),(Seg n):] is set
i is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[i,j] is set
c7 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
n + 1 is V11() V12() integer ext-real set
(n + 1) - j is V11() V12() integer ext-real set
c8 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
(n + 1) - i is V11() V12() integer ext-real set
M * (i,j) is Element of the carrier of K
M * (c7,c8) is Element of the carrier of K
[c7,c8] is set
((n + 1) - j) - ((n + 1) - i) is V11() V12() integer ext-real set
(((n + 1) - j) - ((n + 1) - i)) mod n is V11() V12() integer ext-real set
((((n + 1) - j) - ((n + 1) - i)) mod n) + 1 is V11() V12() integer ext-real set
p . (((((n + 1) - j) - ((n + 1) - i)) mod n) + 1) is set
i - j is V11() V12() integer ext-real set
(i - j) mod n is V11() V12() integer ext-real set
((i - j) mod n) + 1 is V11() V12() integer ext-real set
p . (((i - j) mod n) + 1) is set

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

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 () is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width M ) } is set
[:(dom M),(Seg ()):] is set
j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
n + 1 is V11() V12() integer ext-real set
(n + 1) - i is V11() V12() integer ext-real set
c7 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
(n + 1) - p is V11() V12() integer ext-real set
M * (p,i) is Element of the carrier of K
M * (j,c7) is Element of the carrier of K
- (M * (j,c7)) is Element of the carrier of K
Seg n is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
[:(Seg n),(Seg n):] is set
[j,c7] is set
- (0. K) is Element of the carrier of K

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

Indices c7 is set
dom c7 is Element of bool NAT
width c7 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width c7) is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width c7 ) } is set
[:(dom c7),(Seg (width c7)):] is set
c7 * (M,p) is Element of the carrier of n
- (c7 * (M,p)) is Element of the carrier of n
(c7 * (M,p)) + (c7 * (M,p)) is Element of the carrier of n
the addF of n is Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like V27([: the carrier of n, the carrier of n:], the carrier of n) Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[: the carrier of n, the carrier of n:] is set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is set
the addF of n . ((c7 * (M,p)),(c7 * (M,p))) is Element of the carrier of n
1_ n is Element of the carrier of n
K142(n) is V49(n) Element of the carrier of n
(1_ n) * (c7 * (M,p)) is Element of the carrier of n
the multF of n is Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like V27([: the carrier of n, the carrier of n:], the carrier of n) Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
the multF of n . ((1_ n),(c7 * (M,p))) is Element of the carrier of n
((1_ n) * (c7 * (M,p))) + (c7 * (M,p)) is Element of the carrier of n
the addF of n . (((1_ n) * (c7 * (M,p))),(c7 * (M,p))) is Element of the carrier of n
((1_ n) * (c7 * (M,p))) + ((1_ n) * (c7 * (M,p))) is Element of the carrier of n
the addF of n . (((1_ n) * (c7 * (M,p))),((1_ n) * (c7 * (M,p)))) is Element of the carrier of n
(1_ n) + (1_ n) is Element of the carrier of n
the addF of n . ((1_ n),(1_ n)) is Element of the carrier of n
((1_ n) + (1_ n)) * (c7 * (M,p)) is Element of the carrier of n
the multF of n . (((1_ n) + (1_ n)),(c7 * (M,p))) is Element of the carrier of n

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

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 () is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width M ) } is set
[:(dom M),(Seg ()):] is set
Seg n is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
[:(Seg n),(Seg n):] is set
i is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[i,j] is set
Indices p is set
dom p is Element of bool NAT
width p is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg () is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width p ) } is set
[:(dom p),(Seg ()):] is set
c7 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
n + 1 is V11() V12() integer ext-real set
(n + 1) - j is V11() V12() integer ext-real set
c8 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
(n + 1) - i is V11() V12() integer ext-real set
p * (i,j) is Element of the carrier of K
p * (c7,c8) is Element of the carrier of K
- (p * (c7,c8)) is Element of the carrier of K
Indices (- M) is set
dom (- M) is Element of bool NAT
width (- M) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width (- M)) is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width (- M) ) } is set
[:(dom (- M)),(Seg (width (- M))):] is set
[c7,c8] is set
(- M) * (i,j) is Element of the carrier of K
M * (i,j) is Element of the carrier of K
- (M * (i,j)) is Element of the carrier of K
M * (c7,c8) is Element of the carrier of K
- (M * (c7,c8)) is Element of the carrier of K
- (- (M * (c7,c8))) is Element of the carrier of K
(- M) * (c7,c8) is Element of the carrier of K
- ((- M) * (c7,c8)) is Element of the carrier of K

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

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

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

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

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

- 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

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

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 () is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width M ) } is set
[:(dom M),(Seg ()):] is set
Seg n is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
[:(Seg n),(Seg n):] is set
i is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[i,j] is set
Indices p is set
dom p is Element of bool NAT
width p is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg () is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width p ) } is set
[:(dom p),(Seg ()):] is set
c7 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
n + 1 is V11() V12() integer ext-real set
(n + 1) - j is V11() V12() integer ext-real set
c8 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
(n + 1) - i is V11() V12() integer ext-real set
p * (i,j) is Element of the carrier of K
p * (c7,c8) is Element of the carrier of K
- (p * (c7,c8)) is Element of the carrier of K
[j,i] is set
[((n + 1) - i),((n + 1) - j)] is set
[((n + 1) - j),((n + 1) - i)] is set
M * (j,i) is Element of the carrier of K
M * (c8,c7) is Element of the carrier of K
- (M * (c8,c7)) is Element of the carrier of K

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

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

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 () is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width p ) } is set
[:(dom p),(Seg ()):] is set
c7 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
n + 1 is V11() V12() integer ext-real set
(n + 1) - i is V11() V12() integer ext-real set
c8 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
(n + 1) - j is V11() V12() integer ext-real set
p * (i,j) is Element of the carrier of K
p * (c7,c8) is Element of the carrier of K
Seg n is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
[:(Seg n),(Seg n):] is set
[c7,c8] is set

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

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

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 () is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width M ) } is set
[:(dom M),(Seg ()):] is set
Seg n is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
[:(Seg n),(Seg n):] is set
i is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[i,j] is set
Indices p is set
dom p is Element of bool NAT
width p is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg () is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width p ) } is set
[:(dom p),(Seg ()):] is set
c7 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
n + 1 is V11() V12() integer ext-real set
(n + 1) - i is V11() V12() integer ext-real set
c8 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
(n + 1) - j is V11() V12() integer ext-real set
p * (i,j) is Element of the carrier of K
p * (c7,c8) is Element of the carrier of K
Indices (- M) is set
dom (- M) is Element of bool NAT
width (- M) is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg (width (- M)) is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width (- M) ) } is set
[:(dom (- M)),(Seg (width (- M))):] is set
[c7,c8] is set
(- M) * (i,j) is Element of the carrier of K
M * (i,j) is Element of the carrier of K
- (M * (i,j)) is Element of the carrier of K
M * (c7,c8) is Element of the carrier of K
- (M * (c7,c8)) is Element of the carrier of K
(- M) * (c7,c8) is Element of the carrier of K

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

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

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

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

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

- 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

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

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 () is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width M ) } is set
[:(dom M),(Seg ()):] is set
Seg n is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
[:(Seg n),(Seg n):] is set
i is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
j is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
[i,j] is set
Indices p is set
dom p is Element of bool NAT
width p is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT
Seg () is Element of bool NAT
{ b1 where b1 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real Element of NAT : ( 1 <= b1 & b1 <= width p ) } is set
[:(dom p),(Seg ()):] is set
c7 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
n + 1 is V11() V12() integer ext-real set
(n + 1) - i is V11() V12() integer ext-real set
c8 is V4() V5() V6() V10() V11() V12() V30() V35() integer ext-real set
(n + 1) - j is V11() V12() integer ext-real set
p * (i,j) is Element of the carrier of K
p * (c7,c8) is Element of the carrier of K
[j,i] is set
[((n + 1) - i),((n + 1) - j)] is set
[((n + 1) - j),((n + 1) - i)] is set
M * (j,i) is Element of the carrier of K
M * (c8,c7) is Element of the carrier of K

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

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 () is Element of bool NAT