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