REAL is set
NAT is non empty V24() V25() V26() V35() V40() V41() Element of bool REAL
bool REAL is set
{} is Function-like functional empty V24() V25() V26() V28() V29() V30() V31() ext-real V35() V40() V42( {} ) V109() set
1 is non empty V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
{{},1} is non empty set
NAT is non empty V24() V25() V26() V35() V40() V41() set
bool NAT is V35() set
bool NAT is V35() set
2 is non empty V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
0 is Function-like functional empty V24() V25() V26() V28() V29() V30() V31() ext-real V35() V40() V42( {} ) V109() Element of NAT
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- n is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- (- n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (- n) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (- (- n)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (- n) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- n) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
Indices (- n) is set
dom (- n) is Element of bool NAT
Seg (width (- n)) is Element of bool NAT
[:(dom (- n)),(Seg (width (- n))):] is set
Indices n is set
dom n is Element of bool NAT
Seg (width n) is Element of bool NAT
[:(dom n),(Seg (width n)):] is set
m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() set
k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() set
[m,k] is set
n * (m,k) is Element of the carrier of K
(- (- n)) * (m,k) is Element of the carrier of K
(- n) * (m,k) is Element of the carrier of K
- (n * (m,k)) is Element of the carrier of K
- (- (n * (m,k))) is Element of the carrier of K
width (- (- n)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (- (- n)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- n is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
0. (K,(len n),(width n)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular Matrix of len n, width n, the carrier of K
(width n) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
0. K is V54(K) Element of the carrier of K
(width n) |-> (0. K) is Relation-like NAT -defined the carrier of K -valued Function-like V42( width n) FinSequence-like Element of (width n) -tuples_on the carrier of K
(len n) |-> ((width n) |-> (0. K)) is Relation-like NAT -defined (width n) -tuples_on the carrier of K -valued Function-like V42( len n) FinSequence-like Element of (len n) -tuples_on ((width n) -tuples_on the carrier of K)
(len n) -tuples_on ((width n) -tuples_on the carrier of K) is functional non empty FinSequence-membered FinSequenceSet of (width n) -tuples_on the carrier of K
len (n + (- n)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (0. (K,(len n),(width n))) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,n,n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- n is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
0. (K,(len n),(width n)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular Matrix of len n, width n, the carrier of K
(width n) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
0. K is V54(K) Element of the carrier of K
(width n) |-> (0. K) is Relation-like NAT -defined the carrier of K -valued Function-like V42( width n) FinSequence-like Element of (width n) -tuples_on the carrier of K
(len n) |-> ((width n) |-> (0. K)) is Relation-like NAT -defined (width n) -tuples_on the carrier of K -valued Function-like V42( len n) FinSequence-like Element of (len n) -tuples_on ((width n) -tuples_on the carrier of K)
(len n) -tuples_on ((width n) -tuples_on the carrier of K) is functional non empty FinSequence-membered FinSequenceSet of (width n) -tuples_on the carrier of K
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
n + k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
m + k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
k + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
0. (K,(len n),(width n)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular Matrix of len n, width n, the carrier of K
(width n) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
0. K is V54(K) Element of the carrier of K
(width n) |-> (0. K) is Relation-like NAT -defined the carrier of K -valued Function-like V42( width n) FinSequence-like Element of (width n) -tuples_on the carrier of K
(len n) |-> ((width n) |-> (0. K)) is Relation-like NAT -defined (width n) -tuples_on the carrier of K -valued Function-like V42( len n) FinSequence-like Element of (len n) -tuples_on ((width n) -tuples_on the carrier of K)
(len n) -tuples_on ((width n) -tuples_on the carrier of K) is functional non empty FinSequence-membered FinSequenceSet of (width n) -tuples_on the carrier of K
n + (k + (- k)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(m + k) + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
m + (k + (- k)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
m + (0. (K,(len n),(width n))) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,n,(- m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- (- m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
n + m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
0. (K,(len n),(width n)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular Matrix of len n, width n, the carrier of K
(width n) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
0. K is V54(K) Element of the carrier of K
(width n) |-> (0. K) is Relation-like NAT -defined the carrier of K -valued Function-like V42( width n) FinSequence-like Element of (width n) -tuples_on the carrier of K
(len n) |-> ((width n) |-> (0. K)) is Relation-like NAT -defined (width n) -tuples_on the carrier of K -valued Function-like V42( len n) FinSequence-like Element of (len n) -tuples_on ((width n) -tuples_on the carrier of K)
(len n) -tuples_on ((width n) -tuples_on the carrier of K) is functional non empty FinSequence-membered FinSequenceSet of (width n) -tuples_on the carrier of K
- n is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n + m) + (- n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
m + n is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(m + n) + (- n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
m + (n + (- n)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
m + (0. (K,(len n),(width n))) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (0. (K,(len n),(width n))) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(K,n,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
0. (K,(len n),(width n)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular Matrix of len n, width n, the carrier of K
(width n) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
0. K is V54(K) Element of the carrier of K
(width n) |-> (0. K) is Relation-like NAT -defined the carrier of K -valued Function-like V42( width n) FinSequence-like Element of (width n) -tuples_on the carrier of K
(len n) |-> ((width n) |-> (0. K)) is Relation-like NAT -defined (width n) -tuples_on the carrier of K -valued Function-like V42( len n) FinSequence-like Element of (len n) -tuples_on ((width n) -tuples_on the carrier of K)
(len n) -tuples_on ((width n) -tuples_on the carrier of K) is functional non empty FinSequence-membered FinSequenceSet of (width n) -tuples_on the carrier of K
len (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (0. (K,(len n),(width n))) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (0. (K,(len n),(width n))) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(n + (- m)) + m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
m + (0. (K,(len n),(width n))) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- m) + m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + ((- m) + m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
m + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (m + (- m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (0. (K,(len n),(width n))) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
n + m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
0. (K,(len n),(width n)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular Matrix of len n, width n, the carrier of K
(width n) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
0. K is V54(K) Element of the carrier of K
(width n) |-> (0. K) is Relation-like NAT -defined the carrier of K -valued Function-like V42( width n) FinSequence-like Element of (width n) -tuples_on the carrier of K
(len n) |-> ((width n) |-> (0. K)) is Relation-like NAT -defined (width n) -tuples_on the carrier of K -valued Function-like V42( len n) FinSequence-like Element of (len n) -tuples_on ((width n) -tuples_on the carrier of K)
(len n) -tuples_on ((width n) -tuples_on the carrier of K) is functional non empty FinSequence-membered FinSequenceSet of (width n) -tuples_on the carrier of K
- n is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(K,n,(- m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- (- m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
K is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() doubleLoopStr
0. (m,K,n) is Relation-like NAT -defined the carrier of m * -valued Function-like FinSequence-like tabular Matrix of K,n, the carrier of m
the carrier of m is non empty non trivial set
the carrier of m * is functional FinSequence-membered FinSequenceSet of the carrier of m
n -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
0. m is V54(m) Element of the carrier of m
n |-> (0. m) is Relation-like NAT -defined the carrier of m -valued Function-like V42(n) FinSequence-like Element of n -tuples_on the carrier of m
K |-> (n |-> (0. m)) is Relation-like NAT -defined n -tuples_on the carrier of m -valued Function-like V42(K) FinSequence-like Element of K -tuples_on (n -tuples_on the carrier of m)
K -tuples_on (n -tuples_on the carrier of m) is functional non empty FinSequence-membered FinSequenceSet of n -tuples_on the carrier of m
- (0. (m,K,n)) is Relation-like NAT -defined the carrier of m * -valued Function-like FinSequence-like tabular FinSequence of the carrier of m *
(0. (m,K,n)) + (0. (m,K,n)) is Relation-like NAT -defined the carrier of m * -valued Function-like FinSequence-like tabular FinSequence of the carrier of m *
len (0. (m,K,n)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (0. (m,K,n)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (0. (m,K,n)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (- (0. (m,K,n))) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(K,m,n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- n is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
m + (- n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
0. (K,(len n),(width n)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular Matrix of len n, width n, the carrier of K
(width n) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
0. K is V54(K) Element of the carrier of K
(width n) |-> (0. K) is Relation-like NAT -defined the carrier of K -valued Function-like V42( width n) FinSequence-like Element of (width n) -tuples_on the carrier of K
(len n) |-> ((width n) |-> (0. K)) is Relation-like NAT -defined (width n) -tuples_on the carrier of K -valued Function-like V42( len n) FinSequence-like Element of (len n) -tuples_on ((width n) -tuples_on the carrier of K)
(len n) -tuples_on ((width n) -tuples_on the carrier of K) is functional non empty FinSequence-membered FinSequenceSet of (width n) -tuples_on the carrier of K
len (- n) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- n) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
- m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(m + (- n)) + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- n) + m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
((- n) + m) + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
m + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- n) + (m + (- m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- n) + (0. (K,(len n),(width n))) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- (0. (K,(len n),(width n))) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (0. (K,(len n),(width n))) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(K,m,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
m + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,n,(K,m,m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- (K,m,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- (K,m,m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
0. (K,(len n),(width n)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular Matrix of len n, width n, the carrier of K
(width n) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
0. K is V54(K) Element of the carrier of K
(width n) |-> (0. K) is Relation-like NAT -defined the carrier of K -valued Function-like V42( width n) FinSequence-like Element of (width n) -tuples_on the carrier of K
(len n) |-> ((width n) |-> (0. K)) is Relation-like NAT -defined (width n) -tuples_on the carrier of K -valued Function-like V42( len n) FinSequence-like Element of (len n) -tuples_on ((width n) -tuples_on the carrier of K)
(len n) -tuples_on ((width n) -tuples_on the carrier of K) is functional non empty FinSequence-membered FinSequenceSet of (width n) -tuples_on the carrier of K
(K,n,(0. (K,(len n),(width n)))) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- (0. (K,(len n),(width n))) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- (0. (K,(len n),(width n)))) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (0. (K,(len n),(width n))) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (K,n,(K,m,m)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
n + m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- (n + m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- n is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- n) + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
width (- n) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width ((- n) + (- m)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (n + m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (n + m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (- n) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len ((- n) + (- m)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(n + m) + ((- n) + (- m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- m) + (- n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n + m) + ((- m) + (- n)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n + m) + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
((n + m) + (- m)) + (- n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
m + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (m + (- m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n + (m + (- m))) + (- n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
0. (K,(len n),(width n)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular Matrix of len n, width n, the carrier of K
(width n) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
0. K is V54(K) Element of the carrier of K
(width n) |-> (0. K) is Relation-like NAT -defined the carrier of K -valued Function-like V42( width n) FinSequence-like Element of (width n) -tuples_on the carrier of K
(len n) |-> ((width n) |-> (0. K)) is Relation-like NAT -defined (width n) -tuples_on the carrier of K -valued Function-like V42( len n) FinSequence-like Element of (len n) -tuples_on ((width n) -tuples_on the carrier of K)
(len n) -tuples_on ((width n) -tuples_on the carrier of K) is functional non empty FinSequence-membered FinSequenceSet of (width n) -tuples_on the carrier of K
n + (0. (K,(len n),(width n))) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n + (0. (K,(len n),(width n)))) + (- n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (- (n + m)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(K,n,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,n,(K,n,m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- (K,n,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- (K,n,m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- n is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (- n) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- n) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
0. (K,(len n),(width n)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular Matrix of len n, width n, the carrier of K
(width n) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
0. K is V54(K) Element of the carrier of K
(width n) |-> (0. K) is Relation-like NAT -defined the carrier of K -valued Function-like V42( width n) FinSequence-like Element of (width n) -tuples_on the carrier of K
(len n) |-> ((width n) |-> (0. K)) is Relation-like NAT -defined (width n) -tuples_on the carrier of K -valued Function-like V42( len n) FinSequence-like Element of (len n) -tuples_on ((width n) -tuples_on the carrier of K)
(len n) -tuples_on ((width n) -tuples_on the carrier of K) is functional non empty FinSequence-membered FinSequenceSet of (width n) -tuples_on the carrier of K
len (0. (K,(len n),(width n))) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (0. (K,(len n),(width n))) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
- (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- n) + (- (- m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + ((- n) + (- (- m))) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- n) + m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + ((- n) + m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n + (- n)) + m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(0. (K,(len n),(width n))) + m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
m + (0. (K,(len n),(width n))) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (K,n,(K,n,m)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(K,n,k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,m,k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
m + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (- k) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- k) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(n + (- k)) + k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- k) + k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
m + ((- k) + k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
k + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
m + (k + (- k)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
0. (K,(len n),(width n)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular Matrix of len n, width n, the carrier of K
(width n) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
0. K is V54(K) Element of the carrier of K
(width n) |-> (0. K) is Relation-like NAT -defined the carrier of K -valued Function-like V42( width n) FinSequence-like Element of (width n) -tuples_on the carrier of K
(len n) |-> ((width n) |-> (0. K)) is Relation-like NAT -defined (width n) -tuples_on the carrier of K -valued Function-like V42( len n) FinSequence-like Element of (len n) -tuples_on ((width n) -tuples_on the carrier of K)
(len n) -tuples_on ((width n) -tuples_on the carrier of K) is functional non empty FinSequence-membered FinSequenceSet of (width n) -tuples_on the carrier of K
m + (0. (K,(len n),(width n))) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + ((- k) + k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (k + (- k)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (0. (K,(len n),(width n))) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(K,k,n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- n is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
k + (- n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,k,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
k + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (- n) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- n) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(- n) + k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- m) + k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
((- n) + k) + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
k + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- m) + (k + (- k)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
0. (K,(len n),(width n)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular Matrix of len n, width n, the carrier of K
(width n) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
0. K is V54(K) Element of the carrier of K
(width n) |-> (0. K) is Relation-like NAT -defined the carrier of K -valued Function-like V42( width n) FinSequence-like Element of (width n) -tuples_on the carrier of K
(len n) |-> ((width n) |-> (0. K)) is Relation-like NAT -defined (width n) -tuples_on the carrier of K -valued Function-like V42( len n) FinSequence-like Element of (len n) -tuples_on ((width n) -tuples_on the carrier of K)
(len n) -tuples_on ((width n) -tuples_on the carrier of K) is functional non empty FinSequence-membered FinSequenceSet of (width n) -tuples_on the carrier of K
(- m) + (0. (K,(len n),(width n))) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- n) + (k + (- k)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- n) + (0. (K,(len n),(width n))) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- (- n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(K,n,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,(K,n,m),k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,n,m) + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,n,k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,(K,n,k),m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,n,k) + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (- k) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- k) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(- m) + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + ((- m) + (- k)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- k) + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + ((- k) + (- m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(K,n,k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,n,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,k,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
k + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,(K,n,m),(K,k,m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- (K,k,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,n,m) + (- (K,k,m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (- k) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- k) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (n + (- m)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (n + (- m)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
- (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- k) + (- (- m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n + (- m)) + ((- k) + (- (- m))) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- k) + m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n + (- m)) + ((- k) + m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
m + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n + (- m)) + (m + (- k)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n + (- m)) + m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
((n + (- m)) + m) + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- m) + m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + ((- m) + m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n + ((- m) + m)) + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
m + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (m + (- m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n + (m + (- m))) + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
0. (K,(len n),(width n)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular Matrix of len n, width n, the carrier of K
(width n) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
0. K is V54(K) Element of the carrier of K
(width n) |-> (0. K) is Relation-like NAT -defined the carrier of K -valued Function-like V42( width n) FinSequence-like Element of (width n) -tuples_on the carrier of K
(len n) |-> ((width n) |-> (0. K)) is Relation-like NAT -defined (width n) -tuples_on the carrier of K -valued Function-like V42( len n) FinSequence-like Element of (len n) -tuples_on ((width n) -tuples_on the carrier of K)
(len n) -tuples_on ((width n) -tuples_on the carrier of K) is functional non empty FinSequence-membered FinSequenceSet of (width n) -tuples_on the carrier of K
n + (0. (K,(len n),(width n))) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n + (0. (K,(len n),(width n)))) + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (K,n,m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (K,(K,n,m),(K,k,m)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (K,n,k) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(K,k,n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- n is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
k + (- n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,k,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
k + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,(K,k,n),(K,k,m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- (K,k,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,k,n) + (- (K,k,m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,m,n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
m + (- n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- n) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(- n) + k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
width ((- n) + k) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
- k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (- k) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- k) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (- n) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len ((- n) + k) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(K,((- n) + k),(k + (- m))) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- (k + (- m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
((- n) + k) + (- (k + (- m))) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- k) + (- (- m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
((- n) + k) + ((- k) + (- (- m))) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- k) + m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
((- n) + k) + ((- k) + m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
((- n) + k) + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(((- n) + k) + (- k)) + m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
k + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- n) + (k + (- k)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
((- n) + (k + (- k))) + m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
0. (K,(len n),(width n)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular Matrix of len n, width n, the carrier of K
(width n) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
0. K is V54(K) Element of the carrier of K
(width n) |-> (0. K) is Relation-like NAT -defined the carrier of K -valued Function-like V42( width n) FinSequence-like Element of (width n) -tuples_on the carrier of K
(len n) |-> ((width n) |-> (0. K)) is Relation-like NAT -defined (width n) -tuples_on the carrier of K -valued Function-like V42( len n) FinSequence-like Element of (len n) -tuples_on ((width n) -tuples_on the carrier of K)
(len n) -tuples_on ((width n) -tuples_on the carrier of K) is functional non empty FinSequence-membered FinSequenceSet of (width n) -tuples_on the carrier of K
(- n) + (0. (K,(len n),(width n))) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
((- n) + (0. (K,(len n),(width n)))) + m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- n) + m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (K,m,n) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (K,(K,k,n),(K,k,m)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (K,k,n) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
M1 is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len M1 is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width M1 is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(K,n,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,k,M1) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- M1 is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
k + (- M1) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,n,k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,m,M1) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
m + (- M1) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (- M1) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- M1) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (k + (- M1)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (k + (- M1)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (n + (- k)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (n + (- k)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (n + (- m)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (n + (- m)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (m + (- M1)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (m + (- M1)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (- k) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- k) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
- (k + (- M1)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n + (- m)) + (- (k + (- M1))) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
0. (K,(len n),(width n)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular Matrix of len n, width n, the carrier of K
(width n) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
0. K is V54(K) Element of the carrier of K
(width n) |-> (0. K) is Relation-like NAT -defined the carrier of K -valued Function-like V42( width n) FinSequence-like Element of (width n) -tuples_on the carrier of K
(len n) |-> ((width n) |-> (0. K)) is Relation-like NAT -defined (width n) -tuples_on the carrier of K -valued Function-like V42( len n) FinSequence-like Element of (len n) -tuples_on ((width n) -tuples_on the carrier of K)
(len n) -tuples_on ((width n) -tuples_on the carrier of K) is functional non empty FinSequence-membered FinSequenceSet of (width n) -tuples_on the carrier of K
- (- M1) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- k) + (- (- M1)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n + (- m)) + ((- k) + (- (- M1))) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- k) + M1 is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n + (- m)) + ((- k) + M1) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n + (- m)) + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
((n + (- m)) + (- k)) + M1 is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- m) + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + ((- m) + (- k)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n + ((- m) + (- k))) + M1 is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- k) + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + ((- k) + (- m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n + ((- k) + (- m))) + M1 is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n + (- k)) + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
((n + (- k)) + (- m)) + M1 is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- m) + M1 is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n + (- k)) + ((- m) + M1) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- m) + (- (- M1)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n + (- k)) + ((- m) + (- (- M1))) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,(n + (- k)),(m + (- M1))) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- (m + (- M1)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n + (- k)) + (- (m + (- M1))) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (K,n,k) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (K,m,M1) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(K,m,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
m + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (K,m,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
0. (K,(len n),(width n)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular Matrix of len n, width n, the carrier of K
(width n) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
0. K is V54(K) Element of the carrier of K
(width n) |-> (0. K) is Relation-like NAT -defined the carrier of K -valued Function-like V42( width n) FinSequence-like Element of (width n) -tuples_on the carrier of K
(len n) |-> ((width n) |-> (0. K)) is Relation-like NAT -defined (width n) -tuples_on the carrier of K -valued Function-like V42( len n) FinSequence-like Element of (len n) -tuples_on ((width n) -tuples_on the carrier of K)
(len n) -tuples_on ((width n) -tuples_on the carrier of K) is functional non empty FinSequence-membered FinSequenceSet of (width n) -tuples_on the carrier of K
n + (0. (K,(len n),(width n))) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (n + (K,m,m)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
n + m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,(n + m),m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n + m) + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,m,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
m + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (K,m,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(K,n,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,n,m) + m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(- m) + m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + ((- m) + m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,m,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
m + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (K,m,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
n + k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,k,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
k + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n + m) + (K,k,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (n + m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (n + m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(- m) + k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n + m) + ((- m) + k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n + m) + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
((n + m) + (- m)) + k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,m,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
m + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (K,m,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n + (K,m,m)) + k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
n + m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,(n + m),k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n + m) + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,n,k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,n,k) + m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (- k) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- k) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (m + (- k)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- k) + m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + ((- k) + m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(K,n,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,n,m) + k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,k,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
k + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,k,m) + n is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(- m) + n is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
((- m) + n) + k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- m) + (n + k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
k + n is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- m) + (k + n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- m) + k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
((- m) + k) + n is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
n + k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,m,k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
m + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,(n + m),(K,m,k)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- (K,m,k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n + m) + (- (K,m,k)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (- k) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- k) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (n + m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (n + m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
0. (K,(len n),(width n)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular Matrix of len n, width n, the carrier of K
(width n) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
0. K is V54(K) Element of the carrier of K
(width n) |-> (0. K) is Relation-like NAT -defined the carrier of K -valued Function-like V42( width n) FinSequence-like Element of (width n) -tuples_on the carrier of K
(len n) |-> ((width n) |-> (0. K)) is Relation-like NAT -defined (width n) -tuples_on the carrier of K -valued Function-like V42( len n) FinSequence-like Element of (len n) -tuples_on ((width n) -tuples_on the carrier of K)
(len n) -tuples_on ((width n) -tuples_on the carrier of K) is functional non empty FinSequence-membered FinSequenceSet of (width n) -tuples_on the carrier of K
n + (0. (K,(len n),(width n))) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n + (0. (K,(len n),(width n)))) + k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
m + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (m + (- m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n + (m + (- m))) + k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n + m) + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
((n + m) + (- m)) + k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- m) + k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n + m) + ((- m) + k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- m) + (- (- k)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n + m) + ((- m) + (- (- k))) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (K,(n + m),(K,m,k)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (n + m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (n + k) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(K,n,k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
k + m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,(n + m),(k + m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- (k + m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n + m) + (- (k + m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (- k) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- k) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(K,m,(- k)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
m + (- (- k)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,(n + m),(K,m,(- k))) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- (K,m,(- k)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n + m) + (- (K,m,(- k))) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
m + k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,(n + m),(m + k)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- (m + k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n + m) + (- (m + k)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
M1 is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len M1 is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width M1 is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
n + m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
k + M1 is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,n,k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,M1,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
M1 + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
M1 + k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n + m) + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
k + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
M1 + (k + (- m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- m) + k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
M1 + ((- m) + k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,m,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
m + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (K,m,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(M1 + (- m)) + k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (M1 + (- m)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (M1 + (- m)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
M1 is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len M1 is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width M1 is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(K,n,k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,M1,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
M1 + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
k + M1 is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (- k) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- k) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(- m) + M1 is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,n,(- m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- (- m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,M1,(- k)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
M1 + (- (- k)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
M1 + k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
M1 is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len M1 is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width M1 is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
n + m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,k,M1) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- M1 is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
k + (- M1) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + M1 is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,k,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
k + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (- M1) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- M1) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(- M1) + k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,n,(- M1)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- (- M1) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- (- M1)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m + k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,n,(m + k)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- (m + k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- (m + k)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,n,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,(K,n,m),k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,n,m) + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(- m) + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + ((- m) + (- k)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(K,m,k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
m + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,n,(K,m,k)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- (K,m,k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- (K,m,k)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,n,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,n,m) + k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (- k) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- k) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(K,(K,n,m),(- k)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,n,m) + (- (- k)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n + (- m)) + k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(K,m,k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
m + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,n,(K,m,k)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- (K,m,k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- (K,m,k)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,k,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
k + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (K,k,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (- k) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- k) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(- k) + m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- ((- k) + m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- ((- k) + m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- (- k)) + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + ((- (- k)) + (- m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (k + (- m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,n,k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,n,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,m,k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
m + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,n,m) + (K,m,k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (n + (- m)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (n + (- m)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(n + (- m)) + m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
((n + (- m)) + m) + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- m) + m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + ((- m) + m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n + ((- m) + m)) + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,m,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
m + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (K,m,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n + (K,m,m)) + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- n is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- (- n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- n is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
0. (K,(len n),(width n)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular Matrix of len n, width n, the carrier of K
(width n) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
0. K is V54(K) Element of the carrier of K
(width n) |-> (0. K) is Relation-like NAT -defined the carrier of K -valued Function-like V42( width n) FinSequence-like Element of (width n) -tuples_on the carrier of K
(len n) |-> ((width n) |-> (0. K)) is Relation-like NAT -defined (width n) -tuples_on the carrier of K -valued Function-like V42( len n) FinSequence-like Element of (len n) -tuples_on ((width n) -tuples_on the carrier of K)
(len n) -tuples_on ((width n) -tuples_on the carrier of K) is functional non empty FinSequence-membered FinSequenceSet of (width n) -tuples_on the carrier of K
- (- n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
- m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
0. (K,(len n),(width n)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular Matrix of len n, width n, the carrier of K
(width n) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
0. K is V54(K) Element of the carrier of K
(width n) |-> (0. K) is Relation-like NAT -defined the carrier of K -valued Function-like V42( width n) FinSequence-like Element of (width n) -tuples_on the carrier of K
(len n) |-> ((width n) |-> (0. K)) is Relation-like NAT -defined (width n) -tuples_on the carrier of K -valued Function-like V42( len n) FinSequence-like Element of (len n) -tuples_on ((width n) -tuples_on the carrier of K)
(len n) -tuples_on ((width n) -tuples_on the carrier of K) is functional non empty FinSequence-membered FinSequenceSet of (width n) -tuples_on the carrier of K
(K,n,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
n + m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n + m) + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,(n + m),m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
- m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
m + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (m + (- m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,m,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (K,m,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
- m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- m) + n is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
((- m) + n) + m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(K,n,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,n,m) + m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
- n is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- n) + m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- ((- n) + m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (- n) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- n) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
- (- n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- (- n)) + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
n + m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- n is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- n) + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- ((- n) + (- m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (- n) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- n) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
- (- n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- (- n)) + (- (- m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- (- m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(K,n,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- (K,n,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,m,n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- n is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
m + (- n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (- n) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- n) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
- (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- n) + (- (- m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- n) + m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
- n is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,(- n),m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- n) + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,(- m),n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- m) + (- n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (- n) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- n) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
- m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- n is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,(- n),m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- n) + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,(- m),(K,(- n),m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- (K,(- n),m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- m) + (- (K,(- n),m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (n + m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (n + m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (- n) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- n) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
- (- n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- (- n)) + (- (- m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- m) + ((- (- n)) + (- (- m))) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- (- m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- m) + (n + (- (- m))) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- m) + (n + m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n + m) + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
- n is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,(- n),m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- n) + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,(K,(- n),m),k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,(- n),m) + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,(- n),k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- n) + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,(K,(- n),k),m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,(- n),k) + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (- n) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- n) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
- n is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,(- n),m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- n) + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,(K,(- n),m),k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,(- n),m) + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,(- m),k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- m) + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,(K,(- m),k),n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,(- m),k) + (- n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,(- m),n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- m) + (- n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,(K,(- m),n),k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,(- m),n) + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
- n is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,(- n),m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- n) + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,(K,(- n),m),k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,(- n),m) + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,(- k),m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- k) + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,(K,(- k),m),n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,(- k),m) + (- n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,(- n),k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- n) + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,(K,(- n),k),m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,(- n),k) + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(K,k,n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- n is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
k + (- n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,k,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
k + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,(K,k,n),(K,k,m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- (K,k,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,k,n) + (- (K,k,m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,n,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- (K,n,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (- n) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- n) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(K,m,n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
m + (- n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- n) + m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(- n) + (- (- m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- (n + (- m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
0. (K,(len n),(width n)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular Matrix of len n, width n, the carrier of K
(width n) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
0. K is V54(K) Element of the carrier of K
(width n) |-> (0. K) is Relation-like NAT -defined the carrier of K -valued Function-like V42( width n) FinSequence-like Element of (width n) -tuples_on the carrier of K
(len n) |-> ((width n) |-> (0. K)) is Relation-like NAT -defined (width n) -tuples_on the carrier of K -valued Function-like V42( len n) FinSequence-like Element of (len n) -tuples_on ((width n) -tuples_on the carrier of K)
(len n) -tuples_on ((width n) -tuples_on the carrier of K) is functional non empty FinSequence-membered FinSequenceSet of (width n) -tuples_on the carrier of K
(K,(0. (K,(len n),(width n))),n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- n is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(0. (K,(len n),(width n))) + (- n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (- n) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (- n) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (0. (K,(len n),(width n))) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (0. (K,(len n),(width n))) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(- n) + (0. (K,(len n),(width n))) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (K,(0. (K,(len n),(width n))),n) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
n + m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,n,(- m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- (- m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
- m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
m + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,n,(m + (- m))) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- (m + (- m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- (m + (- m))) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,m,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,n,(K,m,m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- (K,m,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- (K,m,m)) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(K,n,k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
m + (- k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,m,k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(K,k,n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- n is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
k + (- n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
- m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
k + (- m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(K,k,m) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
K is set
K * is functional FinSequence-membered FinSequenceSet of K
n is Relation-like NAT -defined K * -valued Function-like FinSequence-like tabular FinSequence of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined K * -valued Function-like FinSequence-like tabular FinSequence of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
Indices n is set
dom n is Element of bool NAT
Seg (width n) is Element of bool NAT
[:(dom n),(Seg (width n)):] is set
Indices m is set
dom m is Element of bool NAT
Seg (width m) is Element of bool NAT
[:(dom m),(Seg (width m)):] is set
Seg (len n) is Element of bool NAT
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() doubleLoopStr
the carrier of K is non empty non trivial set
n is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
k is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
len k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
n + m is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
mlt ((n + m),k) is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
mlt (n,k) is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
mlt (m,k) is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
(mlt (n,k)) + (mlt (m,k)) is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
dom k is Element of bool NAT
Seg (len n) is Element of bool NAT
(len n) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
dom (n + m) is Element of bool NAT
M1 is Relation-like Function-like V42( len n) Element of (len n) -tuples_on the carrier of K
M2 is Relation-like Function-like V42( len n) Element of (len n) -tuples_on the carrier of K
M1 + M2 is Relation-like NAT -defined the carrier of K -valued Function-like V42( len n) FinSequence-like Element of (len n) -tuples_on the carrier of K
len (M1 + M2) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
Seg (len (M1 + M2)) is Element of bool NAT
dom (mlt (m,k)) is Element of bool NAT
i is Relation-like Function-like V42( len n) Element of (len n) -tuples_on the carrier of K
mlt (M2,i) is Relation-like NAT -defined the carrier of K -valued Function-like V42( len n) FinSequence-like Element of (len n) -tuples_on the carrier of K
len (mlt (M2,i)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
Seg (len (mlt (M2,i))) is Element of bool NAT
mlt (M1,i) is Relation-like NAT -defined the carrier of K -valued Function-like V42( len n) FinSequence-like Element of (len n) -tuples_on the carrier of K
(mlt (M1,i)) + (mlt (M2,i)) is Relation-like NAT -defined the carrier of K -valued Function-like V42( len n) FinSequence-like Element of (len n) -tuples_on the carrier of K
len ((mlt (M1,i)) + (mlt (M2,i))) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
Seg (len ((mlt (M1,i)) + (mlt (M2,i)))) is Element of bool NAT
dom ((mlt (M1,i)) + (mlt (M2,i))) is V42( len n) Element of bool NAT
dom n is Element of bool NAT
dom m is Element of bool NAT
dom (mlt (n,k)) is Element of bool NAT
len (mlt (M1,i)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
Seg (len (mlt (M1,i))) is Element of bool NAT
dom (mlt ((n + m),k)) is Element of bool NAT
j is V24() V25() V26() V30() V31() ext-real V35() V40() V109() set
(mlt ((n + m),k)) . j is set
((mlt (n,k)) + (mlt (m,k))) . j is set
rng n is set
rng m is set
rng k is set
rng (n + m) 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 V18([: 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
dom the multF of K is Relation-like set
the multF of K .: ((n + m),k) is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
[:(rng (n + m)),(rng k):] is set
(dom (n + m)) /\ (dom k) is Element of bool NAT
k . j is set
dom (M1 + M2) is V42( len n) Element of bool NAT
(n + m) . j is set
m . j is set
n . j is set
<:m,k:> is Relation-like Function-like set
dom <:m,k:> is set
(dom n) /\ (dom n) is Element of bool NAT
[:m,k:] is Relation-like Function-like set
dom [:m,k:] is set
[:(dom m),(dom k):] is set
[j,j] is set
q2 is Element of the carrier of K
e is Element of the carrier of K
[q2,e] is set
the multF of K * (m,k) is Relation-like Function-like set
dom ( the multF of K * (m,k)) is set
[:m,k:] * the multF of K is Relation-like Function-like set
dom ([:m,k:] * the multF of K) is set
[:m,k:] . (j,j) is set
[:m,k:] . [j,j] is set
q2 * e is Element of the carrier of K
the multF of K . (q2,e) is Element of the carrier of K
the multF of K . [q2,e] is set
( the multF of K * (m,k)) . (j,j) is set
( the multF of K * (m,k)) . [j,j] is set
([:m,k:] * the multF of K) . (j,j) is set
([:m,k:] * the multF of K) . [j,j] is set
the multF of K . ([:m,k:] . (j,j)) is set
the multF of K . ((m . j),(k . j)) is set
[(m . j),(k . j)] is set
the multF of K . [(m . j),(k . j)] is set
<:m,k:> . j is set
the multF of K . (<:m,k:> . j) is set
<:m,k:> * the multF of K is Relation-like Function-like set
(<:m,k:> * the multF of K) . j is set
the multF of K .: (m,k) is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
( the multF of K .: (m,k)) . j is set
(mlt (m,k)) . j is set
<:(n + m),k:> is Relation-like Function-like set
dom <:(n + m),k:> is set
( the multF of K .: ((n + m),k)) . j is set
<:(n + m),k:> * the multF of K is Relation-like Function-like set
(<:(n + m),k:> * the multF of K) . j is set
<:(n + m),k:> . j is set
the multF of K . (<:(n + m),k:> . j) is set
q3 is Element of the carrier of K
q3 * e is Element of the carrier of K
the multF of K . (q3,e) is Element of the carrier of K
[q3,e] is set
the multF of K . [q3,e] is set
<:(mlt (n,k)),(mlt (m,k)):> is Relation-like Function-like set
dom <:(mlt (n,k)),(mlt (m,k)):> is set
(dom (mlt (n,k))) /\ (dom (mlt (m,k))) is Element of bool NAT
<:n,m:> is Relation-like Function-like set
dom <:n,m:> is set
(dom n) /\ (dom m) is Element of bool NAT
the addF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like V18([: 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 .: ((mlt (n,k)),(mlt (m,k))) is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
[:n,k:] is Relation-like Function-like set
dom [:n,k:] is set
[:(dom n),(dom k):] is set
<:n,k:> is Relation-like Function-like set
dom <:n,k:> is set
the addF of K .: (n,m) is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
( the addF of K .: (n,m)) . j is set
<:n,m:> * the addF of K is Relation-like Function-like set
(<:n,m:> * the addF of K) . j is set
<:n,m:> . j is set
the addF of K . (<:n,m:> . j) is set
q1 is Element of the carrier of K
q1 + q2 is Element of the carrier of K
the addF of K . (q1,q2) is Element of the carrier of K
[q1,q2] is set
the addF of K . [q1,q2] is set
[q1,e] is set
the multF of K * (n,k) is Relation-like Function-like set
dom ( the multF of K * (n,k)) is set
[:n,k:] * the multF of K is Relation-like Function-like set
dom ([:n,k:] * the multF of K) is set
[:n,k:] . (j,j) is set
[:n,k:] . [j,j] is set
q1 * e is Element of the carrier of K
the multF of K . (q1,e) is Element of the carrier of K
the multF of K . [q1,e] is set
( the multF of K * (n,k)) . (j,j) is set
( the multF of K * (n,k)) . [j,j] is set
([:n,k:] * the multF of K) . (j,j) is set
([:n,k:] * the multF of K) . [j,j] is set
the multF of K . ([:n,k:] . (j,j)) is set
the multF of K . ((n . j),(k . j)) is set
[(n . j),(k . j)] is set
the multF of K . [(n . j),(k . j)] is set
<:n,k:> . j is set
the multF of K . (<:n,k:> . j) is set
<:n,k:> * the multF of K is Relation-like Function-like set
(<:n,k:> * the multF of K) . j is set
the multF of K .: (n,k) is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
( the multF of K .: (n,k)) . j is set
(mlt (n,k)) . j is set
(q1 * e) + (q2 * e) is Element of the carrier of K
the addF of K . ((q1 * e),(q2 * e)) is Element of the carrier of K
[(q1 * e),(q2 * e)] is set
the addF of K . [(q1 * e),(q2 * e)] is set
<:(mlt (n,k)),(mlt (m,k)):> . j is set
the addF of K . (<:(mlt (n,k)),(mlt (m,k)):> . j) is set
<:(mlt (n,k)),(mlt (m,k)):> * the addF of K is Relation-like Function-like set
(<:(mlt (n,k)),(mlt (m,k)):> * the addF of K) . j is set
mlt ((M1 + M2),i) is Relation-like NAT -defined the carrier of K -valued Function-like V42( len n) FinSequence-like Element of (len n) -tuples_on the carrier of K
len (mlt ((M1 + M2),i)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
Seg (len (mlt ((M1 + M2),i))) is Element of bool NAT
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() doubleLoopStr
the carrier of K is non empty non trivial set
n is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
k is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
len k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
n + m is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
mlt (k,(n + m)) is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
mlt (k,n) is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
mlt (k,m) is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
(mlt (k,n)) + (mlt (k,m)) is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
(len n) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
M1 is Relation-like Function-like V42( len n) Element of (len n) -tuples_on the carrier of K
M2 is Relation-like Function-like V42( len n) Element of (len n) -tuples_on the carrier of K
M1 + M2 is Relation-like NAT -defined the carrier of K -valued Function-like V42( len n) FinSequence-like Element of (len n) -tuples_on the carrier of K
i is Relation-like Function-like V42( len n) Element of (len n) -tuples_on the carrier of K
mlt ((M1 + M2),i) is Relation-like NAT -defined the carrier of K -valued Function-like V42( len n) FinSequence-like Element of (len n) -tuples_on the carrier of K
mlt (M1,i) is Relation-like NAT -defined the carrier of K -valued Function-like V42( len n) FinSequence-like Element of (len n) -tuples_on the carrier of K
mlt (m,k) is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
(mlt (M1,i)) + (mlt (m,k)) is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
mlt (M2,i) is Relation-like NAT -defined the carrier of K -valued Function-like V42( len n) FinSequence-like Element of (len n) -tuples_on the carrier of K
(mlt (k,n)) + (mlt (M2,i)) is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
K is non empty set
K * is functional FinSequence-membered FinSequenceSet of K
n is Relation-like NAT -defined K * -valued Function-like FinSequence-like tabular FinSequence of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
K is V24() V25() V26() V30() V31() ext-real V35() V40() V109() set
n is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() doubleLoopStr
the carrier of n is non empty non trivial set
the carrier of n * is functional FinSequence-membered FinSequenceSet of the carrier of n
k is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like tabular FinSequence of the carrier of n *
width k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
M1 is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like tabular FinSequence of the carrier of n *
width M1 is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
Indices k is set
dom k is Element of bool NAT
Seg (width k) is Element of bool NAT
[:(dom k),(Seg (width k)):] is set
k + M1 is Relation-like NAT -defined the carrier of n * -valued Function-like FinSequence-like tabular FinSequence of the carrier of n *
Line ((k + M1),K) is Relation-like NAT -defined the carrier of n -valued Function-like V42( width (k + M1)) FinSequence-like Element of (width (k + M1)) -tuples_on the carrier of n
width (k + M1) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(width (k + M1)) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
Line (k,K) is Relation-like NAT -defined the carrier of n -valued Function-like V42( width k) FinSequence-like Element of (width k) -tuples_on the carrier of n
(width k) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
Line (M1,K) is Relation-like NAT -defined the carrier of n -valued Function-like V42( width M1) FinSequence-like Element of (width M1) -tuples_on the carrier of n
(width M1) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
(Line (k,K)) + (Line (M1,K)) is Relation-like NAT -defined the carrier of n -valued Function-like FinSequence-like FinSequence of the carrier of n
j is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
[K,j] is set
len k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
Seg (len k) is Element of bool NAT
len (k + M1) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
Indices (k + M1) is set
dom (k + M1) is Element of bool NAT
Seg (width (k + M1)) is Element of bool NAT
[:(dom (k + M1)),(Seg (width (k + M1))):] is set
len (Line ((k + M1),K)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
j is V24() V25() V26() V30() V31() ext-real V35() V40() V109() set
(Line ((k + M1),K)) . j is set
((Line (k,K)) + (Line (M1,K))) . j is set
len (Line (M1,K)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
Seg (len (Line (M1,K))) is Element of bool NAT
dom (Line (M1,K)) is V42( width M1) Element of bool NAT
(Line (M1,K)) . j is set
[K,j] is set
(k + M1) * (K,j) is Element of the carrier of n
k * (K,j) is Element of the carrier of n
M1 * (K,j) is Element of the carrier of n
(k * (K,j)) + (M1 * (K,j)) 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 V18([: the carrier of n, the carrier of n:], the carrier of n) Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[: the carrier of n, the carrier of n:] is set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is set
the addF of n . ((k * (K,j)),(M1 * (K,j))) is Element of the carrier of n
[(k * (K,j)),(M1 * (K,j))] is set
the addF of n . [(k * (K,j)),(M1 * (K,j))] is set
len (Line (k,K)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
Seg (len (Line (k,K))) is Element of bool NAT
dom (Line (k,K)) is V42( width k) Element of bool NAT
(Line (k,K)) . j is set
len ((Line (k,K)) + (Line (M1,K))) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
M2 is Relation-like Function-like V42( width k) Element of (width k) -tuples_on the carrier of n
i is Relation-like Function-like V42( width k) Element of (width k) -tuples_on the carrier of n
M2 + i is Relation-like NAT -defined the carrier of n -valued Function-like V42( width k) FinSequence-like Element of (width k) -tuples_on the carrier of n
len (M2 + i) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
dom ((Line (k,K)) + (Line (M1,K))) is Element of bool NAT
q2 is Element of the carrier of n
q1 is Element of the carrier of n
q2 + q1 is Element of the carrier of n
the addF of n . (q2,q1) is Element of the carrier of n
[q2,q1] is set
the addF of n . [q2,q1] is set
len ((Line (k,K)) + (Line (M1,K))) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
M2 is Relation-like Function-like V42( width k) Element of (width k) -tuples_on the carrier of n
i is Relation-like Function-like V42( width k) Element of (width k) -tuples_on the carrier of n
M2 + i is Relation-like NAT -defined the carrier of n -valued Function-like V42( width k) FinSequence-like Element of (width k) -tuples_on the carrier of n
len (M2 + i) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 V24() V25() V26() V30() V31() ext-real V35() V40() V109() set
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
Indices m is set
dom m is Element of bool NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
Seg (width m) is Element of bool NAT
[:(dom m),(Seg (width m)):] is set
m + k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
Col ((m + k),n) is Relation-like NAT -defined the carrier of K -valued Function-like V42( len (m + k)) FinSequence-like Element of (len (m + k)) -tuples_on the carrier of K
len (m + k) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(len (m + k)) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
Col (m,n) is Relation-like NAT -defined the carrier of K -valued Function-like V42( len m) FinSequence-like Element of (len m) -tuples_on the carrier of K
(len m) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
Col (k,n) is Relation-like NAT -defined the carrier of K -valued Function-like V42( len k) FinSequence-like Element of (len k) -tuples_on the carrier of K
(len k) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
(Col (m,n)) + (Col (k,n)) is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
i is V24() V25() V26() V30() V31() ext-real V35() V40() V109() set
[i,n] is set
width (m + k) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
Indices (m + k) is set
dom (m + k) is Element of bool NAT
Seg (width (m + k)) is Element of bool NAT
[:(dom (m + k)),(Seg (width (m + k))):] is set
len (Col ((m + k),n)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
j is V24() V25() V26() V30() V31() ext-real V35() V40() V109() set
(Col ((m + k),n)) . j is set
((Col (m,n)) + (Col (k,n))) . j is set
Seg (len m) is Element of bool NAT
len (Col (k,n)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
Seg (len (Col (k,n))) is Element of bool NAT
dom (Col (k,n)) is V42( len k) Element of bool NAT
(Col (k,n)) . j is set
dom k is Element of bool NAT
len (Col (m,n)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
Seg (len (Col (m,n))) is Element of bool NAT
dom (Col (m,n)) is V42( len m) Element of bool NAT
(Col (m,n)) . j is set
len ((Col (m,n)) + (Col (k,n))) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
M1 is Relation-like Function-like V42( len m) Element of (len m) -tuples_on the carrier of K
M2 is Relation-like Function-like V42( len m) Element of (len m) -tuples_on the carrier of K
M1 + M2 is Relation-like NAT -defined the carrier of K -valued Function-like V42( len m) FinSequence-like Element of (len m) -tuples_on the carrier of K
len (M1 + M2) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
dom ((Col (m,n)) + (Col (k,n))) is Element of bool NAT
q2 is Element of the carrier of K
q1 is Element of the carrier of K
q2 + q1 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 V18([: 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 . (q2,q1) is Element of the carrier of K
[q2,q1] is set
the addF of K . [q2,q1] is set
[j,n] is set
(m + k) * (j,n) is Element of the carrier of K
m * (j,n) is Element of the carrier of K
k * (j,n) is Element of the carrier of K
(m * (j,n)) + (k * (j,n)) is Element of the carrier of K
the addF of K . ((m * (j,n)),(k * (j,n))) is Element of the carrier of K
[(m * (j,n)),(k * (j,n))] is set
the addF of K . [(m * (j,n)),(k * (j,n))] is set
len ((Col (m,n)) + (Col (k,n))) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
M1 is Relation-like Function-like V42( len m) Element of (len m) -tuples_on the carrier of K
M2 is Relation-like Function-like V42( len m) Element of (len m) -tuples_on the carrier of K
M1 + M2 is Relation-like NAT -defined the carrier of K -valued Function-like V42( len m) FinSequence-like Element of (len m) -tuples_on the carrier of K
len (M1 + M2) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() doubleLoopStr
the carrier of K is non empty non trivial set
n is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
n + m is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
Sum (n + m) is Element of the carrier of K
Sum n is Element of the carrier of K
Sum m is Element of the carrier of K
(Sum n) + (Sum m) 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 V18([: 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 . ((Sum n),(Sum m)) is Element of the carrier of K
[(Sum n),(Sum m)] is set
the addF of K . [(Sum n),(Sum m)] is set
(len n) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
k is Relation-like Function-like V42( len n) Element of (len n) -tuples_on the carrier of K
M1 is Relation-like Function-like V42( len n) Element of (len n) -tuples_on the carrier of K
k + M1 is Relation-like NAT -defined the carrier of K -valued Function-like V42( len n) FinSequence-like Element of (len n) -tuples_on the carrier of K
Sum (k + M1) is Element of the carrier of K
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() doubleLoopStr
the carrier of K is non empty non trivial set
the carrier of K * is functional FinSequence-membered FinSequenceSet of the carrier of K
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
n is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m + k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n * (m + k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n * m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
n * k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(n * m) + (n * k) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len (m + k) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (n * (m + k)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (m + k) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (n * (m + k)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (n * m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (n * m) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
M1 is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular Matrix of len n, width m, the carrier of K
Indices M1 is set
dom M1 is Element of bool NAT
width M1 is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
Seg (width M1) is Element of bool NAT
[:(dom M1),(Seg (width M1)):] is set
Indices (n * m) is set
dom (n * m) is Element of bool NAT
Seg (width (n * m)) is Element of bool NAT
[:(dom (n * m)),(Seg (width (n * m))):] is set
len ((n * m) + (n * k)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width ((n * m) + (n * k)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (n * k) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (n * k) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
Indices (n * k) is set
dom (n * k) is Element of bool NAT
Seg (width (n * k)) is Element of bool NAT
[:(dom (n * k)),(Seg (width (n * k))):] is set
M2 is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular Matrix of len n, width m, the carrier of K
i is V24() V25() V26() V30() V31() ext-real V35() V40() V109() set
j is V24() V25() V26() V30() V31() ext-real V35() V40() V109() set
[i,j] is set
M1 * (i,j) is Element of the carrier of K
M2 * (i,j) is Element of the carrier of K
Line (n,i) is Relation-like NAT -defined the carrier of K -valued Function-like V42( width n) FinSequence-like Element of (width n) -tuples_on the carrier of K
(width n) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
len (Line (n,i)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
Col (m,j) is Relation-like NAT -defined the carrier of K -valued Function-like V42( len m) FinSequence-like Element of (len m) -tuples_on the carrier of K
(len m) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
len (Col (m,j)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
Col (k,j) is Relation-like NAT -defined the carrier of K -valued Function-like V42( len k) FinSequence-like Element of (len k) -tuples_on the carrier of K
(len k) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
mlt ((Line (n,i)),(Col (m,j))) is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
len (mlt ((Line (n,i)),(Col (m,j)))) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
q1 is Relation-like Function-like V42( len m) Element of (len m) -tuples_on the carrier of K
q2 is Relation-like Function-like V42( len m) Element of (len m) -tuples_on the carrier of K
mlt (q1,q2) is Relation-like NAT -defined the carrier of K -valued Function-like V42( len m) FinSequence-like Element of (len m) -tuples_on the carrier of K
len (mlt (q1,q2)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
q3 is Relation-like Function-like V42( len m) Element of (len m) -tuples_on the carrier of K
mlt (q1,q3) is Relation-like NAT -defined the carrier of K -valued Function-like V42( len m) FinSequence-like Element of (len m) -tuples_on the carrier of K
len (mlt (q1,q3)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
mlt ((Line (n,i)),(Col (k,j))) is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
len (mlt ((Line (n,i)),(Col (k,j)))) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
dom m is Element of bool NAT
Seg (len m) is Element of bool NAT
1 + 0 is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (Col (k,j)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(n * m) * (i,j) is Element of the carrier of K
(n * k) * (i,j) is Element of the carrier of K
((n * m) * (i,j)) + ((n * k) * (i,j)) 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 V18([: 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 . (((n * m) * (i,j)),((n * k) * (i,j))) is Element of the carrier of K
[((n * m) * (i,j)),((n * k) * (i,j))] is set
the addF of K . [((n * m) * (i,j)),((n * k) * (i,j))] is set
(Line (n,i)) "*" (Col (m,j)) is Element of the carrier of K
((Line (n,i)) "*" (Col (m,j))) + ((n * k) * (i,j)) is Element of the carrier of K
the addF of K . (((Line (n,i)) "*" (Col (m,j))),((n * k) * (i,j))) is Element of the carrier of K
[((Line (n,i)) "*" (Col (m,j))),((n * k) * (i,j))] is set
the addF of K . [((Line (n,i)) "*" (Col (m,j))),((n * k) * (i,j))] is set
(Line (n,i)) "*" (Col (k,j)) is Element of the carrier of K
((Line (n,i)) "*" (Col (m,j))) + ((Line (n,i)) "*" (Col (k,j))) is Element of the carrier of K
the addF of K . (((Line (n,i)) "*" (Col (m,j))),((Line (n,i)) "*" (Col (k,j)))) is Element of the carrier of K
[((Line (n,i)) "*" (Col (m,j))),((Line (n,i)) "*" (Col (k,j)))] is set
the addF of K . [((Line (n,i)) "*" (Col (m,j))),((Line (n,i)) "*" (Col (k,j)))] is set
Sum (mlt ((Line (n,i)),(Col (k,j)))) is Element of the carrier of K
((Line (n,i)) "*" (Col (m,j))) + (Sum (mlt ((Line (n,i)),(Col (k,j))))) is Element of the carrier of K
the addF of K . (((Line (n,i)) "*" (Col (m,j))),(Sum (mlt ((Line (n,i)),(Col (k,j)))))) is Element of the carrier of K
[((Line (n,i)) "*" (Col (m,j))),(Sum (mlt ((Line (n,i)),(Col (k,j)))))] is set
the addF of K . [((Line (n,i)) "*" (Col (m,j))),(Sum (mlt ((Line (n,i)),(Col (k,j)))))] is set
Sum (mlt ((Line (n,i)),(Col (m,j)))) is Element of the carrier of K
(Sum (mlt ((Line (n,i)),(Col (m,j))))) + (Sum (mlt ((Line (n,i)),(Col (k,j))))) is Element of the carrier of K
the addF of K . ((Sum (mlt ((Line (n,i)),(Col (m,j))))),(Sum (mlt ((Line (n,i)),(Col (k,j)))))) is Element of the carrier of K
[(Sum (mlt ((Line (n,i)),(Col (m,j))))),(Sum (mlt ((Line (n,i)),(Col (k,j)))))] is set
the addF of K . [(Sum (mlt ((Line (n,i)),(Col (m,j))))),(Sum (mlt ((Line (n,i)),(Col (k,j)))))] is set
Seg (width m) is Element of bool NAT
[1,j] is set
Indices m is set
[:(dom m),(Seg (width m)):] is set
Col ((m + k),j) is Relation-like NAT -defined the carrier of K -valued Function-like V42( len (m + k)) FinSequence-like Element of (len (m + k)) -tuples_on the carrier of K
(len (m + k)) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
(Line (n,i)) "*" (Col ((m + k),j)) is Element of the carrier of K
mlt ((Line (n,i)),(Col ((m + k),j))) is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
Sum (mlt ((Line (n,i)),(Col ((m + k),j)))) is Element of the carrier of K
(Col (m,j)) + (Col (k,j)) is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
mlt ((Line (n,i)),((Col (m,j)) + (Col (k,j)))) is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
Sum (mlt ((Line (n,i)),((Col (m,j)) + (Col (k,j))))) is Element of the carrier of K
(mlt ((Line (n,i)),(Col (m,j)))) + (mlt ((Line (n,i)),(Col (k,j)))) is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
Sum ((mlt ((Line (n,i)),(Col (m,j)))) + (mlt ((Line (n,i)),(Col (k,j))))) is Element of the carrier of K
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() doubleLoopStr
the carrier of K is non empty non trivial set
the carrier of K * is functional FinSequence-membered FinSequenceSet of the carrier of K
m is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
n is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
len n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m + k is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(m + k) * n is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
m * n is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
k * n is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
(m * n) + (k * n) is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
width (m + k) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width ((m + k) * n) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width n is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (m + k) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len ((m + k) * n) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (m * n) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (m * n) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
M1 is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular Matrix of len m, width n, the carrier of K
Indices M1 is set
dom M1 is Element of bool NAT
width M1 is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
Seg (width M1) is Element of bool NAT
[:(dom M1),(Seg (width M1)):] is set
Indices (m * n) is set
dom (m * n) is Element of bool NAT
Seg (width (m * n)) is Element of bool NAT
[:(dom (m * n)),(Seg (width (m * n))):] is set
len ((m * n) + (k * n)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width ((m * n) + (k * n)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (k * n) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (k * n) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
Indices (k * n) is set
dom (k * n) is Element of bool NAT
Seg (width (k * n)) is Element of bool NAT
[:(dom (k * n)),(Seg (width (k * n))):] is set
M2 is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular Matrix of len m, width n, the carrier of K
i is V24() V25() V26() V30() V31() ext-real V35() V40() V109() set
j is V24() V25() V26() V30() V31() ext-real V35() V40() V109() set
[i,j] is set
M1 * (i,j) is Element of the carrier of K
M2 * (i,j) is Element of the carrier of K
Col (n,j) is Relation-like NAT -defined the carrier of K -valued Function-like V42( len n) FinSequence-like Element of (len n) -tuples_on the carrier of K
(len n) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
len (Col (n,j)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
Line (m,i) is Relation-like NAT -defined the carrier of K -valued Function-like V42( width m) FinSequence-like Element of (width m) -tuples_on the carrier of K
(width m) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
len (Line (m,i)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
Line (k,i) is Relation-like NAT -defined the carrier of K -valued Function-like V42( width k) FinSequence-like Element of (width k) -tuples_on the carrier of K
(width k) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
mlt ((Line (m,i)),(Col (n,j))) is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
len (mlt ((Line (m,i)),(Col (n,j)))) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
q1 is Relation-like Function-like V42( len n) Element of (len n) -tuples_on the carrier of K
q3 is Relation-like Function-like V42( len n) Element of (len n) -tuples_on the carrier of K
mlt (q1,q3) is Relation-like NAT -defined the carrier of K -valued Function-like V42( len n) FinSequence-like Element of (len n) -tuples_on the carrier of K
len (mlt (q1,q3)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
q2 is Relation-like Function-like V42( len n) Element of (len n) -tuples_on the carrier of K
mlt (q2,q3) is Relation-like NAT -defined the carrier of K -valued Function-like V42( len n) FinSequence-like Element of (len n) -tuples_on the carrier of K
len (mlt (q2,q3)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
mlt ((Line (k,i)),(Col (n,j))) is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
len (mlt ((Line (k,i)),(Col (n,j)))) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
1 + 0 is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
Seg (width m) is Element of bool NAT
len (Line (k,i)) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
(m * n) * (i,j) is Element of the carrier of K
(k * n) * (i,j) is Element of the carrier of K
((m * n) * (i,j)) + ((k * n) * (i,j)) 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 V18([: 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 * n) * (i,j)),((k * n) * (i,j))) is Element of the carrier of K
[((m * n) * (i,j)),((k * n) * (i,j))] is set
the addF of K . [((m * n) * (i,j)),((k * n) * (i,j))] is set
(Line (m,i)) "*" (Col (n,j)) is Element of the carrier of K
((Line (m,i)) "*" (Col (n,j))) + ((k * n) * (i,j)) is Element of the carrier of K
the addF of K . (((Line (m,i)) "*" (Col (n,j))),((k * n) * (i,j))) is Element of the carrier of K
[((Line (m,i)) "*" (Col (n,j))),((k * n) * (i,j))] is set
the addF of K . [((Line (m,i)) "*" (Col (n,j))),((k * n) * (i,j))] is set
(Line (k,i)) "*" (Col (n,j)) is Element of the carrier of K
((Line (m,i)) "*" (Col (n,j))) + ((Line (k,i)) "*" (Col (n,j))) is Element of the carrier of K
the addF of K . (((Line (m,i)) "*" (Col (n,j))),((Line (k,i)) "*" (Col (n,j)))) is Element of the carrier of K
[((Line (m,i)) "*" (Col (n,j))),((Line (k,i)) "*" (Col (n,j)))] is set
the addF of K . [((Line (m,i)) "*" (Col (n,j))),((Line (k,i)) "*" (Col (n,j)))] is set
Sum (mlt ((Line (k,i)),(Col (n,j)))) is Element of the carrier of K
((Line (m,i)) "*" (Col (n,j))) + (Sum (mlt ((Line (k,i)),(Col (n,j))))) is Element of the carrier of K
the addF of K . (((Line (m,i)) "*" (Col (n,j))),(Sum (mlt ((Line (k,i)),(Col (n,j)))))) is Element of the carrier of K
[((Line (m,i)) "*" (Col (n,j))),(Sum (mlt ((Line (k,i)),(Col (n,j)))))] is set
the addF of K . [((Line (m,i)) "*" (Col (n,j))),(Sum (mlt ((Line (k,i)),(Col (n,j)))))] is set
Sum (mlt ((Line (m,i)),(Col (n,j)))) is Element of the carrier of K
(Sum (mlt ((Line (m,i)),(Col (n,j))))) + (Sum (mlt ((Line (k,i)),(Col (n,j))))) is Element of the carrier of K
the addF of K . ((Sum (mlt ((Line (m,i)),(Col (n,j))))),(Sum (mlt ((Line (k,i)),(Col (n,j)))))) is Element of the carrier of K
[(Sum (mlt ((Line (m,i)),(Col (n,j))))),(Sum (mlt ((Line (k,i)),(Col (n,j)))))] is set
the addF of K . [(Sum (mlt ((Line (m,i)),(Col (n,j))))),(Sum (mlt ((Line (k,i)),(Col (n,j)))))] is set
Seg (len m) is Element of bool NAT
dom m is Element of bool NAT
[i,1] is set
Indices m is set
[:(dom m),(Seg (width m)):] is set
Line ((m + k),i) is Relation-like NAT -defined the carrier of K -valued Function-like V42( width (m + k)) FinSequence-like Element of (width (m + k)) -tuples_on the carrier of K
(width (m + k)) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
(Line ((m + k),i)) "*" (Col (n,j)) is Element of the carrier of K
mlt ((Line ((m + k),i)),(Col (n,j))) is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
Sum (mlt ((Line ((m + k),i)),(Col (n,j)))) is Element of the carrier of K
(Line (m,i)) + (Line (k,i)) is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
mlt (((Line (m,i)) + (Line (k,i))),(Col (n,j))) is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
Sum (mlt (((Line (m,i)) + (Line (k,i))),(Col (n,j)))) is Element of the carrier of K
(mlt ((Line (m,i)),(Col (n,j)))) + (mlt ((Line (k,i)),(Col (n,j)))) is Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like FinSequence of the carrier of K
Sum ((mlt ((Line (m,i)),(Col (n,j)))) + (mlt ((Line (k,i)),(Col (n,j))))) is Element of the carrier of K
K is non empty non degenerated non trivial right_complementable almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() 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 V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
m is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
k is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
M1 is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular Matrix of n,m, the carrier of K
width M1 is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len M1 is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
M2 is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular Matrix of m,k, the carrier of K
len M2 is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
M1 * M2 is Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like tabular FinSequence of the carrier of K *
width M2 is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
len (M1 * M2) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT
width (M1 * M2) is V24() V25() V26() V30() V31() ext-real V35() V40() V109() Element of NAT