:: MATRIXJ2 semantic presentation

REAL is set
NAT is non empty non trivial V25() V26() V27() non finite cardinal limit_cardinal Element of bool REAL

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

RAT is 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

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

{{},1} is non empty finite V36() set
K705() is set
bool K705() is set
K706() is Element of bool K705()

bool 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

Seg 1 is non empty trivial finite 1 -element V43() Element of bool NAT
{ b1 where b1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b1 & b1 <= 2 ) } is set
{1,2} is non empty finite V36() set

K667(()) is V46() ext-real V165() Element of REAL
n is set
K is set
{K} is non empty trivial finite 1 -element 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} is non empty trivial finite 1 -element 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

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

{ b1 where b1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b1 & b1 <= 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

Indices B is set

width B is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
Seg () is finite width B -element V43() Element of bool NAT
{ b1 where b1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b1 & b1 <= width B ) } is set
[:(dom B),(Seg ()):] 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

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

Seg () is finite width V -element V43() Element of bool NAT
{ b1 where b1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b1 & b1 <= width V ) } is set
[:(dom V),(Seg ()):] is Relation-like finite set

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

Seg () is finite width B -element V43() Element of bool NAT
{ b1 where b1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b1 & b1 <= width B ) } is set
[:(dom B),(Seg ()):] 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

{ b1 where b1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b1 & b1 <= 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

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

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

Indices V is set

width V is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
Seg () is finite width V -element V43() Element of bool NAT
{ b1 where b1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b1 & b1 <= width V ) } is set
[:(dom V),(Seg ()):] 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

the carrier of K is non empty non trivial set
M is Element of the carrier of K

the carrier of K * is functional non empty FinSequence-membered FinSequenceSet of the carrier of K

n -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K

{ b1 where b1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b1 & b1 <= 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

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

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
() . (M,n) 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 \$\$ (diagonal_of_Matrix (K,M,n)) is Element of 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

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

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

{ b1 where b1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set

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
() . (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
() . (M,n) is Element of 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

{ b1 where b1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b1 & b1 <= 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

{ b1 where b1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b1 & b1 <= K ) } is set

the carrier of M is non empty non trivial set

the carrier of M * is functional non empty FinSequence-membered FinSequenceSet of the carrier of M
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

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)),()) 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
{ b1 where b1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b1 & b1 <= 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 . Jk is set
(1. (M,K)) * (n,Jk) is Element of the carrier of M

K440( the carrier of M, the carrier of M,IM,()) 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 . Jk is set
(1. (M,K)) * ((n + 1),Jk) is Element of 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 . 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

the carrier of K is non empty non trivial set

the carrier of K * is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
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

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)),()) 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
{ b1 where b1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b1 & b1 <= 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

{ b1 where b1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
[:(Seg n),(Seg n):] is Relation-like finite set
c11 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
[n,c11] is set
{n,c11} is non empty finite V36() set
{n} is non empty trivial finite V36() 1 -element set
{{n,c11},{n}} is non empty finite V36() set

b1 . c11 is set
(1. (K,n)) * (n,c11) is Element of the carrier of K

K440( the carrier of K, the carrier of K,b1,()) 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) . c11 is set
M * ((1. (K,n)) * (n,c11)) is Element of the carrier of K

P . c11 is set
(K,M,n) * (n,c11) 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

{ b1 where b1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b1 & b1 <= 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

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

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

(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
{ b1 where b1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b1 & b1 <= 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 . K is set
P /. K is Element of 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
c11 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
[K,c11] is set
{K,c11} is non empty finite V36() set
{{K,c11},{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,c11) is Element of the carrier of M
b1 . c11 is set
P . c11 is set
P /. c11 is Element of the carrier of M
(mlt (b1,P)) . c11 is set
(0. M) * (P /. c11) 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
c11 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
P . c11 is set
P /. c11 is Element of the carrier of M
[K,c11] is set
{K,c11} is non empty finite V36() set
{{K,c11},{K}} is non empty finite V36() set
(Line ((M,V,n),K)) . c11 is set
(M,V,n) * (K,c11) 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)) . c11 is set
(0. M) * (P /. c11) 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

{ b1 where b1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b1 & b1 <= 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

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

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

(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
{ b1 where b1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b1 & b1 <= 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

dom c11 is finite T -element Element of bool NAT
c11 . K is set
c11 /. K is Element of the carrier of M

K437( the carrier of M, the carrier of M, the carrier of M, the multF of M,P,c11) 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,c11) is Relation-like Function-like set
K685(P,c11) * the multF of M is Relation-like the carrier of M -valued set
dom (mlt (P,c11)) is finite T -element Element of bool NAT
(mlt (P,c11)) /. K is Element of the carrier of M
(mlt (P,c11)) . K is set
((M,V,n) * (K,K)) * (c11 /. K) is Element of the carrier of M
V * (c11 /. K) is Element of the carrier of M
IM is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
c11 . IM is set
c11 /. 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)),c11) 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)),c11) 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)),c11) is Relation-like Function-like set
K685((Col ((M,V,n),K)),c11) * the multF of M is Relation-like the carrier of M -valued set
(mlt ((Col ((M,V,n),K)),c11)) . IM is set
(0. M) * (c11 /. IM) is Element of the carrier of M
(mlt ((Col ((M,V,n),K)),c11)) . 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
c11 . IM is set
c11 /. IM is Element of the carrier of M
(mlt (P,c11)) . IM is set
(0. M) * (c11 /. IM) is Element of the carrier of M
c11 . b1 is set
c11 /. 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,c11)) /. b1 is Element of the carrier of M
(mlt (P,c11)) . b1 is set
((M,V,n) * (b1,K)) * (c11 /. 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) * (c11 /. b1) is Element of the carrier of M
n is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set

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

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

