:: 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

{1} is non empty trivial finite V36() 1 -element set

Seg 2 is non empty finite 2 -element V43() Element of bool NAT

{ b

{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

[:(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

[:(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

[:(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

[:(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

[:(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

[:(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

[:(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

[:(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

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

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

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

[:(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

[:(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

[:(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

[:(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

[:(Seg n),(Seg n):] is Relation-like finite set

c

[n,c

{n,c

{n} is non empty trivial finite V36() 1 -element set

{{n,c

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

(1. (K,n)) * (n,c

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

M * ((1. (K,n)) * (n,c

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

(K,M,n) * (n,c

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

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

[:(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

[K,c

{K,c

{{K,c

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

b1 . c

P . c

P /. c

(mlt (b1,P)) . c

(0. M) * (P /. c

[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

P . c

P /. c

[K,c

{K,c

{{K,c

(Line ((M,V,n),K)) . c

(M,V,n) * (K,c

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

(0. M) * (P /. c

(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

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

(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

[:(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

dom c

c

c

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

K437( the carrier of M, the carrier of M, the carrier of M, the multF of M,P,c

K685(P,c

K685(P,c

dom (mlt (P,c

(mlt (P,c

(mlt (P,c

((M,V,n) * (K,K)) * (c

V * (c

IM is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set

c

c

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

K437( the carrier of M, the carrier of M, the carrier of M, the multF of M,(Col ((M,V,n),K)),c

K685((Col ((M,V,n),K)),c

K685((Col ((M,V,n),K)),c

(mlt ((Col ((M,V,n),K)),c

(0. M) * (c

(mlt ((Col ((M,V,n),K)),c

{} + 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

c

(mlt (P,c

(0. M) * (c

c

c

(Col ((M,V,n),K)) . b1 is set

(M,V,n) * (b1,K) is Element of the carrier of M

(mlt (P,c

(mlt (P,c

((M,V,n) * (b1,K)) * (c

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

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

[:(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

[:(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

[:(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

[:(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

[:(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

[:(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

[:(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

[P,c

{P,c

{P} is non empty trivial finite V36() 1 -element set

{{P,c

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

Col ((K,M,n),c

(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

mlt ((Line (J,P)),(Col ((K,M,n),c

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

K685((Line (J,P)),(Col ((K,M,n),c

K685((Line (J,P)),(Col ((K,M,n),c

Sum (mlt ((Line (J,P)),(Col ((K,M,n),c

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

(Col ((K,M,n),c

mlt ((Col ((K,M,n),c

K437( the carrier of K, the carrier of K, the carrier of K, the multF of K,(Col ((K,M,n),c

K685((Col ((K,M,n),c

K685((Col ((K,M,n),c

Sum (mlt ((Col ((K,M,n),c

the addF of K $$ (mlt ((Col ((K,M,n),c

(Line (J,P)) . c

J * (P,c

dom (Line (J,P)) is finite width J -element Element of bool NAT

(Line (J,P)) /. c

M * (J * (P,c

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

M * (0. K) is Element of the carrier of K

(1. (K,n)) * (P,c

(1. (K,n)) * (P,c

(1. (K,n)) * (P,c

c

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

(M * (J * (P,c

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

c

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

(c

(power K) . ((- (M ")),((c

- ((power K) . ((- (M ")),((c

M * (- ((power K) . ((- (M ")),((c