:: MATRIX15 semantic presentation

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

RAT is set

NAT is non empty non trivial V26() V27() V28() non finite cardinal limit_cardinal V103() set
bool NAT is non empty non trivial non finite V103() set
bool NAT is non empty non trivial non finite V103() set
K96(NAT) is V24() set
INT is set

2 is non empty V26() V27() V28() V32() finite cardinal V105() ext-real positive non negative complex Element of NAT
1 is non empty V26() V27() V28() V32() finite cardinal V105() ext-real positive non negative complex Element of NAT

is Relation-like non empty non trivial non finite V103() set
is Relation-like non empty non trivial non finite V103() set
bool is non empty non trivial non finite V103() set
K741() is set
3 is non empty V26() V27() V28() V32() finite cardinal V105() ext-real positive non negative complex Element of NAT

Seg 1 is non empty trivial finite 1 -element without_zero V103() Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set
{1} is non empty trivial finite V37() 1 -element without_zero V103() set
Seg 2 is non empty finite 2 -element without_zero V103() Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT : ( 1 <= b1 & b1 <= 2 ) } is set
{1,2} is non empty finite V37() without_zero V103() set

the carrier of n is non empty non trivial V103() set
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
K is Element of the carrier of n

width A is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT

len B is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT

width (A * B) is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
width B is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
len (K * (A * B)) is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
len (A * B) is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
len A is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
width (K * A) is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
len (K * A) is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
len ((K * A) * B) is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
f is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set
X is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set
[f,X] is set
{f,X} is non empty finite V37() set
{f} is non empty trivial finite V37() 1 -element set
{{f,X},{f}} is non empty finite V37() without_zero V103() set
Indices (K * (A * B)) is set
dom (K * (A * B)) is finite Element of bool NAT
width (K * (A * B)) is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
Seg (width (K * (A * B))) is finite width (K * (A * B)) -element without_zero Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT : ( 1 <= b1 & b1 <= width (K * (A * B)) ) } is set
[:(dom (K * (A * B))),(Seg (width (K * (A * B)))):] is Relation-like finite set
Indices (A * B) is set
dom (A * B) is finite Element of bool NAT
Seg (width (A * B)) is finite width (A * B) -element without_zero Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT : ( 1 <= b1 & b1 <= width (A * B) ) } is set
[:(dom (A * B)),(Seg (width (A * B))):] is Relation-like finite set

{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT : ( 1 <= b1 & b1 <= len A ) } is set
Seg (len (A * B)) is finite len (A * B) -element without_zero Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT : ( 1 <= b1 & b1 <= len (A * B) ) } is set
dom ((K * A) * B) is finite Element of bool NAT
Indices ((K * A) * B) is set
width ((K * A) * B) is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
Seg (width ((K * A) * B)) is finite width ((K * A) * B) -element without_zero Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT : ( 1 <= b1 & b1 <= width ((K * A) * B) ) } is set
[:(dom ((K * A) * B)),(Seg (width ((K * A) * B))):] is Relation-like finite set
(K * (A * B)) * (f,X) is Element of the carrier of n
(A * B) * (f,X) is Element of the carrier of n
K * ((A * B) * (f,X)) is Element of the carrier of n
the multF of n is Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like total quasi_total V223( the carrier of n) Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[: the carrier of n, the carrier of n:] is Relation-like set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is set
K560( the carrier of n, the multF of n,K,((A * B) * (f,X))) is Element of the carrier of n

() -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b1 where b1 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of n * : len b1 = width A } is set