{ b1 where b1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b1 & b1 <= 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
() . ((- (M ")),((M9 -' B) + 1)) is Element of the carrier of K
- (() . ((- (M ")),((M9 -' B) + 1))) is Element of the carrier of K

Indices B is set

width B is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
Seg () is finite width B -element V43() Element of bool NAT
{ b1 where b1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b1 & b1 <= width B ) } is set
[:(dom B),(Seg ()):] is Relation-like finite set

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
{ b1 where b1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b1 & b1 <= width (1. (K,n)) ) } is set
[:(dom (1. (K,n))),(Seg (width (1. (K,n)))):] is Relation-like finite set

{ b1 where b1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
[:(Seg n),(Seg n):] is Relation-like finite set

Indices J is set

width J is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
Seg () is finite width J -element V43() Element of bool NAT
{ b1 where b1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b1 & b1 <= width J ) } is set
[:(dom J),(Seg ()):] 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
{ b1 where b1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b1 & b1 <= 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
{ b1 where b1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b1 & b1 <= 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
c11 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
[P,c11] is set
{P,c11} is non empty finite V36() set
{P} is non empty trivial finite V36() 1 -element set
{{P,c11},{P}} is non empty finite V36() set

() -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
(J * (K,M,n)) * (P,c11) is Element of the carrier of K
Col ((K,M,n),c11) 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),c11)) is Element of the carrier of K
mlt ((Line (J,P)),(Col ((K,M,n),c11))) 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),c11))) 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),c11))) is Relation-like Function-like set
K685((Line (J,P)),(Col ((K,M,n),c11))) * the multF of K is Relation-like the carrier of K -valued set
Sum (mlt ((Line (J,P)),(Col ((K,M,n),c11)))) 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),c11)))) is Element of the carrier of K
(Col ((K,M,n),c11)) "*" (Line (J,P)) is Element of the carrier of K
mlt ((Col ((K,M,n),c11)),(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),c11)),(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),c11)),(Line (J,P))) is Relation-like Function-like set
K685((Col ((K,M,n),c11)),(Line (J,P))) * the multF of K is Relation-like the carrier of K -valued set
Sum (mlt ((Col ((K,M,n),c11)),(Line (J,P)))) is Element of the carrier of K
the addF of K \$\$ (mlt ((Col ((K,M,n),c11)),(Line (J,P)))) is Element of the carrier of K
(Line (J,P)) . c11 is set
J * (P,c11) is Element of the carrier of K
dom (Line (J,P)) is finite width J -element Element of bool NAT
(Line (J,P)) /. c11 is Element of the carrier of K
M * (J * (P,c11)) 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
() . ((- (M ")),((P -' P) + 1)) is Element of the carrier of K
- (() . ((- (M ")),((P -' P) + 1))) is Element of the carrier of K
M * (- (() . ((- (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
() . ((- (M ")),({} + 1)) is Element of the carrier of K
- (() . ((- (M ")),({} + 1))) is Element of the carrier of K
M * (- (() . ((- (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,c11) is Element of the carrier of K
M * (0. K) is Element of the carrier of K
(1. (K,n)) * (P,c11) is Element of the carrier of K
(1. (K,n)) * (P,c11) is Element of the carrier of K
(1. (K,n)) * (P,c11) is Element of the carrier of K
c11 - 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,c11)) is Element of the carrier of K
(M * (J * (P,c11))) + (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
() . ((- (M ")),((KER -' P) + 1)) is Element of the carrier of K
c11 -' P is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
c11 - P is V46() ext-real V165() set
KER - P is V46() ext-real V165() set
- (() . ((- (M ")),((KER -' P) + 1))) is Element of the carrier of K
(M * (J * (P,c11))) + (- (() . ((- (M ")),((KER -' P) + 1)))) is Element of the carrier of K
(c11 -' P) + 1 is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
() . ((- (M ")),((c11 -' P) + 1)) is Element of the carrier of K
- (() . ((- (M ")),((c11 -' P) + 1))) is Element of the carrier of K
M * (- (() . ((- (M ")),((c11 -' P) + 1)))) is