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
{ 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
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
{ 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
Seg (len A) is finite 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 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
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
{ 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
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
{ 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)))),(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
{ 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
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
{ 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 (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
{ 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
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
{ 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
- 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
{ 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
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
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
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
{ 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
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
{ 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
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
c13 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
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
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
{ 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
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
{ 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
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
{ 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
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
{ 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
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
{ 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,(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
{ 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
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
{ 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
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
{ 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
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
{ 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
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
{ 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 | (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
{ 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
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
{ 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
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
{ 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
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
{ 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
Seg A is finite 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 <= A ) } is set
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
{ 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
Seg K is finite 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 <= 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
Seg A is finite 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 <= 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
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
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
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT : ( 1 <= b1 & b1 <= len (idseq K) ) } is set
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 + b1) where b1 is V26() V27() V28() V32() finite cardinal V105() ext-real non negative complex Element of NAT : b1 in dom (idseq K) } 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