(len B) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b1 where b1 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of n * : len b1 = len B } is set
(Line (A,f)) "*" (Col (B,X)) is Element of the carrier of n
mlt ((Line (A,f)),(Col (B,X))) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
K498( the carrier of n, the carrier of n, the carrier of n, the multF of n,(Line (A,f)),(Col (B,X))) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Sum (mlt ((Line (A,f)),(Col (B,X)))) is Element of the carrier of n
the addF of n is Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like total quasi_total V223( the carrier of n) V224( the carrier of n) Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
the addF of n \$\$ (mlt ((Line (A,f)),(Col (B,X)))) is Element of the carrier of n
K * ((Line (A,f)) "*" (Col (B,X))) is Element of the carrier of n
K560( the carrier of n, the multF of n,K,((Line (A,f)) "*" (Col (B,X)))) is Element of the carrier of n
K * (mlt ((Line (A,f)),(Col (B,X)))) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
K multfield is Relation-like the carrier of n -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [: the carrier of n, the carrier of n:]
bool [: the carrier of n, the carrier of n:] is set
id the carrier of n is Relation-like the carrier of n -defined the carrier of n -valued Function-like one-to-one non empty total quasi_total Element of bool [: the carrier of n, the carrier of n:]
the multF of n [;] (K,(id the carrier of n)) is Relation-like the carrier of n -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [: the carrier of n, the carrier of n:]
K501( the carrier of n, the carrier of n,(mlt ((Line (A,f)),(Col (B,X)))),()) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Sum (K * (mlt ((Line (A,f)),(Col (B,X))))) is Element of the carrier of n
the addF of n \$\$ (K * (mlt ((Line (A,f)),(Col (B,X))))) is Element of the carrier of n

K501( the carrier of n, the carrier of n,(Line (A,f)),()) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
mlt ((K * (Line (A,f))),(Col (B,X))) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
K498( the carrier of n, the carrier of n, the carrier of n, the multF of n,(K * (Line (A,f))),(Col (B,X))) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Sum (mlt ((K * (Line (A,f))),(Col (B,X)))) is Element of the carrier of n
the addF of n \$\$ (mlt ((K * (Line (A,f))),(Col (B,X)))) is Element of the carrier of n
Line ((K * A),f) is Relation-like NAT -defined the carrier of n -valued Function-like finite width (K * A) -element FinSequence-like FinSubsequence-like Element of (width (K * A)) -tuples_on the carrier of n
(width (K * A)) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b1 where b1 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of n * : len b1 = width (K * A) } is set
(Line ((K * A),f)) "*" (Col (B,X)) is Element of the carrier of n
mlt ((Line ((K * A),f)),(Col (B,X))) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
K498( the carrier of n, the carrier of n, the carrier of n, the multF of n,(Line ((K * A),f)),(Col (B,X))) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Sum (mlt ((Line ((K * A),f)),(Col (B,X)))) is Element of the carrier of n
the addF of n \$\$ (mlt ((Line ((K * A),f)),(Col (B,X)))) is Element of the carrier of n
((K * A) * B) * (f,X) is Element of the carrier of n

the carrier of n is non empty non trivial V103() set
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
1_ n is Element of the carrier of n
1. n is non zero Element of the carrier of n
K is Element of the carrier of n
A is Element of the carrier of n
K * A is Element of the carrier of n
the multF of n is Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like total quasi_total V223( the carrier of n) Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[: the carrier of n, the carrier of n:] is Relation-like set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is set
K560( the carrier of n, the multF of n,K,A) is Element of the carrier of n

X is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set
BX is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set
[X,BX] is set
{X,BX} is non empty finite V37() set
{X} is non empty trivial finite V37() 1 -element set
{{X,BX},{X}} is non empty finite V37() without_zero V103() set
Indices B is set

width B is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT

