:: MATRIX_3 semantic presentation

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
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = 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
{ b₁ where b₁ 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 b₁ = 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
c₁₀ is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
[j,c₁₀] is V23() set
p * (j,c₁₀) is Element of the carrier of n
K * (j,c₁₀) is Element of the carrier of n
- (K * (j,c₁₀)) is Element of the carrier of n
i * (j,c₁₀) 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
c₁₀ 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
[c₁₀,h] is V23() set
i * (c₁₀,h) is Element of the carrier of n
K * (c₁₀,h) is Element of the carrier of n
M * (c₁₀,h) is Element of the carrier of n
(K * (c₁₀,h)) + (M * (c₁₀,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 * (c₁₀,h)),(M * (c₁₀,h))) is Element of the carrier of n
[(K * (c₁₀,h)),(M * (c₁₀,h))] is V23() set
the addF of n . [(K * (c₁₀,h)),(M * (c₁₀,h))] is set
p * (c₁₀,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
{ b₁ where b₁ is Relation-like NAT -defined the carrier of M -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of M * : len b₁ = 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
{ b₁ where b₁ 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 b₁ = 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
{ b₁ where b₁ is Relation-like NAT -defined the carrier of M -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of M * : len b₁ = 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
{ b₁ where b₁ is Relation-like NAT -defined the carrier of M -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of M * : len b₁ = 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
{ b₁ where b₁ 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 b₁ = 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
{ b₁ where b₁ is Relation-like NAT -defined the carrier of M -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of M * : len b₁ = 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
{ b₁ where b₁ 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 b₁ = 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
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = 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
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = 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
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = 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
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = 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
{ b₁ where b₁ is Relation-like NAT -defined the carrier of K -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of K * : len b₁ = 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
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
0. 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
{ b₁ where b₁ is Relation-like NAT -defined the carrier of K -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of K * : len b₁ = 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
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
p1 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
[M,p1] is V23() set
Col ((1. (K,n)),p1) is Relation-like NAT -defined the carrier of K -valued Function-like V48() V55( len (1. (K,n))) FinSequence-like FinSubsequence-like Element of (len (1. (K,n))) -tuples_on the carrier of K
len (1. (K,n)) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
(len (1. (K,n))) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
{ b₁ where b₁ is Relation-like NAT -defined the carrier of K -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of K * : len b₁ = len (1. (K,n)) } is set
(Col ((1. (K,n)),p1)) . M 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
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
0. 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
p1 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
[M,p1] is V23() set
Col ((1. (K,n)),p1) is Relation-like NAT -defined the carrier of K -valued Function-like V48() V55( len (1. (K,n))) FinSequence-like FinSubsequence-like Element of (len (1. (K,n))) -tuples_on the carrier of K
len (1. (K,n)) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
(len (1. (K,n))) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
{ b₁ where b₁ is Relation-like NAT -defined the carrier of K -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of K * : len b₁ = len (1. (K,n)) } is set
(Col ((1. (K,n)),p1)) . M is set
(1. (K,n)) * (M,p1) is Element of the carrier of K
n is non empty right_complementable add-associative right_zeroed addLoopStr
the carrier of n is non empty set
0. n is V68(n) Element of the carrier of n
K is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
dom K is V48() Element of bool NAT
Sum K 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 FinSequence of the carrier of n
dom M is V48() Element of bool NAT
Sum M is Element of the carrier of n
p1 is Element of the carrier of n
<*p1*> is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty trivial V48() V55(1) FinSequence-like FinSubsequence-like Element of 1 -tuples_on the carrier of n
1 -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
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = 1 } is set
M ^ <*p1*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
dom (M ^ <*p1*>) is non empty V48() Element of bool NAT
Sum (M ^ <*p1*>) is Element of the carrier of n
len M is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
(len M) + 1 is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V48() V53() Element of NAT
Seg ((len M) + 1) is non empty V48() V55((len M) + 1) Element of bool NAT
p2 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
M . p2 is set
(M ^ <*p1*>) . p2 is set
len (M ^ <*p1*>) is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V48() V53() Element of NAT
len <*p1*> is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V48() V53() Element of NAT
(len M) + (len <*p1*>) is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V48() V53() Element of NAT
(M ^ <*p1*>) . ((len M) + 1) is set
Sum <*p1*> is Element of the carrier of n
(Sum M) + (Sum <*p1*>) 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) 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 . ((Sum M),(Sum <*p1*>)) is Element of the carrier of n
[(Sum M),(Sum <*p1*>)] is V23() set
the addF of n . [(Sum M),(Sum <*p1*>)] is set
(Sum M) + p1 is Element of the carrier of n
the addF of n . ((Sum M),p1) is Element of the carrier of n
[(Sum M),p1] is V23() set
the addF of n . [(Sum M),p1] is set
(0. n) + (0. n) is Element of the carrier of n
the addF of n . ((0. n),(0. n)) is Element of the carrier of n
[(0. n),(0. n)] is V23() set
the addF of n . [(0. n),(0. n)] is set
p2 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
M . p2 is set
<*> the carrier of n is Relation-like non-empty empty-yielding NAT -defined the carrier of n -valued 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( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of the carrier of n
[:NAT, the carrier of n:] is Relation-like non empty non trivial V48() set
dom (<*> the carrier of n) 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( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of bool NAT
Sum (<*> the carrier of n) is Element of the carrier of n
n is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
K is non empty right_complementable add-associative right_zeroed addLoopStr
the carrier of K is non empty set
0. K is V68(K) Element of the carrier of K
n |-> (0. K) is Relation-like NAT -defined the carrier of K -valued Function-like V48() V55(n) FinSequence-like FinSubsequence-like Element of n -tuples_on the carrier of K
n -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
the carrier of K * is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
{ b₁ where b₁ is Relation-like NAT -defined the carrier of K -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of K * : len b₁ = n } is set
Seg n is V48() V55(n) Element of bool NAT
(Seg n) --> (0. K) is Relation-like Seg n -defined {(0. K)} -valued Function-like total V26( Seg n,{(0. K)}) V48() FinSequence-like FinSubsequence-like Element of bool [:(Seg n),{(0. K)}:]
{(0. K)} is non empty trivial V48() V55(1) set
[:(Seg n),{(0. K)}:] is Relation-like V48() set
bool [:(Seg n),{(0. K)}:] is non empty cup-closed diff-closed preBoolean V48() V52() set
Sum (n |-> (0. K)) is Element of the carrier of K
dom (n |-> (0. K)) is V48() V55(n) Element of bool NAT
p1 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
(n |-> (0. K)) . p1 is set
n is non empty right_complementable add-associative right_zeroed addLoopStr
the carrier of n is non empty set
0. n is V68(n) Element of the carrier of n
K is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
dom K is V48() Element of bool NAT
Sum K is Element of the carrier of n
M is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
K . M is set
Seg M is V48() V55(M) Element of bool NAT
K | (Seg M) is Relation-like NAT -defined Seg M -defined NAT -defined the carrier of n -valued Function-like V48() FinSubsequence-like Element of bool [:NAT, the carrier of n:]
[:NAT, the carrier of n:] is Relation-like non empty non trivial V48() set
bool [:NAT, the carrier of n:] is non empty non trivial cup-closed diff-closed preBoolean V48() set
(dom K) /\ (Seg M) is V48() Element of bool NAT
p2 is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
dom p2 is V48() Element of bool NAT
len 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 FinSequence of the carrier of n
p is Element of the carrier of n
<*p*> is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty trivial V48() V55(1) FinSequence-like FinSubsequence-like Element of 1 -tuples_on the carrier of n
1 -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
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = 1 } is set
i ^ <*p*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
i is Relation-like NAT -defined Function-like V48() FinSequence-like FinSubsequence-like set
p2 ^ i is Relation-like NAT -defined Function-like V48() FinSequence-like FinSubsequence-like set
j is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
dom j is V48() Element of bool NAT
len j is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Seg (len j) is V48() V55( len j) Element of bool NAT
c₁₀ is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
j . c₁₀ is set
(len p2) + c₁₀ is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
K . ((len p2) + c₁₀) is set
c₁₀ is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
j . c₁₀ is set
(len j) |-> (0. n) is Relation-like NAT -defined the carrier of n -valued Function-like V48() V55( len j) FinSequence-like FinSubsequence-like Element of (len j) -tuples_on the carrier of n
(len j) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = len j } is set
(Seg (len j)) --> (0. n) is Relation-like Seg (len j) -defined {(0. n)} -valued Function-like total V26( Seg (len j),{(0. n)}) V48() FinSequence-like FinSubsequence-like Element of bool [:(Seg (len j)),{(0. n)}:]
{(0. n)} is non empty trivial V48() V55(1) set
[:(Seg (len j)),{(0. n)}:] is Relation-like V48() set
bool [:(Seg (len j)),{(0. n)}:] is non empty cup-closed diff-closed preBoolean V48() V52() set
((len j) |-> (0. n)) . c₁₀ is set
dom i is V48() Element of bool NAT
len i is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Seg (len i) is V48() V55( len i) Element of bool NAT
len K is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
len <*p*> is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V48() V53() Element of NAT
(len i) + (len <*p*>) is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V48() V53() Element of NAT
(len i) + 1 is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V48() V53() Element of NAT
p2 . M is set
p1 is Element of the carrier of n
c₁₀ is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
i . c₁₀ is set
p2 . c₁₀ is set
K . c₁₀ is set
c₁₀ is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
i . c₁₀ is set
(len i) |-> (0. n) is Relation-like NAT -defined the carrier of n -valued Function-like V48() V55( len i) FinSequence-like FinSubsequence-like Element of (len i) -tuples_on the carrier of n
(len i) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = len i } is set
(Seg (len i)) --> (0. n) is Relation-like Seg (len i) -defined {(0. n)} -valued Function-like total V26( Seg (len i),{(0. n)}) V48() FinSequence-like FinSubsequence-like Element of bool [:(Seg (len i)),{(0. n)}:]
[:(Seg (len i)),{(0. n)}:] is Relation-like V48() set
bool [:(Seg (len i)),{(0. n)}:] is non empty cup-closed diff-closed preBoolean V48() V52() set
((len i) |-> (0. n)) . c₁₀ is set
len ((len i) |-> (0. n)) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
len ((len j) |-> (0. n)) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Sum (i ^ <*p*>) is Element of the carrier of n
Sum ((len j) |-> (0. n)) is Element of the carrier of n
(Sum (i ^ <*p*>)) + (Sum ((len j) |-> (0. n))) 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) 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 . ((Sum (i ^ <*p*>)),(Sum ((len j) |-> (0. n)))) is Element of the carrier of n
[(Sum (i ^ <*p*>)),(Sum ((len j) |-> (0. n)))] is V23() set
the addF of n . [(Sum (i ^ <*p*>)),(Sum ((len j) |-> (0. n)))] is set
(Sum (i ^ <*p*>)) + (0. n) is Element of the carrier of n
the addF of n . ((Sum (i ^ <*p*>)),(0. n)) is Element of the carrier of n
[(Sum (i ^ <*p*>)),(0. n)] is V23() set
the addF of n . [(Sum (i ^ <*p*>)),(0. n)] is set
Sum ((len i) |-> (0. n)) is Element of the carrier of n
(Sum ((len i) |-> (0. n))) + p is Element of the carrier of n
the addF of n . ((Sum ((len i) |-> (0. n))),p) is Element of the carrier of n
[(Sum ((len i) |-> (0. n))),p] is V23() set
the addF of n . [(Sum ((len i) |-> (0. n))),p] is set
(0. n) + p1 is Element of the carrier of n
the addF of n . ((0. n),p1) is Element of the carrier of n
[(0. n),p1] is V23() set
the addF of n . [(0. n),p1] is 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
K is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
M is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
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
len K is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
len M is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
min ((len K),(len 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 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
1. n is V68(n) Element of the carrier of n
0. n is V68(n) Element of the carrier of n
K is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
dom K is V48() Element of bool 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
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
dom (mlt (K,M)) is V48() Element of bool NAT
p1 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
K . p1 is set
M . p1 is set
p2 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
(mlt (K,M)) . p2 is set
len K is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Seg (len K) is V48() V55( len K) Element of bool NAT
dom M is V48() Element of bool NAT
len M is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Seg (len M) is V48() V55( len M) Element of bool NAT
len (mlt (K,M)) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Seg (len (mlt (K,M))) is V48() V55( len (mlt (K,M))) Element of bool NAT
min ((len K),(len M)) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
(dom K) /\ (dom M) is V48() Element of bool NAT
i is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
M . i is set
i is Element of the carrier of n
i * (1. n) 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 . (i,(1. n)) is Element of the carrier of n
[i,(1. n)] is V23() set
the multF of n . [i,(1. n)] is set
K . p2 is set
p is Element of the carrier of n
(0. n) * 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 . ((0. n),p) is Element of the carrier of n
[(0. n),p] is V23() set
the multF of n . [(0. n),p] is set
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
0. 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
{ b₁ where b₁ is Relation-like NAT -defined the carrier of K -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of K * : len b₁ = 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
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
0. 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
p1 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
[M,p1] is V23() set
Col ((1. (K,n)),p1) is Relation-like NAT -defined the carrier of K -valued Function-like V48() V55( len (1. (K,n))) FinSequence-like FinSubsequence-like Element of (len (1. (K,n))) -tuples_on the carrier of K
len (1. (K,n)) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
(len (1. (K,n))) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
{ b₁ where b₁ is Relation-like NAT -defined the carrier of K -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of K * : len b₁ = len (1. (K,n)) } is set
(Col ((1. (K,n)),p1)) . M is set
(1. (K,n)) * (M,p1) is Element of the carrier of K
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
1. n is V68(n) Element of the carrier of n
0. n is V68(n) Element of the carrier of n
K is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
dom K is V48() Element of bool 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
dom M is V48() Element of bool 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
Sum (mlt (K,M)) is Element of the carrier of n
p1 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
K . p1 is set
M . p1 is set
p2 is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
dom p2 is V48() Element of bool NAT
i is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
p2 . i is set
len K is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Seg (len K) is V48() V55( len K) Element of bool NAT
len M is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Seg (len M) is V48() V55( len M) Element of bool NAT
dom (mlt (K,M)) is V48() Element of bool NAT
len (mlt (K,M)) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Seg (len (mlt (K,M))) is V48() V55( len (mlt (K,M))) Element of bool NAT
min ((len K),(len M)) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
(dom K) /\ (dom M) is V48() Element of bool NAT
p2 . p1 is set
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
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
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
M 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
(K,(1. (K,n)),M) is Relation-like NAT -defined the carrier of K * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of K *
len (1. (K,n)) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
len M is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
width (1. (K,n)) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
len (K,(1. (K,n)),M) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
dom M is V48() Element of bool NAT
Seg (len M) is V48() V55( len M) Element of bool 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
Indices (K,(1. (K,n)),M) is set
dom (K,(1. (K,n)),M) is V48() Element of bool NAT
width (K,(1. (K,n)),M) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Seg (width (K,(1. (K,n)),M)) is V48() V55( width (K,(1. (K,n)),M)) Element of bool NAT
[:(dom (K,(1. (K,n)),M)),(Seg (width (K,(1. (K,n)),M))):] is Relation-like V48() set
Seg (len (K,(1. (K,n)),M)) is V48() V55( len (K,(1. (K,n)),M)) Element of bool NAT
Seg (width (1. (K,n))) is V48() V55( width (1. (K,n))) Element of bool NAT
Line ((1. (K,n)),p2) 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
{ b₁ where b₁ is Relation-like NAT -defined the carrier of K -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of K * : len b₁ = width (1. (K,n)) } is set
len (Line ((1. (K,n)),p2)) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Seg (len (Line ((1. (K,n)),p2))) is V48() V55( len (Line ((1. (K,n)),p2))) Element of bool NAT
dom (Line ((1. (K,n)),p2)) is V48() V55( width (1. (K,n))) Element of bool NAT
dom (1. (K,n)) is V48() Element of bool NAT
Seg (len (1. (K,n))) is V48() V55( len (1. (K,n))) Element of bool NAT
[p2,p2] is V23() set
[:(dom (1. (K,n))),(Seg (width (1. (K,n)))):] is Relation-like V48() set
Indices (1. (K,n)) is set
(Line ((1. (K,n)),p2)) . p2 is set
1. K is V68(K) Element of the carrier of K
p is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
[p2,p] is V23() set
(Line ((1. (K,n)),p2)) . p is set
0. K is V68(K) Element of the carrier of K
Col (M,i) is Relation-like NAT -defined the carrier of K -valued Function-like V48() V55( len M) FinSequence-like FinSubsequence-like Element of (len M) -tuples_on the carrier of K
(len M) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
{ b₁ where b₁ is Relation-like NAT -defined the carrier of K -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of K * : len b₁ = len M } is set
len (Col (M,i)) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Seg (len (Col (M,i))) is V48() V55( len (Col (M,i))) Element of bool NAT
dom (Col (M,i)) is V48() V55( len M) Element of bool NAT
(K,(1. (K,n)),M) * (p2,i) is Element of the carrier of K
(Line ((1. (K,n)),p2)) "*" (Col (M,i)) is Element of the carrier of K
mlt ((Line ((1. (K,n)),p2)),(Col (M,i))) is Relation-like NAT -defined the carrier of K -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of K
Sum (mlt ((Line ((1. (K,n)),p2)),(Col (M,i)))) is Element of the carrier of K
(Col (M,i)) . p2 is set
M * (p2,i) is Element of the carrier of K
width M is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
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
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
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
M 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
(K,M,(1. (K,n))) is Relation-like NAT -defined the carrier of K * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of K *
width (1. (K,n)) 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
len (1. (K,n)) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
width (K,M,(1. (K,n))) 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
Indices (K,M,(1. (K,n))) is set
dom (K,M,(1. (K,n))) is V48() Element of bool NAT
Seg (width (K,M,(1. (K,n)))) is V48() V55( width (K,M,(1. (K,n)))) Element of bool NAT
[:(dom (K,M,(1. (K,n)))),(Seg (width (K,M,(1. (K,n))))):] is Relation-like V48() set
Seg (width (1. (K,n))) is V48() V55( width (1. (K,n))) Element of bool NAT
Col ((1. (K,n)),i) is Relation-like NAT -defined the carrier of K -valued Function-like V48() V55( len (1. (K,n))) FinSequence-like FinSubsequence-like Element of (len (1. (K,n))) -tuples_on the carrier of K
(len (1. (K,n))) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
{ b₁ where b₁ is Relation-like NAT -defined the carrier of K -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of K * : len b₁ = len (1. (K,n)) } is set
len (Col ((1. (K,n)),i)) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Seg (len (Col ((1. (K,n)),i))) is V48() V55( len (Col ((1. (K,n)),i))) Element of bool NAT
dom (Col ((1. (K,n)),i)) is V48() V55( len (1. (K,n))) Element of bool NAT
Seg (width M) is V48() V55( width M) Element of bool NAT
p is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
Seg (len (1. (K,n))) is V48() V55( len (1. (K,n))) Element of bool NAT
dom (1. (K,n)) is V48() Element of bool NAT
[p,i] is V23() set
[:(dom (1. (K,n))),(Seg (width (1. (K,n)))):] is Relation-like V48() set
Indices (1. (K,n)) is set
(Col ((1. (K,n)),i)) . p is set
0. K is V68(K) Element of the carrier of K
[i,i] is V23() set
(Col ((1. (K,n)),i)) . i is set
1. K is V68(K) Element of the carrier of K
Line (M,p2) is Relation-like NAT -defined the carrier of K -valued Function-like V48() V55( width M) FinSequence-like FinSubsequence-like Element of (width M) -tuples_on the carrier of K
(width M) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
{ b₁ where b₁ is Relation-like NAT -defined the carrier of K -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of K * : len b₁ = width M } is set
len (Line (M,p2)) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Seg (len (Line (M,p2))) is V48() V55( len (Line (M,p2))) Element of bool NAT
dom (Line (M,p2)) is V48() V55( width M) Element of bool NAT
(K,M,(1. (K,n))) * (p2,i) is Element of the carrier of K
(Line (M,p2)) "*" (Col ((1. (K,n)),i)) is Element of the carrier of K
(Col ((1. (K,n)),i)) "*" (Line (M,p2)) is Element of the carrier of K
mlt ((Col ((1. (K,n)),i)),(Line (M,p2))) is Relation-like NAT -defined the carrier of K -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of K
Sum (mlt ((Col ((1. (K,n)),i)),(Line (M,p2)))) is Element of the carrier of K
(Line (M,p2)) . i is set
M * (p2,i) is Element of the carrier of K
len (K,M,(1. (K,n))) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
len M 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
K is Element of the carrier of n
<*K*> is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty trivial V48() V55(1) FinSequence-like FinSubsequence-like Element of 1 -tuples_on the carrier of n
1 -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
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = 1 } is set
<*<*K*>*> is Relation-like NAT -defined the carrier of n * -valued Function-like constant non empty trivial V48() V55(1) FinSequence-like FinSubsequence-like tabular Matrix of 1,1, the carrier of n
M is Element of the carrier of n
<*M*> is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty trivial V48() V55(1) FinSequence-like FinSubsequence-like Element of 1 -tuples_on the carrier of n
<*<*M*>*> is Relation-like NAT -defined the carrier of n * -valued Function-like constant non empty trivial V48() V55(1) FinSequence-like FinSubsequence-like tabular Matrix of 1,1, 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 *
K * M 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 . (K,M) is Element of the carrier of n
[K,M] is V23() set
the multF of n . [K,M] is set
<*(K * M)*> is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty trivial V48() V55(1) FinSequence-like FinSubsequence-like Element of 1 -tuples_on the carrier of n
<*<*(K * M)*>*> is Relation-like NAT -defined the carrier of n * -valued Function-like constant non empty trivial V48() V55(1) FinSequence-like FinSubsequence-like tabular Matrix of 1,1, 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 1,1, the carrier of n
p2 is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular Matrix of 1,1, the carrier of n
(n,p1,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 *
Line (p1,1) is Relation-like NAT -defined the carrier of n -valued Function-like V48() V55( width p1) FinSequence-like FinSubsequence-like Element of (width p1) -tuples_on the carrier of n
width p1 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
(width p1) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = width p1 } is set
len (Line (p1,1)) 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
(Line (p1,1)) . 1 is set
<*<*K*>*> * (1,1) is Element of the carrier of n
Line (<*<*K*>*>,1) 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*>*> is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
(width <*<*K*>*>) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = width <*<*K*>*> } is set
len p2 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Seg (len p2) is V48() V55( len p2) Element of bool NAT
dom p2 is V48() Element of bool NAT
Col (p2,1) is Relation-like NAT -defined the carrier of n -valued Function-like V48() V55( len p2) FinSequence-like FinSubsequence-like Element of (len p2) -tuples_on the carrier of n
(len p2) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = len p2 } is set
(Col (p2,1)) . 1 is set
<*<*M*>*> * (1,1) is Element of the carrier of n
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 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
p is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular Matrix of 1,1, the carrier of n
len p is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Seg (len p) is V48() V55( len p) Element of bool NAT
dom p is V48() Element of bool NAT
Indices p is set
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
len (Col (p2,1)) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Col (<*<*M*>*>,1) 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*>*> is non empty V34() V35() V36() V40() V41() ext-real positive non negative V45() V48() V53() Element of NAT
(len <*<*M*>*>) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = len <*<*M*>*> } is set
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*> "*" <*M*> is Element of the carrier of n
<*<*(K * M)*>*> * (i,j) 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
K is Element of the carrier of n
p1 is Element of the carrier of n
i is Element of the carrier of n
i is Element of the carrier of n
(K,p1) ][ (i,i) is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular Matrix of 2,2, the carrier of n
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
M is Element of the carrier of n
p2 is Element of the carrier of n
p is Element of the carrier of n
j is Element of the carrier of n
(M,p2) ][ (p,j) is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular Matrix of 2,2, the carrier of n
(n,((K,p1) ][ (i,i)),((M,p2) ][ (p,j))) is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
K * M 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 . (K,M) is Element of the carrier of n
[K,M] is V23() set
the multF of n . [K,M] is set
p1 * p is Element of the carrier of n
the multF of n . (p1,p) is Element of the carrier of n
[p1,p] is V23() set
the multF of n . [p1,p] is set
(K * M) + (p1 * p) is Element of the carrier of n
the addF of n is Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like 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 addF of n . ((K * M),(p1 * p)) is Element of the carrier of n
[(K * M),(p1 * p)] is V23() set
the addF of n . [(K * M),(p1 * p)] is set
K * p2 is Element of the carrier of n
the multF of n . (K,p2) is Element of the carrier of n
[K,p2] is V23() set
the multF of n . [K,p2] is set
p1 * j is Element of the carrier of n
the multF of n . (p1,j) is Element of the carrier of n
[p1,j] is V23() set
the multF of n . [p1,j] is set
(K * p2) + (p1 * j) is Element of the carrier of n
the addF of n . ((K * p2),(p1 * j)) is Element of the carrier of n
[(K * p2),(p1 * j)] is V23() set
the addF of n . [(K * p2),(p1 * j)] is set
i * M is Element of the carrier of n
the multF of n . (i,M) is Element of the carrier of n
[i,M] is V23() set
the multF of n . [i,M] is set
i * p is Element of the carrier of n
the multF of n . (i,p) is Element of the carrier of n
[i,p] is V23() set
the multF of n . [i,p] is set
(i * M) + (i * p) is Element of the carrier of n
the addF of n . ((i * M),(i * p)) is Element of the carrier of n
[(i * M),(i * p)] is V23() set
the addF of n . [(i * M),(i * p)] is set
i * p2 is Element of the carrier of n
the multF of n . (i,p2) is Element of the carrier of n
[i,p2] is V23() set
the multF of n . [i,p2] is set
i * j is Element of the carrier of n
the multF of n . (i,j) is Element of the carrier of n
[i,j] is V23() set
the multF of n . [i,j] is set
(i * p2) + (i * j) is Element of the carrier of n
the addF of n . ((i * p2),(i * j)) is Element of the carrier of n
[(i * p2),(i * j)] is V23() set
the addF of n . [(i * p2),(i * j)] is set
(((K * M) + (p1 * p)),((K * p2) + (p1 * j))) ][ (((i * M) + (i * p)),((i * p2) + (i * j))) is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular Matrix of 2,2, the carrier of n
c₁₀ is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular Matrix of 2,2, the carrier of n
width c₁₀ is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Line (c₁₀,2) is Relation-like NAT -defined the carrier of n -valued Function-like V48() V55( width c₁₀) FinSequence-like FinSubsequence-like Element of (width c₁₀) -tuples_on the carrier of n
(width c₁₀) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = width c₁₀ } is set
(Line (c₁₀,2)) . 2 is set
c₁₀ * (2,2) is Element of the carrier of n
len (Line (c₁₀,2)) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
(Line (c₁₀,2)) . 1 is set
c₁₀ * (2,1) is Element of the carrier of n
<*i,i*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty V48() V55(2) FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Line (c₁₀,1) is Relation-like NAT -defined the carrier of n -valued Function-like V48() V55( width c₁₀) FinSequence-like FinSubsequence-like Element of (width c₁₀) -tuples_on the carrier of n
(Line (c₁₀,1)) . 2 is set
c₁₀ * (1,2) is Element of the carrier of n
len (Line (c₁₀,1)) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
(Line (c₁₀,1)) . 1 is set
c₁₀ * (1,1) is Element of the carrier of n
<*K,p1*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty V48() V55(2) FinSequence-like FinSubsequence-like FinSequence of the carrier of n
h is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular Matrix of 2,2, the carrier of n
Col (h,2) is Relation-like NAT -defined the carrier of n -valued Function-like V48() V55( len h) FinSequence-like FinSubsequence-like Element of (len h) -tuples_on the carrier of n
len h is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
(len h) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = len h } is set
len (Col (h,2)) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Col (h,1) is Relation-like NAT -defined the carrier of n -valued Function-like V48() V55( len h) FinSequence-like FinSubsequence-like Element of (len h) -tuples_on the carrier of n
len (Col (h,1)) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
(n,c₁₀,h) 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 h is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
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
len c₁₀ 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
Seg (len h) is V48() V55( len h) Element of bool NAT
dom h is V48() Element of bool NAT
(Col (h,2)) . 2 is set
h * (2,2) is Element of the carrier of n
(Col (h,2)) . 1 is set
h * (1,2) is Element of the carrier of n
<*p2,j*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty V48() V55(2) FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(Col (h,1)) . 2 is set
h * (2,1) is Element of the carrier of n
(Col (h,1)) . 1 is set
h * (1,1) is Element of the carrier of n
<*M,p*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty V48() V55(2) FinSequence-like FinSubsequence-like FinSequence of the carrier of n
p is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular Matrix of 2,2, the carrier of n
dom p is V48() Element of bool NAT
len p is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Seg (len p) is V48() V55( len p) Element of bool NAT
Indices p is set
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 2),(Seg 2):] is Relation-like non empty V48() set
a is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
l is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
[a,l] is V23() set
p * (1,1) is Element of the carrier of n
<*K,p1*> "*" <*M,p*> is Element of the carrier of n
k9 is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular Matrix of 2,2, the carrier of n
k9 * (1,1) is Element of the carrier of n
p * (1,2) is Element of the carrier of n
<*K,p1*> "*" <*p2,j*> is Element of the carrier of n
k9 is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular Matrix of 2,2, the carrier of n
k9 * (1,2) is Element of the carrier of n
p * (2,1) is Element of the carrier of n
<*i,i*> "*" <*M,p*> is Element of the carrier of n
k9 is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular Matrix of 2,2, the carrier of n
k9 * (2,1) is Element of the carrier of n
p * (2,2) is Element of the carrier of n
<*i,i*> "*" <*p2,j*> is Element of the carrier of n
k9 is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular Matrix of 2,2, the carrier of n
k9 * (2,2) is Element of the carrier of n
p * (1,1) is Element of the carrier of n
k9 is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular Matrix of 2,2, the carrier of n
k9 * (1,1) is Element of the carrier of n
p * (1,2) is Element of the carrier of n
k9 * (1,2) is Element of the carrier of n
p * (2,1) is Element of the carrier of n
k9 * (2,1) is Element of the carrier of n
p * (2,2) is Element of the carrier of n
k9 * (2,2) is Element of the carrier of n
p * (1,1) is Element of the carrier of n
k9 is Relation-like NAT -defined the carrier of n * -valued Function-like V48() FinSequence-like FinSubsequence-like tabular Matrix of 2,2, the carrier of n
k9 * (1,1) is Element of the carrier of n
p * (1,2) is Element of the carrier of n
k9 * (1,2) is Element of the carrier of n
p * (2,1) is Element of the carrier of n
k9 * (2,1) is Element of the carrier of n
p * (2,2) is Element of the carrier of n
k9 * (2,2) is Element of the carrier of n
p * (a,l) is Element of the carrier of n
k9 * (a,l) 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 *
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
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,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 *
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 *
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 *
(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 *
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
width (n,(M @),(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
width (n,K,M) 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,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
len (n,(M @),(K @)) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
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
Indices (n,(M @),(K @)) is set
dom (n,(M @),(K @)) is V48() Element of bool NAT
Seg (width (n,(M @),(K @))) is V48() V55( width (n,(M @),(K @))) Element of bool NAT
[:(dom (n,(M @),(K @))),(Seg (width (n,(M @),(K @)))):] is Relation-like V48() set
dom (M @) is V48() Element of bool NAT
Seg (width (K @)) is V48() V55( width (K @)) Element of bool NAT
[:(dom (M @)),(Seg (width (K @))):] is Relation-like V48() set
(n,(M @),(K @)) * (p1,p2) is Element of the carrier of n
((n,K,M) @) * (p1,p2) is Element of the carrier of n
dom K is V48() Element of bool NAT
Col ((K @),p2) is Relation-like NAT -defined the carrier of n -valued Function-like V48() V55( len (K @)) FinSequence-like FinSubsequence-like Element of (len (K @)) -tuples_on the carrier of n
(len (K @)) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = len (K @) } is set
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
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = width K } is set
Seg (len K) is V48() V55( len K) Element of bool NAT
Seg (len (n,K,M)) is V48() V55( len (n,K,M)) Element of bool NAT
dom (n,K,M) is V48() Element of bool NAT
Seg (width M) is V48() V55( width M) Element of bool NAT
Seg (width (n,K,M)) is V48() V55( width (n,K,M)) Element of bool NAT
[p2,p1] is V23() set
[:(dom (n,K,M)),(Seg (width (n,K,M))):] is Relation-like V48() set
Indices (n,K,M) is set
Line ((M @),p1) is Relation-like NAT -defined the carrier of n -valued Function-like V48() V55( width (M @)) FinSequence-like FinSubsequence-like Element of (width (M @)) -tuples_on the carrier of n
(width (M @)) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = width (M @) } is set
Col (M,p1) 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
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = len M } is set
(n,(M @),(K @)) * (p1,p2) is Element of the carrier of n
(Col (M,p1)) "*" (Line (K,p2)) is Element of the carrier of n
(Line (K,p2)) "*" (Col (M,p1)) is Element of the carrier of n
(n,K,M) * (p2,p1) is Element of the carrier of n
((n,K,M) @) * (p1,p2) is Element of the carrier of n
len ((n,K,M) @) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
n is non empty set
Fin n is non empty cup-closed diff-closed preBoolean set
K is non empty set
Fin K is non empty cup-closed diff-closed preBoolean set
M is V48() Element of Fin n
p1 is V48() Element of Fin K
[:M,p1:] is Relation-like V48() set
[:n,K:] is Relation-like non empty set
Fin [:n,K:] is non empty cup-closed diff-closed preBoolean set
M is non empty set
[:M,M:] is Relation-like non empty set
[:[:M,M:],M:] is Relation-like non empty set
bool [:[:M,M:],M:] is non empty cup-closed diff-closed preBoolean set
n is non empty set
[:n,M:] is Relation-like non empty set
bool [:n,M:] is non empty cup-closed diff-closed preBoolean set
K is non empty set
[:K,M:] is Relation-like non empty set
bool [:K,M:] is non empty cup-closed diff-closed preBoolean set
p1 is Relation-like [:M,M:] -defined M -valued Function-like non empty total V26([:M,M:],M) Element of bool [:[:M,M:],M:]
p2 is Relation-like n -defined M -valued Function-like non empty total V26(n,M) Element of bool [:n,M:]
i is Relation-like K -defined M -valued Function-like non empty total V26(K,M) Element of bool [:K,M:]
p1 * (p2,i) is Relation-like Function-like set
[:n,K:] is Relation-like non empty set
[:[:n,K:],M:] is Relation-like non empty set
bool [:[:n,K:],M:] is non empty cup-closed diff-closed preBoolean set
M is non empty set
[:M,M:] is Relation-like non empty set
[:[:M,M:],M:] is Relation-like non empty set
bool [:[:M,M:],M:] is non empty cup-closed diff-closed preBoolean set
n is non empty set
[:n,M:] is Relation-like non empty set
bool [:n,M:] is non empty cup-closed diff-closed preBoolean set
K is non empty set
[:K,M:] is Relation-like non empty set
bool [:K,M:] is non empty cup-closed diff-closed preBoolean set
Fin n is non empty cup-closed diff-closed preBoolean set
Fin K is non empty cup-closed diff-closed preBoolean set
[:n,K:] is Relation-like non empty set
[:K,n:] is Relation-like non empty set
p1 is Relation-like [:M,M:] -defined M -valued Function-like non empty total V26([:M,M:],M) Element of bool [:[:M,M:],M:]
p2 is Relation-like [:M,M:] -defined M -valued Function-like non empty total V26([:M,M:],M) Element of bool [:[:M,M:],M:]
i is Relation-like n -defined M -valued Function-like non empty total V26(n,M) Element of bool [:n,M:]
p is Relation-like K -defined M -valued Function-like non empty total V26(K,M) Element of bool [:K,M:]
(n,K,M,p2,i,p) is Relation-like [:n,K:] -defined M -valued Function-like non empty total V26([:n,K:],M) Element of bool [:[:n,K:],M:]
[:[:n,K:],M:] is Relation-like non empty set
bool [:[:n,K:],M:] is non empty cup-closed diff-closed preBoolean set
(K,n,M,p2,p,i) is Relation-like [:K,n:] -defined M -valued Function-like non empty total V26([:K,n:],M) Element of bool [:[:K,n:],M:]
[:[:K,n:],M:] is Relation-like non empty set
bool [:[:K,n:],M:] is non empty cup-closed diff-closed preBoolean set
i is V48() Element of Fin n
j is V48() Element of Fin K
(K,n,j,i) is Relation-like V48() Element of Fin [:K,n:]
Fin [:K,n:] is non empty cup-closed diff-closed preBoolean set
(n,K,i,j) is Relation-like V48() Element of Fin [:n,K:]
Fin [:n,K:] is non empty cup-closed diff-closed preBoolean set
p1 $$ ((n,K,i,j),(n,K,M,p2,i,p)) is Element of M
p1 $$ ((K,n,j,i),(K,n,M,p2,p,i)) is Element of M
c₁₀ is Relation-like Function-like set
proj1 c₁₀ is set
h is set
k9 is set
c₁₀ . h is set
c₁₀ . k9 is set
k is set
p is set
[k,p] is V23() set
c₁₀ . (k,p) is set
c₁₀ . [k,p] is set
[p,k] is V23() set
a is set
l is set
[a,l] is V23() set
c₁₀ . (a,l) is set
c₁₀ . [a,l] is set
[l,a] is V23() set
h is set
c₁₀ . h is set
k9 is set
k is set
[k9,k] is V23() set
c₁₀ . (k9,k) is set
c₁₀ . [k9,k] is set
[k,k9] is V23() set
c₁₀ * (n,K,M,p2,i,p) is Relation-like M -valued Function-like set
h is Relation-like [:M,M:] -defined M -valued Function-like non empty total V26([:M,M:],M) Element of bool [:[:M,M:],M:]
(K,n,M,h,p,i) is Relation-like [:K,n:] -defined M -valued Function-like non empty total V26([:K,n:],M) Element of bool [:[:K,n:],M:]
proj1 (K,n,M,h,p,i) is Relation-like non empty set
(n,K,M,h,i,p) is Relation-like [:n,K:] -defined M -valued Function-like non empty total V26([:n,K:],M) Element of bool [:[:n,K:],M:]
proj1 (n,K,M,h,i,p) is Relation-like non empty set
k9 is set
c₁₀ . k9 is set
k is set
p is set
[k,p] is V23() set
c₁₀ . (k,p) is set
c₁₀ . [k,p] is set
[p,k] is V23() set
k9 is set
(K,n,M,h,p,i) . k9 is set
c₁₀ . k9 is set
(n,K,M,h,i,p) . (c₁₀ . k9) is set
k is set
p is set
[k,p] is V23() set
a is Element of n
l is Element of K
[a,l] is V23() set
[l,a] is V23() set
c₁₀ . (l,a) is set
c₁₀ . [l,a] is set
(n,K,M,h,i,p) . (c₁₀ . (l,a)) is set
(n,K,M,h,i,p) . (a,l) is Element of M
(n,K,M,h,i,p) . [a,l] is set
i . a is Element of M
p . l is Element of M
h . ((i . a),(p . l)) is Element of M
[(i . a),(p . l)] is V23() set
h . [(i . a),(p . l)] is set
h . ((p . l),(i . a)) is Element of M
[(p . l),(i . a)] is V23() set
h . [(p . l),(i . a)] is set
(K,n,M,h,p,i) . (l,a) is Element of M
(K,n,M,h,p,i) . [l,a] is set
c₁₀ .: (K,n,j,i) is V48() set
h is set
k9 is set
k is set
[k9,k] is V23() set
[k,k9] is V23() set
c₁₀ . (k,k9) is set
c₁₀ . [k,k9] is set
k9 is set
c₁₀ . k9 is set
k is set
p is set
[k,p] is V23() set
c₁₀ . (k,p) is set
c₁₀ . [k,p] is set
[p,k] is V23() set
[:[:K,n:],[:n,K:]:] is Relation-like non empty set
bool [:[:K,n:],[:n,K:]:] is non empty cup-closed diff-closed preBoolean set
h is Relation-like [:K,n:] -defined [:n,K:] -valued Function-like non empty total V26([:K,n:],[:n,K:]) Element of bool [:[:K,n:],[:n,K:]:]
(n,K,M,p2,i,p) * h is Relation-like [:K,n:] -defined M -valued Function-like non empty total V26([:K,n:],M) Element of bool [:[:K,n:],M:]
p1 $$ ((K,n,j,i),((n,K,M,p2,i,p) * h)) is Element of M
n is non empty set
[:n,n:] is Relation-like non empty set
[:[:n,n:],n:] is Relation-like non empty set
bool [:[:n,n:],n:] is non empty cup-closed diff-closed preBoolean set
K is non empty set
[:K,n:] is Relation-like non empty set
bool [:K,n:] is non empty cup-closed diff-closed preBoolean set
M is non empty set
[:M,n:] is Relation-like non empty set
bool [:M,n:] is non empty cup-closed diff-closed preBoolean set
[:K,M:] is Relation-like non empty set
p1 is Relation-like [:n,n:] -defined n -valued Function-like non empty total V26([:n,n:],n) Element of bool [:[:n,n:],n:]
p2 is Relation-like [:n,n:] -defined n -valued Function-like non empty total V26([:n,n:],n) Element of bool [:[:n,n:],n:]
i is Relation-like K -defined n -valued Function-like non empty total V26(K,n) Element of bool [:K,n:]
p is Relation-like M -defined n -valued Function-like non empty total V26(M,n) Element of bool [:M,n:]
(K,M,n,p2,i,p) is Relation-like [:K,M:] -defined n -valued Function-like non empty total V26([:K,M:],n) Element of bool [:[:K,M:],n:]
[:[:K,M:],n:] is Relation-like non empty set
bool [:[:K,M:],n:] is non empty cup-closed diff-closed preBoolean set
i is Relation-like [:n,n:] -defined n -valued Function-like non empty total V26([:n,n:],n) Element of bool [:[:n,n:],n:]
(K,M,n,i,i,p) is Relation-like [:K,M:] -defined n -valued Function-like non empty total V26([:K,M:],n) Element of bool [:[:K,M:],n:]
proj1 (K,M,n,i,i,p) is Relation-like non empty set
j is Element of K
c₁₀ is Element of M
[j,c₁₀] is V23() set
p . c₁₀ is Element of n
proj1 i is non empty set
h is Element of n
(proj1 i) --> h is Relation-like proj1 i -defined n -valued Function-like non empty total V26( proj1 i,n) Element of bool [:(proj1 i),n:]
[:(proj1 i),n:] is Relation-like non empty set
bool [:(proj1 i),n:] is non empty cup-closed diff-closed preBoolean set
<:i,((proj1 i) --> h):> is Relation-like Function-like set
proj1 <:i,((proj1 i) --> h):> is set
proj1 ((proj1 i) --> h) is non empty set
(proj1 i) /\ (proj1 ((proj1 i) --> h)) is set
(proj1 i) /\ (proj1 i) is set
proj2 i is non empty set
proj2 ((proj1 i) --> h) is non empty set
[:(proj2 i),(proj2 ((proj1 i) --> h)):] is Relation-like non empty set
proj1 i is Relation-like non empty set
proj2 <:i,((proj1 i) --> h):> is set
<:i,((proj1 i) --> h):> * i is Relation-like n -valued Function-like set
proj1 (<:i,((proj1 i) --> h):> * i) is set
i [:] (i,h) is Relation-like K -defined n -valued Function-like non empty total V26(K,n) Element of bool [:K,n:]
proj1 (i [:] (i,h)) is non empty set
{.j.} is non empty trivial V48() V55(1) Element of Fin K
Fin K is non empty cup-closed diff-closed preBoolean set
{.c₁₀.} is non empty trivial V48() V55(1) Element of Fin M
Fin M is non empty cup-closed diff-closed preBoolean set
p1 $$ ({.c₁₀.},p) is Element of n
i [:] (i,(p1 $$ ({.c₁₀.},p))) is Relation-like K -defined n -valued Function-like non empty total V26(K,n) Element of bool [:K,n:]
p1 $$ ({.j.},(i [:] (i,(p1 $$ ({.c₁₀.},p))))) is Element of n
(i [:] (i,(p1 $$ ({.c₁₀.},p)))) . j is Element of n
i [:] (i,(p . c₁₀)) is Relation-like K -defined n -valued Function-like non empty total V26(K,n) Element of bool [:K,n:]
(i [:] (i,(p . c₁₀))) . j is Element of n
i . j is Element of n
i . ((i . j),(p . c₁₀)) is Element of n
[(i . j),(p . c₁₀)] is V23() set
i . [(i . j),(p . c₁₀)] is set
(K,M,{.j.},{.c₁₀.}) is Relation-like non empty V48() Element of Fin [:K,M:]
Fin [:K,M:] is non empty cup-closed diff-closed preBoolean set
p1 $$ ((K,M,{.j.},{.c₁₀.}),(K,M,n,i,i,p)) is Element of n
k9 is Element of [:K,M:]
{.k9.} is non empty trivial V48() V55(1) Element of Fin [:K,M:]
p1 $$ ({.k9.},(K,M,n,i,i,p)) is Element of n
(K,M,n,i,i,p) . (j,c₁₀) is Element of n
(K,M,n,i,i,p) . [j,c₁₀] is set
j is Element of K
{.j.} is non empty trivial V48() V55(1) Element of Fin K
c₁₀ is Element of M
{.c₁₀.} is non empty trivial V48() V55(1) Element of Fin M
(K,M,{.j.},{.c₁₀.}) is Relation-like non empty V48() Element of Fin [:K,M:]
p1 $$ ((K,M,{.j.},{.c₁₀.}),(K,M,n,p2,i,p)) is Element of n
p1 $$ ({.c₁₀.},p) is Element of n
p2 [:] (i,(p1 $$ ({.c₁₀.},p))) is Relation-like K -defined n -valued Function-like non empty total V26(K,n) Element of bool [:K,n:]
p1 $$ ({.j.},(p2 [:] (i,(p1 $$ ({.c₁₀.},p))))) is Element of n
n is non empty set
[:n,n:] is Relation-like non empty set
[:[:n,n:],n:] is Relation-like non empty set
bool [:[:n,n:],n:] is non empty cup-closed diff-closed preBoolean set
K is non empty set
[:K,n:] is Relation-like non empty set
bool [:K,n:] is non empty cup-closed diff-closed preBoolean set
M is non empty set
[:M,n:] is Relation-like non empty set
bool [:M,n:] is non empty cup-closed diff-closed preBoolean set
Fin K is non empty cup-closed diff-closed preBoolean set
Fin M is non empty cup-closed diff-closed preBoolean set
[:K,M:] is Relation-like non empty set
p1 is Relation-like [:n,n:] -defined n -valued Function-like non empty total V26([:n,n:],n) Element of bool [:[:n,n:],n:]
p2 is Relation-like [:n,n:] -defined n -valued Function-like non empty total V26([:n,n:],n) Element of bool [:[:n,n:],n:]
i is Relation-like K -defined n -valued Function-like non empty total V26(K,n) Element of bool [:K,n:]
p is Relation-like M -defined n -valued Function-like non empty total V26(M,n) Element of bool [:M,n:]
(K,M,n,p2,i,p) is Relation-like [:K,M:] -defined n -valued Function-like non empty total V26([:K,M:],n) Element of bool [:[:K,M:],n:]
[:[:K,M:],n:] is Relation-like non empty set
bool [:[:K,M:],n:] is non empty cup-closed diff-closed preBoolean set
j is V48() Element of Fin M
p1 $$ (j,p) is Element of n
p2 [:] (i,(p1 $$ (j,p))) is Relation-like K -defined n -valued Function-like non empty total V26(K,n) Element of bool [:K,n:]
c₁₀ is Element of K
{.c₁₀.} is non empty trivial V48() V55(1) Element of Fin K
{}. M 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 Fin M
(K,M,{.c₁₀.},({}. M)) is Relation-like V48() Element of Fin [:K,M:]
Fin [:K,M:] is non empty cup-closed diff-closed preBoolean set
p1 $$ ((K,M,{.c₁₀.},({}. M)),(K,M,n,p2,i,p)) is Element of n
p1 $$ (({}. M),p) is Element of n
p2 [:] (i,(p1 $$ (({}. M),p))) is Relation-like K -defined n -valued Function-like non empty total V26(K,n) Element of bool [:K,n:]
p1 $$ ({.c₁₀.},(p2 [:] (i,(p1 $$ (({}. M),p))))) is Element of n
the_unity_wrt p1 is Element of n
{}. [:K,M:] 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 Fin [:K,M:]
k9 is V48() Element of Fin [:K,M:]
{c₁₀} is non empty trivial V48() V55(1) set
[:{c₁₀},({}. M):] is Relation-like V48() set
proj1 i is non empty set
(proj1 i) --> (the_unity_wrt p1) is Relation-like proj1 i -defined n -valued Function-like non empty total V26( proj1 i,n) Element of bool [:(proj1 i),n:]
[:(proj1 i),n:] is Relation-like non empty set
bool [:(proj1 i),n:] is non empty cup-closed diff-closed preBoolean set
<:i,((proj1 i) --> (the_unity_wrt p1)):> is Relation-like Function-like set
proj1 <:i,((proj1 i) --> (the_unity_wrt p1)):> is set
proj1 ((proj1 i) --> (the_unity_wrt p1)) is non empty set
(proj1 i) /\ (proj1 ((proj1 i) --> (the_unity_wrt p1))) is set
(proj1 i) /\ (proj1 i) is set
proj2 i is non empty set
proj2 ((proj1 i) --> (the_unity_wrt p1)) is non empty set
[:(proj2 i),(proj2 ((proj1 i) --> (the_unity_wrt p1))):] is Relation-like non empty set
proj1 p2 is Relation-like non empty set
proj2 <:i,((proj1 i) --> (the_unity_wrt p1)):> is set
<:i,((proj1 i) --> (the_unity_wrt p1)):> * p2 is Relation-like n -valued Function-like set
proj1 (<:i,((proj1 i) --> (the_unity_wrt p1)):> * p2) is set
p2 [:] (i,(the_unity_wrt p1)) is Relation-like K -defined n -valued Function-like non empty total V26(K,n) Element of bool [:K,n:]
proj1 (p2 [:] (i,(the_unity_wrt p1))) is non empty set
p1 $$ ({.c₁₀.},(p2 [:] (i,(the_unity_wrt p1)))) is Element of n
(p2 [:] (i,(the_unity_wrt p1))) . c₁₀ is Element of n
i . c₁₀ is Element of n
p2 . ((i . c₁₀),(the_unity_wrt p1)) is Element of n
[(i . c₁₀),(the_unity_wrt p1)] is V23() set
p2 . [(i . c₁₀),(the_unity_wrt p1)] is set
h is V48() Element of Fin M
(K,M,{.c₁₀.},h) is Relation-like V48() Element of Fin [:K,M:]
p1 $$ ((K,M,{.c₁₀.},h),(K,M,n,p2,i,p)) is Element of n
p1 $$ (h,p) is Element of n
p2 [:] (i,(p1 $$ (h,p))) is Relation-like K -defined n -valued Function-like non empty total V26(K,n) Element of bool [:K,n:]
p1 $$ ({.c₁₀.},(p2 [:] (i,(p1 $$ (h,p))))) is Element of n
k9 is Element of M
{.k9.} is non empty trivial V48() V55(1) Element of Fin M
h \/ {.k9.} is non empty V48() Element of Fin M
(K,M,{.c₁₀.},(h \/ {.k9.})) is Relation-like non empty V48() Element of Fin [:K,M:]
p1 $$ ((K,M,{.c₁₀.},(h \/ {.k9.})),(K,M,n,p2,i,p)) is Element of n
p1 $$ ((h \/ {.k9.}),p) is Element of n
p2 [:] (i,(p1 $$ ((h \/ {.k9.}),p))) is Relation-like K -defined n -valued Function-like non empty total V26(K,n) Element of bool [:K,n:]
p1 $$ ({.c₁₀.},(p2 [:] (i,(p1 $$ ((h \/ {.k9.}),p))))) is Element of n
{k9} is non empty trivial V48() V55(1) set
h \/ {k9} is non empty V48() set
{k9} is non empty trivial V48() V55(1) set
{c₁₀} is non empty trivial V48() V55(1) set
[:{c₁₀},h:] is Relation-like V48() set
k is V48() Element of Fin M
[:{c₁₀},k:] is Relation-like V48() set
(K,M,{.c₁₀.},k) is Relation-like V48() Element of Fin [:K,M:]
(K,M,{.c₁₀.},h) \/ (K,M,{.c₁₀.},k) is Relation-like V48() Element of Fin [:K,M:]
p1 $$ (((K,M,{.c₁₀.},h) \/ (K,M,{.c₁₀.},k)),(K,M,n,p2,i,p)) is Element of n
p1 $$ ((K,M,{.c₁₀.},k),(K,M,n,p2,i,p)) is Element of n
p1 . ((p1 $$ ((K,M,{.c₁₀.},h),(K,M,n,p2,i,p))),(p1 $$ ((K,M,{.c₁₀.},k),(K,M,n,p2,i,p)))) is Element of n
[(p1 $$ ((K,M,{.c₁₀.},h),(K,M,n,p2,i,p))),(p1 $$ ((K,M,{.c₁₀.},k),(K,M,n,p2,i,p)))] is V23() set
p1 . [(p1 $$ ((K,M,{.c₁₀.},h),(K,M,n,p2,i,p))),(p1 $$ ((K,M,{.c₁₀.},k),(K,M,n,p2,i,p)))] is set
p1 $$ (k,p) is Element of n
p2 [:] (i,(p1 $$ (k,p))) is Relation-like K -defined n -valued Function-like non empty total V26(K,n) Element of bool [:K,n:]
p1 $$ ({.c₁₀.},(p2 [:] (i,(p1 $$ (k,p))))) is Element of n
p1 . ((p1 $$ ({.c₁₀.},(p2 [:] (i,(p1 $$ (h,p)))))),(p1 $$ ({.c₁₀.},(p2 [:] (i,(p1 $$ (k,p))))))) is Element of n
[(p1 $$ ({.c₁₀.},(p2 [:] (i,(p1 $$ (h,p)))))),(p1 $$ ({.c₁₀.},(p2 [:] (i,(p1 $$ (k,p))))))] is V23() set
p1 . [(p1 $$ ({.c₁₀.},(p2 [:] (i,(p1 $$ (h,p)))))),(p1 $$ ({.c₁₀.},(p2 [:] (i,(p1 $$ (k,p))))))] is set
p1 .: ((p2 [:] (i,(p1 $$ (h,p)))),(p2 [:] (i,(p1 $$ (k,p))))) is Relation-like K -defined n -valued Function-like non empty total V26(K,n) Element of bool [:K,n:]
p1 $$ ({.c₁₀.},(p1 .: ((p2 [:] (i,(p1 $$ (h,p)))),(p2 [:] (i,(p1 $$ (k,p))))))) is Element of n
p1 . ((p1 $$ (h,p)),(p1 $$ (k,p))) is Element of n
[(p1 $$ (h,p)),(p1 $$ (k,p))] is V23() set
p1 . [(p1 $$ (h,p)),(p1 $$ (k,p))] is set
p2 [:] (i,(p1 . ((p1 $$ (h,p)),(p1 $$ (k,p))))) is Relation-like K -defined n -valued Function-like non empty total V26(K,n) Element of bool [:K,n:]
p1 $$ ({.c₁₀.},(p2 [:] (i,(p1 . ((p1 $$ (h,p)),(p1 $$ (k,p))))))) is Element of n
c₁₀ is Element of K
{.c₁₀.} is non empty trivial V48() V55(1) Element of Fin K
(K,M,{.c₁₀.},j) is Relation-like V48() Element of Fin [:K,M:]
p1 $$ ((K,M,{.c₁₀.},j),(K,M,n,p2,i,p)) is Element of n
p1 $$ ({.c₁₀.},(p2 [:] (i,(p1 $$ (j,p))))) is Element of n
n is non empty set
[:n,n:] is Relation-like non empty set
[:[:n,n:],n:] is Relation-like non empty set
bool [:[:n,n:],n:] is non empty cup-closed diff-closed preBoolean set
K is non empty set
[:K,n:] is Relation-like non empty set
bool [:K,n:] is non empty cup-closed diff-closed preBoolean set
M is non empty set
[:M,n:] is Relation-like non empty set
bool [:M,n:] is non empty cup-closed diff-closed preBoolean set
Fin K is non empty cup-closed diff-closed preBoolean set
Fin M is non empty cup-closed diff-closed preBoolean set
[:K,M:] is Relation-like non empty set
p1 is Relation-like [:n,n:] -defined n -valued Function-like non empty total V26([:n,n:],n) Element of bool [:[:n,n:],n:]
p2 is Relation-like [:n,n:] -defined n -valued Function-like non empty total V26([:n,n:],n) Element of bool [:[:n,n:],n:]
i is Relation-like K -defined n -valued Function-like non empty total V26(K,n) Element of bool [:K,n:]
p is Relation-like M -defined n -valued Function-like non empty total V26(M,n) Element of bool [:M,n:]
(K,M,n,p2,i,p) is Relation-like [:K,M:] -defined n -valued Function-like non empty total V26([:K,M:],n) Element of bool [:[:K,M:],n:]
[:[:K,M:],n:] is Relation-like non empty set
bool [:[:K,M:],n:] is non empty cup-closed diff-closed preBoolean set
i is V48() Element of Fin K
j is V48() Element of Fin M
(K,M,i,j) is Relation-like V48() Element of Fin [:K,M:]
Fin [:K,M:] is non empty cup-closed diff-closed preBoolean set
p1 $$ ((K,M,i,j),(K,M,n,p2,i,p)) is Element of n
p1 $$ (j,p) is Element of n
p2 [:] (i,(p1 $$ (j,p))) is Relation-like K -defined n -valued Function-like non empty total V26(K,n) Element of bool [:K,n:]
p1 $$ (i,(p2 [:] (i,(p1 $$ (j,p))))) is Element of n
c₁₀ is V48() Element of Fin K
(K,M,c₁₀,j) is Relation-like V48() Element of Fin [:K,M:]
p1 $$ ((K,M,c₁₀,j),(K,M,n,p2,i,p)) is Element of n
p1 $$ (c₁₀,(p2 [:] (i,(p1 $$ (j,p))))) is Element of n
h is Element of K
{.h.} is non empty trivial V48() V55(1) Element of Fin K
c₁₀ \/ {.h.} is non empty V48() Element of Fin K
(K,M,(c₁₀ \/ {.h.}),j) is Relation-like V48() Element of Fin [:K,M:]
p1 $$ ((K,M,(c₁₀ \/ {.h.}),j),(K,M,n,p2,i,p)) is Element of n
p1 $$ ((c₁₀ \/ {.h.}),(p2 [:] (i,(p1 $$ (j,p))))) is Element of n
{h} is non empty trivial V48() V55(1) set
c₁₀ \/ {h} is non empty V48() set
{h} is non empty trivial V48() V55(1) set
k9 is V48() Element of Fin K
(K,M,k9,j) is Relation-like V48() Element of Fin [:K,M:]
(K,M,c₁₀,j) \/ (K,M,k9,j) is Relation-like V48() Element of Fin [:K,M:]
p1 $$ (((K,M,c₁₀,j) \/ (K,M,k9,j)),(K,M,n,p2,i,p)) is Element of n
p1 $$ ((K,M,k9,j),(K,M,n,p2,i,p)) is Element of n
p1 . ((p1 $$ ((K,M,c₁₀,j),(K,M,n,p2,i,p))),(p1 $$ ((K,M,k9,j),(K,M,n,p2,i,p)))) is Element of n
[(p1 $$ ((K,M,c₁₀,j),(K,M,n,p2,i,p))),(p1 $$ ((K,M,k9,j),(K,M,n,p2,i,p)))] is V23() set
p1 . [(p1 $$ ((K,M,c₁₀,j),(K,M,n,p2,i,p))),(p1 $$ ((K,M,k9,j),(K,M,n,p2,i,p)))] is set
p1 $$ (k9,(p2 [:] (i,(p1 $$ (j,p))))) is Element of n
p1 . ((p1 $$ (c₁₀,(p2 [:] (i,(p1 $$ (j,p)))))),(p1 $$ (k9,(p2 [:] (i,(p1 $$ (j,p))))))) is Element of n
[(p1 $$ (c₁₀,(p2 [:] (i,(p1 $$ (j,p)))))),(p1 $$ (k9,(p2 [:] (i,(p1 $$ (j,p))))))] is V23() set
p1 . [(p1 $$ (c₁₀,(p2 [:] (i,(p1 $$ (j,p)))))),(p1 $$ (k9,(p2 [:] (i,(p1 $$ (j,p))))))] is set
{}. K 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 Fin K
(K,M,({}. K),j) is Relation-like V48() Element of Fin [:K,M:]
p1 $$ ((K,M,({}. K),j),(K,M,n,p2,i,p)) is Element of n
p1 $$ (({}. K),(p2 [:] (i,(p1 $$ (j,p))))) is Element of n
{}. [:K,M:] 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 Fin [:K,M:]
c₁₀ is V48() Element of Fin [:K,M:]
the_unity_wrt p1 is Element of n
n is non empty set
[:n,n:] is Relation-like non empty set
[:[:n,n:],n:] is Relation-like non empty set
bool [:[:n,n:],n:] is non empty cup-closed diff-closed preBoolean set
K is non empty set
[:K,n:] is Relation-like non empty set
bool [:K,n:] is non empty cup-closed diff-closed preBoolean set
M is non empty set
[:M,n:] is Relation-like non empty set
bool [:M,n:] is non empty cup-closed diff-closed preBoolean set
[:K,M:] is Relation-like non empty set
p1 is Relation-like [:n,n:] -defined n -valued Function-like non empty total V26([:n,n:],n) Element of bool [:[:n,n:],n:]
p2 is Relation-like [:n,n:] -defined n -valued Function-like non empty total V26([:n,n:],n) Element of bool [:[:n,n:],n:]
i is Relation-like K -defined n -valued Function-like non empty total V26(K,n) Element of bool [:K,n:]
p is Relation-like M -defined n -valued Function-like non empty total V26(M,n) Element of bool [:M,n:]
(K,M,n,p2,i,p) is Relation-like [:K,M:] -defined n -valued Function-like non empty total V26([:K,M:],n) Element of bool [:[:K,M:],n:]
[:[:K,M:],n:] is Relation-like non empty set
bool [:[:K,M:],n:] is non empty cup-closed diff-closed preBoolean set
i is Element of K
{.i.} is non empty trivial V48() V55(1) Element of Fin K
Fin K is non empty cup-closed diff-closed preBoolean set
j is Element of M
{.j.} is non empty trivial V48() V55(1) Element of Fin M
Fin M is non empty cup-closed diff-closed preBoolean set
(K,M,{.i.},{.j.}) is Relation-like non empty V48() Element of Fin [:K,M:]
Fin [:K,M:] is non empty cup-closed diff-closed preBoolean set
p1 $$ ((K,M,{.i.},{.j.}),(K,M,n,p2,i,p)) is Element of n
[:M,K:] is Relation-like non empty set
(M,K,{.j.},{.i.}) is Relation-like non empty V48() Element of Fin [:M,K:]
Fin [:M,K:] is non empty cup-closed diff-closed preBoolean set
(M,K,n,p2,p,i) is Relation-like [:M,K:] -defined n -valued Function-like non empty total V26([:M,K:],n) Element of bool [:[:M,K:],n:]
[:[:M,K:],n:] is Relation-like non empty set
bool [:[:M,K:],n:] is non empty cup-closed diff-closed preBoolean set
p1 $$ ((M,K,{.j.},{.i.}),(M,K,n,p2,p,i)) is Element of n
p1 $$ ({.i.},i) is Element of n
p2 [:] (p,(p1 $$ ({.i.},i))) is Relation-like M -defined n -valued Function-like non empty total V26(M,n) Element of bool [:M,n:]
p1 $$ ({.j.},(p2 [:] (p,(p1 $$ ({.i.},i))))) is Element of n
p2 [;] ((p1 $$ ({.i.},i)),p) is Relation-like M -defined n -valued Function-like non empty total V26(M,n) Element of bool [:M,n:]
p1 $$ ({.j.},(p2 [;] ((p1 $$ ({.i.},i)),p))) is Element of n
i is Element of K
{.i.} is non empty trivial V48() V55(1) Element of Fin K
j is Element of M
{.j.} is non empty trivial V48() V55(1) Element of Fin M
(K,M,{.i.},{.j.}) is Relation-like non empty V48() Element of Fin [:K,M:]
p1 $$ ((K,M,{.i.},{.j.}),(K,M,n,p2,i,p)) is Element of n
p1 $$ ({.i.},i) is Element of n
p2 [;] ((p1 $$ ({.i.},i)),p) is Relation-like M -defined n -valued Function-like non empty total V26(M,n) Element of bool [:M,n:]
p1 $$ ({.j.},(p2 [;] ((p1 $$ ({.i.},i)),p))) is Element of n
n is non empty set
[:n,n:] is Relation-like non empty set
[:[:n,n:],n:] is Relation-like non empty set
bool [:[:n,n:],n:] is non empty cup-closed diff-closed preBoolean set
K is non empty set
[:K,n:] is Relation-like non empty set
bool [:K,n:] is non empty cup-closed diff-closed preBoolean set
M is non empty set
[:M,n:] is Relation-like non empty set
bool [:M,n:] is non empty cup-closed diff-closed preBoolean set
Fin K is non empty cup-closed diff-closed preBoolean set
Fin M is non empty cup-closed diff-closed preBoolean set
[:K,M:] is Relation-like non empty set
p1 is Relation-like [:n,n:] -defined n -valued Function-like non empty total V26([:n,n:],n) Element of bool [:[:n,n:],n:]
p2 is Relation-like [:n,n:] -defined n -valued Function-like non empty total V26([:n,n:],n) Element of bool [:[:n,n:],n:]
i is Relation-like K -defined n -valued Function-like non empty total V26(K,n) Element of bool [:K,n:]
p is Relation-like M -defined n -valued Function-like non empty total V26(M,n) Element of bool [:M,n:]
(K,M,n,p2,i,p) is Relation-like [:K,M:] -defined n -valued Function-like non empty total V26([:K,M:],n) Element of bool [:[:K,M:],n:]
[:[:K,M:],n:] is Relation-like non empty set
bool [:[:K,M:],n:] is non empty cup-closed diff-closed preBoolean set
i is V48() Element of Fin K
p1 $$ (i,i) is Element of n
p2 [;] ((p1 $$ (i,i)),p) is Relation-like M -defined n -valued Function-like non empty total V26(M,n) Element of bool [:M,n:]
j is V48() Element of Fin M
(K,M,i,j) is Relation-like V48() Element of Fin [:K,M:]
Fin [:K,M:] is non empty cup-closed diff-closed preBoolean set
p1 $$ ((K,M,i,j),(K,M,n,p2,i,p)) is Element of n
p1 $$ (j,(p2 [;] ((p1 $$ (i,i)),p))) is Element of n
[:M,K:] is Relation-like non empty set
(M,K,j,i) is Relation-like V48() Element of Fin [:M,K:]
Fin [:M,K:] is non empty cup-closed diff-closed preBoolean set
(M,K,n,p2,p,i) is Relation-like [:M,K:] -defined n -valued Function-like non empty total V26([:M,K:],n) Element of bool [:[:M,K:],n:]
[:[:M,K:],n:] is Relation-like non empty set
bool [:[:M,K:],n:] is non empty cup-closed diff-closed preBoolean set
p1 $$ ((M,K,j,i),(M,K,n,p2,p,i)) is Element of n
p2 [:] (p,(p1 $$ (i,i))) is Relation-like M -defined n -valued Function-like non empty total V26(M,n) Element of bool [:M,n:]
p1 $$ (j,(p2 [:] (p,(p1 $$ (i,i))))) is Element of n
n is non empty set
[:n,n:] is Relation-like non empty set
[:[:n,n:],n:] is Relation-like non empty set
bool [:[:n,n:],n:] is non empty cup-closed diff-closed preBoolean set
K is non empty set
M is non empty set
[:K,M:] is Relation-like non empty set
[:[:K,M:],n:] is Relation-like non empty set
bool [:[:K,M:],n:] is non empty cup-closed diff-closed preBoolean set
[:K,n:] is Relation-like non empty set
bool [:K,n:] is non empty cup-closed diff-closed preBoolean set
Fin M is non empty cup-closed diff-closed preBoolean set
K86(M,n) is functional non empty M4(M,n)
p1 is Relation-like [:n,n:] -defined n -valued Function-like non empty total V26([:n,n:],n) Element of bool [:[:n,n:],n:]
p2 is Relation-like [:K,M:] -defined n -valued Function-like non empty total V26([:K,M:],n) Element of bool [:[:K,M:],n:]
curry p2 is Relation-like K -defined K86(M,n) -valued Function-like non empty total V26(K,K86(M,n)) Element of bool [:K,K86(M,n):]
[:K,K86(M,n):] is Relation-like non empty set
bool [:K,K86(M,n):] is non empty cup-closed diff-closed preBoolean set
i is Relation-like K -defined n -valued Function-like non empty total V26(K,n) Element of bool [:K,n:]
p is V48() Element of Fin M
i is Element of K
j is Relation-like Function-like set
proj1 j is set
(curry p2) . i is Relation-like M -defined n -valued Function-like total V26(M,n) Element of K86(M,n)
proj1 ((curry p2) . i) is set
j * p2 is Relation-like n -valued Function-like set
proj1 (j * p2) is set
proj2 j is set
proj1 p2 is Relation-like non empty set
proj2 p2 is non empty set
c₁₀ is Relation-like Function-like set
proj1 c₁₀ is set
proj2 c₁₀ is set
c₁₀ is set
h is set
j . h is set
[i,h] is V23() set
c₁₀ is set
((curry p2) . i) . c₁₀ is set
(j * p2) . c₁₀ is set
proj1 p2 is Relation-like non empty set
proj2 p2 is non empty set
j . c₁₀ is set
p2 . (j . c₁₀) is set
p2 . (i,c₁₀) is set
[i,c₁₀] is V23() set
p2 . [i,c₁₀] is set
h is Relation-like Function-like set
proj1 h is set
proj2 h is set
{i} is non empty trivial V48() V55(1) set
[:{i},p:] is Relation-like V48() set
j .: p is V48() set
c₁₀ is set
h is set
k9 is set
[h,k9] is V23() set
j . k9 is set
[i,k9] is V23() set
h is set
j . h is set
[i,h] is V23() set
c₁₀ is set
h is set
j . c₁₀ is set
j . h is set
[i,c₁₀] is V23() set
[i,h] is V23() set
[:M,[:K,M:]:] is Relation-like non empty set
bool [:M,[:K,M:]:] is non empty cup-closed diff-closed preBoolean set
{.i.} is non empty trivial V48() V55(1) Element of Fin K
Fin K is non empty cup-closed diff-closed preBoolean set
(K,M,{.i.},p) is Relation-like V48() Element of Fin [:K,M:]
Fin [:K,M:] is non empty cup-closed diff-closed preBoolean set
p1 $$ ((K,M,{.i.},p),p2) is Element of n
c₁₀ is Relation-like M -defined [:K,M:] -valued Function-like non empty total V26(M,[:K,M:]) Element of bool [:M,[:K,M:]:]
p2 * c₁₀ is Relation-like M -defined n -valued Function-like non empty total V26(M,n) Element of bool [:M,n:]
[:M,n:] is Relation-like non empty set
bool [:M,n:] is non empty cup-closed diff-closed preBoolean set
p1 $$ (p,(p2 * c₁₀)) is Element of n
p1 $$ (p,((curry p2) . i)) is Element of n
i . i is Element of n
p1 $$ ({.i.},i) is Element of n
i is Element of K
{.i.} is non empty trivial V48() V55(1) Element of Fin K
(K,M,{.i.},p) is Relation-like V48() Element of Fin [:K,M:]
p1 $$ ((K,M,{.i.},p),p2) is Element of n
p1 $$ ({.i.},i) is Element of n
n is non empty set
[:n,n:] is Relation-like non empty set
[:[:n,n:],n:] is Relation-like non empty set
bool [:[:n,n:],n:] is non empty cup-closed diff-closed preBoolean set
K is non empty set
M is non empty set
[:K,M:] is Relation-like non empty set
[:[:K,M:],n:] is Relation-like non empty set
bool [:[:K,M:],n:] is non empty cup-closed diff-closed preBoolean set
[:K,n:] is Relation-like non empty set
bool [:K,n:] is non empty cup-closed diff-closed preBoolean set
Fin K is non empty cup-closed diff-closed preBoolean set
Fin M is non empty cup-closed diff-closed preBoolean set
K86(M,n) is functional non empty M4(M,n)
p1 is Relation-like [:n,n:] -defined n -valued Function-like non empty total V26([:n,n:],n) Element of bool [:[:n,n:],n:]
p2 is Relation-like [:K,M:] -defined n -valued Function-like non empty total V26([:K,M:],n) Element of bool [:[:K,M:],n:]
curry p2 is Relation-like K -defined K86(M,n) -valued Function-like non empty total V26(K,K86(M,n)) Element of bool [:K,K86(M,n):]
[:K,K86(M,n):] is Relation-like non empty set
bool [:K,K86(M,n):] is non empty cup-closed diff-closed preBoolean set
i is Relation-like K -defined n -valued Function-like non empty total V26(K,n) Element of bool [:K,n:]
p is V48() Element of Fin K
p1 $$ (p,i) is Element of n
i is V48() Element of Fin M
(K,M,p,i) is Relation-like V48() Element of Fin [:K,M:]
Fin [:K,M:] is non empty cup-closed diff-closed preBoolean set
p1 $$ ((K,M,p,i),p2) is Element of n
j is V48() Element of Fin K
(K,M,j,i) is Relation-like V48() Element of Fin [:K,M:]
p1 $$ ((K,M,j,i),p2) is Element of n
p1 $$ (j,i) is Element of n
c₁₀ is Element of K
{.c₁₀.} is non empty trivial V48() V55(1) Element of Fin K
j \/ {.c₁₀.} is non empty V48() Element of Fin K
(K,M,(j \/ {.c₁₀.}),i) is Relation-like V48() Element of Fin [:K,M:]
p1 $$ ((K,M,(j \/ {.c₁₀.}),i),p2) is Element of n
p1 $$ ((j \/ {.c₁₀.}),i) is Element of n
{c₁₀} is non empty trivial V48() V55(1) set
j \/ {c₁₀} is non empty V48() set
{c₁₀} is non empty trivial V48() V55(1) set
h is V48() Element of Fin K
(K,M,h,i) is Relation-like V48() Element of Fin [:K,M:]
(K,M,j,i) \/ (K,M,h,i) is Relation-like V48() Element of Fin [:K,M:]
p1 $$ (((K,M,j,i) \/ (K,M,h,i)),p2) is Element of n
p1 $$ ((K,M,h,i),p2) is Element of n
p1 . ((p1 $$ ((K,M,j,i),p2)),(p1 $$ ((K,M,h,i),p2))) is Element of n
[(p1 $$ ((K,M,j,i),p2)),(p1 $$ ((K,M,h,i),p2))] is V23() set
p1 . [(p1 $$ ((K,M,j,i),p2)),(p1 $$ ((K,M,h,i),p2))] is set
p1 $$ (h,i) is Element of n
p1 . ((p1 $$ (j,i)),(p1 $$ (h,i))) is Element of n
[(p1 $$ (j,i)),(p1 $$ (h,i))] is V23() set
p1 . [(p1 $$ (j,i)),(p1 $$ (h,i))] is set
{}. K 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 Fin K
(K,M,({}. K),i) is Relation-like V48() Element of Fin [:K,M:]
p1 $$ ((K,M,({}. K),i),p2) is Element of n
p1 $$ (({}. K),i) is Element of n
{}. [:K,M:] 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 Fin [:K,M:]
j is V48() Element of Fin [:K,M:]
the_unity_wrt p1 is Element of n
n is non empty set
[:n,n:] is Relation-like non empty set
[:[:n,n:],n:] is Relation-like non empty set
bool [:[:n,n:],n:] is non empty cup-closed diff-closed preBoolean set
K is non empty set
M is non empty set
[:K,M:] is Relation-like non empty set
[:[:K,M:],n:] is Relation-like non empty set
bool [:[:K,M:],n:] is non empty cup-closed diff-closed preBoolean set
[:M,n:] is Relation-like non empty set
bool [:M,n:] is non empty cup-closed diff-closed preBoolean set
Fin K is non empty cup-closed diff-closed preBoolean set
K86(K,n) is functional non empty M4(K,n)
p1 is Relation-like [:n,n:] -defined n -valued Function-like non empty total V26([:n,n:],n) Element of bool [:[:n,n:],n:]
p2 is Relation-like [:K,M:] -defined n -valued Function-like non empty total V26([:K,M:],n) Element of bool [:[:K,M:],n:]
curry' p2 is Relation-like M -defined K86(K,n) -valued Function-like non empty total V26(M,K86(K,n)) Element of bool [:M,K86(K,n):]
[:M,K86(K,n):] is Relation-like non empty set
bool [:M,K86(K,n):] is non empty cup-closed diff-closed preBoolean set
i is Relation-like M -defined n -valued Function-like non empty total V26(M,n) Element of bool [:M,n:]
p is V48() Element of Fin K
i is Element of M
j is Relation-like Function-like set
proj1 j is set
(curry' p2) . i is Relation-like K -defined n -valued Function-like total V26(K,n) Element of K86(K,n)
proj1 ((curry' p2) . i) is set
j * p2 is Relation-like n -valued Function-like set
proj1 (j * p2) is set
proj2 j is set
proj1 p2 is Relation-like non empty set
proj2 p2 is non empty set
c₁₀ is Relation-like Function-like set
proj1 c₁₀ is set
proj2 c₁₀ is set
c₁₀ is set
h is set
j . h is set
[h,i] is V23() set
c₁₀ is set
((curry' p2) . i) . c₁₀ is set
(j * p2) . c₁₀ is set
proj1 p2 is Relation-like non empty set
proj2 p2 is non empty set
j . c₁₀ is set
p2 . (j . c₁₀) is set
p2 . (c₁₀,i) is set
[c₁₀,i] is V23() set
p2 . [c₁₀,i] is set
h is Relation-like Function-like set
proj1 h is set
proj2 h is set
{i} is non empty trivial V48() V55(1) set
[:p,{i}:] is Relation-like V48() set
j .: p is V48() set
c₁₀ is set
h is set
k9 is set
[h,k9] is V23() set
j . h is set
[h,i] is V23() set
h is set
j . h is set
[h,i] is V23() set
c₁₀ is set
h is set
j . c₁₀ is set
j . h is set
[c₁₀,i] is V23() set
[h,i] is V23() set
[:K,[:K,M:]:] is Relation-like non empty set
bool [:K,[:K,M:]:] is non empty cup-closed diff-closed preBoolean set
{.i.} is non empty trivial V48() V55(1) Element of Fin M
Fin M is non empty cup-closed diff-closed preBoolean set
(K,M,p,{.i.}) is Relation-like V48() Element of Fin [:K,M:]
Fin [:K,M:] is non empty cup-closed diff-closed preBoolean set
p1 $$ ((K,M,p,{.i.}),p2) is Element of n
c₁₀ is Relation-like K -defined [:K,M:] -valued Function-like non empty total V26(K,[:K,M:]) Element of bool [:K,[:K,M:]:]
p2 * c₁₀ is Relation-like K -defined n -valued Function-like non empty total V26(K,n) Element of bool [:K,n:]
[:K,n:] is Relation-like non empty set
bool [:K,n:] is non empty cup-closed diff-closed preBoolean set
p1 $$ (p,(p2 * c₁₀)) is Element of n
p1 $$ (p,((curry' p2) . i)) is Element of n
i . i is Element of n
p1 $$ ({.i.},i) is Element of n
i is Element of M
{.i.} is non empty trivial V48() V55(1) Element of Fin M
(K,M,p,{.i.}) is Relation-like V48() Element of Fin [:K,M:]
p1 $$ ((K,M,p,{.i.}),p2) is Element of n
p1 $$ ({.i.},i) is Element of n
n is non empty set
[:n,n:] is Relation-like non empty set
[:[:n,n:],n:] is Relation-like non empty set
bool [:[:n,n:],n:] is non empty cup-closed diff-closed preBoolean set
K is non empty set
M is non empty set
[:K,M:] is Relation-like non empty set
[:[:K,M:],n:] is Relation-like non empty set
bool [:[:K,M:],n:] is non empty cup-closed diff-closed preBoolean set
[:M,n:] is Relation-like non empty set
bool [:M,n:] is non empty cup-closed diff-closed preBoolean set
Fin K is non empty cup-closed diff-closed preBoolean set
Fin M is non empty cup-closed diff-closed preBoolean set
K86(K,n) is functional non empty M4(K,n)
p1 is Relation-like [:n,n:] -defined n -valued Function-like non empty total V26([:n,n:],n) Element of bool [:[:n,n:],n:]
p2 is Relation-like [:K,M:] -defined n -valued Function-like non empty total V26([:K,M:],n) Element of bool [:[:K,M:],n:]
curry' p2 is Relation-like M -defined K86(K,n) -valued Function-like non empty total V26(M,K86(K,n)) Element of bool [:M,K86(K,n):]
[:M,K86(K,n):] is Relation-like non empty set
bool [:M,K86(K,n):] is non empty cup-closed diff-closed preBoolean set
i is Relation-like M -defined n -valued Function-like non empty total V26(M,n) Element of bool [:M,n:]
p is V48() Element of Fin K
i is V48() Element of Fin M
(K,M,p,i) is Relation-like V48() Element of Fin [:K,M:]
Fin [:K,M:] is non empty cup-closed diff-closed preBoolean set
p1 $$ ((K,M,p,i),p2) is Element of n
p1 $$ (i,i) is Element of n
j is V48() Element of Fin M
(K,M,p,j) is Relation-like V48() Element of Fin [:K,M:]
p1 $$ ((K,M,p,j),p2) is Element of n
p1 $$ (j,i) is Element of n
c₁₀ is Element of M
{.c₁₀.} is non empty trivial V48() V55(1) Element of Fin M
j \/ {.c₁₀.} is non empty V48() Element of Fin M
(K,M,p,(j \/ {.c₁₀.})) is Relation-like V48() Element of Fin [:K,M:]
p1 $$ ((K,M,p,(j \/ {.c₁₀.})),p2) is Element of n
p1 $$ ((j \/ {.c₁₀.}),i) is Element of n
{c₁₀} is non empty trivial V48() V55(1) set
j \/ {c₁₀} is non empty V48() set
{c₁₀} is non empty trivial V48() V55(1) set
h is V48() Element of Fin M
(K,M,p,h) is Relation-like V48() Element of Fin [:K,M:]
(K,M,p,j) \/ (K,M,p,h) is Relation-like V48() Element of Fin [:K,M:]
p1 $$ (((K,M,p,j) \/ (K,M,p,h)),p2) is Element of n
p1 $$ ((K,M,p,h),p2) is Element of n
p1 . ((p1 $$ ((K,M,p,j),p2)),(p1 $$ ((K,M,p,h),p2))) is Element of n
[(p1 $$ ((K,M,p,j),p2)),(p1 $$ ((K,M,p,h),p2))] is V23() set
p1 . [(p1 $$ ((K,M,p,j),p2)),(p1 $$ ((K,M,p,h),p2))] is set
p1 $$ (h,i) is Element of n
p1 . ((p1 $$ (j,i)),(p1 $$ (h,i))) is Element of n
[(p1 $$ (j,i)),(p1 $$ (h,i))] is V23() set
p1 . [(p1 $$ (j,i)),(p1 $$ (h,i))] is set
{}. M 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 Fin M
(K,M,p,({}. M)) is Relation-like V48() Element of Fin [:K,M:]
p1 $$ ((K,M,p,({}. M)),p2) is Element of n
p1 $$ (({}. M),i) is Element of n
{}. [:K,M:] 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 Fin [:K,M:]
j is V48() Element of Fin [:K,M:]
the_unity_wrt p1 is Element 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 *
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
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
(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,(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 *
len (n,M,p1) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
width (n,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
width (n,K,(n,M,p1)) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
dom (n,M,p1) is V48() Element of bool NAT
dom M is V48() Element of bool NAT
Indices (n,M,p1) is set
Seg (width (n,M,p1)) is V48() V55( width (n,M,p1)) Element of bool NAT
[:(dom (n,M,p1)),(Seg (width (n,M,p1))):] is Relation-like V48() set
Seg (width p1) is V48() V55( width p1) Element of bool NAT
[:(dom M),(Seg (width p1)):] is Relation-like V48() set
Seg (len M) is V48() V55( len M) Element of bool NAT
len (n,K,(n,M,p1)) 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
dom (n,K,(n,M,p1)) is V48() Element of bool NAT
dom K is V48() Element of bool NAT
Indices (n,K,(n,M,p1)) is set
Seg (width (n,K,(n,M,p1))) is V48() V55( width (n,K,(n,M,p1))) Element of bool NAT
[:(dom (n,K,(n,M,p1))),(Seg (width (n,K,(n,M,p1)))):] is Relation-like V48() set
[:(dom K),(Seg (width p1)):] is Relation-like V48() set
0. n is V68(n) 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
width (n,K,M) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
width (n,(n,K,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
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
Seg (width M) is V48() V55( width M) Element of bool NAT
[:(dom K),(Seg (width M)):] is Relation-like V48() set
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
findom M is V48() Element of Fin NAT
findom p1 is V48() Element of Fin 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
[:NAT,NAT:] is Relation-like non empty non trivial V48() set
[:[:NAT,NAT:], the carrier of n:] is Relation-like non empty non trivial V48() set
bool [:[:NAT,NAT:], the carrier of n:] is non empty non trivial cup-closed diff-closed preBoolean V48() set
j is Relation-like [:NAT,NAT:] -defined the carrier of n -valued Function-like non empty total V26([:NAT,NAT:], the carrier of n) Element of bool [:[:NAT,NAT:], the carrier of n:]
K86(NAT, the carrier of n) is functional non empty M4( NAT , the carrier of n)
curry j is Relation-like NAT -defined K86(NAT, the carrier of n) -valued Function-like non empty total V26( NAT ,K86(NAT, the carrier of n)) Element of bool [:NAT,K86(NAT, the carrier of n):]
[:NAT,K86(NAT, the carrier of n):] is Relation-like non empty non trivial V48() set
bool [:NAT,K86(NAT, the carrier of n):] is non empty non trivial cup-closed diff-closed preBoolean V48() set
Line (K,p) 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
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = width K } is set
c₁₀ is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
(curry j) . c₁₀ is Relation-like NAT -defined the carrier of n -valued Function-like total V26( NAT , the carrier of n) Element of K86(NAT, the carrier of n)
((curry j) . c₁₀) | (dom M) is Relation-like NAT -defined dom M -defined NAT -defined the carrier of n -valued Function-like V48() Element of bool [:NAT, the carrier of n:]
[:NAT, the carrier of n:] is Relation-like non empty non trivial V48() set
bool [:NAT, the carrier of n:] is non empty non trivial cup-closed diff-closed preBoolean V48() set
Col (M,c₁₀) 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
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = len M } is set
mlt ((Line (K,p)),(Col (M,c₁₀))) is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
p1 * (c₁₀,i) is Element of the carrier of n
(p1 * (c₁₀,i)) * (mlt ((Line (K,p)),(Col (M,c₁₀)))) is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
{c₁₀} is non empty trivial V48() V52() V55(1) set
proj1 (curry j) is non empty set
proj1 j is Relation-like non empty set
proj1 ((curry j) . c₁₀) is set
proj2 [:NAT,NAT:] is non empty set
[:{c₁₀},(proj2 [:NAT,NAT:]):] is Relation-like non empty set
[:NAT,NAT:] /\ [:{c₁₀},(proj2 [:NAT,NAT:]):] is Relation-like set
proj2 ([:NAT,NAT:] /\ [:{c₁₀},(proj2 [:NAT,NAT:]):]) is set
[:{c₁₀},NAT:] is Relation-like non empty non trivial V48() set
[:{c₁₀},NAT:] /\ [:NAT,NAT:] is Relation-like set
proj2 ([:{c₁₀},NAT:] /\ [:NAT,NAT:]) is set
proj2 [:{c₁₀},NAT:] is non empty set
proj1 (((curry j) . c₁₀) | (dom M)) is V48() set
NAT /\ (dom M) is V48() Element of bool NAT
len (mlt ((Line (K,p)),(Col (M,c₁₀)))) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
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 multF of n .: ((Line (K,p)),(Col (M,c₁₀))) is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len ( the multF of n .: ((Line (K,p)),(Col (M,c₁₀)))) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
len (Line (K,p)) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
len (Col (M,c₁₀)) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
h is Element of the carrier of n
h multfield is Relation-like the carrier of n -defined the carrier of n -valued Function-like non empty total V26( the carrier of n, the carrier of n) Element of bool [: the carrier of n, the carrier of n:]
bool [: the carrier of n, the carrier of n:] is non empty cup-closed diff-closed preBoolean set
proj1 (h multfield) is non empty set
k9 is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
h * k9 is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(h multfield) * k9 is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
proj2 k9 is V48() set
dom (h * k9) is V48() Element of bool NAT
dom k9 is V48() Element of bool NAT
dom ( the multF of n .: ((Line (K,p)),(Col (M,c₁₀)))) is V48() Element of bool NAT
Seg (len ( the multF of n .: ((Line (K,p)),(Col (M,c₁₀))))) is V48() V55( len ( the multF of n .: ((Line (K,p)),(Col (M,c₁₀))))) Element of bool NAT
k is set
p is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
k9 . p is set
(((curry j) . c₁₀) | (dom M)) . k is set
((curry j) . c₁₀) . p is Element of the carrier of n
j . (c₁₀,p) is Element of the carrier of n
[c₁₀,p] is V23() set
j . [c₁₀,p] is set
K * (p,p) is Element of the carrier of n
M * (p,c₁₀) is Element of the carrier of n
(K * (p,p)) * (M * (p,c₁₀)) is Element of the carrier of n
the multF of n . ((K * (p,p)),(M * (p,c₁₀))) is Element of the carrier of n
[(K * (p,p)),(M * (p,c₁₀))] is V23() set
the multF of n . [(K * (p,p)),(M * (p,c₁₀))] is set
((K * (p,p)) * (M * (p,c₁₀))) * (p1 * (c₁₀,i)) is Element of the carrier of n
the multF of n . (((K * (p,p)) * (M * (p,c₁₀))),(p1 * (c₁₀,i))) is Element of the carrier of n
[((K * (p,p)) * (M * (p,c₁₀))),(p1 * (c₁₀,i))] is V23() set
the multF of n . [((K * (p,p)) * (M * (p,c₁₀))),(p1 * (c₁₀,i))] is set
(Line (K,p)) . p is set
the multF of n . (((Line (K,p)) . p),(M * (p,c₁₀))) is set
[((Line (K,p)) . p),(M * (p,c₁₀))] is V23() set
the multF of n . [((Line (K,p)) . p),(M * (p,c₁₀))] is set
the multF of n . (( the multF of n . (((Line (K,p)) . p),(M * (p,c₁₀)))),(p1 * (c₁₀,i))) is set
[( the multF of n . (((Line (K,p)) . p),(M * (p,c₁₀)))),(p1 * (c₁₀,i))] is V23() set
the multF of n . [( the multF of n . (((Line (K,p)) . p),(M * (p,c₁₀)))),(p1 * (c₁₀,i))] is set
(Col (M,c₁₀)) . p is set
the multF of n . (((Line (K,p)) . p),((Col (M,c₁₀)) . p)) is set
[((Line (K,p)) . p),((Col (M,c₁₀)) . p)] is V23() set
the multF of n . [((Line (K,p)) . p),((Col (M,c₁₀)) . p)] is set
the multF of n . (( the multF of n . (((Line (K,p)) . p),((Col (M,c₁₀)) . p))),(p1 * (c₁₀,i))) is set
[( the multF of n . (((Line (K,p)) . p),((Col (M,c₁₀)) . p))),(p1 * (c₁₀,i))] is V23() set
the multF of n . [( the multF of n . (((Line (K,p)) . p),((Col (M,c₁₀)) . p))),(p1 * (c₁₀,i))] is set
( the multF of n .: ((Line (K,p)),(Col (M,c₁₀)))) . p is set
the multF of n . ((( the multF of n .: ((Line (K,p)),(Col (M,c₁₀)))) . p),(p1 * (c₁₀,i))) is set
[(( the multF of n .: ((Line (K,p)),(Col (M,c₁₀)))) . p),(p1 * (c₁₀,i))] is V23() set
the multF of n . [(( the multF of n .: ((Line (K,p)),(Col (M,c₁₀)))) . p),(p1 * (c₁₀,i))] is set
a is Element of the carrier of n
a * h is Element of the carrier of n
the multF of n . (a,h) is Element of the carrier of n
[a,h] is V23() set
the multF of n . [a,h] is set
((p1 * (c₁₀,i)) * (mlt ((Line (K,p)),(Col (M,c₁₀))))) . k is set
dom ((p1 * (c₁₀,i)) * (mlt ((Line (K,p)),(Col (M,c₁₀))))) is V48() Element of bool NAT
the_unity_wrt the addF of n is Element of the carrier of n
i is V48() Element of Fin NAT
curry' j is Relation-like NAT -defined K86(NAT, the carrier of n) -valued Function-like non empty total V26( NAT ,K86(NAT, the carrier of n)) Element of bool [:NAT,K86(NAT, the carrier of n):]
p2 is V48() Element of Fin NAT
[:NAT, the carrier of n:] is Relation-like non empty non trivial V48() set
bool [:NAT, the carrier of n:] is non empty non trivial cup-closed diff-closed preBoolean V48() set
c₁₀ is Relation-like NAT -defined the carrier of n -valued Function-like non empty total V26( NAT , the carrier of n) Element of bool [:NAT, the carrier of n:]
dom p1 is V48() Element of bool NAT
c₁₀ | (dom p1) is Relation-like NAT -defined dom p1 -defined NAT -defined the carrier of n -valued Function-like V48() Element of bool [:NAT, the carrier of n:]
proj1 (c₁₀ | (dom p1)) is V48() set
proj1 c₁₀ is non empty set
(proj1 c₁₀) /\ (dom p1) is V48() Element of bool NAT
NAT /\ (dom p1) is V48() Element of bool NAT
Line ((n,K,M),p) is Relation-like NAT -defined the carrier of n -valued Function-like V48() V55( width (n,K,M)) FinSequence-like FinSubsequence-like Element of (width (n,K,M)) -tuples_on the carrier of n
(width (n,K,M)) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = width (n,K,M) } is set
len (Line ((n,K,M),p)) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Col (p1,i) is Relation-like NAT -defined the carrier of n -valued Function-like V48() V55( len p1) FinSequence-like FinSubsequence-like Element of (len p1) -tuples_on the carrier of n
(len p1) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = len p1 } is set
len (Col (p1,i)) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
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 multF of n .: ((Line ((n,K,M),p)),(Col (p1,i))) is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len ( the multF of n .: ((Line ((n,K,M),p)),(Col (p1,i)))) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
[p,i] is V23() set
h is set
k9 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
dom ( the multF of n .: ((Line ((n,K,M),p)),(Col (p1,i)))) is V48() Element of bool NAT
Col (M,k9) 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
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = len M } is set
mlt ((Line (K,p)),(Col (M,k9))) is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
p1 * (k9,i) is Element of the carrier of n
p is Element of the carrier of n
p multfield is Relation-like the carrier of n -defined the carrier of n -valued Function-like non empty total V26( the carrier of n, the carrier of n) Element of bool [: the carrier of n, the carrier of n:]
bool [: the carrier of n, the carrier of n:] is non empty cup-closed diff-closed preBoolean set
proj1 (p multfield) is non empty 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
p * k is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(p multfield) * k is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
proj2 k is V48() set
dom (p * k) is V48() Element of bool NAT
dom k is V48() Element of bool NAT
len (Line (K,p)) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
len (Col (M,k9)) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
the multF of n .: ((Line (K,p)),(Col (M,k9))) is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len ( the multF of n .: ((Line (K,p)),(Col (M,k9)))) 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
(p1 * (k9,i)) * (mlt ((Line (K,p)),(Col (M,k9)))) is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
dom ((p1 * (k9,i)) * (mlt ((Line (K,p)),(Col (M,k9))))) is V48() Element of bool NAT
[#] (((p1 * (k9,i)) * (mlt ((Line (K,p)),(Col (M,k9))))),(0. n)) is Relation-like NAT -defined the carrier of n -valued Function-like non empty total V26( NAT , the carrier of n) Element of bool [:NAT, the carrier of n:]
([#] (((p1 * (k9,i)) * (mlt ((Line (K,p)),(Col (M,k9))))),(0. n))) | (dom M) is Relation-like NAT -defined dom M -defined NAT -defined the carrier of n -valued Function-like V48() Element of bool [:NAT, the carrier of n:]
(curry j) . k9 is Relation-like NAT -defined the carrier of n -valued Function-like total V26( NAT , the carrier of n) Element of K86(NAT, the carrier of n)
((curry j) . k9) | (dom M) is Relation-like NAT -defined dom M -defined NAT -defined the carrier of n -valued Function-like V48() Element of bool [:NAT, the carrier of n:]
[p,k9] is V23() set
(c₁₀ | (dom p1)) . h is set
c₁₀ . k9 is Element of the carrier of n
the addF of n $$ (p2,((curry j) . k9)) is Element of the carrier of n
the addF of n $$ (p2,([#] (((p1 * (k9,i)) * (mlt ((Line (K,p)),(Col (M,k9))))),(0. n)))) is Element of the carrier of n
the addF of n "**" (p * k) is Element of the carrier of n
Sum (p * k) is Element of the carrier of n
Sum (mlt ((Line (K,p)),(Col (M,k9)))) is Element of the carrier of n
(p1 * (k9,i)) * (Sum (mlt ((Line (K,p)),(Col (M,k9))))) is Element of the carrier of n
the multF of n . ((p1 * (k9,i)),(Sum (mlt ((Line (K,p)),(Col (M,k9)))))) is Element of the carrier of n
[(p1 * (k9,i)),(Sum (mlt ((Line (K,p)),(Col (M,k9)))))] is V23() set
the multF of n . [(p1 * (k9,i)),(Sum (mlt ((Line (K,p)),(Col (M,k9)))))] is set
(Line (K,p)) "*" (Col (M,k9)) is Element of the carrier of n
(p1 * (k9,i)) * ((Line (K,p)) "*" (Col (M,k9))) is Element of the carrier of n
the multF of n . ((p1 * (k9,i)),((Line (K,p)) "*" (Col (M,k9)))) is Element of the carrier of n
[(p1 * (k9,i)),((Line (K,p)) "*" (Col (M,k9)))] is V23() set
the multF of n . [(p1 * (k9,i)),((Line (K,p)) "*" (Col (M,k9)))] is set
(n,K,M) * (p,k9) is Element of the carrier of n
((n,K,M) * (p,k9)) * (p1 * (k9,i)) is Element of the carrier of n
the multF of n . (((n,K,M) * (p,k9)),(p1 * (k9,i))) is Element of the carrier of n
[((n,K,M) * (p,k9)),(p1 * (k9,i))] is V23() set
the multF of n . [((n,K,M) * (p,k9)),(p1 * (k9,i))] is set
(Line ((n,K,M),p)) . k9 is set
the multF of n . (((Line ((n,K,M),p)) . k9),(p1 * (k9,i))) is set
[((Line ((n,K,M),p)) . k9),(p1 * (k9,i))] is V23() set
the multF of n . [((Line ((n,K,M),p)) . k9),(p1 * (k9,i))] is set
(Col (p1,i)) . k9 is set
the multF of n . (((Line ((n,K,M),p)) . k9),((Col (p1,i)) . k9)) is set
[((Line ((n,K,M),p)) . k9),((Col (p1,i)) . k9)] is V23() set
the multF of n . [((Line ((n,K,M),p)) . k9),((Col (p1,i)) . k9)] is set
( the multF of n .: ((Line ((n,K,M),p)),(Col (p1,i)))) . k9 is set
mlt ((Line ((n,K,M),p)),(Col (p1,i))) is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(mlt ((Line ((n,K,M),p)),(Col (p1,i)))) . h is set
len (mlt ((Line ((n,K,M),p)),(Col (p1,i)))) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
dom (mlt ((Line ((n,K,M),p)),(Col (p1,i)))) is V48() Element of bool NAT
[#] ((mlt ((Line ((n,K,M),p)),(Col (p1,i)))),(0. n)) is Relation-like NAT -defined the carrier of n -valued Function-like non empty total V26( NAT , the carrier of n) Element of bool [:NAT, the carrier of n:]
([#] ((mlt ((Line ((n,K,M),p)),(Col (p1,i)))),(0. n))) | (dom p1) is Relation-like NAT -defined dom p1 -defined NAT -defined the carrier of n -valued Function-like V48() Element of bool [:NAT, the carrier of n:]
Col ((n,M,p1),i) is Relation-like NAT -defined the carrier of n -valued Function-like V48() V55( len (n,M,p1)) FinSequence-like FinSubsequence-like Element of (len (n,M,p1)) -tuples_on the carrier of n
(len (n,M,p1)) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = len (n,M,p1) } is set
len (Col ((n,M,p1),i)) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
the multF of n .: ((Line (K,p)),(Col ((n,M,p1),i))) is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len ( the multF of n .: ((Line (K,p)),(Col ((n,M,p1),i)))) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
mlt ((Line (K,p)),(Col ((n,M,p1),i))) 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 ((Line (K,p)),(Col ((n,M,p1),i)))) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
dom (mlt ((Line (K,p)),(Col ((n,M,p1),i)))) is V48() Element of bool NAT
[#] ((mlt ((Line (K,p)),(Col ((n,M,p1),i)))),(0. n)) is Relation-like NAT -defined the carrier of n -valued Function-like non empty total V26( NAT , the carrier of n) Element of bool [:NAT, the carrier of n:]
([#] ((mlt ((Line (K,p)),(Col ((n,M,p1),i)))),(0. n))) | (dom M) is Relation-like NAT -defined dom M -defined NAT -defined the carrier of n -valued Function-like V48() Element of bool [:NAT, the carrier of n:]
h is Relation-like NAT -defined the carrier of n -valued Function-like non empty total V26( NAT , the carrier of n) Element of bool [:NAT, the carrier of n:]
h | (dom M) is Relation-like NAT -defined dom M -defined NAT -defined the carrier of n -valued Function-like V48() Element of bool [:NAT, the carrier of n:]
proj1 (h | (dom M)) is V48() set
proj1 h is non empty set
(proj1 h) /\ (dom M) is V48() Element of bool NAT
NAT /\ (dom M) is V48() Element of bool NAT
k9 is set
k is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Seg (width K) is V48() V55( width K) Element of bool NAT
[k,i] is V23() set
Line (M,k) is Relation-like NAT -defined the carrier of n -valued Function-like V48() V55( width M) FinSequence-like FinSubsequence-like Element of (width M) -tuples_on the carrier of n
(width M) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = width M } is set
mlt ((Line (M,k)),(Col (p1,i))) is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
K * (p,k) is Element of the carrier of n
len (mlt ((Line (M,k)),(Col (p1,i)))) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
the multF of n .: ((Line (M,k)),(Col (p1,i))) is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len ( the multF of n .: ((Line (M,k)),(Col (p1,i)))) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
proj1 j is Relation-like non empty set
(curry' j) . k is Relation-like NAT -defined the carrier of n -valued Function-like total V26( NAT , the carrier of n) Element of K86(NAT, the carrier of n)
proj2 j is non empty set
((curry' j) . k) | (dom p1) is Relation-like NAT -defined dom p1 -defined NAT -defined the carrier of n -valued Function-like V48() Element of bool [:NAT, the carrier of n:]
proj1 (((curry' j) . k) | (dom p1)) is V48() set
l is Relation-like Function-like set
proj1 l is set
proj2 l is set
dom ( the multF of n .: ((Line (K,p)),(Col ((n,M,p1),i)))) is V48() Element of bool NAT
len (Line (M,k)) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
a is Element of the carrier of n
a multfield is Relation-like the carrier of n -defined the carrier of n -valued Function-like non empty total V26( the carrier of n, the carrier of n) Element of bool [: the carrier of n, the carrier of n:]
proj1 (a multfield) is non empty set
p is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
a * p is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(a multfield) * p is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
proj2 p is V48() set
dom (a * p) is V48() Element of bool NAT
dom p is V48() Element of bool NAT
(K * (p,k)) * (mlt ((Line (M,k)),(Col (p1,i)))) is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
dom ((K * (p,k)) * (mlt ((Line (M,k)),(Col (p1,i))))) is V48() Element of bool NAT
l is set
l9 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
dom ( the multF of n .: ((Line (M,k)),(Col (p1,i)))) is V48() Element of bool NAT
p . l9 is set
(((curry' j) . k) | (dom p1)) . l is set
((curry' j) . k) . l9 is Element of the carrier of n
j . (l9,k) is Element of the carrier of n
[l9,k] is V23() set
j . [l9,k] is set
M * (k,l9) is Element of the carrier of n
(K * (p,k)) * (M * (k,l9)) is Element of the carrier of n
the multF of n . ((K * (p,k)),(M * (k,l9))) is Element of the carrier of n
[(K * (p,k)),(M * (k,l9))] is V23() set
the multF of n . [(K * (p,k)),(M * (k,l9))] is set
p1 * (l9,i) is Element of the carrier of n
((K * (p,k)) * (M * (k,l9))) * (p1 * (l9,i)) is Element of the carrier of n
the multF of n . (((K * (p,k)) * (M * (k,l9))),(p1 * (l9,i))) is Element of the carrier of n
[((K * (p,k)) * (M * (k,l9))),(p1 * (l9,i))] is V23() set
the multF of n . [((K * (p,k)) * (M * (k,l9))),(p1 * (l9,i))] is set
(M * (k,l9)) * (p1 * (l9,i)) is Element of the carrier of n
the multF of n . ((M * (k,l9)),(p1 * (l9,i))) is Element of the carrier of n
[(M * (k,l9)),(p1 * (l9,i))] is V23() set
the multF of n . [(M * (k,l9)),(p1 * (l9,i))] is set
(K * (p,k)) * ((M * (k,l9)) * (p1 * (l9,i))) is Element of the carrier of n
the multF of n . ((K * (p,k)),((M * (k,l9)) * (p1 * (l9,i)))) is Element of the carrier of n
[(K * (p,k)),((M * (k,l9)) * (p1 * (l9,i)))] is V23() set
the multF of n . [(K * (p,k)),((M * (k,l9)) * (p1 * (l9,i)))] is set
(Line (M,k)) . l9 is set
the multF of n . (((Line (M,k)) . l9),(p1 * (l9,i))) is set
[((Line (M,k)) . l9),(p1 * (l9,i))] is V23() set
the multF of n . [((Line (M,k)) . l9),(p1 * (l9,i))] is set
the multF of n . ((K * (p,k)),( the multF of n . (((Line (M,k)) . l9),(p1 * (l9,i))))) is set
[(K * (p,k)),( the multF of n . (((Line (M,k)) . l9),(p1 * (l9,i))))] is V23() set
the multF of n . [(K * (p,k)),( the multF of n . (((Line (M,k)) . l9),(p1 * (l9,i))))] is set
(Col (p1,i)) . l9 is set
the multF of n . (((Line (M,k)) . l9),((Col (p1,i)) . l9)) is set
[((Line (M,k)) . l9),((Col (p1,i)) . l9)] is V23() set
the multF of n . [((Line (M,k)) . l9),((Col (p1,i)) . l9)] is set
the multF of n . ((K * (p,k)),( the multF of n . (((Line (M,k)) . l9),((Col (p1,i)) . l9)))) is set
[(K * (p,k)),( the multF of n . (((Line (M,k)) . l9),((Col (p1,i)) . l9)))] is V23() set
the multF of n . [(K * (p,k)),( the multF of n . (((Line (M,k)) . l9),((Col (p1,i)) . l9)))] is set
( the multF of n .: ((Line (M,k)),(Col (p1,i)))) . l9 is set
the multF of n . ((K * (p,k)),(( the multF of n .: ((Line (M,k)),(Col (p1,i)))) . l9)) is set
[(K * (p,k)),(( the multF of n .: ((Line (M,k)),(Col (p1,i)))) . l9)] is V23() set
the multF of n . [(K * (p,k)),(( the multF of n .: ((Line (M,k)),(Col (p1,i)))) . l9)] is set
b is Element of the carrier of n
a * b is Element of the carrier of n
the multF of n . (a,b) is Element of the carrier of n
[a,b] is V23() set
the multF of n . [a,b] is set
((K * (p,k)) * (mlt ((Line (M,k)),(Col (p1,i))))) . l is set
c₁₉ is Relation-like Function-like set
proj1 c₁₉ is set
proj2 c₁₉ is set
[#] (((K * (p,k)) * (mlt ((Line (M,k)),(Col (p1,i))))),(0. n)) is Relation-like NAT -defined the carrier of n -valued Function-like non empty total V26( NAT , the carrier of n) Element of bool [:NAT, the carrier of n:]
([#] (((K * (p,k)) * (mlt ((Line (M,k)),(Col (p1,i))))),(0. n))) | (dom p1) is Relation-like NAT -defined dom p1 -defined NAT -defined the carrier of n -valued Function-like V48() Element of bool [:NAT, the carrier of n:]
(h | (dom M)) . k9 is set
h . k is Element of the carrier of n
the addF of n $$ (i,((curry' j) . k)) is Element of the carrier of n
the addF of n $$ (i,([#] (((K * (p,k)) * (mlt ((Line (M,k)),(Col (p1,i))))),(0. n)))) is Element of the carrier of n
the addF of n "**" (a * p) is Element of the carrier of n
Sum (a * p) is Element of the carrier of n
Sum (mlt ((Line (M,k)),(Col (p1,i)))) is Element of the carrier of n
(K * (p,k)) * (Sum (mlt ((Line (M,k)),(Col (p1,i))))) is Element of the carrier of n
the multF of n . ((K * (p,k)),(Sum (mlt ((Line (M,k)),(Col (p1,i)))))) is Element of the carrier of n
[(K * (p,k)),(Sum (mlt ((Line (M,k)),(Col (p1,i)))))] is V23() set
the multF of n . [(K * (p,k)),(Sum (mlt ((Line (M,k)),(Col (p1,i)))))] is set
(Line (M,k)) "*" (Col (p1,i)) is Element of the carrier of n
(K * (p,k)) * ((Line (M,k)) "*" (Col (p1,i))) is Element of the carrier of n
the multF of n . ((K * (p,k)),((Line (M,k)) "*" (Col (p1,i)))) is Element of the carrier of n
[(K * (p,k)),((Line (M,k)) "*" (Col (p1,i)))] is V23() set
the multF of n . [(K * (p,k)),((Line (M,k)) "*" (Col (p1,i)))] is set
(n,M,p1) * (k,i) is Element of the carrier of n
(K * (p,k)) * ((n,M,p1) * (k,i)) is Element of the carrier of n
the multF of n . ((K * (p,k)),((n,M,p1) * (k,i))) is Element of the carrier of n
[(K * (p,k)),((n,M,p1) * (k,i))] is V23() set
the multF of n . [(K * (p,k)),((n,M,p1) * (k,i))] is set
(Line (K,p)) . k is set
the multF of n . (((Line (K,p)) . k),((n,M,p1) * (k,i))) is set
[((Line (K,p)) . k),((n,M,p1) * (k,i))] is V23() set
the multF of n . [((Line (K,p)) . k),((n,M,p1) * (k,i))] is set
(Col ((n,M,p1),i)) . k is set
the multF of n . (((Line (K,p)) . k),((Col ((n,M,p1),i)) . k)) is set
[((Line (K,p)) . k),((Col ((n,M,p1),i)) . k)] is V23() set
the multF of n . [((Line (K,p)) . k),((Col ((n,M,p1),i)) . k)] is set
( the multF of n .: ((Line (K,p)),(Col ((n,M,p1),i)))) . k is set
(mlt ((Line (K,p)),(Col ((n,M,p1),i)))) . k9 is set
(n,(n,K,M),p1) * (p,i) is Element of the carrier of n
(Line ((n,K,M),p)) "*" (Col (p1,i)) is Element of the carrier of n
Sum (mlt ((Line ((n,K,M),p)),(Col (p1,i)))) is Element of the carrier of n
the addF of n "**" (mlt ((Line ((n,K,M),p)),(Col (p1,i)))) is Element of the carrier of n
the addF of n $$ ((findom p1),([#] ((mlt ((Line ((n,K,M),p)),(Col (p1,i)))),(0. n)))) is Element of the carrier of n
the addF of n $$ (i,c₁₀) is Element of the carrier of n
(NAT,NAT,i,p2) is Relation-like V48() Element of Fin [:NAT,NAT:]
Fin [:NAT,NAT:] is non empty cup-closed diff-closed preBoolean set
the addF of n $$ ((NAT,NAT,i,p2),j) is Element of the carrier of n
the addF of n $$ (p2,h) is Element of the carrier of n
findom (mlt ((Line (K,p)),(Col ((n,M,p1),i)))) is V48() Element of Fin NAT
[#] ((mlt ((Line (K,p)),(Col ((n,M,p1),i)))),(the_unity_wrt the addF of n)) is Relation-like NAT -defined the carrier of n -valued Function-like non empty total V26( NAT , the carrier of n) Element of bool [:NAT, the carrier of n:]
the addF of n $$ ((findom (mlt ((Line (K,p)),(Col ((n,M,p1),i))))),([#] ((mlt ((Line (K,p)),(Col ((n,M,p1),i)))),(the_unity_wrt the addF of n)))) is Element of the carrier of n
the addF of n "**" (mlt ((Line (K,p)),(Col ((n,M,p1),i)))) is Element of the carrier of n
Sum (mlt ((Line (K,p)),(Col ((n,M,p1),i)))) is Element of the carrier of n
(Line (K,p)) "*" (Col ((n,M,p1),i)) is Element of the carrier of n
(n,K,(n,M,p1)) * (p,i) is Element of the carrier of n
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
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
n is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
Permutations n is non empty permutational set
len (Permutations n) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Seg (len (Permutations n)) is V48() V55( len (Permutations n)) Element of bool NAT
p1 is Relation-like Seg (len (Permutations n)) -defined Seg (len (Permutations n)) -valued Function-like one-to-one total V26( Seg (len (Permutations n)), Seg (len (Permutations n))) V27( Seg (len (Permutations n))) V28( Seg (len (Permutations n)), Seg (len (Permutations n))) V48() Element of Permutations n
M 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
p2 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Seg p2 is V48() V55(p2) Element of bool NAT
Seg n is V48() V55(n) Element of bool NAT
[:(Seg n),(Seg n):] is Relation-like V48() set
bool [:(Seg n),(Seg n):] is non empty cup-closed diff-closed preBoolean V48() V52() set
p is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
p1 . p is set
i is Relation-like Seg n -defined Seg n -valued Function-like total V26( Seg n, Seg n) V48() Element of bool [:(Seg n),(Seg n):]
i . p is set
i is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
M * (p,i) is Element of the carrier of K
j is Element of the carrier of K
c₁₀ is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
M * (p,c₁₀) is Element of the carrier of K
i is Relation-like NAT -defined the carrier of K -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of K
dom i is V48() Element of bool NAT
len 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
p1 . p is set
i . p is set
i is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
M * (p,i) is Element of the carrier of K
p2 is Relation-like NAT -defined the carrier of K -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of K
len p2 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
dom p2 is V48() Element of bool NAT
i is Relation-like NAT -defined the carrier of K -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of K
len i is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
dom i is V48() Element of bool NAT
Seg n is V48() V55(n) Element of bool NAT
[:(Seg n),(Seg n):] is Relation-like V48() set
bool [:(Seg n),(Seg n):] is non empty cup-closed diff-closed preBoolean V48() V52() set
i is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
p2 . i is set
i . i is set
p is Relation-like Seg n -defined Seg n -valued Function-like total V26( Seg n, Seg n) V48() Element of bool [:(Seg n),(Seg n):]
p . i is set
j is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
M * (i,j) is Element of the carrier of K
p2 is Relation-like NAT -defined the carrier of K -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of K
len p2 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
dom p2 is V48() Element of bool NAT
i is Relation-like NAT -defined the carrier of K -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of K
len i is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
dom i is V48() Element of bool NAT
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
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
n is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
Permutations n is non empty permutational set
[:(Permutations n), the carrier of K:] is Relation-like non empty set
bool [:(Permutations n), the carrier of K:] is non empty cup-closed diff-closed preBoolean set
len (Permutations n) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Seg (len (Permutations n)) is V48() V55( len (Permutations n)) Element of bool NAT
M 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 multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like non empty total V26([: the carrier of K, the carrier of K:], the carrier of K) commutative Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is Relation-like non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is Relation-like non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty cup-closed diff-closed preBoolean set
p1 is Relation-like Permutations n -defined the carrier of K -valued Function-like non empty total V26( Permutations n, the carrier of K) Element of bool [:(Permutations n), the carrier of K:]
p2 is Relation-like Seg (len (Permutations n)) -defined Seg (len (Permutations n)) -valued Function-like one-to-one total V26( Seg (len (Permutations n)), Seg (len (Permutations n))) V27( Seg (len (Permutations n))) V28( Seg (len (Permutations n)), Seg (len (Permutations n))) V48() Element of Permutations n
p1 . p2 is Element of the carrier of K
(n,K,M,p2) is Relation-like NAT -defined the carrier of K -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of K
the multF of K "**" (n,K,M,p2) is Element of the carrier of K
- (( the multF of K "**" (n,K,M,p2)),p2) is Element of the carrier of K
p1 is Relation-like Permutations n -defined the carrier of K -valued Function-like non empty total V26( Permutations n, the carrier of K) Element of bool [:(Permutations n), the carrier of K:]
p2 is Relation-like Permutations n -defined the carrier of K -valued Function-like non empty total V26( Permutations n, the carrier of K) Element of bool [:(Permutations n), the carrier of K:]
i is Relation-like Seg (len (Permutations n)) -defined Seg (len (Permutations n)) -valued Function-like one-to-one total V26( Seg (len (Permutations n)), Seg (len (Permutations n))) V27( Seg (len (Permutations n))) V28( Seg (len (Permutations n)), Seg (len (Permutations n))) V48() Element of Permutations n
p1 . i is Element of the carrier of K
(n,K,M,i) is Relation-like NAT -defined the carrier of K -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of K
the multF of K "**" (n,K,M,i) is Element of the carrier of K
- (( the multF of K "**" (n,K,M,i)),i) is Element of the carrier of K
p2 . i is Element of the carrier of K
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
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
n is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
Permutations n is non empty permutational set
the addF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like non empty total V26([: the carrier of K, the carrier of K:], the carrier of K) commutative associative Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is Relation-like non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is Relation-like non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty cup-closed diff-closed preBoolean set
FinOmega (Permutations n) is V48() Element of Fin (Permutations n)
Fin (Permutations n) is non empty cup-closed diff-closed preBoolean set
M 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
(n,K,M) is Relation-like Permutations n -defined the carrier of K -valued Function-like non empty total V26( Permutations n, the carrier of K) Element of bool [:(Permutations n), the carrier of K:]
[:(Permutations n), the carrier of K:] is Relation-like non empty set
bool [:(Permutations n), the carrier of K:] is non empty cup-closed diff-closed preBoolean set
the addF of K $$ ((FinOmega (Permutations n)),(n,K,M)) is Element of the carrier of K
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 Element of the carrier of n
<*K*> is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty trivial V48() V55(1) FinSequence-like FinSubsequence-like Element of 1 -tuples_on the carrier of n
1 -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
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = 1 } is set
<*<*K*>*> is Relation-like NAT -defined the carrier of n * -valued Function-like constant non empty trivial V48() V55(1) FinSequence-like FinSubsequence-like tabular Matrix of 1,1, the carrier of n
(1,n,<*<*K*>*>) 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
FinOmega (Permutations 1) is V48() Element of Fin (Permutations 1)
Fin (Permutations 1) is non empty cup-closed diff-closed preBoolean set
(1,n,<*<*K*>*>) is Relation-like Permutations 1 -defined the carrier of n -valued Function-like non empty total V26( Permutations 1, the carrier of n) Element of bool [:(Permutations 1), the carrier of n:]
[:(Permutations 1), the carrier of n:] is Relation-like non empty set
bool [:(Permutations 1), the carrier of n:] is non empty cup-closed diff-closed preBoolean set
the addF of n $$ ((FinOmega (Permutations 1)),(1,n,<*<*K*>*>)) is Element of the carrier of n
(1,n,<*<*K*>*>) . (idseq 1) is set
len (Permutations 1) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
Seg (len (Permutations 1)) is V48() V55( len (Permutations 1)) Element of bool NAT
p1 is Relation-like Seg (len (Permutations 1)) -defined Seg (len (Permutations 1)) -valued Function-like one-to-one total V26( Seg (len (Permutations 1)), Seg (len (Permutations 1))) V27( Seg (len (Permutations 1))) V28( Seg (len (Permutations 1)), Seg (len (Permutations 1))) V48() Element of Permutations 1
- (K,p1) is Element of the carrier of n
p2 is Relation-like Seg (len (Permutations 1)) -defined Seg (len (Permutations 1)) -valued Function-like one-to-one total V26( Seg (len (Permutations 1)), Seg (len (Permutations 1))) V27( Seg (len (Permutations 1))) V28( Seg (len (Permutations 1)), Seg (len (Permutations 1))) V48() Element of Permutations 1
(1,n,<*<*K*>*>,p1) is Relation-like NAT -defined the carrier of n -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len (1,n,<*<*K*>*>,p1) is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
dom (1,n,<*<*K*>*>,p1) is V48() Element of bool NAT
p1 . 1 is set
(1,n,<*<*K*>*>,p1) . 1 is set
<*<*K*>*> * (1,1) is Element of the carrier of n
(1,n,<*<*K*>*>) . p1 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 multF of n "**" (1,n,<*<*K*>*>,p1) is Element of the carrier of n
- (( the multF of n "**" (1,n,<*<*K*>*>,p1)),p1) is Element of the carrier of n
1 |-> K is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty trivial V48() V55(1) FinSequence-like FinSubsequence-like Element of 1 -tuples_on the carrier of n
(Seg 1) --> K is Relation-like Seg 1 -defined {K} -valued Function-like non empty total V26( Seg 1,{K}) V48() FinSequence-like FinSubsequence-like Element of bool [:(Seg 1),{K}:]
{K} is non empty trivial V48() V55(1) set
[:(Seg 1),{K}:] is Relation-like non empty V48() set
bool [:(Seg 1),{K}:] is non empty cup-closed diff-closed preBoolean V48() V52() 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
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
n is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
Seg n is V48() V55(n) Element of bool NAT
M 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
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 K -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of K
len p2 is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() Element of NAT
dom p2 is V48() Element of bool NAT
Seg p1 is V48() V55(p1) Element of bool NAT
i is V34() V35() V36() V40() V41() ext-real non negative V45() V48() V53() set
p2 . i is set
M * (i,i) is Element of the carrier of K
p1 is Relation-like NAT -defined the carrier of K -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of K
len 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 K -valued Function-like V48() FinSequence-like FinSubsequence-like FinSequence of the carrier of K
len p2 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
p1 . i is set
M * (i,i) is Element of the carrier of K
p2 . i is set
dom p1 is V48() Element of bool NAT
dom p2 is V48() Element of bool NAT