REAL is set
NAT is non empty non trivial V34() V35() V36() V48() V53() V54() Element of bool REAL
bool REAL is non empty cup-closed diff-closed preBoolean set
{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V34() V35() V36() V38() V39() V40() V41() ext-real non positive non negative V45() V48() V49() V52() V53() V55( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set
COMPLEX is set
NAT is non empty non trivial V34() V35() V36() V48() V53() V54() set
bool NAT is non empty non trivial cup-closed diff-closed preBoolean V48() set
bool NAT is non empty non trivial cup-closed diff-closed preBoolean V48() set
Fin NAT is non empty cup-closed diff-closed preBoolean set
1 is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V48() V53() Element of NAT
[:1,1:] is Relation-like non empty V48() set
bool [:1,1:] is non empty cup-closed diff-closed preBoolean V48() V52() set
[:[:1,1:],1:] is Relation-like non empty V48() set
bool [:[:1,1:],1:] is non empty cup-closed diff-closed preBoolean V48() V52() set
2 is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V48() V53() Element of NAT
{{},1} is non empty V48() V52() set
3 is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V48() V53() Element of NAT
0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V34() V35() V36() V38() V39() V40() V41() ext-real non positive non negative V45() V48() V49() V52() V53() V55( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT
Seg 1 is non empty trivial V48() V55(1) Element of bool NAT
{1} is non empty trivial V48() V52() V55(1) set
Seg 2 is non empty V48() V55(2) Element of bool NAT
{1,2} is non empty V48() V52() set
[1,1] is V23() set
Permutations 1 is non empty permutational set
idseq 1 is Relation-like NAT -defined Function-like constant non empty trivial V48() V55(1) FinSequence-like FinSubsequence-like set
id (Seg 1) is Relation-like Seg 1 -defined Seg 1 -valued V6() V8() V9() V13() Function-like one-to-one non empty total V26( Seg 1, Seg 1) V27( Seg 1) V28( Seg 1, Seg 1) V48() Element of bool [:(Seg 1),(Seg 1):]
[:(Seg 1),(Seg 1):] is Relation-like non empty V48() set
bool [:(Seg 1),(Seg 1):] is non empty cup-closed diff-closed preBoolean V48() V52() set
{(idseq 1)} is functional non empty trivial V48() V52() V55(1) set
M is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
n is non empty non degenerated non trivial right_complementable almost_left_invertible V111() V123() associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V144() left_unital doubleLoopStr
the carrier of n is non empty non trivial set
M -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b1 where b1 is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b1 = M } is set
K is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
0. n is V68(n) Element of the carrier of n
M |-> (0. n) is Relation-like NAT -defined the carrier of n -valued Function-like V48() V55(M) FinSequence-like FinSubsequence-like Element of M -tuples_on the carrier of n
Seg M is V48() V55(M) Element of bool NAT
(Seg M) --> (0. n) is Relation-like Seg M -defined {(0. n)} -valued Function-like total V26( Seg M,{(0. n)}) V48() FinSequence-like FinSubsequence-like Element of bool [:(Seg M),{(0. n)}:]
{(0. n)} is non empty trivial V48() V55(1) set
[:(Seg M),{(0. n)}:] is Relation-like V48() set
bool [:(Seg M),{(0. n)}:] is non empty cup-closed diff-closed preBoolean V48() V52() set
K |-> (M |-> (0. n)) is Relation-like NAT -defined M -tuples_on the carrier of n -valued Function-like V48() V55(K) FinSequence-like FinSubsequence-like Element of K -tuples_on (M -tuples_on the carrier of n)
K -tuples_on (M -tuples_on the carrier of n) is functional non empty FinSequence-membered FinSequenceSet of M -tuples_on the carrier of n
(M -tuples_on the carrier of n) * is functional non empty FinSequence-membered FinSequenceSet of M -tuples_on the carrier of n
{ b1 where b1 is Relation-like NAT -defined M -tuples_on the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like Element of (M -tuples_on the carrier of n) * : len b1 = K } is set
Seg K is V48() V55(K) Element of bool NAT
(Seg K) --> (M |-> (0. n)) is Relation-like Seg K -defined {(M |-> (0. n))} -valued Function-like total V26( Seg K,{(M |-> (0. n))}) V48() FinSequence-like FinSubsequence-like Element of bool [:(Seg K),{(M |-> (0. n))}:]
{(M |-> (0. n))} is functional non empty trivial V48() V52() V55(1) set
[:(Seg K),{(M |-> (0. n))}:] is Relation-like V48() set
bool [:(Seg K),{(M |-> (0. n))}:] is non empty cup-closed diff-closed preBoolean V48() V52() set
n is non empty non degenerated non trivial right_complementable almost_left_invertible V111() V123() associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V144() left_unital doubleLoopStr
the carrier of n is non empty non trivial set
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
K is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
len K is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
width K is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Indices K is set
dom K is V48() Element of bool NAT
Seg (width K) is V48() V55( width K) Element of bool NAT
[:(dom K),(Seg (width K)):] is Relation-like V48() set
p1 is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular Matrix of len K, width K, the carrier of n
Indices p1 is set
dom p1 is V48() Element of bool NAT
width p1 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Seg (width p1) is V48() V55( width p1) Element of bool NAT
[:(dom p1),(Seg (width p1)):] is Relation-like V48() set
p2 is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular Matrix of len K, width K, the carrier of n
Indices p2 is set
dom p2 is V48() Element of bool NAT
width p2 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Seg (width p2) is V48() V55( width p2) Element of bool NAT
[:(dom p2),(Seg (width p2)):] is Relation-like V48() set
Seg (len K) is V48() V55( len K) Element of bool NAT
[:(Seg (len K)),(Seg (width K)):] is Relation-like V48() set
len p1 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
len p1 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
len p1 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
len p1 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
i is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
len i is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
width i is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
p is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
i is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
[p,i] is V23() set
i * (p,i) is Element of the carrier of n
K * (p,i) is Element of the carrier of n
- (K * (p,i)) is Element of the carrier of n
M is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
len M is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
width M is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
p1 is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
len p1 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
width p1 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
i is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular Matrix of len K, width K, the carrier of n
Indices i is set
dom i is V48() Element of bool NAT
width i is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Seg (width i) is V48() V55( width i) Element of bool NAT
[:(dom i),(Seg (width i)):] is Relation-like V48() set
Seg (len K) is V48() V55( len K) Element of bool NAT
[:(Seg (len K)),(Seg (width K)):] is Relation-like V48() set
p is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular Matrix of len K, width K, the carrier of n
Indices p is set
dom p is V48() Element of bool NAT
width p is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Seg (width p) is V48() V55( width p) Element of bool NAT
[:(dom p),(Seg (width p)):] is Relation-like V48() set
[:(Seg (len K)),(Seg (width p)):] is Relation-like V48() set
i is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular Matrix of len K, width K, the carrier of n
Indices i is set
dom i is V48() Element of bool NAT
width i is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Seg (width i) is V48() V55( width i) Element of bool NAT
[:(dom i),(Seg (width i)):] is Relation-like V48() set
[:(Seg (len K)),(Seg (width i)):] is Relation-like V48() set
len p is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
len i is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
j is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
c10 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
[j,c10] is V23() set
p * (j,c10) is Element of the carrier of n
K * (j,c10) is Element of the carrier of n
- (K * (j,c10)) is Element of the carrier of n
i * (j,c10) is Element of the carrier of n
n is non empty non degenerated non trivial right_complementable almost_left_invertible V111() V123() associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V144() left_unital doubleLoopStr
the carrier of n is non empty non trivial set
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
K is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
len K is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
width K is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Indices K is set
dom K is V48() Element of bool NAT
Seg (width K) is V48() V55( width K) Element of bool NAT
[:(dom K),(Seg (width K)):] is Relation-like V48() set
M is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
i is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular Matrix of len K, width K, the carrier of n
Indices i is set
dom i is V48() Element of bool NAT
width i is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Seg (width i) is V48() V55( width i) Element of bool NAT
[:(dom i),(Seg (width i)):] is Relation-like V48() set
p2 is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular Matrix of len K, width K, the carrier of n
Indices p2 is set
dom p2 is V48() Element of bool NAT
width p2 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Seg (width p2) is V48() V55( width p2) Element of bool NAT
[:(dom p2),(Seg (width p2)):] is Relation-like V48() set
Seg (len K) is V48() V55( len K) Element of bool NAT
[:(Seg (len K)),(Seg (width K)):] is Relation-like V48() set
len i is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
len i is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
len i is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
len i is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
p is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
len p is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
width p is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
i is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
j is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
[i,j] is V23() set
p * (i,j) is Element of the carrier of n
K * (i,j) is Element of the carrier of n
M * (i,j) is Element of the carrier of n
(K * (i,j)) + (M * (i,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 non empty total V26([: the carrier of n, the carrier of n:], the carrier of n) commutative associative Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[: the carrier of n, the carrier of n:] is Relation-like non empty set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like non empty set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty cup-closed diff-closed preBoolean set
the addF of n . ((K * (i,j)),(M * (i,j))) is Element of the carrier of n
[(K * (i,j)),(M * (i,j))] is V23() set
the addF of n . [(K * (i,j)),(M * (i,j))] is set
p2 is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
len p2 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
width p2 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
i is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
len i is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
width i is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
j is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular Matrix of len K, width K, the carrier of n
Indices j is set
dom j is V48() Element of bool NAT
width j is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Seg (width j) is V48() V55( width j) Element of bool NAT
[:(dom j),(Seg (width j)):] is Relation-like V48() set
Seg (len K) is V48() V55( len K) Element of bool NAT
[:(Seg (len K)),(Seg (width K)):] is Relation-like V48() set
i is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular Matrix of len K, width K, the carrier of n
Indices i is set
dom i is V48() Element of bool NAT
width i is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Seg (width i) is V48() V55( width i) Element of bool NAT
[:(dom i),(Seg (width i)):] is Relation-like V48() set
[:(Seg (len K)),(Seg (width i)):] is Relation-like V48() set
p is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular Matrix of len K, width K, the carrier of n
Indices p is set
dom p is V48() Element of bool NAT
width p is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Seg (width p) is V48() V55( width p) Element of bool NAT
[:(dom p),(Seg (width p)):] is Relation-like V48() set
[:(Seg (len K)),(Seg (width p)):] is Relation-like V48() set
len i is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
len p is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
c10 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
h is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
[c10,h] is V23() set
i * (c10,h) is Element of the carrier of n
K * (c10,h) is Element of the carrier of n
M * (c10,h) is Element of the carrier of n
(K * (c10,h)) + (M * (c10,h)) 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 non empty total V26([: the carrier of n, the carrier of n:], the carrier of n) commutative associative Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[: the carrier of n, the carrier of n:] is Relation-like non empty set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like non empty set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty cup-closed diff-closed preBoolean set
the addF of n . ((K * (c10,h)),(M * (c10,h))) is Element of the carrier of n
[(K * (c10,h)),(M * (c10,h))] is V23() set
the addF of n . [(K * (c10,h)),(M * (c10,h))] is set
p * (c10,h) is Element of the carrier of n
n is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
K is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
M is non empty non degenerated non trivial right_complementable almost_left_invertible V111() V123() associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V144() left_unital doubleLoopStr
(M,n,K) is Relation-like NAT -defined the carrier of M * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular Matrix of n,K, the carrier of M
the carrier of M is non empty non trivial set
the carrier of M * is functional non empty FinSequence-membered FinSequenceSet of the carrier of M
K -tuples_on the carrier of M is functional non empty FinSequence-membered FinSequenceSet of the carrier of M
{ b1 where b1 is Relation-like NAT -defined the carrier of M -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of M * : len b1 = K } is set
0. M is V68(M) Element of the carrier of M
K |-> (0. M) is Relation-like NAT -defined the carrier of M -valued Function-like V48() V55(K) FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of M
Seg K is V48() V55(K) Element of bool NAT
(Seg K) --> (0. M) is Relation-like Seg K -defined {(0. M)} -valued Function-like total V26( Seg K,{(0. M)}) V48() FinSequence-like FinSubsequence-like Element of bool [:(Seg K),{(0. M)}:]
{(0. M)} is non empty trivial V48() V55(1) set
[:(Seg K),{(0. M)}:] is Relation-like V48() set
bool [:(Seg K),{(0. M)}:] is non empty cup-closed diff-closed preBoolean V48() V52() set
n |-> (K |-> (0. M)) is Relation-like NAT -defined K -tuples_on the carrier of M -valued Function-like V48() V55(n) FinSequence-like FinSubsequence-like Element of n -tuples_on (K -tuples_on the carrier of M)
n -tuples_on (K -tuples_on the carrier of M) is functional non empty FinSequence-membered FinSequenceSet of K -tuples_on the carrier of M
(K -tuples_on the carrier of M) * is functional non empty FinSequence-membered FinSequenceSet of K -tuples_on the carrier of M
{ b1 where b1 is Relation-like NAT -defined K -tuples_on the carrier of M -valued Function-like V48() FinSequence-like FinSubsequence-like Element of (K -tuples_on the carrier of M) * : len b1 = n } is set
Seg n is V48() V55(n) Element of bool NAT
(Seg n) --> (K |-> (0. M)) is Relation-like Seg n -defined {(K |-> (0. M))} -valued Function-like total V26( Seg n,{(K |-> (0. M))}) V48() FinSequence-like FinSubsequence-like Element of bool [:(Seg n),{(K |-> (0. M))}:]
{(K |-> (0. M))} is functional non empty trivial V48() V52() V55(1) set
[:(Seg n),{(K |-> (0. M))}:] is Relation-like V48() set
bool [:(Seg n),{(K |-> (0. M))}:] is non empty cup-closed diff-closed preBoolean V48() V52() set
Indices (M,n,K) is set
dom (M,n,K) is V48() Element of bool NAT
width (M,n,K) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Seg (width (M,n,K)) is V48() V55( width (M,n,K)) Element of bool NAT
[:(dom (M,n,K)),(Seg (width (M,n,K))):] is Relation-like V48() set
p1 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
p2 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
[p1,p2] is V23() set
(M,n,K) * (p1,p2) is Element of the carrier of M
[:(Seg n),(Seg (width (M,n,K))):] is Relation-like V48() set
[:(Seg n),(Seg K):] is Relation-like V48() set
i is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
i |-> (0. M) is Relation-like NAT -defined the carrier of M -valued Function-like V48() V55(i) FinSequence-like FinSubsequence-like Element of i -tuples_on the carrier of M
i -tuples_on the carrier of M is functional non empty FinSequence-membered FinSequenceSet of the carrier of M
{ b1 where b1 is Relation-like NAT -defined the carrier of M -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of M * : len b1 = i } is set
Seg i is V48() V55(i) Element of bool NAT
(Seg i) --> (0. M) is Relation-like Seg i -defined {(0. M)} -valued Function-like total V26( Seg i,{(0. M)}) V48() FinSequence-like FinSubsequence-like Element of bool [:(Seg i),{(0. M)}:]
[:(Seg i),{(0. M)}:] is Relation-like V48() set
bool [:(Seg i),{(0. M)}:] is non empty cup-closed diff-closed preBoolean V48() V52() set
(i |-> (0. M)) . p2 is set
(M,n,K) . p1 is Relation-like NAT -defined Function-like V48() FinSequence-like FinSubsequence-like set
n is non empty non degenerated non trivial right_complementable almost_left_invertible V111() V123() associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V144() left_unital doubleLoopStr
the carrier of n is non empty non trivial set
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
K is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
len K is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
M is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
len M is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
width K is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
width M is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
(n,K,M) is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
(n,M,K) is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
width (n,K,M) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
width (n,M,K) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
len (n,K,M) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
dom K is V48() Element of bool NAT
dom (n,K,M) is V48() Element of bool NAT
Indices K is set
Seg (width K) is V48() V55( width K) Element of bool NAT
[:(dom K),(Seg (width K)):] is Relation-like V48() set
Indices (n,K,M) is set
Seg (width (n,K,M)) is V48() V55( width (n,K,M)) Element of bool NAT
[:(dom (n,K,M)),(Seg (width (n,K,M))):] is Relation-like V48() set
dom M is V48() Element of bool NAT
Indices M is set
Seg (width M) is V48() V55( width M) Element of bool NAT
[:(dom M),(Seg (width M)):] is Relation-like V48() set
p1 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
p2 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
[p1,p2] is V23() set
(n,K,M) * (p1,p2) is Element of the carrier of n
M * (p1,p2) is Element of the carrier of n
K * (p1,p2) is Element of the carrier of n
(M * (p1,p2)) + (K * (p1,p2)) 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 non empty total V26([: the carrier of n, the carrier of n:], the carrier of n) commutative associative Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[: the carrier of n, the carrier of n:] is Relation-like non empty set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like non empty set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty cup-closed diff-closed preBoolean set
the addF of n . ((M * (p1,p2)),(K * (p1,p2))) is Element of the carrier of n
[(M * (p1,p2)),(K * (p1,p2))] is V23() set
the addF of n . [(M * (p1,p2)),(K * (p1,p2))] is set
(n,M,K) * (p1,p2) is Element of the carrier of n
len (n,M,K) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
n is non empty non degenerated non trivial right_complementable almost_left_invertible V111() V123() associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V144() left_unital doubleLoopStr
the carrier of n is non empty non trivial set
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
K is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
len K is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
M is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
len M is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
width K is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
width M is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
(n,K,M) is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
p1 is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
(n,(n,K,M),p1) is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
(n,M,p1) is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
(n,K,(n,M,p1)) is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
dom K is V48() Element of bool NAT
dom M is V48() Element of bool NAT
Indices M is set
Seg (width M) is V48() V55( width M) Element of bool NAT
[:(dom M),(Seg (width M)):] is Relation-like V48() set
Seg (width K) is V48() V55( width K) Element of bool NAT
[:(dom K),(Seg (width K)):] is Relation-like V48() set
Indices K is set
width (n,(n,K,M),p1) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
width (n,K,M) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
len (n,K,(n,M,p1)) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
width (n,K,(n,M,p1)) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
len (n,K,M) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
len (n,(n,K,M),p1) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
dom (n,(n,K,M),p1) is V48() Element of bool NAT
Indices (n,(n,K,M),p1) is set
Seg (width (n,(n,K,M),p1)) is V48() V55( width (n,(n,K,M),p1)) Element of bool NAT
[:(dom (n,(n,K,M),p1)),(Seg (width (n,(n,K,M),p1))):] is Relation-like V48() set
dom (n,K,M) is V48() Element of bool NAT
Indices (n,K,M) is set
Seg (width (n,K,M)) is V48() V55( width (n,K,M)) Element of bool NAT
[:(dom (n,K,M)),(Seg (width (n,K,M))):] is Relation-like V48() set
p2 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
i is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
[p2,i] is V23() set
(n,(n,K,M),p1) * (p2,i) is Element of the carrier of n
(n,K,M) * (p2,i) is Element of the carrier of n
p1 * (p2,i) is Element of the carrier of n
((n,K,M) * (p2,i)) + (p1 * (p2,i)) 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 non empty total V26([: the carrier of n, the carrier of n:], the carrier of n) commutative associative Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[: the carrier of n, the carrier of n:] is Relation-like non empty set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like non empty set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty cup-closed diff-closed preBoolean set
the addF of n . (((n,K,M) * (p2,i)),(p1 * (p2,i))) is Element of the carrier of n
[((n,K,M) * (p2,i)),(p1 * (p2,i))] is V23() set
the addF of n . [((n,K,M) * (p2,i)),(p1 * (p2,i))] is set
K * (p2,i) is Element of the carrier of n
M * (p2,i) is Element of the carrier of n
(K * (p2,i)) + (M * (p2,i)) is Element of the carrier of n
the addF of n . ((K * (p2,i)),(M * (p2,i))) is Element of the carrier of n
[(K * (p2,i)),(M * (p2,i))] is V23() set
the addF of n . [(K * (p2,i)),(M * (p2,i))] is set
((K * (p2,i)) + (M * (p2,i))) + (p1 * (p2,i)) is Element of the carrier of n
the addF of n . (((K * (p2,i)) + (M * (p2,i))),(p1 * (p2,i))) is Element of the carrier of n
[((K * (p2,i)) + (M * (p2,i))),(p1 * (p2,i))] is V23() set
the addF of n . [((K * (p2,i)) + (M * (p2,i))),(p1 * (p2,i))] is set
(M * (p2,i)) + (p1 * (p2,i)) is Element of the carrier of n
the addF of n . ((M * (p2,i)),(p1 * (p2,i))) is Element of the carrier of n
[(M * (p2,i)),(p1 * (p2,i))] is V23() set
the addF of n . [(M * (p2,i)),(p1 * (p2,i))] is set
(K * (p2,i)) + ((M * (p2,i)) + (p1 * (p2,i))) is Element of the carrier of n
the addF of n . ((K * (p2,i)),((M * (p2,i)) + (p1 * (p2,i)))) is Element of the carrier of n
[(K * (p2,i)),((M * (p2,i)) + (p1 * (p2,i)))] is V23() set
the addF of n . [(K * (p2,i)),((M * (p2,i)) + (p1 * (p2,i)))] is set
(n,M,p1) * (p2,i) is Element of the carrier of n
(K * (p2,i)) + ((n,M,p1) * (p2,i)) is Element of the carrier of n
the addF of n . ((K * (p2,i)),((n,M,p1) * (p2,i))) is Element of the carrier of n
[(K * (p2,i)),((n,M,p1) * (p2,i))] is V23() set
the addF of n . [(K * (p2,i)),((n,M,p1) * (p2,i))] is set
(n,K,(n,M,p1)) * (p2,i) is Element of the carrier of n
n is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
K is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
M is non empty non degenerated non trivial right_complementable almost_left_invertible V111() V123() associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V144() left_unital doubleLoopStr
the carrier of M is non empty non trivial set
the carrier of M * is functional non empty FinSequence-membered FinSequenceSet of the carrier of M
(M,n,K) is Relation-like NAT -defined the carrier of M * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular Matrix of n,K, the carrier of M
K -tuples_on the carrier of M is functional non empty FinSequence-membered FinSequenceSet of the carrier of M
{ b1 where b1 is Relation-like NAT -defined the carrier of M -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of M * : len b1 = K } is set
0. M is V68(M) Element of the carrier of M
K |-> (0. M) is Relation-like NAT -defined the carrier of M -valued Function-like V48() V55(K) FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of M
Seg K is V48() V55(K) Element of bool NAT
(Seg K) --> (0. M) is Relation-like Seg K -defined {(0. M)} -valued Function-like total V26( Seg K,{(0. M)}) V48() FinSequence-like FinSubsequence-like Element of bool [:(Seg K),{(0. M)}:]
{(0. M)} is non empty trivial V48() V55(1) set
[:(Seg K),{(0. M)}:] is Relation-like V48() set
bool [:(Seg K),{(0. M)}:] is non empty cup-closed diff-closed preBoolean V48() V52() set
n |-> (K |-> (0. M)) is Relation-like NAT -defined K -tuples_on the carrier of M -valued Function-like V48() V55(n) FinSequence-like FinSubsequence-like Element of n -tuples_on (K -tuples_on the carrier of M)
n -tuples_on (K -tuples_on the carrier of M) is functional non empty FinSequence-membered FinSequenceSet of K -tuples_on the carrier of M
(K -tuples_on the carrier of M) * is functional non empty FinSequence-membered FinSequenceSet of K -tuples_on the carrier of M
{ b1 where b1 is Relation-like NAT -defined K -tuples_on the carrier of M -valued Function-like V48() FinSequence-like FinSubsequence-like Element of (K -tuples_on the carrier of M) * : len b1 = n } is set
Seg n is V48() V55(n) Element of bool NAT
(Seg n) --> (K |-> (0. M)) is Relation-like Seg n -defined {(K |-> (0. M))} -valued Function-like total V26( Seg n,{(K |-> (0. M))}) V48() FinSequence-like FinSubsequence-like Element of bool [:(Seg n),{(K |-> (0. M))}:]
{(K |-> (0. M))} is functional non empty trivial V48() V52() V55(1) set
[:(Seg n),{(K |-> (0. M))}:] is Relation-like V48() set
bool [:(Seg n),{(K |-> (0. M))}:] is non empty cup-closed diff-closed preBoolean V48() V52() set
p1 is Relation-like NAT -defined the carrier of M * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular Matrix of n,K, the carrier of M
(M,p1,(M,n,K)) is Relation-like NAT -defined the carrier of M * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of M *
width p1 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
width (M,p1,(M,n,K)) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Indices p1 is set
dom p1 is V48() Element of bool NAT
Seg (width p1) is V48() V55( width p1) Element of bool NAT
[:(dom p1),(Seg (width p1)):] is Relation-like V48() set
[:(Seg n),(Seg K):] is Relation-like V48() set
len p1 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
len (M,p1,(M,n,K)) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
dom (M,p1,(M,n,K)) is V48() Element of bool NAT
Indices (M,p1,(M,n,K)) is set
Seg (width (M,p1,(M,n,K))) is V48() V55( width (M,p1,(M,n,K))) Element of bool NAT
[:(dom (M,p1,(M,n,K))),(Seg (width (M,p1,(M,n,K)))):] is Relation-like V48() set
Indices (M,n,K) is set
dom (M,n,K) is V48() Element of bool NAT
width (M,n,K) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Seg (width (M,n,K)) is V48() V55( width (M,n,K)) Element of bool NAT
[:(dom (M,n,K)),(Seg (width (M,n,K))):] is Relation-like V48() set
p2 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
i is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
[p2,i] is V23() set
(M,p1,(M,n,K)) * (p2,i) is Element of the carrier of M
p1 * (p2,i) is Element of the carrier of M
(M,n,K) * (p2,i) is Element of the carrier of M
(p1 * (p2,i)) + ((M,n,K) * (p2,i)) is Element of the carrier of M
the addF of M is Relation-like [: the carrier of M, the carrier of M:] -defined the carrier of M -valued Function-like non empty total V26([: the carrier of M, the carrier of M:], the carrier of M) commutative associative Element of bool [:[: the carrier of M, the carrier of M:], the carrier of M:]
[: the carrier of M, the carrier of M:] is Relation-like non empty set
[:[: the carrier of M, the carrier of M:], the carrier of M:] is Relation-like non empty set
bool [:[: the carrier of M, the carrier of M:], the carrier of M:] is non empty cup-closed diff-closed preBoolean set
the addF of M . ((p1 * (p2,i)),((M,n,K) * (p2,i))) is Element of the carrier of M
[(p1 * (p2,i)),((M,n,K) * (p2,i))] is V23() set
the addF of M . [(p1 * (p2,i)),((M,n,K) * (p2,i))] is set
(p1 * (p2,i)) + (0. M) is Element of the carrier of M
the addF of M . ((p1 * (p2,i)),(0. M)) is Element of the carrier of M
[(p1 * (p2,i)),(0. M)] is V23() set
the addF of M . [(p1 * (p2,i)),(0. M)] is set
width p1 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
width (M,p1,(M,n,K)) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
len p1 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
len (M,p1,(M,n,K)) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
dom p1 is V48() Element of bool NAT
dom (M,p1,(M,n,K)) is V48() Element of bool NAT
Indices p1 is set
Seg (width p1) is V48() V55( width p1) Element of bool NAT
[:(dom p1),(Seg (width p1)):] is Relation-like V48() set
Indices (M,p1,(M,n,K)) is set
Seg (width (M,p1,(M,n,K))) is V48() V55( width (M,p1,(M,n,K))) Element of bool NAT
[:(dom (M,p1,(M,n,K))),(Seg (width (M,p1,(M,n,K)))):] is Relation-like V48() set
p2 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
i is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
[p2,i] is V23() set
(M,p1,(M,n,K)) * (p2,i) is Element of the carrier of M
p1 * (p2,i) is Element of the carrier of M
n is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
K is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
M is non empty non degenerated non trivial right_complementable almost_left_invertible V111() V123() associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V144() left_unital doubleLoopStr
the carrier of M is non empty non trivial set
the carrier of M * is functional non empty FinSequence-membered FinSequenceSet of the carrier of M
(M,n,K) is Relation-like NAT -defined the carrier of M * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular Matrix of n,K, the carrier of M
K -tuples_on the carrier of M is functional non empty FinSequence-membered FinSequenceSet of the carrier of M
{ b1 where b1 is Relation-like NAT -defined the carrier of M -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of M * : len b1 = K } is set
0. M is V68(M) Element of the carrier of M
K |-> (0. M) is Relation-like NAT -defined the carrier of M -valued Function-like V48() V55(K) FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of M
Seg K is V48() V55(K) Element of bool NAT
(Seg K) --> (0. M) is Relation-like Seg K -defined {(0. M)} -valued Function-like total V26( Seg K,{(0. M)}) V48() FinSequence-like FinSubsequence-like Element of bool [:(Seg K),{(0. M)}:]
{(0. M)} is non empty trivial V48() V55(1) set
[:(Seg K),{(0. M)}:] is Relation-like V48() set
bool [:(Seg K),{(0. M)}:] is non empty cup-closed diff-closed preBoolean V48() V52() set
n |-> (K |-> (0. M)) is Relation-like NAT -defined K -tuples_on the carrier of M -valued Function-like V48() V55(n) FinSequence-like FinSubsequence-like Element of n -tuples_on (K -tuples_on the carrier of M)
n -tuples_on (K -tuples_on the carrier of M) is functional non empty FinSequence-membered FinSequenceSet of K -tuples_on the carrier of M
(K -tuples_on the carrier of M) * is functional non empty FinSequence-membered FinSequenceSet of K -tuples_on the carrier of M
{ b1 where b1 is Relation-like NAT -defined K -tuples_on the carrier of M -valued Function-like V48() FinSequence-like FinSubsequence-like Element of (K -tuples_on the carrier of M) * : len b1 = n } is set
Seg n is V48() V55(n) Element of bool NAT
(Seg n) --> (K |-> (0. M)) is Relation-like Seg n -defined {(K |-> (0. M))} -valued Function-like total V26( Seg n,{(K |-> (0. M))}) V48() FinSequence-like FinSubsequence-like Element of bool [:(Seg n),{(K |-> (0. M))}:]
{(K |-> (0. M))} is functional non empty trivial V48() V52() V55(1) set
[:(Seg n),{(K |-> (0. M))}:] is Relation-like V48() set
bool [:(Seg n),{(K |-> (0. M))}:] is non empty cup-closed diff-closed preBoolean V48() V52() set
p1 is Relation-like NAT -defined the carrier of M * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular Matrix of n,K, the carrier of M
(M,p1) is Relation-like NAT -defined the carrier of M * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of M *
(M,p1,(M,p1)) is Relation-like NAT -defined the carrier of M * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of M *
width (M,p1) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
width p1 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
len (M,p1,(M,p1)) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
len p1 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
width (M,p1,(M,p1)) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
len (M,p1) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
len (M,n,K) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
width (M,n,K) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
dom p1 is V48() Element of bool NAT
dom (M,p1) is V48() Element of bool NAT
dom (M,p1,(M,p1)) is V48() Element of bool NAT
Indices p1 is set
Seg (width p1) is V48() V55( width p1) Element of bool NAT
[:(dom p1),(Seg (width p1)):] is Relation-like V48() set
Indices (M,p1) is set
Seg (width (M,p1)) is V48() V55( width (M,p1)) Element of bool NAT
[:(dom (M,p1)),(Seg (width (M,p1))):] is Relation-like V48() set
Indices (M,p1,(M,p1)) is set
Seg (width (M,p1,(M,p1))) is V48() V55( width (M,p1,(M,p1))) Element of bool NAT
[:(dom (M,p1,(M,p1))),(Seg (width (M,p1,(M,p1)))):] is Relation-like V48() set
Seg (width (M,p1)) is V48() V55( width (M,p1)) Element of bool NAT
Seg 0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty proper V34() V35() V36() V38() V39() V40() V41() ext-real non positive non negative V45() V48() V49() V52() V53() V55( 0 ) V55( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of bool NAT
dom (M,p1) is V48() Element of bool NAT
Indices (M,p1) is set
[:(dom (M,p1)),(Seg (width (M,p1))):] is Relation-like V48() set
[:(Seg 0),(Seg (width (M,p1))):] is Relation-like V48() set
[:(Seg 0),(Seg 0):] is Relation-like V48() set
dom (M,p1,(M,p1)) is V48() Element of bool NAT
Indices (M,p1,(M,p1)) is set
Seg (width (M,p1,(M,p1))) is V48() V55( width (M,p1,(M,p1))) Element of bool NAT
[:(dom (M,p1,(M,p1))),(Seg (width (M,p1,(M,p1)))):] is Relation-like V48() set
len (M,n,K) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
width (M,n,K) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Indices p1 is set
dom p1 is V48() Element of bool NAT
Seg (width p1) is V48() V55( width p1) Element of bool NAT
[:(dom p1),(Seg (width p1)):] is Relation-like V48() set
len (M,n,K) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
width (M,n,K) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Indices p1 is set
dom p1 is V48() Element of bool NAT
Seg (width p1) is V48() V55( width p1) Element of bool NAT
[:(dom p1),(Seg (width p1)):] is Relation-like V48() set
Indices (M,p1) is set
dom (M,p1) is V48() Element of bool NAT
Seg (width (M,p1)) is V48() V55( width (M,p1)) Element of bool NAT
[:(dom (M,p1)),(Seg (width (M,p1))):] is Relation-like V48() set
Indices (M,p1,(M,p1)) is set
dom (M,p1,(M,p1)) is V48() Element of bool NAT
Seg (width (M,p1,(M,p1))) is V48() V55( width (M,p1,(M,p1))) Element of bool NAT
[:(dom (M,p1,(M,p1))),(Seg (width (M,p1,(M,p1)))):] is Relation-like V48() set
len (M,n,K) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
width (M,n,K) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Indices p1 is set
dom p1 is V48() Element of bool NAT
Seg (width p1) is V48() V55( width p1) Element of bool NAT
[:(dom p1),(Seg (width p1)):] is Relation-like V48() set
Indices (M,p1) is set
dom (M,p1) is V48() Element of bool NAT
Seg (width (M,p1)) is V48() V55( width (M,p1)) Element of bool NAT
[:(dom (M,p1)),(Seg (width (M,p1))):] is Relation-like V48() set
Indices (M,p1,(M,p1)) is set
dom (M,p1,(M,p1)) is V48() Element of bool NAT
Seg (width (M,p1,(M,p1))) is V48() V55( width (M,p1,(M,p1))) Element of bool NAT
[:(dom (M,p1,(M,p1))),(Seg (width (M,p1,(M,p1)))):] is Relation-like V48() set
Indices (M,n,K) is set
dom (M,n,K) is V48() Element of bool NAT
Seg (width (M,n,K)) is V48() V55( width (M,n,K)) Element of bool NAT
[:(dom (M,n,K)),(Seg (width (M,n,K))):] is Relation-like V48() set
p2 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
i is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
[p2,i] is V23() set
(M,p1,(M,p1)) * (p2,i) is Element of the carrier of M
p1 * (p2,i) is Element of the carrier of M
(M,p1) * (p2,i) is Element of the carrier of M
(p1 * (p2,i)) + ((M,p1) * (p2,i)) is Element of the carrier of M
the addF of M is Relation-like [: the carrier of M, the carrier of M:] -defined the carrier of M -valued Function-like non empty total V26([: the carrier of M, the carrier of M:], the carrier of M) commutative associative Element of bool [:[: the carrier of M, the carrier of M:], the carrier of M:]
[: the carrier of M, the carrier of M:] is Relation-like non empty set
[:[: the carrier of M, the carrier of M:], the carrier of M:] is Relation-like non empty set
bool [:[: the carrier of M, the carrier of M:], the carrier of M:] is non empty cup-closed diff-closed preBoolean set
the addF of M . ((p1 * (p2,i)),((M,p1) * (p2,i))) is Element of the carrier of M
[(p1 * (p2,i)),((M,p1) * (p2,i))] is V23() set
the addF of M . [(p1 * (p2,i)),((M,p1) * (p2,i))] is set
- (p1 * (p2,i)) is Element of the carrier of M
(p1 * (p2,i)) + (- (p1 * (p2,i))) is Element of the carrier of M
the addF of M . ((p1 * (p2,i)),(- (p1 * (p2,i)))) is Element of the carrier of M
[(p1 * (p2,i)),(- (p1 * (p2,i)))] is V23() set
the addF of M . [(p1 * (p2,i)),(- (p1 * (p2,i)))] is set
(M,n,K) * (p2,i) is Element of the carrier of M
n is non empty non degenerated non trivial right_complementable almost_left_invertible V111() V123() associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V144() left_unital doubleLoopStr
the carrier of n is non empty non trivial set
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
K is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
width K is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
M is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
len M is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
len K is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
width M is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
p1 is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular Matrix of len K, width M, the carrier of n
Indices p1 is set
dom p1 is V48() Element of bool NAT
width p1 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Seg (width p1) is V48() V55( width p1) Element of bool NAT
[:(dom p1),(Seg (width p1)):] is Relation-like V48() set
len p1 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
p2 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
i is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
[p2,i] is V23() set
p1 * (p2,i) is Element of the carrier of n
Line (K,p2) is Relation-like NAT -defined the carrier of n -valued Function-like V48() V55( width K) FinSequence-like FinSubsequence-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
{ b1 where b1 is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b1 = width K } is set
Col (M,i) is Relation-like NAT -defined the carrier of n -valued Function-like V48() V55( len M) FinSequence-like FinSubsequence-like Element of (len M) -tuples_on the carrier of n
(len M) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b1 where b1 is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b1 = len M } is set
(Line (K,p2)) "*" (Col (M,i)) is Element of the carrier of n
p1 is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
len p1 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
width p1 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Indices p1 is set
dom p1 is V48() Element of bool NAT
Seg (width p1) is V48() V55( width p1) Element of bool NAT
[:(dom p1),(Seg (width p1)):] is Relation-like V48() set
p2 is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
len p2 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
width p2 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Indices p2 is set
dom p2 is V48() Element of bool NAT
Seg (width p2) is V48() V55( width p2) Element of bool NAT
[:(dom p2),(Seg (width p2)):] is Relation-like V48() set
i is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
p is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
[i,p] is V23() set
p1 * (i,p) is Element of the carrier of n
Line (K,i) is Relation-like NAT -defined the carrier of n -valued Function-like V48() V55( width K) FinSequence-like FinSubsequence-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
{ b1 where b1 is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b1 = width K } is set
Col (M,p) is Relation-like NAT -defined the carrier of n -valued Function-like V48() V55( len M) FinSequence-like FinSubsequence-like Element of (len M) -tuples_on the carrier of n
(len M) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b1 where b1 is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b1 = len M } is set
(Line (K,i)) "*" (Col (M,p)) is Element of the carrier of n
p2 * (i,p) is Element of the carrier of n
p1 is non empty non degenerated non trivial right_complementable almost_left_invertible V111() V123() associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V144() left_unital doubleLoopStr
the carrier of p1 is non empty non trivial set
the carrier of p1 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of p1
n is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
K is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
p2 is Relation-like NAT -defined the carrier of p1 * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular Matrix of n,K, the carrier of p1
width p2 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
M is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
i is Relation-like NAT -defined the carrier of p1 * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular Matrix of width p2,M, the carrier of p1
(p1,p2,i) is Relation-like NAT -defined the carrier of p1 * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of p1 *
len p2 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
width i is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
len i is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
len (p1,p2,i) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
width (p1,p2,i) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
n is non empty non degenerated non trivial right_complementable almost_left_invertible V111() V123() associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V144() left_unital doubleLoopStr
the carrier of n is non empty non trivial set
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
K is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
len K is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
width K is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Indices K is set
dom K is V48() Element of bool NAT
Seg (width K) is V48() V55( width K) Element of bool NAT
[:(dom K),(Seg (width K)):] is Relation-like V48() set
M is Element of the carrier of n
p1 is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular Matrix of len K, width K, the carrier of n
Indices p1 is set
dom p1 is V48() Element of bool NAT
width p1 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Seg (width p1) is V48() V55( width p1) Element of bool NAT
[:(dom p1),(Seg (width p1)):] is Relation-like V48() set
len p1 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
p2 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
i is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
[p2,i] is V23() set
p1 * (p2,i) is Element of the carrier of n
K * (p2,i) is Element of the carrier of n
M * (K * (p2,i)) is Element of the carrier of n
the multF of n is Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like non empty total V26([: the carrier of n, the carrier of n:], the carrier of n) commutative Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[: the carrier of n, the carrier of n:] is Relation-like non empty set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like non empty set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty cup-closed diff-closed preBoolean set
the multF of n . (M,(K * (p2,i))) is Element of the carrier of n
[M,(K * (p2,i))] is V23() set
the multF of n . [M,(K * (p2,i))] is set
p1 is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
len p1 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
width p1 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
p2 is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
len p2 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
width p2 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
dom p1 is V48() Element of bool NAT
Indices p1 is set
Seg (width p1) is V48() V55( width p1) Element of bool NAT
[:(dom p1),(Seg (width p1)):] is Relation-like V48() set
i is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
p is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
[i,p] is V23() set
p1 * (i,p) is Element of the carrier of n
K * (i,p) is Element of the carrier of n
M * (K * (i,p)) is Element of the carrier of n
the multF of n is Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like non empty total V26([: the carrier of n, the carrier of n:], the carrier of n) commutative Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[: the carrier of n, the carrier of n:] is Relation-like non empty set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like non empty set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty cup-closed diff-closed preBoolean set
the multF of n . (M,(K * (i,p))) is Element of the carrier of n
[M,(K * (i,p))] is V23() set
the multF of n . [M,(K * (i,p))] is set
p2 * (i,p) is Element of the carrier of n
n is non empty non degenerated non trivial right_complementable almost_left_invertible V111() V123() associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V144() left_unital doubleLoopStr
the carrier of n is non empty non trivial set
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
K is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
M is Element of the carrier of n
(n,K,M) is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
n is non empty non degenerated non trivial right_complementable almost_left_invertible V111() V123() associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V144() left_unital doubleLoopStr
the carrier of n is non empty non trivial set
K is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len K is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
M is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len M is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
mlt (K,M) is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len (mlt (K,M)) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
p1 is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
the multF of n is Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like non empty total V26([: the carrier of n, the carrier of n:], the carrier of n) commutative Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[: the carrier of n, the carrier of n:] is Relation-like non empty set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like non empty set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty cup-closed diff-closed preBoolean set
the multF of n .: (K,M) is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
n is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
K is non empty non degenerated non trivial right_complementable almost_left_invertible V111() V123() associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V144() left_unital doubleLoopStr
1. (K,n) is Relation-like NAT -defined the carrier of K * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular Matrix of n,n, the carrier of K
the carrier of K is non empty non trivial set
the carrier of K * is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
Indices (1. (K,n)) is set
dom (1. (K,n)) is V48() Element of bool NAT
width (1. (K,n)) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Seg (width (1. (K,n))) is V48() V55( width (1. (K,n))) Element of bool NAT
[:(dom (1. (K,n))),(Seg (width (1. (K,n)))):] is Relation-like V48() set
1. K is V68(K) Element of the carrier of K
M is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
Line ((1. (K,n)),M) is Relation-like NAT -defined the carrier of K -valued Function-like V48() V55( width (1. (K,n))) FinSequence-like FinSubsequence-like Element of (width (1. (K,n))) -tuples_on the carrier of K
(width (1. (K,n))) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
{ b1 where b1 is Relation-like NAT -defined the carrier of K -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of K * : len b1 = width (1. (K,n)) } is set
p1 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
[M,p1] is V23() set
(Line ((1. (K,n)),M)) . p1 is set
(1. (K,n)) * (M,p1) is Element of the carrier of K
n is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
K is non empty non degenerated non trivial right_complementable almost_left_invertible V111() V123() associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V144() left_unital doubleLoopStr
1. (K,n) is Relation-like NAT -defined the carrier of K * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular Matrix of n,n, the carrier of K
the carrier of K is non empty non trivial set
the carrier of K * is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
Indices (1. (K,n)) is set
dom (1. (K,n)) is V48() Element of bool NAT