{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT : ( 1 <= b1 & b1 <= width B ) } is set
[:(dom B),(Seg ()):] is Relation-like finite set
B * (X,BX) is Element of the carrier of n
(1_ n) * (B * (X,BX)) is Element of the carrier of n
K560( the carrier of n, the multF of n,(1_ n),(B * (X,BX))) is Element of the carrier of n
((1_ n) * B) * (X,BX) is Element of the carrier of n
len (K * (A * B)) is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
len (A * B) is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
len B is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
len ((K * A) * B) is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
Indices (A * B) is set
dom (A * B) is finite Element of bool NAT
width (A * B) is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
Seg (width (A * B)) is finite width (A * B) -element without_zero Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT : ( 1 <= b1 & b1 <= width (A * B) ) } is set
[:(dom (A * B)),(Seg (width (A * B))):] is Relation-like finite set
Indices (K * (A * B)) is set
dom (K * (A * B)) is finite Element of bool NAT
width (K * (A * B)) is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
Seg (width (K * (A * B))) is finite width (K * (A * B)) -element without_zero Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT : ( 1 <= b1 & b1 <= width (K * (A * B)) ) } is set
[:(dom (K * (A * B))),(Seg (width (K * (A * B)))):] is Relation-like finite set
X is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set
BX is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set
[X,BX] is set
{X,BX} is non empty finite V37() set
{X} is non empty trivial finite V37() 1 -element set
{{X,BX},{X}} is non empty finite V37() without_zero V103() set
(K * (A * B)) * (X,BX) is Element of the carrier of n
(A * B) * (X,BX) is Element of the carrier of n
K * ((A * B) * (X,BX)) is Element of the carrier of n
K560( the carrier of n, the multF of n,K,((A * B) * (X,BX))) is Element of the carrier of n
B * (X,BX) is Element of the carrier of n
A * (B * (X,BX)) is Element of the carrier of n
K560( the carrier of n, the multF of n,A,(B * (X,BX))) is Element of the carrier of n
K * (A * (B * (X,BX))) is Element of the carrier of n
K560( the carrier of n, the multF of n,K,(A * (B * (X,BX)))) is Element of the carrier of n
(K * A) * (B * (X,BX)) is Element of the carrier of n
K560( the carrier of n, the multF of n,(K * A),(B * (X,BX))) is Element of the carrier of n
((K * A) * B) * (X,BX) is Element of the carrier of n
width ((K * A) * B) is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
len ((1_ n) * B) is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
width ((1_ n) * B) is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT

the carrier of n is non empty non trivial V103() set
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n

Indices K is set

width K is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT

{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT : ( 1 <= b1 & b1 <= width K ) } is set
[:(dom K),(Seg ()):] is Relation-like finite set

Indices (- K) is set
dom (- K) is finite Element of bool NAT
width (- K) is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
Seg (width (- K)) is finite width (- K) -element without_zero Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT : ( 1 <= b1 & b1 <= width (- K) ) } is set
[:(dom (- K)),(Seg (width (- K))):] is Relation-like finite set
len K is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT

{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT : ( 1 <= b1 & b1 <= len K ) } is set
len (- K) is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
Seg (len (- K)) is finite len (- K) -element without_zero Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT : ( 1 <= b1 & b1 <= len (- K) ) } is set
n is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set

the carrier of K is non empty non trivial V103() set
0. K is zero Element of the carrier of K
power K is Relation-like [: the carrier of K,NAT:] -defined the carrier of K -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of K,NAT:], the carrier of K:]
[: the carrier of K,NAT:] is Relation-like non empty non trivial non finite V103() set
[:[: the carrier of K,NAT:], the carrier of K:] is Relation-like non empty non trivial non finite V103() set
bool [:[: the carrier of K,NAT:], the carrier of K:] is non empty non trivial non finite V103() set
A is Element of the carrier of K
() . (A,n) is Element of the carrier of K
B is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set
B + 1 is non empty V26() V27() V28() V32() finite cardinal V105() ext-real positive non negative complex Element of NAT
() . (A,B) is Element of the carrier of K
BA is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set
() . (A,BA) is Element of the carrier of K
(() . (A,B)) * A 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 quasi_total V223( 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
K560( the carrier of K, the multF of K,(() . (A,B)),A) is Element of the carrier of K
1_ K is Element of the carrier of K
1. K is non zero Element of the carrier of K
B is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set
() . (A,B) is Element of the carrier of K
the carrier of n is non empty set

len K is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT

len A is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT

len B is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT

len BA is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT

(K ^ B) + (A ^ BA) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
the addF of n is Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like total quasi_total Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[: the carrier of n, the carrier of n:] is Relation-like set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is set
K498( the carrier of n, the carrier of n, the carrier of n, the addF of n,(K ^ B),(A ^ BA)) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

K498( the carrier of n, the carrier of n, the carrier of n, the addF of n,K,A) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

K498( the carrier of n, the carrier of n, the carrier of n, the addF of n,B,BA) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(K + A) ^ (B + BA) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(len B) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b1 where b1 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of n * : len b1 = len B } is set
(len K) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b1 where b1 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of n * : len b1 = len K } is set
(len K) + (len B) is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT

