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

bool REAL is set

RAT is set

{} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V26() V27() V28() V30() V31() V32() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V105() Function-yielding V147() ext-real non positive non negative complex V185() V186() V187() V188() set

the Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V26() V27() V28() V30() V31() V32() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V105() Function-yielding V147() ext-real non positive non negative complex V185() V186() V187() V188() set is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V26() V27() V28() V30() V31() V32() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V105() Function-yielding V147() ext-real non positive non negative complex V185() V186() V187() V188() 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

COMPLEX 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

[:COMPLEX,COMPLEX:] is Relation-like set

bool [:COMPLEX,COMPLEX:] is set

[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like set

bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is set

[:REAL,REAL:] is Relation-like set

bool [:REAL,REAL:] is set

[:[:REAL,REAL:],REAL:] is Relation-like set

bool [:[:REAL,REAL:],REAL:] is set

[:RAT,RAT:] is Relation-like set

bool [:RAT,RAT:] is set

[:[:RAT,RAT:],RAT:] is Relation-like set

bool [:[:RAT,RAT:],RAT:] is set

[:INT,INT:] is Relation-like set

bool [:INT,INT:] is set

[:[:INT,INT:],INT:] is Relation-like set

bool [:[:INT,INT:],INT:] is set

[:NAT,NAT:] is Relation-like non empty non trivial non finite V103() set

[:[:NAT,NAT:],NAT:] is Relation-like non empty non trivial non finite V103() set

bool [:[:NAT,NAT:],NAT:] 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

0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V26() V27() V28() V30() V31() V32() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V105() Function-yielding V147() ext-real non positive non negative complex V185() V186() V187() V188() Element of NAT

card {} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V26() V27() V28() V30() V31() V32() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V105() Function-yielding V147() ext-real non positive non negative complex V185() V186() V187() V188() set

Seg 1 is non empty trivial finite 1 -element without_zero V103() Element of bool NAT

{ b

{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

{ b

{1,2} is non empty finite V37() without_zero V103() set

Sgm {} is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V185() V186() V187() V188() FinSequence of NAT

n is non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital V139() V141() right-distributive left-distributive right_unital well-unital V153() left_unital Abelian add-associative right_zeroed doubleLoopStr

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

A is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V147() tabular FinSequence-yielding FinSequence of the carrier of n *

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

K * A is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V147() tabular FinSequence-yielding FinSequence of the carrier of n *

B is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V147() tabular FinSequence-yielding FinSequence of the carrier of n *

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

(K * A) * B is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V147() tabular FinSequence-yielding FinSequence of the carrier of n *

A * B is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V147() tabular FinSequence-yielding FinSequence of the carrier of n *

K * (A * B) is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V147() tabular FinSequence-yielding FinSequence of the carrier of n *

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

{ b

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

{ b

[:(dom (A * B)),(Seg (width (A * B))):] is Relation-like finite set

Seg (len A) is finite len A -element without_zero Element of bool NAT

{ b

Seg (len (A * B)) is finite len (A * B) -element without_zero Element of bool NAT

{ b

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

{ b

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

Line (A,f) is Relation-like NAT -defined the carrier of n -valued Function-like finite width A -element FinSequence-like FinSubsequence-like Element of (width A) -tuples_on the carrier of n

(width A) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n

{ b

Col (B,X) is Relation-like NAT -defined the carrier of n -valued Function-like finite len B -element FinSequence-like FinSubsequence-like Element of (len B) -tuples_on the carrier of n

(len B) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n

{ b

(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)))),(K multfield)) 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

K * (Line (A,f)) is Relation-like NAT -defined the carrier of n -valued Function-like finite width A -element FinSequence-like FinSubsequence-like Element of (width A) -tuples_on the carrier of n

K501( the carrier of n, the carrier of n,(Line (A,f)),(K multfield)) 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

{ b

(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

n is non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital V139() V141() right-distributive left-distributive right_unital well-unital V153() left_unital Abelian add-associative right_zeroed doubleLoopStr

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

B is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V147() tabular FinSequence-yielding FinSequence of the carrier of n *

(1_ n) * B is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V147() tabular FinSequence-yielding FinSequence of the carrier of n *

A * B is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V147() tabular FinSequence-yielding FinSequence of the carrier of n *

K * (A * B) is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V147() tabular FinSequence-yielding FinSequence of the carrier of n *

(K * A) * B is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V147() tabular FinSequence-yielding FinSequence 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

dom B is finite Element of bool NAT

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

Seg (width B) is finite width B -element without_zero Element of bool NAT

{ b

[:(dom B),(Seg (width B)):] 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

{ b

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

{ b

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

n is non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital V139() V141() right-distributive left-distributive right_unital well-unital V153() left_unital Abelian add-associative right_zeroed doubleLoopStr

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 Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V147() tabular FinSequence-yielding FinSequence of the carrier of n *

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

{ b

[:(dom K),(Seg (width K)):] is Relation-like finite set

- K is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V147() tabular FinSequence-yielding FinSequence of the carrier of n *

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

{ b

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

Seg (len K) is finite len K -element without_zero Element of bool NAT

{ b

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

{ b

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

K is non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital V139() V141() right-distributive left-distributive right_unital well-unital V153() left_unital Abelian add-associative right_zeroed doubleLoopStr

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

(power 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

(power K) . (A,B) is Element of the carrier of K

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

(power K) . (A,BA) is Element of the carrier of K

((power 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,((power 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

(power K) . (A,B) is Element of the carrier of K

n is non empty addLoopStr

the carrier of n is non empty set

K 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

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 A is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT

B 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 is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT

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 BA is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT

K ^ B is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

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

(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

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

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

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

{ b

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

{ b

(len K) + (len B) 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 -element FinSequence-like FinSubsequence-like Element of (len K) -tuples_on the carrier of n

x is Relation-like NAT -defined the carrier of n -valued Function-like finite len B -element FinSequence-like FinSubsequence-like Element of (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 FinSequence of the carrier of n

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

BX is Relation-like NAT -defined the carrier of n -valued Function-like finite len K -element FinSequence-like FinSubsequence-like Element of (len K) -tuples_on the carrier of n

f is Relation-like NAT -defined the carrier of n -valued Function-like finite len B -element FinSequence-like FinSubsequence-like Element of (len B) -tuples_on the carrier of n

BX ^ 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

X + BX is Relation-like NAT -defined the carrier of n -valued Function-like finite len K -element FinSequence-like FinSubsequence-like Element of (len K) -tuples_on the carrier of n

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

x + f is Relation-like NAT -defined the carrier of n -valued Function-like finite len B -element FinSequence-like FinSubsequence-like Element of (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,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

{ b

MV 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

lA 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

c

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

{ b

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

dom K is finite 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

Seg (len K) is finite len K -element without_zero Element of bool NAT

{ b

K . y is set

dom X is finite len K -element Element of bool NAT

dom BX is finite len K -element Element of bool NAT

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

dom B is finite Element of bool 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

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

dom x is finite len B -element Element of bool NAT

Seg (len B) is finite len B -element without_zero Element of bool NAT

{ b

dom f is finite len B -element Element of bool NAT

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

dom K is finite Element of bool NAT

dom B is finite Element of bool 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 + 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

K is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of 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

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

B is Element of the carrier of n

B * (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

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),(B multfield)) 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 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,(B multfield)) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

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

K501( the carrier of n, the carrier of n,A,(B multfield)) 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

{ b

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

{ b

(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

{ b

AB is Relation-like NAT -defined the carrier of n -valued Function-like finite len K -element FinSequence-like FinSubsequence-like Element of (len K) -tuples_on the carrier of n

x is Relation-like NAT -defined the carrier of n -valued Function-like finite len A -element FinSequence-like FinSubsequence-like Element of (len A) -tuples_on the carrier of n

AB ^ 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

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

B * AB is Relation-like NAT -defined the carrier of n -valued Function-like finite len K -element FinSequence-like FinSubsequence-like Element of (len K) -tuples_on the carrier of n

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

B * x is Relation-like NAT -defined the carrier of n -valued Function-like finite len A -element FinSequence-like FinSubsequence-like Element of (len A) -tuples_on the carrier of n

K501( the carrier of n, the carrier of n,x,(B multfield)) 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

{ 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

dom f is finite (len K) + (len A) -element Element of bool NAT

dom K is finite Element of bool NAT

rng K is finite set

K . BX is set

dom AB is finite len K -element Element of bool NAT

Seg (len K) is finite len K -element without_zero Element of bool NAT

{ b

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,(B multfield)) 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

dom A is finite Element of bool NAT

rng A is finite set

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

Seg (len A) is finite len A -element without_zero Element of bool NAT

{ b

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

dom x is finite len A -element Element of bool NAT

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,(B multfield)) 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

dom K is finite Element of bool NAT

dom A is finite Element of bool NAT

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,(B multfield)) 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,(B multfield)) 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

n is Relation-like Function-like set

dom n is set

K is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng K is finite set

A is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng A is finite set

B is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

K (#) n is Relation-like NAT -defined Function-like finite set

BA is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

A (#) n is Relation-like NAT -defined Function-like finite set

K ^ A is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

(K ^ A) (#) n is Relation-like NAT -defined Function-like finite set

B ^ BA is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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

{ b

rng (K ^ A) is finite set

(rng K) \/ (rng A) is finite set

dom ((K ^ A) (#) n) is finite set

dom B is finite Element of bool NAT

dom K is finite Element of bool NAT

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

dom A 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

n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V185() V186() V187() V188() FinSequence of NAT

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

dom n is finite Element of bool NAT

Sgm (rng n) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V185() V186() V187() V188() FinSequence of NAT

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

Seg K is finite K -element without_zero Element of bool NAT

{ b

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

A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V185() V186() V187() V188() FinSequence 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

dom A is finite Element of bool NAT

Sgm (rng A) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V185() V186() V187() V188() FinSequence of NAT

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

Seg B is finite B -element without_zero Element of bool NAT

{ b

A | n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V185() V186() V187() V188() FinSequence of NAT

Seg n is finite n -element without_zero Element of bool NAT

{ b

A | (Seg n) is Relation-like NAT -defined Seg n -defined NAT -defined NAT -valued RAT -valued Function-like finite FinSubsequence-like V185() V186() V187() V188() set

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

<*(A . (n + 1))*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like 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

(A | n) ^ <*(A . (n + 1))*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like 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

{ b

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

Sgm (rng (A | n)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V185() V186() V187() V188() FinSequence of NAT

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

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

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

(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

n 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

dom n is finite Element of bool NAT

Sgm (rng n) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V185() V186() V187() V188() FinSequence of NAT

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

Seg K is finite K -element without_zero Element of bool NAT

{ b

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

A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V185() V186() V187() V188() FinSequence 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

Seg B is finite B -element without_zero Element of bool NAT

{ b

dom A is finite Element of bool NAT

Sgm (rng A) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V185() V186() V187() V188() FinSequence of NAT

n is non empty right_complementable V95() Abelian add-associative right_zeroed addLoopStr

the carrier of n is non empty set

0. n is zero Element of 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

dom K is finite Element of bool NAT

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

Seg (len K) is finite len K -element without_zero Element of bool NAT

{ b

Seg A is finite A -element without_zero Element of bool NAT

{ b

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

K | (Seg A) is Relation-like NAT -defined Seg A -defined NAT -defined the carrier of n -valued Function-like finite FinSubsequence-like set

AB is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

(K | A) ^ AB is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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

x is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

dom x 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

Seg (len x) is finite len x -element without_zero Element of bool NAT

{ b

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

Seg K is finite K -element without_zero Element of bool NAT

{ b

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

{ b

Seg A is finite A -element without_zero Element of bool NAT

{ b

(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

NAT * is functional non empty FinSequence-membered FinSequenceSet of NAT

{ b

(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

idseq K is Relation-like NAT -defined Function-like finite K -element FinSequence-like FinSubsequence-like set

id (Seg K) is Relation-like Seg K -defined Seg K -valued Function-like one-to-one total quasi_total finite Element of bool [:(Seg K),(Seg K):]

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

bool [:(Seg K),(Seg K):] is finite V37() set

dom (idseq K) is finite K -element Element of bool NAT

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

Seg (len (idseq K)) is finite len (idseq K) -element without_zero Element of bool NAT

{ b

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

B Shift (idseq K) is Relation-like NAT -defined Function-like FinSubsequence-like set

dom (B Shift (idseq K)) is set

{ (B + b

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