:: MATRIXJ2 semantic presentation

REAL is set
NAT is non empty non trivial V25() V26() V27() non finite cardinal limit_cardinal Element of bool REAL
bool REAL is set
K633() is strict algebraic-closed doubleLoopStr
the carrier of K633() is set
NAT is non empty non trivial V25() V26() V27() non finite cardinal limit_cardinal set
bool NAT is non trivial non finite set
bool NAT is non trivial non finite set
K95(NAT) is V24() set
INT is set
COMPLEX is set
RAT is set
{} is Relation-like non-empty empty-yielding RAT -valued functional empty V25() V26() V27() V29() V30() V31() finite finite-yielding V36() cardinal {} -element FinSequence-like FinSequence-membered V46() ext-real non positive non negative V165() V174() V175() V176() V177() set
2 is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
1 is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
0 is Relation-like non-empty empty-yielding RAT -valued functional empty V25() V26() V27() V29() V30() V31() finite finite-yielding V36() cardinal {} -element FinSequence-like FinSequence-membered V46() ext-real non positive non negative V165() V174() V175() V176() V177() Element of NAT
K478(0,1,2) is finite set
[:K478(0,1,2),K478(0,1,2):] is Relation-like finite set
[:[:K478(0,1,2),K478(0,1,2):],K478(0,1,2):] is Relation-like finite set
bool [:[:K478(0,1,2),K478(0,1,2):],K478(0,1,2):] is finite V36() set
bool [:K478(0,1,2),K478(0,1,2):] is finite V36() set
[:REAL,REAL:] is Relation-like set
bool [:REAL,REAL:] is set
{{},1} is non empty finite V36() set
K705() is set
bool K705() is set
K706() is Element of bool K705()
[:COMPLEX,COMPLEX:] is Relation-like set
bool [:COMPLEX,COMPLEX:] is set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is set
[:[:REAL,REAL:],REAL:] is Relation-like set
bool [:[:REAL,REAL:],REAL:] is set
[:RAT,RAT:] is Relation-like set
bool [:RAT,RAT:] is set
[:[:RAT,RAT:],RAT:] is Relation-like set
bool [:[:RAT,RAT:],RAT:] is set
[:INT,INT:] is Relation-like set
bool [:INT,INT:] is set
[:[:INT,INT:],INT:] is Relation-like set
bool [:[:INT,INT:],INT:] is set
[:NAT,NAT:] is Relation-like non trivial non finite set
[:[:NAT,NAT:],NAT:] is Relation-like non trivial non finite set
bool [:[:NAT,NAT:],NAT:] is non trivial non finite set
K843() is set
3 is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
card {} is Relation-like non-empty empty-yielding RAT -valued functional empty V25() V26() V27() V29() V30() V31() finite finite-yielding V36() cardinal {} -element FinSequence-like FinSequence-membered V46() ext-real non positive non negative V165() V174() V175() V176() V177() set
Seg 1 is non empty trivial finite 1 -element V43() Element of bool NAT
{ b₁ where b₁ is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b₁ & b₁ <= 1 ) } is set
{1} is non empty trivial finite V36() 1 -element set
Seg 2 is non empty finite 2 -element V43() Element of bool NAT
{ b₁ where b₁ is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b₁ & b₁ <= 2 ) } is set
{1,2} is non empty finite V36() set
<*> REAL is Relation-like non-empty empty-yielding NAT -defined REAL -valued Function-like functional empty V25() V26() V27() V29() V30() V31() finite finite-yielding V36() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V46() ext-real non positive non negative V165() V174() V175() V176() V177() Function-yielding V201() FinSequence of REAL
K667((<*> REAL)) is V46() ext-real V165() Element of REAL
n is set
K is set
{K} is non empty trivial finite 1 -element set
M is Relation-like Function-like set
dom M is set
M +* (n,K) is Relation-like Function-like set
rng (M +* (n,K)) is set
rng M is set
M . n is set
{(M . n)} is non empty trivial finite 1 -element set
(rng M) \ {(M . n)} is Element of bool (rng M)
bool (rng M) is set
((rng M) \ {(M . n)}) \/ {K} is non empty set
n .--> K is Relation-like {n} -defined Function-like one-to-one finite set
{n} is non empty trivial finite 1 -element set
{n} --> K is Relation-like {n} -defined {K} -valued Function-like constant non empty total V18({n},{K}) finite Element of bool [:{n},{K}:]
[:{n},{K}:] is Relation-like finite set
bool [:{n},{K}:] is finite V36() set
dom (n .--> K) is finite set
rng (n .--> K) is finite set
M +* (n .--> K) is Relation-like Function-like set
rng (M +* (n .--> K)) is set
(dom M) \ {n} is Element of bool (dom M)
bool (dom M) is set
M .: ((dom M) \ {n}) is set
(M .: ((dom M) \ {n})) \/ {K} is non empty set
M .: (dom M) is set
M .: {n} is finite set
(M .: (dom M)) \ (M .: {n}) is Element of bool (M .: (dom M))
bool (M .: (dom M)) is set
((M .: (dom M)) \ (M .: {n})) \/ {K} is non empty set
Im (M,n) is set
(rng M) \ (Im (M,n)) is Element of bool (rng M)
((rng M) \ (Im (M,n))) \/ {K} is non empty set
n is non empty non degenerated non trivial right_complementable almost_left_invertible unital V131() V133() right-distributive left-distributive right_unital well-unital V142() left_unital V152() V153() V154() 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
M is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
K is Element of the carrier of n
1_ n is Element of the carrier of n
1. n is V65(n) Element of the carrier of n
the OneF of n is Element of the carrier of n
0. n is V65(n) Element of the carrier of n
the ZeroF of n is Element of the carrier of n
V is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
Seg V is finite V -element V43() Element of bool NAT
{ b₁ where b₁ is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b₁ & b₁ <= V ) } is set
[:(Seg V),(Seg V):] is Relation-like finite set
B is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
B + 1 is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
M9 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
[B,M9] is set
{B,M9} is non empty finite V36() set
{B} is non empty trivial finite V36() 1 -element set
{{B,M9},{B}} is non empty finite V36() set
B is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Function-yielding V201() Matrix of V,V, the carrier of n
Indices B is set
dom B is finite Element of bool NAT
width B is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
Seg (width B) is finite width B -element V43() Element of bool NAT
{ b₁ where b₁ is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b₁ & b₁ <= width B ) } is set
[:(dom B),(Seg (width B)):] is Relation-like finite set
len B is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
M9 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
T is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
[M9,T] is set
{M9,T} is non empty finite V36() set
{M9} is non empty trivial finite V36() 1 -element set
{{M9,T},{M9}} is non empty finite V36() set
B * (M9,T) is Element of the carrier of n
M9 + 1 is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
V is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Function-yielding V201() FinSequence of the carrier of n *
len V is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
width V is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
Indices V is set
dom V is finite Element of bool NAT
Seg (width V) is finite width V -element V43() Element of bool NAT
{ b₁ where b₁ is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b₁ & b₁ <= width V ) } is set
[:(dom V),(Seg (width V)):] is Relation-like finite set
B is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Function-yielding V201() FinSequence of the carrier of n *
len B is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
width B is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
Indices B is set
dom B is finite Element of bool NAT
Seg (width B) is finite width B -element V43() Element of bool NAT
{ b₁ where b₁ is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b₁ & b₁ <= width B ) } is set
[:(dom B),(Seg (width B)):] is Relation-like finite set
M9 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
T is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
[M9,T] is set
{M9,T} is non empty finite V36() set
{M9} is non empty trivial finite V36() 1 -element set
{{M9,T},{M9}} is non empty finite V36() set
Seg M is finite M -element V43() Element of bool NAT
{ b₁ where b₁ is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b₁ & b₁ <= M ) } is set
[:(Seg M),(Seg M):] is Relation-like finite set
M9 + 1 is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
V * (M9,T) is Element of the carrier of n
B * (M9,T) is Element of the carrier of n
n is non empty non degenerated non trivial right_complementable almost_left_invertible unital V131() V133() right-distributive left-distributive right_unital well-unital V142() left_unital V152() V153() V154() doubleLoopStr
the carrier of n is non empty non trivial set
K is Element of the carrier of n
M is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
(n,K,M) is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Function-yielding V201() FinSequence of the carrier of n *
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
len (n,K,M) is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
width (n,K,M) is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
B is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
M9 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
[B,M9] is set
{B,M9} is non empty finite V36() set
{B} is non empty trivial finite V36() 1 -element set
{{B,M9},{B}} is non empty finite V36() set
V is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Function-yielding V201() Matrix of M,M, the carrier of n
Indices V is set
dom V is finite Element of bool NAT
width V is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
Seg (width V) is finite width V -element V43() Element of bool NAT
{ b₁ where b₁ is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b₁ & b₁ <= width V ) } is set
[:(dom V),(Seg (width V)):] is Relation-like finite set
B + 1 is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
V * (B,M9) is Element of the carrier of n
0. n is V65(n) Element of the carrier of n
the ZeroF of n is Element of the carrier of n
n is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital V131() V133() right-distributive left-distributive right_unital well-unital V142() left_unital V152() V153() V154() doubleLoopStr
the carrier of K is non empty non trivial set
M is Element of the carrier of K
(K,M,n) is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Function-yielding V201() upper_triangular Matrix of n,n, the carrier of K
the carrier of K * is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
diagonal_of_Matrix (K,M,n) is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of K
n |-> M is Relation-like NAT -defined the carrier of K -valued Function-like finite n -element 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
Seg n is finite n -element V43() Element of bool NAT
{ b₁ where b₁ is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
[:(Seg n),(Seg n):] is Relation-like finite set
Indices (K,M,n) is set
dom (K,M,n) is finite Element of bool NAT
width (K,M,n) is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
Seg (width (K,M,n)) is finite width (K,M,n) -element V43() Element of bool NAT
{ b₁ where b₁ is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b₁ & b₁ <= width (K,M,n) ) } is set
[:(dom (K,M,n)),(Seg (width (K,M,n))):] is Relation-like finite set
B is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
[B,B] is set
{B,B} is non empty finite V36() set
{B} is non empty trivial finite V36() 1 -element set
{{B,B},{B}} is non empty finite V36() set
(diagonal_of_Matrix (K,M,n)) . B is set
(K,M,n) * (B,B) is Element of the carrier of K
(n |-> M) . B is set
len (diagonal_of_Matrix (K,M,n)) is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
len (n |-> M) is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
n is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital V131() V133() right-distributive left-distributive right_unital well-unital V142() left_unital V152() V153() V154() doubleLoopStr
the carrier of K is non empty non trivial set
power K is Relation-like [: the carrier of K,NAT:] -defined the carrier of K -valued Function-like total V18([: the carrier of K,NAT:], the carrier of K) Element of bool [:[: the carrier of K,NAT:], the carrier of K:]
[: the carrier of K,NAT:] is Relation-like non trivial non finite set
[:[: the carrier of K,NAT:], the carrier of K:] is Relation-like non trivial non finite set
bool [:[: the carrier of K,NAT:], the carrier of K:] is non trivial non finite set
M is Element of the carrier of K
(K,M,n) is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Function-yielding V201() upper_triangular Matrix of n,n, the carrier of K
the carrier of K * is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
Det (K,M,n) is Element of the carrier of K
(power K) . (M,n) is Element of the carrier of K
diagonal_of_Matrix (K,M,n) is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of K
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like total V18([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is Relation-like set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is Relation-like set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is set
the multF of K $$ (diagonal_of_Matrix (K,M,n)) is Element of the carrier of K
n |-> M is Relation-like NAT -defined the carrier of K -valued Function-like finite n -element 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
Product (n |-> M) is Element of the carrier of K
the multF of K $$ (n |-> M) is Element of the carrier of K
n is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital V131() V133() right-distributive left-distributive right_unital well-unital V142() left_unital V152() V153() V154() doubleLoopStr
the carrier of K is non empty non trivial set
0. K is V65(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
M is Element of the carrier of K
(K,M,n) is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Function-yielding V201() upper_triangular Matrix of n,n, the carrier of K
the carrier of K * is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
Det (K,M,n) is Element of the carrier of K
Seg n is finite n -element V43() Element of bool NAT
{ b₁ where b₁ is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
n |-> M is Relation-like NAT -defined the carrier of K -valued Function-like finite n -element 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
dom (n |-> M) is finite n -element Element of bool NAT
(n |-> M) . n is set
Product (n |-> M) is Element of the carrier of K
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like total V18([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is Relation-like set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is Relation-like set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is set
the multF of K $$ (n |-> M) is Element of the carrier of K
power K is Relation-like [: the carrier of K,NAT:] -defined the carrier of K -valued Function-like total V18([: the carrier of K,NAT:], the carrier of K) Element of bool [:[: the carrier of K,NAT:], the carrier of K:]
[: the carrier of K,NAT:] is Relation-like non trivial non finite set
[:[: the carrier of K,NAT:], the carrier of K:] is Relation-like non trivial non finite set
bool [:[: the carrier of K,NAT:], the carrier of K:] is non trivial non finite set
(power K) . (M,n) is Element of the carrier of K
Det (K,M,n) is Element of the carrier of K
power K is Relation-like [: the carrier of K,NAT:] -defined the carrier of K -valued Function-like total V18([: the carrier of K,NAT:], the carrier of K) Element of bool [:[: the carrier of K,NAT:], the carrier of K:]
[: the carrier of K,NAT:] is Relation-like non trivial non finite set
[:[: the carrier of K,NAT:], the carrier of K:] is Relation-like non trivial non finite set
bool [:[: the carrier of K,NAT:], the carrier of K:] is non trivial non finite set
(power K) . (M,n) is Element of the carrier of K
n |-> M is Relation-like NAT -defined the carrier of K -valued Function-like finite n -element 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
Product (n |-> M) is Element of the carrier of K
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like total V18([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is Relation-like set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is Relation-like set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is set
the multF of K $$ (n |-> M) is Element of the carrier of K
dom (n |-> M) is finite n -element Element of bool NAT
Seg n is finite n -element V43() Element of bool NAT
{ b₁ where b₁ is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
B is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
(n |-> M) . B is set
n is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
n + 1 is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
K is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
Seg K is finite K -element V43() Element of bool NAT
{ b₁ where b₁ is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b₁ & b₁ <= K ) } is set
M is non empty non degenerated non trivial right_complementable almost_left_invertible unital V131() V133() right-distributive left-distributive right_unital well-unital V142() left_unital V152() V153() V154() doubleLoopStr
the carrier of M is non empty non trivial set
1. (M,K) is Relation-like NAT -defined the carrier of M * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Function-yielding V201() Matrix of K,K, the carrier of M
the carrier of M * is functional non empty FinSequence-membered FinSequenceSet of the carrier of M
width (1. (M,K)) is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
Line ((1. (M,K)),n) is Relation-like NAT -defined the carrier of M -valued Function-like finite width (1. (M,K)) -element FinSequence-like FinSubsequence-like Element of (width (1. (M,K))) -tuples_on the carrier of M
(width (1. (M,K))) -tuples_on the carrier of M is functional non empty FinSequence-membered FinSequenceSet of the carrier of M
Line ((1. (M,K)),(n + 1)) is Relation-like NAT -defined the carrier of M -valued Function-like finite width (1. (M,K)) -element FinSequence-like FinSubsequence-like Element of (width (1. (M,K))) -tuples_on the carrier of M
V is Element of the carrier of M
(M,V,K) is Relation-like NAT -defined the carrier of M * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Function-yielding V201() upper_triangular Matrix of K,K, the carrier of M
Line ((M,V,K),n) is Relation-like NAT -defined the carrier of M -valued Function-like finite width (M,V,K) -element FinSequence-like FinSubsequence-like Element of (width (M,V,K)) -tuples_on the carrier of M
width (M,V,K) is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
(width (M,V,K)) -tuples_on the carrier of M is functional non empty FinSequence-membered FinSequenceSet of the carrier of M
V * (Line ((1. (M,K)),n)) is Relation-like NAT -defined the carrier of M -valued Function-like finite width (1. (M,K)) -element FinSequence-like FinSubsequence-like Element of (width (1. (M,K))) -tuples_on the carrier of M
V multfield is Relation-like the carrier of M -defined the carrier of M -valued Function-like non empty total V18( the carrier of M, the carrier of M) Element of bool [: the carrier of M, the carrier of M:]
[: the carrier of M, the carrier of M:] is Relation-like set
bool [: the carrier of M, the carrier of M:] is set
the multF of M is Relation-like [: the carrier of M, the carrier of M:] -defined the carrier of M -valued Function-like total V18([: the carrier of M, the carrier of M:], the carrier of M) Element of bool [:[: the carrier of M, the carrier of M:], the carrier of M:]
[:[: the carrier of M, the carrier of M:], the carrier of M:] is Relation-like set
bool [:[: the carrier of M, the carrier of M:], the carrier of M:] is set
id the carrier of M is Relation-like the carrier of M -defined the carrier of M -valued non empty total V18( the carrier of M, the carrier of M) Element of bool [: the carrier of M, the carrier of M:]
the multF of M [;] (V,(id the carrier of M)) is Relation-like the carrier of M -defined the carrier of M -valued Function-like non empty total V18( the carrier of M, the carrier of M) Element of bool [: the carrier of M, the carrier of M:]
K440( the carrier of M, the carrier of M,(Line ((1. (M,K)),n)),(V multfield)) is Relation-like NAT -defined the carrier of M -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of M
(V * (Line ((1. (M,K)),n))) + (Line ((1. (M,K)),(n + 1))) is Relation-like NAT -defined the carrier of M -valued Function-like finite width (1. (M,K)) -element FinSequence-like FinSubsequence-like Element of (width (1. (M,K))) -tuples_on 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 total V18([: the carrier of M, the carrier of M:], the carrier of M) Element of bool [:[: the carrier of M, the carrier of M:], the carrier of M:]
K437( the carrier of M, the carrier of M, the carrier of M, the addF of M,(V * (Line ((1. (M,K)),n))),(Line ((1. (M,K)),(n + 1)))) is Relation-like NAT -defined the carrier of M -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of M
K685((V * (Line ((1. (M,K)),n))),(Line ((1. (M,K)),(n + 1)))) is Relation-like Function-like set
K685((V * (Line ((1. (M,K)),n))),(Line ((1. (M,K)),(n + 1)))) * the addF of M is Relation-like the carrier of M -valued set
Indices (1. (M,K)) is set
dom (1. (M,K)) is finite Element of bool NAT
Seg (width (1. (M,K))) is finite width (1. (M,K)) -element V43() Element of bool NAT
{ b₁ where b₁ is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b₁ & b₁ <= width (1. (M,K)) ) } is set
[:(dom (1. (M,K))),(Seg (width (1. (M,K)))):] is Relation-like finite set
Indices (M,V,K) is set
dom (M,V,K) is finite Element of bool NAT
Seg (width (M,V,K)) is finite width (M,V,K) -element V43() Element of bool NAT
{ b₁ where b₁ is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b₁ & b₁ <= width (M,V,K) ) } is set
[:(dom (M,V,K)),(Seg (width (M,V,K))):] is Relation-like finite set
B is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
B -tuples_on the carrier of M is functional non empty FinSequence-membered FinSequenceSet of the carrier of M
[:(Seg K),(Seg K):] is Relation-like finite set
Jk is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
IM is Relation-like NAT -defined the carrier of M -valued Function-like finite B -element FinSequence-like FinSubsequence-like Element of B -tuples_on the carrier of M
IM . Jk is set
(1. (M,K)) * (n,Jk) is Element of the carrier of M
V * IM is Relation-like NAT -defined the carrier of M -valued Function-like finite B -element FinSequence-like FinSubsequence-like Element of B -tuples_on the carrier of M
K440( the carrier of M, the carrier of M,IM,(V multfield)) is Relation-like NAT -defined the carrier of M -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of M
(V * IM) . Jk is set
V * ((1. (M,K)) * (n,Jk)) is Element of the carrier of M
[n,Jk] is set
{n,Jk} is non empty finite V36() set
{n} is non empty trivial finite V36() 1 -element set
{{n,Jk},{n}} is non empty finite V36() set
[(n + 1),Jk] is set
{(n + 1),Jk} is non empty finite V36() set
{(n + 1)} is non empty trivial finite V36() 1 -element set
{{(n + 1),Jk},{(n + 1)}} is non empty finite V36() set
KER is Relation-like NAT -defined the carrier of M -valued Function-like finite B -element FinSequence-like FinSubsequence-like Element of B -tuples_on the carrier of M
KER . Jk is set
(1. (M,K)) * ((n + 1),Jk) is Element of the carrier of M
(V * IM) + KER is Relation-like NAT -defined the carrier of M -valued Function-like finite B -element FinSequence-like FinSubsequence-like Element of B -tuples_on the carrier of M
K437( the carrier of M, the carrier of M, the carrier of M, the addF of M,(V * IM),KER) is Relation-like NAT -defined the carrier of M -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of M
K685((V * IM),KER) is Relation-like Function-like set
K685((V * IM),KER) * the addF of M is Relation-like the carrier of M -valued set
((V * IM) + KER) . Jk is set
(V * ((1. (M,K)) * (n,Jk))) + ((1. (M,K)) * ((n + 1),Jk)) is Element of the carrier of M
FK is Relation-like NAT -defined the carrier of M -valued Function-like finite B -element FinSequence-like FinSubsequence-like Element of B -tuples_on the carrier of M
FK . Jk is set
(M,V,K) * (n,Jk) is Element of the carrier of M
0. M is V65(M) Element of the carrier of M
the ZeroF of M is Element of the carrier of M
V + (0. M) is Element of the carrier of M
1_ M is Element of the carrier of M
1. M is V65(M) Element of the carrier of M
the OneF of M is Element of the carrier of M
V * (1_ M) is Element of the carrier of M
(V * (1_ M)) + (0. M) is Element of the carrier of M
(V * ((1. (M,K)) * (n,Jk))) + (0. M) is Element of the carrier of M
1_ M is Element of the carrier of M
1. M is V65(M) Element of the carrier of M
the OneF of M is Element of the carrier of M
0. M is V65(M) Element of the carrier of M
the ZeroF of M is Element of the carrier of M
(0. M) + (1_ M) is Element of the carrier of M
V * (0. M) is Element of the carrier of M
(V * (0. M)) + (1_ M) is Element of the carrier of M
(V * ((1. (M,K)) * (n,Jk))) + (1_ M) is Element of the carrier of M
0. M is V65(M) Element of the carrier of M
the ZeroF of M is Element of the carrier of M
(0. M) + (0. M) is Element of the carrier of M
V * (0. M) is Element of the carrier of M
(V * (0. M)) + (0. M) is Element of the carrier of M
(V * ((1. (M,K)) * (n,Jk))) + (0. M) is Element of the carrier of M
n is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital V131() V133() right-distributive left-distributive right_unital well-unital V142() left_unital V152() V153() V154() doubleLoopStr
the carrier of K is non empty non trivial set
1. (K,n) is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Function-yielding V201() Matrix of n,n, the carrier of K
the carrier of K * is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
width (1. (K,n)) is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
Line ((1. (K,n)),n) is Relation-like NAT -defined the carrier of K -valued Function-like finite width (1. (K,n)) -element 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
M is Element of the carrier of K
(K,M,n) is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Function-yielding V201() upper_triangular Matrix of n,n, the carrier of K
Line ((K,M,n),n) is Relation-like NAT -defined the carrier of K -valued Function-like finite width (K,M,n) -element FinSequence-like FinSubsequence-like Element of (width (K,M,n)) -tuples_on the carrier of K
width (K,M,n) is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
(width (K,M,n)) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
M * (Line ((1. (K,n)),n)) is Relation-like NAT -defined the carrier of K -valued Function-like finite width (1. (K,n)) -element FinSequence-like FinSubsequence-like Element of (width (1. (K,n))) -tuples_on the carrier of K
M multfield is Relation-like the carrier of K -defined the carrier of K -valued Function-like non empty total V18( the carrier of K, the carrier of K) Element of bool [: the carrier of K, the carrier of K:]
[: the carrier of K, the carrier of K:] is Relation-like set
bool [: the carrier of K, the carrier of K:] is set
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like total V18([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[:[: the carrier of K, the carrier of K:], the carrier of K:] is Relation-like set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is set
id the carrier of K is Relation-like the carrier of K -defined the carrier of K -valued non empty total V18( the carrier of K, the carrier of K) Element of bool [: the carrier of K, the carrier of K:]
the multF of K [;] (M,(id the carrier of K)) is Relation-like the carrier of K -defined the carrier of K -valued Function-like non empty total V18( the carrier of K, the carrier of K) Element of bool [: the carrier of K, the carrier of K:]
K440( the carrier of K, the carrier of K,(Line ((1. (K,n)),n)),(M multfield)) is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of K
Indices (1. (K,n)) is set
dom (1. (K,n)) is finite Element of bool NAT
Seg (width (1. (K,n))) is finite width (1. (K,n)) -element V43() Element of bool NAT
{ b₁ where b₁ is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b₁ & b₁ <= width (1. (K,n)) ) } is set
[:(dom (1. (K,n))),(Seg (width (1. (K,n)))):] is Relation-like finite set
Indices (K,M,n) is set
dom (K,M,n) is finite Element of bool NAT
Seg (width (K,M,n)) is finite width (K,M,n) -element V43() Element of bool NAT
{ b₁ where b₁ is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b₁ & b₁ <= width (K,M,n) ) } is set
[:(dom (K,M,n)),(Seg (width (K,M,n))):] is Relation-like finite set
J is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
J -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
Seg n is finite n -element V43() Element of bool NAT
{ b₁ where b₁ is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
[:(Seg n),(Seg n):] is Relation-like finite set
c₁₁ is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
[n,c₁₁] is set
{n,c₁₁} is non empty finite V36() set
{n} is non empty trivial finite V36() 1 -element set
{{n,c₁₁},{n}} is non empty finite V36() set
b1 is Relation-like NAT -defined the carrier of K -valued Function-like finite J -element FinSequence-like FinSubsequence-like Element of J -tuples_on the carrier of K
b1 . c₁₁ is set
(1. (K,n)) * (n,c₁₁) is Element of the carrier of K
M * b1 is Relation-like NAT -defined the carrier of K -valued Function-like finite J -element FinSequence-like FinSubsequence-like Element of J -tuples_on the carrier of K
K440( the carrier of K, the carrier of K,b1,(M multfield)) is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of K
(M * b1) . c₁₁ is set
M * ((1. (K,n)) * (n,c₁₁)) is Element of the carrier of K
P is Relation-like NAT -defined the carrier of K -valued Function-like finite J -element FinSequence-like FinSubsequence-like Element of J -tuples_on the carrier of K
P . c₁₁ is set
(K,M,n) * (n,c₁₁) is Element of the carrier of K
1_ K is Element of the carrier of K
1. K is V65(K) Element of the carrier of K
the OneF of K is Element of the carrier of K
M * (1_ K) is Element of the carrier of K
n + 1 is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
n + 1 is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
0. K is V65(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
M * (0. K) is Element of the carrier of K
n + 1 is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
n is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
Seg n is finite n -element V43() Element of bool NAT
{ b₁ where b₁ is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
K is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
K + 1 is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
M is non empty non degenerated non trivial right_complementable almost_left_invertible unital V131() V133() right-distributive left-distributive right_unital well-unital V142() left_unital V152() V153() V154() doubleLoopStr
the carrier of M is non empty non trivial set
n -tuples_on the carrier of M is functional non empty FinSequence-membered FinSequenceSet of the carrier of M
V is Element of the carrier of M
(M,V,n) is Relation-like NAT -defined the carrier of M * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Function-yielding V201() upper_triangular Matrix of n,n, the carrier of M
the carrier of M * is functional non empty FinSequence-membered FinSequenceSet of the carrier of M
Line ((M,V,n),K) is Relation-like NAT -defined the carrier of M -valued Function-like finite width (M,V,n) -element FinSequence-like FinSubsequence-like Element of (width (M,V,n)) -tuples_on the carrier of M
width (M,V,n) is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
(width (M,V,n)) -tuples_on the carrier of M is functional non empty FinSequence-membered FinSequenceSet of the carrier of M
B is Relation-like NAT -defined the carrier of M -valued Function-like finite n -element FinSequence-like FinSubsequence-like Element of n -tuples_on the carrier of M
(Line ((M,V,n),K)) "*" B is Element of the carrier of M
mlt ((Line ((M,V,n),K)),B) is Relation-like NAT -defined the carrier of M -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of M
the multF of M is Relation-like [: the carrier of M, the carrier of M:] -defined the carrier of M -valued Function-like total V18([: the carrier of M, the carrier of M:], the carrier of M) 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 set
[:[: the carrier of M, the carrier of M:], the carrier of M:] is Relation-like set
bool [:[: the carrier of M, the carrier of M:], the carrier of M:] is set
K437( the carrier of M, the carrier of M, the carrier of M, the multF of M,(Line ((M,V,n),K)),B) is Relation-like NAT -defined the carrier of M -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of M
K685((Line ((M,V,n),K)),B) is Relation-like Function-like set
K685((Line ((M,V,n),K)),B) * the multF of M is Relation-like the carrier of M -valued set
Sum (mlt ((Line ((M,V,n),K)),B)) 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 total V18([: the carrier of M, the carrier of M:], the carrier of M) Element of bool [:[: the carrier of M, the carrier of M:], the carrier of M:]
the addF of M $$ (mlt ((Line ((M,V,n),K)),B)) is Element of the carrier of M
B /. K is Element of the carrier of M
V * (B /. K) is Element of the carrier of M
B /. (K + 1) is Element of the carrier of M
(V * (B /. K)) + (B /. (K + 1)) is Element of the carrier of M
(Line ((M,V,n),K)) . K is set
(M,V,n) * (K,K) is Element of the carrier of M
Indices (M,V,n) is set
dom (M,V,n) is finite Element of bool NAT
Seg (width (M,V,n)) is finite width (M,V,n) -element V43() Element of bool NAT
{ b₁ where b₁ is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b₁ & b₁ <= width (M,V,n) ) } is set
[:(dom (M,V,n)),(Seg (width (M,V,n))):] is Relation-like finite set
[:(Seg n),(Seg n):] is Relation-like finite set
[K,K] is set
{K,K} is non empty finite V36() set
{K} is non empty trivial finite V36() 1 -element set
{{K,K},{K}} is non empty finite V36() set
T is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
T -tuples_on the carrier of M is functional non empty FinSequence-membered FinSequenceSet of the carrier of M
P is Relation-like NAT -defined the carrier of M -valued Function-like finite T -element FinSequence-like FinSubsequence-like Element of T -tuples_on the carrier of M
dom P is finite T -element Element of bool NAT
P . K is set
P /. K is Element of the carrier of M
b1 is Relation-like NAT -defined the carrier of M -valued Function-like finite T -element FinSequence-like FinSubsequence-like Element of T -tuples_on the carrier of M
mlt (b1,P) is Relation-like NAT -defined the carrier of M -valued Function-like finite T -element FinSequence-like FinSubsequence-like Element of T -tuples_on the carrier of M
K437( the carrier of M, the carrier of M, the carrier of M, the multF of M,b1,P) is Relation-like NAT -defined the carrier of M -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of M
K685(b1,P) is Relation-like Function-like set
K685(b1,P) * the multF of M is Relation-like the carrier of M -valued set
dom (mlt (b1,P)) is finite T -element Element of bool NAT
c₁₁ is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
[K,c₁₁] is set
{K,c₁₁} is non empty finite V36() set
{{K,c₁₁},{K}} is non empty finite V36() set
0. M is V65(M) Element of the carrier of M
the ZeroF of M is Element of the carrier of M
(M,V,n) * (K,c₁₁) is Element of the carrier of M
b1 . c₁₁ is set
P . c₁₁ is set
P /. c₁₁ is Element of the carrier of M
(mlt (b1,P)) . c₁₁ is set
(0. M) * (P /. c₁₁) is Element of the carrier of M
[K,(K + 1)] is set
{K,(K + 1)} is non empty finite V36() set
{{K,(K + 1)},{K}} is non empty finite V36() set
b1 . K is set
(mlt (b1,P)) /. K is Element of the carrier of M
(mlt (b1,P)) . K is set
((M,V,n) * (K,K)) * (P /. K) is Element of the carrier of M
V * (P /. K) is Element of the carrier of M
P . (K + 1) is set
P /. (K + 1) is Element of the carrier of M
(M,V,n) * (K,(K + 1)) is Element of the carrier of M
b1 . (K + 1) is set
(mlt (b1,P)) /. (K + 1) is Element of the carrier of M
(mlt (b1,P)) . (K + 1) is set
((M,V,n) * (K,(K + 1))) * (P /. (K + 1)) is Element of the carrier of M
1_ M is Element of the carrier of M
1. M is V65(M) Element of the carrier of M
the OneF of M is Element of the carrier of M
(1_ M) * (P /. (K + 1)) is Element of the carrier of M
c₁₁ is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
P . c₁₁ is set
P /. c₁₁ is Element of the carrier of M
[K,c₁₁] is set
{K,c₁₁} is non empty finite V36() set
{{K,c₁₁},{K}} is non empty finite V36() set
(Line ((M,V,n),K)) . c₁₁ is set
(M,V,n) * (K,c₁₁) is Element of the carrier of M
0. M is V65(M) Element of the carrier of M
the ZeroF of M is Element of the carrier of M
mlt ((Line ((M,V,n),K)),P) is Relation-like NAT -defined the carrier of M -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of M
K437( the carrier of M, the carrier of M, the carrier of M, the multF of M,(Line ((M,V,n),K)),P) is Relation-like NAT -defined the carrier of M -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of M
K685((Line ((M,V,n),K)),P) is Relation-like Function-like set
K685((Line ((M,V,n),K)),P) * the multF of M is Relation-like the carrier of M -valued set
(mlt ((Line ((M,V,n),K)),P)) . c₁₁ is set
(0. M) * (P /. c₁₁) is Element of the carrier of M
(mlt ((Line ((M,V,n),K)),P)) . K is set
((M,V,n) * (K,K)) * (P /. K) is Element of the carrier of M
n is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
Seg n is finite n -element V43() Element of bool NAT
{ b₁ where b₁ is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
K is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
K - 1 is V46() ext-real V165() set
M is non empty non degenerated non trivial right_complementable almost_left_invertible unital V131() V133() right-distributive left-distributive right_unital well-unital V142() left_unital V152() V153() V154() doubleLoopStr
the carrier of M is non empty non trivial set
n -tuples_on the carrier of M is functional non empty FinSequence-membered FinSequenceSet of the carrier of M
V is Element of the carrier of M
(M,V,n) is Relation-like NAT -defined the carrier of M * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Function-yielding V201() upper_triangular Matrix of n,n, the carrier of M
the carrier of M * is functional non empty FinSequence-membered FinSequenceSet of the carrier of M
Col ((M,V,n),K) is Relation-like NAT -defined the carrier of M -valued Function-like finite len (M,V,n) -element FinSequence-like FinSubsequence-like Element of (len (M,V,n)) -tuples_on the carrier of M
len (M,V,n) is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
(len (M,V,n)) -tuples_on the carrier of M is functional non empty FinSequence-membered FinSequenceSet of the carrier of M
J is Relation-like NAT -defined the carrier of M -valued Function-like finite n -element FinSequence-like FinSubsequence-like Element of n -tuples_on the carrier of M
(Col ((M,V,n),K)) "*" J is Element of the carrier of M
mlt ((Col ((M,V,n),K)),J) is Relation-like NAT -defined the carrier of M -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of M
the multF of M is Relation-like [: the carrier of M, the carrier of M:] -defined the carrier of M -valued Function-like total V18([: the carrier of M, the carrier of M:], the carrier of M) 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 set
[:[: the carrier of M, the carrier of M:], the carrier of M:] is Relation-like set
bool [:[: the carrier of M, the carrier of M:], the carrier of M:] is set
K437( the carrier of M, the carrier of M, the carrier of M, the multF of M,(Col ((M,V,n),K)),J) is Relation-like NAT -defined the carrier of M -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of M
K685((Col ((M,V,n),K)),J) is Relation-like Function-like set
K685((Col ((M,V,n),K)),J) * the multF of M is Relation-like the carrier of M -valued set
Sum (mlt ((Col ((M,V,n),K)),J)) 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 total V18([: the carrier of M, the carrier of M:], the carrier of M) Element of bool [:[: the carrier of M, the carrier of M:], the carrier of M:]
the addF of M $$ (mlt ((Col ((M,V,n),K)),J)) is Element of the carrier of M
J /. K is Element of the carrier of M
V * (J /. K) is Element of the carrier of M
J /. (K - 1) is Element of the carrier of M
(V * (J /. K)) + (J /. (K - 1)) is Element of the carrier of M
dom (M,V,n) is finite Element of bool NAT
Seg (len (M,V,n)) is finite len (M,V,n) -element V43() Element of bool NAT
{ b₁ where b₁ is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b₁ & b₁ <= len (M,V,n) ) } is set
(Col ((M,V,n),K)) . K is set
(M,V,n) * (K,K) is Element of the carrier of M
b1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
b1 + 1 is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
Indices (M,V,n) is set
width (M,V,n) is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
Seg (width (M,V,n)) is finite width (M,V,n) -element V43() Element of bool NAT
{ b₁ where b₁ is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b₁ & b₁ <= width (M,V,n) ) } is set
[:(dom (M,V,n)),(Seg (width (M,V,n))):] is Relation-like finite set
[:(Seg n),(Seg n):] is Relation-like finite set
[K,K] is set
{K,K} is non empty finite V36() set
{K} is non empty trivial finite V36() 1 -element set
{{K,K},{K}} is non empty finite V36() set
T is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
T -tuples_on the carrier of M is functional non empty FinSequence-membered FinSequenceSet of the carrier of M
c₁₁ is Relation-like NAT -defined the carrier of M -valued Function-like finite T -element FinSequence-like FinSubsequence-like Element of T -tuples_on the carrier of M
dom c₁₁ is finite T -element Element of bool NAT
c₁₁ . K is set
c₁₁ /. K is Element of the carrier of M
P is Relation-like NAT -defined the carrier of M -valued Function-like finite T -element FinSequence-like FinSubsequence-like Element of T -tuples_on the carrier of M
mlt (P,c₁₁) is Relation-like NAT -defined the carrier of M -valued Function-like finite T -element FinSequence-like FinSubsequence-like Element of T -tuples_on the carrier of M
K437( the carrier of M, the carrier of M, the carrier of M, the multF of M,P,c₁₁) is Relation-like NAT -defined the carrier of M -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of M
K685(P,c₁₁) is Relation-like Function-like set
K685(P,c₁₁) * the multF of M is Relation-like the carrier of M -valued set
dom (mlt (P,c₁₁)) is finite T -element Element of bool NAT
(mlt (P,c₁₁)) /. K is Element of the carrier of M
(mlt (P,c₁₁)) . K is set
((M,V,n) * (K,K)) * (c₁₁ /. K) is Element of the carrier of M
V * (c₁₁ /. K) is Element of the carrier of M
IM is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
c₁₁ . IM is set
c₁₁ /. IM is Element of the carrier of M
IM + 1 is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
[IM,K] is set
{IM,K} is non empty finite V36() set
{IM} is non empty trivial finite V36() 1 -element set
{{IM,K},{IM}} is non empty finite V36() set
(Col ((M,V,n),K)) . IM is set
(M,V,n) * (IM,K) is Element of the carrier of M
0. M is V65(M) Element of the carrier of M
the ZeroF of M is Element of the carrier of M
mlt ((Col ((M,V,n),K)),c₁₁) is Relation-like NAT -defined the carrier of M -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of M
K437( the carrier of M, the carrier of M, the carrier of M, the multF of M,(Col ((M,V,n),K)),c₁₁) is Relation-like NAT -defined the carrier of M -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of M
K685((Col ((M,V,n),K)),c₁₁) is Relation-like Function-like set
K685((Col ((M,V,n),K)),c₁₁) * the multF of M is Relation-like the carrier of M -valued set
(mlt ((Col ((M,V,n),K)),c₁₁)) . IM is set
(0. M) * (c₁₁ /. IM) is Element of the carrier of M
(mlt ((Col ((M,V,n),K)),c₁₁)) . K is set
{} + 1 is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
[b1,K] is set
{b1,K} is non empty finite V36() set
{b1} is non empty trivial finite V36() 1 -element set
{{b1,K},{b1}} is non empty finite V36() set
IM is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
[IM,K] is set
{IM,K} is non empty finite V36() set
{IM} is non empty trivial finite V36() 1 -element set
{{IM,K},{IM}} is non empty finite V36() set
IM + 1 is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
0. M is V65(M) Element of the carrier of M
the ZeroF of M is Element of the carrier of M
(M,V,n) * (IM,K) is Element of the carrier of M
P . IM is set
c₁₁ . IM is set
c₁₁ /. IM is Element of the carrier of M
(mlt (P,c₁₁)) . IM is set
(0. M) * (c₁₁ /. IM) is Element of the carrier of M
c₁₁ . b1 is set
c₁₁ /. b1 is Element of the carrier of M
(Col ((M,V,n),K)) . b1 is set
(M,V,n) * (b1,K) is Element of the carrier of M
(mlt (P,c₁₁)) /. b1 is Element of the carrier of M
(mlt (P,c₁₁)) . b1 is set
((M,V,n) * (b1,K)) * (c₁₁ /. b1) is Element of the carrier of M
1_ M is Element of the carrier of M
1. M is V65(M) Element of the carrier of M
the OneF of M is Element of the carrier of M
(1_ M) * (c₁₁ /. b1) is Element of the carrier of M
n is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital V131() V133() right-distributive left-distributive right_unital well-unital V142() left_unital V152() V153() V154() doubleLoopStr
the carrier of K is non empty non trivial set
0. K is V65(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
the carrier of K * is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
power K is Relation-like [: the carrier of K,NAT:] -defined the carrier of K -valued Function-like total V18([: the carrier of K,NAT:], the carrier of K) Element of bool [:[: the carrier of K,NAT:], the carrier of K:]
[: the carrier of K,NAT:] is Relation-like non trivial non finite set
[:[: the carrier of K,NAT:], the carrier of K:] is Relation-like non trivial non finite set
bool [:[: the carrier of K,NAT:], the carrier of K:] is non trivial non finite set
M is Element of the carrier of K
(K,M,n) is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Function-yielding V201() upper_triangular Matrix of n,n, the carrier of K
(K,M,n) ~ is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Function-yielding V201() Matrix of n,n, the carrier of K
M " is Element of the carrier of K
- (M ") is Element of the carrier of K
V is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
Seg V is finite V -element V43() Element of bool NAT
{ b₁ where b₁ is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b₁ & b₁ <= V ) } is set
[:(Seg V),(Seg V):] is Relation-like finite set
B is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
M9 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
[B,M9] is set
{B,M9} is non empty finite V36() set
{B} is non empty trivial finite V36() 1 -element set
{{B,M9},{B}} is non empty finite V36() set
M9 -' B is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
(M9 -' B) + 1 is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
(power K) . ((- (M ")),((M9 -' B) + 1)) is Element of the carrier of K
- ((power K) . ((- (M ")),((M9 -' B) + 1))) is Element of the carrier of K
B is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Function-yielding V201() Matrix of V,V, the carrier of K
Indices B is set
dom B is finite Element of bool NAT
width B is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
Seg (width B) is finite width B -element V43() Element of bool NAT
{ b₁ where b₁ is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b₁ & b₁ <= width B ) } is set
[:(dom B),(Seg (width B)):] is Relation-like finite set
1. (K,n) is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Function-yielding V201() Matrix of n,n, the carrier of K
Indices (1. (K,n)) is set
dom (1. (K,n)) is finite Element of bool NAT
width (1. (K,n)) is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
Seg (width (1. (K,n))) is finite width (1. (K,n)) -element V43() Element of bool NAT
{ b₁ where b₁ is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b₁ & b₁ <= width (1. (K,n)) ) } is set
[:(dom (1. (K,n))),(Seg (width (1. (K,n)))):] is Relation-like finite set
Seg n is finite n -element V43() Element of bool NAT
{ b₁ where b₁ is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
[:(Seg n),(Seg n):] is Relation-like finite set
J is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Function-yielding V201() Matrix of n,n, the carrier of K
J * (K,M,n) is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Function-yielding V201() Matrix of n,n, the carrier of K
Indices J is set
dom J is finite Element of bool NAT
width J is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
Seg (width J) is finite width J -element V43() Element of bool NAT
{ b₁ where b₁ is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b₁ & b₁ <= width J ) } is set
[:(dom J),(Seg (width J)):] is Relation-like finite set
Indices (K,M,n) is set
dom (K,M,n) is finite Element of bool NAT
width (K,M,n) is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
Seg (width (K,M,n)) is finite width (K,M,n) -element V43() Element of bool NAT
{ b₁ where b₁ is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b₁ & b₁ <= width (K,M,n) ) } is set
[:(dom (K,M,n)),(Seg (width (K,M,n))):] is Relation-like finite set
Indices (J * (K,M,n)) is set
dom (J * (K,M,n)) is finite Element of bool NAT
width (J * (K,M,n)) is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
Seg (width (J * (K,M,n))) is finite width (J * (K,M,n)) -element V43() Element of bool NAT
{ b₁ where b₁ is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b₁ & b₁ <= width (J * (K,M,n)) ) } is set
[:(dom (J * (K,M,n))),(Seg (width (J * (K,M,n)))):] is Relation-like finite set
len (K,M,n) is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
P is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
c₁₁ is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
[P,c₁₁] is set
{P,c₁₁} is non empty finite V36() set
{P} is non empty trivial finite V36() 1 -element set
{{P,c₁₁},{P}} is non empty finite V36() set
Line (J,P) is Relation-like NAT -defined the carrier of K -valued Function-like finite width J -element FinSequence-like FinSubsequence-like Element of (width J) -tuples_on the carrier of K
(width J) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
(J * (K,M,n)) * (P,c₁₁) is Element of the carrier of K
Col ((K,M,n),c₁₁) is Relation-like NAT -defined the carrier of K -valued Function-like finite len (K,M,n) -element FinSequence-like FinSubsequence-like Element of (len (K,M,n)) -tuples_on the carrier of K
(len (K,M,n)) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
(Line (J,P)) "*" (Col ((K,M,n),c₁₁)) is Element of the carrier of K
mlt ((Line (J,P)),(Col ((K,M,n),c₁₁))) is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of K
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like total V18([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is Relation-like set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is Relation-like set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is set
K437( the carrier of K, the carrier of K, the carrier of K, the multF of K,(Line (J,P)),(Col ((K,M,n),c₁₁))) is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of K
K685((Line (J,P)),(Col ((K,M,n),c₁₁))) is Relation-like Function-like set
K685((Line (J,P)),(Col ((K,M,n),c₁₁))) * the multF of K is Relation-like the carrier of K -valued set
Sum (mlt ((Line (J,P)),(Col ((K,M,n),c₁₁)))) is Element of the carrier of K
the addF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like total V18([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
the addF of K $$ (mlt ((Line (J,P)),(Col ((K,M,n),c₁₁)))) is Element of the carrier of K
(Col ((K,M,n),c₁₁)) "*" (Line (J,P)) is Element of the carrier of K
mlt ((Col ((K,M,n),c₁₁)),(Line (J,P))) is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of K
K437( the carrier of K, the carrier of K, the carrier of K, the multF of K,(Col ((K,M,n),c₁₁)),(Line (J,P))) is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of K
K685((Col ((K,M,n),c₁₁)),(Line (J,P))) is Relation-like Function-like set
K685((Col ((K,M,n),c₁₁)),(Line (J,P))) * the multF of K is Relation-like the carrier of K -valued set
Sum (mlt ((Col ((K,M,n),c₁₁)),(Line (J,P)))) is Element of the carrier of K
the addF of K $$ (mlt ((Col ((K,M,n),c₁₁)),(Line (J,P)))) is Element of the carrier of K
(Line (J,P)) . c₁₁ is set
J * (P,c₁₁) is Element of the carrier of K
dom (Line (J,P)) is finite width J -element Element of bool NAT
(Line (J,P)) /. c₁₁ is Element of the carrier of K
M * (J * (P,c₁₁)) is Element of the carrier of K
P -' P is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
(P -' P) + 1 is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
(power K) . ((- (M ")),((P -' P) + 1)) is Element of the carrier of K
- ((power K) . ((- (M ")),((P -' P) + 1))) is Element of the carrier of K
M * (- ((power K) . ((- (M ")),((P -' P) + 1)))) is Element of the carrier of K
{} + 1 is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
(power K) . ((- (M ")),({} + 1)) is Element of the carrier of K
- ((power K) . ((- (M ")),({} + 1))) is Element of the carrier of K
M * (- ((power K) . ((- (M ")),({} + 1)))) is Element of the carrier of K
- (- (M ")) is Element of the carrier of K
M * (- (- (M "))) is Element of the carrier of K
M * (M ") is Element of the carrier of K
1_ K is Element of the carrier of K
1. K is V65(K) Element of the carrier of K
the OneF of K is Element of the carrier of K
(1. (K,n)) * (P,c₁₁) is Element of the carrier of K
M * (0. K) is Element of the carrier of K
(1. (K,n)) * (P,c₁₁) is Element of the carrier of K
(1. (K,n)) * (P,c₁₁) is Element of the carrier of K
(1. (K,n)) * (P,c₁₁) is Element of the carrier of K
c₁₁ - 1 is V46() ext-real V165() set
KER is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
KER + 1 is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
{} + 1 is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
[P,KER] is set
{P,KER} is non empty finite V36() set
{{P,KER},{P}} is non empty finite V36() set
(Line (J,P)) /. KER is Element of the carrier of K
(Line (J,P)) . KER is set
J * (P,KER) is Element of the carrier of K
M * (J * (P,c₁₁)) is Element of the carrier of K
(M * (J * (P,c₁₁))) + (J * (P,KER)) is Element of the carrier of K
KER -' P is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
(KER -' P) + 1 is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
(power K) . ((- (M ")),((KER -' P) + 1)) is Element of the carrier of K
c₁₁ -' P is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
c₁₁ - P is V46() ext-real V165() set
KER - P is V46() ext-real V165() set
- ((power K) . ((- (M ")),((KER -' P) + 1))) is Element of the carrier of K
(M * (J * (P,c₁₁))) + (- ((power K) . ((- (M ")),((KER -' P) + 1)))) is Element of the carrier of K
(c₁₁ -' P) + 1 is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
(power K) . ((- (M ")),((c₁₁ -' P) + 1)) is Element of the carrier of K
- ((power K) . ((- (M ")),((c₁₁ -' P) + 1))) is Element of the carrier of K
M * (- ((power K) . ((- (M ")),((c₁₁ -' P) + 1)))) is