(len K) + (len B) is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT

K498( the carrier of n, the carrier of n, the carrier of n, the addF of n,X,BX) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

K498( the carrier of n, the carrier of n, the carrier of n, the addF of n,x,f) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(X + BX) ^ (x + f) is Relation-like NAT -defined the carrier of n -valued Function-like finite (len K) + (len B) -element FinSequence-like FinSubsequence-like FinSequence of the carrier of n
((len K) + (len B)) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b1 where b1 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of n * : len b1 = (len K) + (len B) } is set

y is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set
Seg ((len K) + (len B)) is finite (len K) + (len B) -element without_zero Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT : ( 1 <= b1 & b1 <= (len K) + (len B) ) } is set
x is Relation-like NAT -defined the carrier of n -valued Function-like finite (len K) + (len B) -element FinSequence-like FinSubsequence-like Element of ((len K) + (len B)) -tuples_on the carrier of n
dom x is finite (len K) + (len B) -element Element of bool NAT

rng K is finite set
rng A is finite set
dom (X + BX) is finite len K -element Element of bool NAT

{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT : ( 1 <= b1 & b1 <= len K ) } is set
K . y is set

A . y is set
x . y is set
x is Element of the carrier of n
x is Relation-like NAT -defined the carrier of n -valued Function-like finite (len K) + (len B) -element FinSequence-like FinSubsequence-like Element of ((len K) + (len B)) -tuples_on the carrier of n
x . y is set
j is Element of the carrier of n
x + x is Relation-like NAT -defined the carrier of n -valued Function-like finite (len K) + (len B) -element FinSequence-like FinSubsequence-like Element of ((len K) + (len B)) -tuples_on the carrier of n
K498( the carrier of n, the carrier of n, the carrier of n, the addF of n,x,x) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(x + x) . y is set
x + j is Element of the carrier of n
K560( the carrier of n, the addF of n,x,j) is Element of the carrier of n
(X + BX) . y is set
y is Relation-like NAT -defined the carrier of n -valued Function-like finite (len K) + (len B) -element FinSequence-like FinSubsequence-like Element of ((len K) + (len B)) -tuples_on the carrier of n
y . y is set

x is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set
(len K) + x is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
x is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set
(len K) + x is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
B . x is set
rng B is finite set
rng BA is finite set

{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT : ( 1 <= b1 & b1 <= len B ) } is set

BA . x is set
x . y is set
j is Element of the carrier of n
dom (x + f) is finite len B -element Element of bool NAT
len (X + BX) is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
x is Relation-like NAT -defined the carrier of n -valued Function-like finite (len K) + (len B) -element FinSequence-like FinSubsequence-like Element of ((len K) + (len B)) -tuples_on the carrier of n
x . y is set
x is Element of the carrier of n
x + x is Relation-like NAT -defined the carrier of n -valued Function-like finite (len K) + (len B) -element FinSequence-like FinSubsequence-like Element of ((len K) + (len B)) -tuples_on the carrier of n
K498( the carrier of n, the carrier of n, the carrier of n, the addF of n,x,x) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(x + x) . y is set
j + x is Element of the carrier of n
K560( the carrier of n, the addF of n,j,x) is Element of the carrier of n
(x + f) . x is set
y is Relation-like NAT -defined the carrier of n -valued Function-like finite (len K) + (len B) -element FinSequence-like FinSubsequence-like Element of ((len K) + (len B)) -tuples_on the carrier of n
y . y is set

x is Relation-like NAT -defined the carrier of n -valued Function-like finite (len K) + (len B) -element FinSequence-like FinSubsequence-like Element of ((len K) + (len B)) -tuples_on the carrier of n
x + x is Relation-like NAT -defined the carrier of n -valued Function-like finite (len K) + (len B) -element FinSequence-like FinSubsequence-like Element of ((len K) + (len B)) -tuples_on the carrier of n
K498( the carrier of n, the carrier of n, the carrier of n, the addF of n,x,x) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(x + x) . y is set
y is Relation-like NAT -defined the carrier of n -valued Function-like finite (len K) + (len B) -element FinSequence-like FinSubsequence-like Element of ((len K) + (len B)) -tuples_on the carrier of n
y . y is set
x is Relation-like NAT -defined the carrier of n -valued Function-like finite (len K) + (len B) -element FinSequence-like FinSubsequence-like Element of ((len K) + (len B)) -tuples_on the carrier of n
x + x is Relation-like NAT -defined the carrier of n -valued Function-like finite (len K) + (len B) -element FinSequence-like FinSubsequence-like Element of ((len K) + (len B)) -tuples_on the carrier of n
K498( the carrier of n, the carrier of n, the carrier of n, the addF of n,x,x) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(x + x) . y is set
y is Relation-like NAT -defined the carrier of n -valued Function-like finite (len K) + (len B) -element FinSequence-like FinSubsequence-like Element of ((len K) + (len B)) -tuples_on the carrier of n
y . y is set
n is non empty multMagma
the carrier of n is non empty set

B is Element of the carrier of n

B multfield is Relation-like the carrier of n -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [: the carrier of n, the carrier of n:]
[: the carrier of n, the carrier of n:] is Relation-like set
bool [: the carrier of n, the carrier of n:] is set
the multF of n is Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like total quasi_total Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is set
id the carrier of n is Relation-like the carrier of n -defined the carrier of n -valued Function-like one-to-one non empty total quasi_total Element of bool [: the carrier of n, the carrier of n:]
the multF of n [;] (B,(id the carrier of n)) is Relation-like the carrier of n -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [: the carrier of n, the carrier of n:]
K501( the carrier of n, the carrier of n,(K ^ A),()) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

K501( the carrier of n, the carrier of n,K,()) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

K501( the carrier of n, the carrier of n,A,()) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(B * K) ^ (B * A) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len K is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
(len K) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b1 where b1 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of n * : len b1 = len K } is set
len A is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
(len A) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b1 where b1 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of n * : len b1 = len A } is set
(len K) + (len A) is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
((len K) + (len A)) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b1 where b1 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of n * : len b1 = (len K) + (len A) } is set

(len K) + (len A) is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT

K501( the carrier of n, the carrier of n,AB,()) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

K501( the carrier of n, the carrier of n,x,()) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(B * AB) ^ (B * x) is Relation-like NAT -defined the carrier of n -valued Function-like finite (len K) + (len A) -element FinSequence-like FinSubsequence-like FinSequence of the carrier of n
BX is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set
Seg ((len K) + (len A)) is finite (len K) + (len A) -element without_zero Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT : ( 1 <= b1 & b1 <= (len K) + (len A) ) } is set
f is Relation-like NAT -defined the carrier of n -valued Function-like finite (len K) + (len A) -element FinSequence-like FinSubsequence-like Element of ((len K) + (len A)) -tuples_on the carrier of n
dom f is finite (len K) + (len A) -element Element of bool NAT

rng K is finite set
K . BX is set

{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT : ( 1 <= b1 & b1 <= len K ) } is set
dom (B * AB) is finite len K -element Element of bool NAT
f . BX is set
MV is Element of the carrier of n
B * f is Relation-like NAT -defined the carrier of n -valued Function-like finite (len K) + (len A) -element FinSequence-like FinSubsequence-like Element of ((len K) + (len A)) -tuples_on the carrier of n
K501( the carrier of n, the carrier of n,f,()) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(B * f) . BX is set
B * MV is Element of the carrier of n
K560( the carrier of n, the multF of n,B,MV) is Element of the carrier of n
(B * AB) . BX is set
X is Relation-like NAT -defined the carrier of n -valued Function-like finite (len K) + (len A) -element FinSequence-like FinSubsequence-like Element of ((len K) + (len A)) -tuples_on the carrier of n
X . BX is set

rng A is finite set
dom (B * x) is finite len A -element Element of bool NAT

{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT : ( 1 <= b1 & b1 <= len A ) } is set
len (B * AB) is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
MV is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set
(len K) + MV is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
MV is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set
(len K) + MV is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
A . MV is set

f . BX is set
lA is Element of the carrier of n
B * f is Relation-like NAT -defined the carrier of n -valued Function-like finite (len K) + (len A) -element FinSequence-like FinSubsequence-like Element of ((len K) + (len A)) -tuples_on the carrier of n
K501( the carrier of n, the carrier of n,f,()) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(B * f) . BX is set
B * lA is Element of the carrier of n
K560( the carrier of n, the multF of n,B,lA) is Element of the carrier of n
(B * x) . MV is set
X is Relation-like NAT -defined the carrier of n -valued Function-like finite (len K) + (len A) -element FinSequence-like FinSubsequence-like Element of ((len K) + (len A)) -tuples_on the carrier of n
X . BX is set

B * f is Relation-like NAT -defined the carrier of n -valued Function-like finite (len K) + (len A) -element FinSequence-like FinSubsequence-like Element of ((len K) + (len A)) -tuples_on the carrier of n
K501( the carrier of n, the carrier of n,f,()) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(B * f) . BX is set
X is Relation-like NAT -defined the carrier of n -valued Function-like finite (len K) + (len A) -element FinSequence-like FinSubsequence-like Element of ((len K) + (len A)) -tuples_on the carrier of n
X . BX is set
B * f is Relation-like NAT -defined the carrier of n -valued Function-like finite (len K) + (len A) -element FinSequence-like FinSubsequence-like Element of ((len K) + (len A)) -tuples_on the carrier of n
K501( the carrier of n, the carrier of n,f,()) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(B * f) . BX is set
X is Relation-like NAT -defined the carrier of n -valued Function-like finite (len K) + (len A) -element FinSequence-like FinSubsequence-like Element of ((len K) + (len A)) -tuples_on the carrier of n
X . BX is set

dom n is set

rng K is finite set

rng A is finite set

dom (K ^ A) is finite Element of bool NAT
len K is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
len A is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
(len K) + (len A) is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
Seg ((len K) + (len A)) is finite (len K) + (len A) -element without_zero Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT : ( 1 <= b1 & b1 <= (len K) + (len A) ) } is set
rng (K ^ A) is finite set
(rng K) \/ (rng A) is finite set
dom ((K ^ A) (#) n) is finite set

len B is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
dom BA is finite Element of bool NAT

len BA is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
dom (B ^ BA) is finite Element of bool NAT
AB is set
x is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
(B ^ BA) . x is set
B . x is set
K . x is set
n . (K . x) is set
(K ^ A) . x is set
n . ((K ^ A) . x) is set
((K ^ A) (#) n) . x is set
x is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
f is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set
(len K) + f is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
(B ^ BA) . x is set
BA . f is set
A . f is set
n . (A . f) is set
(K ^ A) . x is set
n . ((K ^ A) . x) is set
((K ^ A) (#) n) . x is set
x is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
(B ^ BA) . x is set
((K ^ A) (#) n) . x is set
x is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
(B ^ BA) . x is set
((K ^ A) (#) n) . x is set
(B ^ BA) . AB is set
((K ^ A) (#) n) . AB is set

len n is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
rng n is finite V195() V196() V197() V200() set

K is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set

{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT : ( 1 <= b1 & b1 <= K ) } is set
n is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set
n + 1 is non empty V26() V27() V28() V32() finite cardinal V105() ext-real positive non negative complex Element of NAT

len A is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
rng A is finite V195() V196() V197() V200() set

B is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set

{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT : ( 1 <= b1 & b1 <= B ) } is set

{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT : ( 1 <= b1 & b1 <= n ) } is set

A . (n + 1) is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set

[1,(A . (n + 1))] is set
{1,(A . (n + 1))} is non empty finite V37() set
{{1,(A . (n + 1))},{1}} is non empty finite V37() without_zero V103() set
{[1,(A . (n + 1))]} is Relation-like Function-like constant non empty trivial finite 1 -element set

rng (A | n) is finite V195() V196() V197() V200() set
dom (A | n) is finite Element of bool NAT
AB is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set
(A | n) . AB is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set
x is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set
(A | n) . x is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set
A . AB is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set
A . x is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set
len (A | n) is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
Seg (n + 1) is non empty finite n + 1 -element without_zero V103() Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT : ( 1 <= b1 & b1 <= n + 1 ) } is set
AB is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
x is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
{(A . (n + 1))} is non empty trivial finite V37() 1 -element Element of bool NAT
f is set
(A | n) . f is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set
X is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
A . X is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set
(A | n) . X is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set

rng <*(A . (n + 1))*> is non empty trivial finite 1 -element set
(rng (A | n)) \/ (rng <*(A . (n + 1))*>) is non empty finite set

(A | n) ^ (Sgm {(A . (n + 1))}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V185() V186() V187() V188() FinSequence of NAT

rng n is finite V195() V196() V197() V200() set

K is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set

{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT : ( 1 <= b1 & b1 <= K ) } is set
len n is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT

len A is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
rng A is finite V195() V196() V197() V200() set
B is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set

{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT : ( 1 <= b1 & b1 <= B ) } is set

the carrier of n is non empty set
0. n is zero Element of the carrier of n

Sum K is Element of the carrier of n
the addF of n is Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like total quasi_total V223( the carrier of n) V224( the carrier of n) Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[: the carrier of n, the carrier of n:] is Relation-like set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is set
the addF of n \$\$ K is Element of the carrier of n
A is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set
B is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set
len K is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT

{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT : ( 1 <= b1 & b1 <= len K ) } is set

{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT : ( 1 <= b1 & b1 <= A ) } is set

len (K | A) is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
dom (K | A) is finite Element of bool NAT

f is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set
A + f is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set
X is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set
BX is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
A + BX is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
len x is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT

{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT : ( 1 <= b1 & b1 <= len x ) } is set
A + 1 is non empty V26() V27() V28() V32() finite cardinal V105() ext-real positive non negative complex Element of NAT
X + A is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set
x . X is set
K . (A + BX) is set
Sum x is Element of the carrier of n
the addF of n \$\$ x is Element of the carrier of n
x . f is set
K . B is set
K /. B is Element of the carrier of n
X is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set
(K | A) . X is set
BX is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
K . BX is set
Sum (K | A) is Element of the carrier of n
the addF of n \$\$ (K | A) is Element of the carrier of n
(K | A) . A is set
K . A is set
K /. A is Element of the carrier of n
(K /. A) + (K /. B) is Element of the carrier of n
K560( the carrier of n, the addF of n,(K /. A),(K /. B)) is Element of the carrier of n
A is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set
K /. A is Element of the carrier of n
B is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set
K /. B is Element of the carrier of n
(K /. A) + (K /. B) is Element of the carrier of n
K560( the carrier of n, the addF of n,(K /. A),(K /. B)) is Element of the carrier of n
BA is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set
K . BA is set
n is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set
K is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set

{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT : ( 1 <= b1 & b1 <= K ) } is set
A is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set
A + K is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set
Seg (A + K) is finite A + K -element without_zero Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT : ( 1 <= b1 & b1 <= A + K ) } is set

{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT : ( 1 <= b1 & b1 <= A ) } is set
(Seg (A + K)) \ (Seg A) is finite without_zero Element of bool NAT
Sgm ((Seg (A + K)) \ (Seg A)) is Relation-like NAT -defined NAT -valued Function-like finite card ((Seg (A + K)) \ (Seg A)) -element FinSequence-like FinSubsequence-like V185() V186() V187() V188() Element of (card ((Seg (A + K)) \ (Seg A))) -tuples_on NAT
card ((Seg (A + K)) \ (Seg A)) is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
(card ((Seg (A + K)) \ (Seg A))) -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT

{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of NAT * : len b1 = card ((Seg (A + K)) \ (Seg A)) } is set
(Sgm ((Seg (A + K)) \ (Seg A))) . n is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set
A + n is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex set

[:(Seg K),(Seg K):] is Relation-like finite set
bool [:(Seg K),(Seg K):] is finite V37() set
dom () is finite K -element Element of bool NAT
len () is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
Seg (len ()) is finite len () -element without_zero Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT : ( 1 <= b1 & b1 <= len () ) } is set
B is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT

dom (B Shift ()) is set
{ (B + b1) where b1 is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT : b1 in dom () } is set
AB is set
x is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
x - A is V105() ext-real complex set
f is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
A + f is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
AB is set
x is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT
A + x is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of