REAL is non empty non trivial non finite complex-membered ext-real-membered real-membered V71() set
NAT is V8() non empty non trivial non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V71() Element of bool REAL
bool REAL is non empty non trivial non finite set
RAT is non empty non trivial non finite complex-membered ext-real-membered real-membered rational-membered V71() set
{} is Relation-like non-empty empty-yielding RAT -valued V8() V12() functional empty trivial ext-real non positive non negative complex V40() integer finite finite-yielding V48() cardinal {} -element FinSequence-like FinSequence-membered V55() V56() V57() V58() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V71() set
COMPLEX is non empty non trivial non finite complex-membered V71() set
INT is non empty non trivial non finite complex-membered ext-real-membered real-membered rational-membered integer-membered V71() set
[:COMPLEX,COMPLEX:] is Relation-like non empty non trivial non finite V55() set
bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like non empty non trivial non finite V55() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite set
[:REAL,REAL:] is Relation-like non empty non trivial non finite V55() V56() V57() set
bool [:REAL,REAL:] is non empty non trivial non finite set
[:[:REAL,REAL:],REAL:] is Relation-like non empty non trivial non finite V55() V56() V57() set
bool [:[:REAL,REAL:],REAL:] is non empty non trivial non finite set
[:RAT,RAT:] is Relation-like RAT -valued non empty non trivial non finite V55() V56() V57() set
bool [:RAT,RAT:] is non empty non trivial non finite set
[:[:RAT,RAT:],RAT:] is Relation-like RAT -valued non empty non trivial non finite V55() V56() V57() set
bool [:[:RAT,RAT:],RAT:] is non empty non trivial non finite set
[:INT,INT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V55() V56() V57() set
bool [:INT,INT:] is non empty non trivial non finite set
[:[:INT,INT:],INT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V55() V56() V57() set
bool [:[:INT,INT:],INT:] is non empty non trivial non finite set
[:NAT,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V55() V56() V57() V58() set
[:[:NAT,NAT:],NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V55() V56() V57() V58() set
bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite set
NAT is V8() non empty non trivial non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V71() set
bool NAT is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
K107(NAT) is V34() set
1 is V8() V12() non empty ext-real positive non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
2 is V8() V12() non empty ext-real positive non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
3 is V8() V12() non empty ext-real positive non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
0 is Relation-like non-empty empty-yielding RAT -valued V8() V12() functional empty trivial ext-real non positive non negative complex V40() integer V43() finite finite-yielding V48() cardinal {} -element FinSequence-like FinSequence-membered V55() V56() V57() V58() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V71() Element of NAT
<*> INT is Relation-like non-empty empty-yielding NAT -defined INT -valued V8() V12() Function-like one-to-one functional empty trivial proper ext-real non positive non negative complex V40() integer finite finite-yielding V48() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V55() V56() V57() V58() V59() V60() V61() V62() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V71() FinSequence of INT
[:NAT,INT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V55() V56() V57() set
@ 1 is ext-real complex V40() integer V43() Element of INT
{{}} is non empty trivial finite V48() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
addcomplex is Relation-like Function-like V25([:COMPLEX,COMPLEX:], COMPLEX ) commutative associative having_a_unity V55() Element of bool [:[:COMPLEX,COMPLEX:],COMPLEX:]
addreal is Relation-like Function-like V25([:REAL,REAL:], REAL ) commutative associative having_a_unity V55() V56() V57() Element of bool [:[:REAL,REAL:],REAL:]
addint is Relation-like INT -valued Function-like V25([:INT,INT:], INT ) commutative associative having_a_unity V55() V56() V57() Element of bool [:[:INT,INT:],INT:]
the_unity_wrt addcomplex is complex Element of COMPLEX
the_unity_wrt addint is ext-real complex V40() integer V43() Element of INT
n is V8() V12() non empty ext-real positive non negative complex V40() integer finite cardinal set
Segm n is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
n is set
a is V8() V12() ext-real non negative complex V40() integer finite cardinal set
Segm a is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
n is Relation-like INT -valued Function-like V25([:INT,INT:], INT ) V55() V56() V57() Element of bool [:[:INT,INT:],INT:]
a is ext-real complex V40() integer V43() Element of INT
b is ext-real complex V40() integer V43() Element of INT
n . (a,b) is ext-real complex V40() integer V43() Element of INT
[a,b] is non empty set
{a,b} is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{a} is non empty trivial finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered set
{{a,b},{a}} is non empty finite V48() set
n . [a,b] is ext-real complex V40() integer set
a + b is ext-real complex V40() integer V43() Element of INT
addreal . (a,b) is set
addreal . [a,b] is ext-real complex V40() set
a is ext-real complex V40() integer V43() Element of INT
b is ext-real complex V40() integer V43() Element of INT
n . (a,b) is ext-real complex V40() integer V43() Element of INT
[a,b] is non empty set
{a,b} is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{a} is non empty trivial finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered set
{{a,b},{a}} is non empty finite V48() set
n . [a,b] is ext-real complex V40() integer set
addreal . (a,b) is set
addreal . [a,b] is ext-real complex V40() set
a + b is ext-real complex V40() integer V43() Element of INT
addint . (a,b) is ext-real complex V40() integer V43() Element of INT
addint . [a,b] is ext-real complex V40() integer set
n is ext-real complex V40() integer V43() Element of INT
n is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V55() V56() V57() FinSequence of INT
Sum n is complex set
addint $$ n is ext-real complex V40() integer V43() Element of INT
[#] (n,(the_unity_wrt addint)) is Relation-like INT -valued Function-like V25( NAT , INT ) V55() V56() V57() Element of bool [:NAT,INT:]
bool [:NAT,INT:] is non empty non trivial non finite set
K504(INT,NAT,(the_unity_wrt addint)) is Relation-like RAT -valued INT -valued V10() Function-like V25( NAT , INT ) V55() V56() V57() Element of bool [:NAT,INT:]
K276(INT,K504(INT,NAT,(the_unity_wrt addint)),n) is Relation-like INT -valued Function-like V25( NAT , INT ) V55() V56() V57() Element of bool [:NAT,INT:]
rng n is finite complex-membered ext-real-membered real-membered rational-membered integer-membered Element of bool REAL
j2 is Relation-like NAT -defined COMPLEX -valued Function-like finite FinSequence-like FinSubsequence-like V55() FinSequence of COMPLEX
[#] (j2,(the_unity_wrt addcomplex)) is Relation-like Function-like V25( NAT , COMPLEX ) V55() Element of bool [:NAT,COMPLEX:]
[:NAT,COMPLEX:] is Relation-like non empty non trivial non finite V55() set
bool [:NAT,COMPLEX:] is non empty non trivial non finite set
K504(COMPLEX,NAT,(the_unity_wrt addcomplex)) is Relation-like V10() Function-like V25( NAT , COMPLEX ) V55() Element of bool [:NAT,COMPLEX:]
K276(COMPLEX,K504(COMPLEX,NAT,(the_unity_wrt addcomplex)),j2) is Relation-like Function-like V25( NAT , COMPLEX ) V55() Element of bool [:NAT,COMPLEX:]
dom j2 is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
c7 is V8() V12() ext-real non negative complex V40() integer finite cardinal set
Seg c7 is finite c7 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
{ b1 where b1 is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( 1 <= b1 & b1 <= c7 ) } is set
finSeg c7 is finite c7 -element Element of K107(NAT)
addint $$ ((finSeg c7),([#] (n,(the_unity_wrt addint)))) is ext-real complex V40() integer V43() Element of INT
addcomplex $$ j2 is complex Element of COMPLEX
addcomplex $$ ((finSeg c7),([#] (j2,(the_unity_wrt addcomplex)))) is complex Element of COMPLEX
b is V8() V12() ext-real non negative complex V40() integer finite cardinal set
finSeg b is finite b -element Element of K107(NAT)
{ b1 where b1 is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( 1 <= b1 & b1 <= b ) } is set
addint $$ ((finSeg b),([#] (n,(the_unity_wrt addint)))) is ext-real complex V40() integer V43() Element of INT
addcomplex $$ ((finSeg b),([#] (j2,(the_unity_wrt addcomplex)))) is complex Element of COMPLEX
b + 1 is V8() V12() non empty ext-real positive non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
finSeg (b + 1) is non empty finite b + 1 -element Element of K107(NAT)
{ b1 where b1 is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( 1 <= b1 & b1 <= b + 1 ) } is set
addint $$ ((finSeg (b + 1)),([#] (n,(the_unity_wrt addint)))) is ext-real complex V40() integer V43() Element of INT
addcomplex $$ ((finSeg (b + 1)),([#] (j2,(the_unity_wrt addcomplex)))) is complex Element of COMPLEX
([#] (n,(the_unity_wrt addint))) . (b + 1) is ext-real complex V40() integer V43() Element of INT
Seg b is finite b -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
{.(b + 1).} is non empty trivial finite V48() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K107(NAT)
(finSeg b) \/ {.(b + 1).} is non empty finite Element of K107(NAT)
addint $$ (((finSeg b) \/ {.(b + 1).}),([#] (n,(the_unity_wrt addint)))) is ext-real complex V40() integer V43() Element of INT
addint . ((addint $$ ((finSeg b),([#] (n,(the_unity_wrt addint))))),(([#] (n,(the_unity_wrt addint))) . (b + 1))) is ext-real complex V40() integer V43() Element of INT
[(addint $$ ((finSeg b),([#] (n,(the_unity_wrt addint))))),(([#] (n,(the_unity_wrt addint))) . (b + 1))] is non empty set
{(addint $$ ((finSeg b),([#] (n,(the_unity_wrt addint))))),(([#] (n,(the_unity_wrt addint))) . (b + 1))} is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{(addint $$ ((finSeg b),([#] (n,(the_unity_wrt addint)))))} is non empty trivial finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered set
{{(addint $$ ((finSeg b),([#] (n,(the_unity_wrt addint))))),(([#] (n,(the_unity_wrt addint))) . (b + 1))},{(addint $$ ((finSeg b),([#] (n,(the_unity_wrt addint)))))}} is non empty finite V48() set
addint . [(addint $$ ((finSeg b),([#] (n,(the_unity_wrt addint))))),(([#] (n,(the_unity_wrt addint))) . (b + 1))] is ext-real complex V40() integer set
(addint $$ ((finSeg b),([#] (n,(the_unity_wrt addint))))) + (([#] (n,(the_unity_wrt addint))) . (b + 1)) is ext-real complex V40() integer V43() Element of INT
([#] (j2,(the_unity_wrt addcomplex))) . (b + 1) is complex Element of COMPLEX
addcomplex . ((addcomplex $$ ((finSeg b),([#] (j2,(the_unity_wrt addcomplex))))),(([#] (j2,(the_unity_wrt addcomplex))) . (b + 1))) is complex Element of COMPLEX
[(addcomplex $$ ((finSeg b),([#] (j2,(the_unity_wrt addcomplex))))),(([#] (j2,(the_unity_wrt addcomplex))) . (b + 1))] is non empty set
{(addcomplex $$ ((finSeg b),([#] (j2,(the_unity_wrt addcomplex))))),(([#] (j2,(the_unity_wrt addcomplex))) . (b + 1))} is non empty finite complex-membered set
{(addcomplex $$ ((finSeg b),([#] (j2,(the_unity_wrt addcomplex)))))} is non empty trivial finite 1 -element complex-membered set
{{(addcomplex $$ ((finSeg b),([#] (j2,(the_unity_wrt addcomplex))))),(([#] (j2,(the_unity_wrt addcomplex))) . (b + 1))},{(addcomplex $$ ((finSeg b),([#] (j2,(the_unity_wrt addcomplex)))))}} is non empty finite V48() set
addcomplex . [(addcomplex $$ ((finSeg b),([#] (j2,(the_unity_wrt addcomplex))))),(([#] (j2,(the_unity_wrt addcomplex))) . (b + 1))] is complex set
addcomplex $$ (((finSeg b) \/ {.(b + 1).}),([#] (j2,(the_unity_wrt addcomplex)))) is complex Element of COMPLEX
Seg 0 is Relation-like non-empty empty-yielding RAT -valued V8() V12() functional empty trivial proper ext-real non positive non negative complex V40() integer finite finite-yielding V48() cardinal 0 -element {} -element FinSequence-like FinSequence-membered V55() V56() V57() V58() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V71() Element of bool NAT
{ b1 where b1 is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( 1 <= b1 & b1 <= 0 ) } is set
{}. NAT is Relation-like non-empty empty-yielding RAT -valued V8() V12() functional empty trivial ext-real non positive non negative complex V40() integer finite finite-yielding V48() cardinal {} -element FinSequence-like FinSequence-membered V55() V56() V57() V58() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V71() Element of K107(NAT)
finSeg 0 is Relation-like non-empty empty-yielding RAT -valued V8() V12() functional empty trivial ext-real non positive non negative complex V40() integer finite finite-yielding V48() cardinal 0 -element {} -element FinSequence-like FinSequence-membered V55() V56() V57() V58() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V71() Element of K107(NAT)
addint $$ ((finSeg 0),([#] (n,(the_unity_wrt addint)))) is ext-real complex V40() integer V43() Element of INT
addcomplex $$ ((finSeg 0),([#] (j2,(the_unity_wrt addcomplex)))) is complex Element of COMPLEX
n is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V55() V56() V57() FinSequence of INT
Sum n is complex set
addint $$ n is ext-real complex V40() integer V43() Element of INT
addint $$ n is ext-real complex V40() integer V43() Element of INT
a is ext-real complex V40() integer V43() Element of INT
b is ext-real complex V40() integer V43() Element of INT
((<*> INT)) is ext-real complex V40() integer V43() Element of INT
addint $$ (<*> INT) is ext-real complex V40() integer V43() Element of INT
len (<*> INT) is Relation-like non-empty empty-yielding RAT -valued V8() V12() functional empty trivial ext-real non positive non negative complex V40() integer V43() finite finite-yielding V48() cardinal {} -element FinSequence-like FinSequence-membered V55() V56() V57() V58() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V71() Element of NAT
n is non empty unital Group-like associative multMagma
the carrier of n is non empty set
a is Element of the carrier of n
(len (<*> INT)) |-> a is Relation-like NAT -defined the carrier of n -valued Function-like finite len (<*> INT) -element FinSequence-like FinSubsequence-like Element of (len (<*> INT)) -tuples_on the carrier of n
(len (<*> INT)) -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 (<*> INT) } is set
Seg (len (<*> INT)) is Relation-like non-empty empty-yielding RAT -valued V8() V12() functional empty trivial proper ext-real non positive non negative complex V40() integer finite finite-yielding V48() cardinal len (<*> INT) -element {} -element FinSequence-like FinSequence-membered V55() V56() V57() V58() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V71() Element of bool NAT
{ b1 where b1 is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( 1 <= b1 & b1 <= len (<*> INT) ) } is set
K503((Seg (len (<*> INT))),a) is Relation-like non-empty empty-yielding NAT -defined RAT -valued V8() V10() V12() Function-like one-to-one functional empty trivial non proper V25( Seg (len (<*> INT)),{a}) ext-real non positive non negative complex V40() integer finite finite-yielding V48() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V55() V56() V57() V58() V59() V60() V61() V62() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V71() Element of bool [:(Seg (len (<*> INT))),{a}:]
{a} is non empty trivial finite 1 -element set
[:(Seg (len (<*> INT))),{a}:] is Relation-like non-empty empty-yielding RAT -valued V8() V12() functional empty trivial ext-real non positive non negative complex V40() integer finite finite-yielding V48() cardinal {} -element FinSequence-like FinSequence-membered V55() V56() V57() V58() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V71() set
bool [:(Seg (len (<*> INT))),{a}:] is non empty finite V48() set
((len (<*> INT)) |-> a) |^ (<*> INT) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Product (((len (<*> INT)) |-> a) |^ (<*> INT)) is Element of the carrier of n
the multF of n is Relation-like Function-like V25([: the carrier of n, the carrier of n:], the carrier of n) associative having_a_unity 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 non empty set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like non empty set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty set
the multF of n $$ (((len (<*> INT)) |-> a) |^ (<*> INT)) is Element of the carrier of n
a |^ ((<*> INT)) is Element of the carrier of n
<*> the carrier of n is Relation-like non-empty empty-yielding NAT -defined the carrier of n -valued V8() V12() Function-like one-to-one functional empty trivial proper ext-real non positive non negative complex V40() integer finite finite-yielding V48() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V55() V56() V57() V58() V59() V60() V61() V62() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V71() FinSequence of the carrier of n
[:NAT, the carrier of n:] is Relation-like non empty non trivial non finite set
(<*> the carrier of n) |^ (<*> INT) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
1_ n is non being_of_order_0 Element of the carrier of n
n is non empty unital Group-like associative multMagma
the carrier of n is non empty set
a is Element of the carrier of n
b is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V55() V56() V57() FinSequence of INT
len b is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(len b) |-> a 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
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
Seg (len b) is finite len b -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
{ b1 where b1 is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( 1 <= b1 & b1 <= len b ) } is set
K503((Seg (len b)),a) is Relation-like NAT -defined Function-like V25( Seg (len b),{a}) finite FinSequence-like FinSubsequence-like Element of bool [:(Seg (len b)),{a}:]
{a} is non empty trivial finite 1 -element set
[:(Seg (len b)),{a}:] is Relation-like finite set
bool [:(Seg (len b)),{a}:] is non empty finite V48() set
((len b) |-> a) |^ b is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Product (((len b) |-> a) |^ b) is Element of the carrier of n
the multF of n is Relation-like Function-like V25([: the carrier of n, the carrier of n:], the carrier of n) associative having_a_unity 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 non empty set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like non empty set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty set
the multF of n $$ (((len b) |-> a) |^ b) is Element of the carrier of n
(b) is ext-real complex V40() integer V43() Element of INT
addint $$ b is ext-real complex V40() integer V43() Element of INT
a |^ (b) is Element of the carrier of n
e is ext-real complex V40() integer V43() Element of INT
<*e*> is Relation-like NAT -defined INT -valued Function-like one-to-one non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V55() V56() V57() V59() V60() V61() V62() FinSequence of INT
[1,e] is non empty set
{1,e} is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{1} is non empty trivial finite V48() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{1,e},{1}} is non empty finite V48() set
{[1,e]} is Relation-like non empty trivial finite 1 -element set
b ^ <*e*> is Relation-like NAT -defined INT -valued Function-like non empty finite FinSequence-like FinSubsequence-like V55() V56() V57() FinSequence of INT
len (b ^ <*e*>) is V8() V12() non empty ext-real positive non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(len (b ^ <*e*>)) |-> a is Relation-like NAT -defined the carrier of n -valued Function-like finite len (b ^ <*e*>) -element FinSequence-like FinSubsequence-like Element of (len (b ^ <*e*>)) -tuples_on the carrier of n
(len (b ^ <*e*>)) -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 ^ <*e*>) } is set
Seg (len (b ^ <*e*>)) is non empty finite len (b ^ <*e*>) -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
{ b1 where b1 is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( 1 <= b1 & b1 <= len (b ^ <*e*>) ) } is set
K503((Seg (len (b ^ <*e*>))),a) is Relation-like NAT -defined Function-like V25( Seg (len (b ^ <*e*>)),{a}) finite FinSequence-like FinSubsequence-like Element of bool [:(Seg (len (b ^ <*e*>))),{a}:]
[:(Seg (len (b ^ <*e*>))),{a}:] is Relation-like non empty finite set
bool [:(Seg (len (b ^ <*e*>))),{a}:] is non empty finite V48() set
((len (b ^ <*e*>)) |-> a) |^ (b ^ <*e*>) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Product (((len (b ^ <*e*>)) |-> a) |^ (b ^ <*e*>)) is Element of the carrier of n
the multF of n $$ (((len (b ^ <*e*>)) |-> a) |^ (b ^ <*e*>)) is Element of the carrier of n
((b ^ <*e*>)) is ext-real complex V40() integer V43() Element of INT
addint $$ (b ^ <*e*>) is ext-real complex V40() integer V43() Element of INT
a |^ ((b ^ <*e*>)) is Element of the carrier of n
len ((len b) |-> a) is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
<*a*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of n
[1,a] is non empty set
{1,a} is non empty finite set
{{1,a},{1}} is non empty finite V48() set
{[1,a]} is Relation-like non empty trivial finite 1 -element set
len <*a*> is V8() V12() non empty ext-real positive non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
len <*e*> is V8() V12() non empty ext-real positive non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(len b) + 1 is V8() V12() non empty ext-real positive non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
((len b) + 1) |-> a is Relation-like NAT -defined the carrier of n -valued Function-like finite (len b) + 1 -element FinSequence-like FinSubsequence-like Element of ((len b) + 1) -tuples_on the carrier of n
((len b) + 1) -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) + 1 } is set
Seg ((len b) + 1) is non empty finite (len b) + 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
{ b1 where b1 is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( 1 <= b1 & b1 <= (len b) + 1 ) } is set
K503((Seg ((len b) + 1)),a) is Relation-like NAT -defined Function-like V25( Seg ((len b) + 1),{a}) finite FinSequence-like FinSubsequence-like Element of bool [:(Seg ((len b) + 1)),{a}:]
[:(Seg ((len b) + 1)),{a}:] is Relation-like non empty finite set
bool [:(Seg ((len b) + 1)),{a}:] is non empty finite V48() set
(((len b) + 1) |-> a) |^ (b ^ <*e*>) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Product ((((len b) + 1) |-> a) |^ (b ^ <*e*>)) is Element of the carrier of n
the multF of n $$ ((((len b) + 1) |-> a) |^ (b ^ <*e*>)) is Element of the carrier of n
((len b) |-> a) ^ <*a*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty finite (len b) + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(len b) + 1 is V8() V12() non empty ext-real positive non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(((len b) |-> a) ^ <*a*>) |^ (b ^ <*e*>) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Product ((((len b) |-> a) ^ <*a*>) |^ (b ^ <*e*>)) is Element of the carrier of n
the multF of n $$ ((((len b) |-> a) ^ <*a*>) |^ (b ^ <*e*>)) is Element of the carrier of n
<*a*> |^ <*e*> 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) |-> a) |^ b) ^ (<*a*> |^ <*e*>) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Product ((((len b) |-> a) |^ b) ^ (<*a*> |^ <*e*>)) is Element of the carrier of n
the multF of n $$ ((((len b) |-> a) |^ b) ^ (<*a*> |^ <*e*>)) is Element of the carrier of n
@ e is ext-real complex V40() integer V43() Element of INT
@ (@ e) is ext-real complex V40() integer V43() Element of INT
<*(@ (@ e))*> is Relation-like NAT -defined INT -valued Function-like one-to-one non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V55() V56() V57() V59() V60() V61() V62() FinSequence of INT
[1,(@ (@ e))] is non empty set
{1,(@ (@ e))} is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{{1,(@ (@ e))},{1}} is non empty finite V48() set
{[1,(@ (@ e))]} is Relation-like non empty trivial finite 1 -element set
<*a*> |^ <*(@ (@ e))*> is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Product (<*a*> |^ <*(@ (@ e))*>) is Element of the carrier of n
the multF of n $$ (<*a*> |^ <*(@ (@ e))*>) is Element of the carrier of n
(Product (((len b) |-> a) |^ b)) * (Product (<*a*> |^ <*(@ (@ e))*>)) is Element of the carrier of n
the multF of n . ((Product (((len b) |-> a) |^ b)),(Product (<*a*> |^ <*(@ (@ e))*>))) is Element of the carrier of n
[(Product (((len b) |-> a) |^ b)),(Product (<*a*> |^ <*(@ (@ e))*>))] is non empty set
{(Product (((len b) |-> a) |^ b)),(Product (<*a*> |^ <*(@ (@ e))*>))} is non empty finite set
{(Product (((len b) |-> a) |^ b))} is non empty trivial finite 1 -element set
{{(Product (((len b) |-> a) |^ b)),(Product (<*a*> |^ <*(@ (@ e))*>))},{(Product (((len b) |-> a) |^ b))}} is non empty finite V48() set
the multF of n . [(Product (((len b) |-> a) |^ b)),(Product (<*a*> |^ <*(@ (@ e))*>))] is set
a |^ (@ e) is Element of the carrier of n
<*(a |^ (@ e))*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of n
[1,(a |^ (@ e))] is non empty set
{1,(a |^ (@ e))} is non empty finite set
{{1,(a |^ (@ e))},{1}} is non empty finite V48() set
{[1,(a |^ (@ e))]} is Relation-like non empty trivial finite 1 -element set
Product <*(a |^ (@ e))*> is Element of the carrier of n
the multF of n $$ <*(a |^ (@ e))*> is Element of the carrier of n
(Product (((len b) |-> a) |^ b)) * (Product <*(a |^ (@ e))*>) is Element of the carrier of n
the multF of n . ((Product (((len b) |-> a) |^ b)),(Product <*(a |^ (@ e))*>)) is Element of the carrier of n
[(Product (((len b) |-> a) |^ b)),(Product <*(a |^ (@ e))*>)] is non empty set
{(Product (((len b) |-> a) |^ b)),(Product <*(a |^ (@ e))*>)} is non empty finite set
{{(Product (((len b) |-> a) |^ b)),(Product <*(a |^ (@ e))*>)},{(Product (((len b) |-> a) |^ b))}} is non empty finite V48() set
the multF of n . [(Product (((len b) |-> a) |^ b)),(Product <*(a |^ (@ e))*>)] is set
(a |^ (b)) * (a |^ (@ e)) is Element of the carrier of n
the multF of n . ((a |^ (b)),(a |^ (@ e))) is Element of the carrier of n
[(a |^ (b)),(a |^ (@ e))] is non empty set
{(a |^ (b)),(a |^ (@ e))} is non empty finite set
{(a |^ (b))} is non empty trivial finite 1 -element set
{{(a |^ (b)),(a |^ (@ e))},{(a |^ (b))}} is non empty finite V48() set
the multF of n . [(a |^ (b)),(a |^ (@ e))] is set
(b) + (@ e) is ext-real complex V40() integer V43() Element of INT
a |^ ((b) + (@ e)) is Element of the carrier of n
n is non empty unital Group-like associative multMagma
the carrier of n is non empty set
a is Element of the carrier of n
b is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V55() V56() V57() FinSequence of INT
len b is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(len b) |-> a 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
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
Seg (len b) is finite len b -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
{ b1 where b1 is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( 1 <= b1 & b1 <= len b ) } is set
K503((Seg (len b)),a) is Relation-like NAT -defined Function-like V25( Seg (len b),{a}) finite FinSequence-like FinSubsequence-like Element of bool [:(Seg (len b)),{a}:]
{a} is non empty trivial finite 1 -element set
[:(Seg (len b)),{a}:] is Relation-like finite set
bool [:(Seg (len b)),{a}:] is non empty finite V48() set
((len b) |-> a) |^ b is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Product (((len b) |-> a) |^ b) is Element of the carrier of n
the multF of n is Relation-like Function-like V25([: the carrier of n, the carrier of n:], the carrier of n) associative having_a_unity 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 non empty set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like non empty set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty set
the multF of n $$ (((len b) |-> a) |^ b) is Element of the carrier of n
(b) is ext-real complex V40() integer V43() Element of INT
addint $$ b is ext-real complex V40() integer V43() Element of INT
a |^ (b) is Element of the carrier of n
e is ext-real complex V40() integer V43() Element of INT
<*e*> is Relation-like NAT -defined INT -valued Function-like one-to-one non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V55() V56() V57() V59() V60() V61() V62() FinSequence of INT
[1,e] is non empty set
{1,e} is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{1} is non empty trivial finite V48() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{1,e},{1}} is non empty finite V48() set
{[1,e]} is Relation-like non empty trivial finite 1 -element set
b ^ <*e*> is Relation-like NAT -defined INT -valued Function-like non empty finite FinSequence-like FinSubsequence-like V55() V56() V57() FinSequence of INT
len (b ^ <*e*>) is V8() V12() non empty ext-real positive non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(len (b ^ <*e*>)) |-> a is Relation-like NAT -defined the carrier of n -valued Function-like finite len (b ^ <*e*>) -element FinSequence-like FinSubsequence-like Element of (len (b ^ <*e*>)) -tuples_on the carrier of n
(len (b ^ <*e*>)) -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 ^ <*e*>) } is set
Seg (len (b ^ <*e*>)) is non empty finite len (b ^ <*e*>) -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
{ b1 where b1 is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( 1 <= b1 & b1 <= len (b ^ <*e*>) ) } is set
K503((Seg (len (b ^ <*e*>))),a) is Relation-like NAT -defined Function-like V25( Seg (len (b ^ <*e*>)),{a}) finite FinSequence-like FinSubsequence-like Element of bool [:(Seg (len (b ^ <*e*>))),{a}:]
[:(Seg (len (b ^ <*e*>))),{a}:] is Relation-like non empty finite set
bool [:(Seg (len (b ^ <*e*>))),{a}:] is non empty finite V48() set
((len (b ^ <*e*>)) |-> a) |^ (b ^ <*e*>) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Product (((len (b ^ <*e*>)) |-> a) |^ (b ^ <*e*>)) is Element of the carrier of n
the multF of n $$ (((len (b ^ <*e*>)) |-> a) |^ (b ^ <*e*>)) is Element of the carrier of n
((b ^ <*e*>)) is ext-real complex V40() integer V43() Element of INT
addint $$ (b ^ <*e*>) is ext-real complex V40() integer V43() Element of INT
a |^ ((b ^ <*e*>)) is Element of the carrier of n
(len (<*> INT)) |-> a is Relation-like NAT -defined the carrier of n -valued Function-like finite len (<*> INT) -element FinSequence-like FinSubsequence-like Element of (len (<*> INT)) -tuples_on the carrier of n
(len (<*> INT)) -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 (<*> INT) } is set
Seg (len (<*> INT)) is Relation-like non-empty empty-yielding RAT -valued V8() V12() functional empty trivial proper ext-real non positive non negative complex V40() integer finite finite-yielding V48() cardinal len (<*> INT) -element {} -element FinSequence-like FinSequence-membered V55() V56() V57() V58() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V71() Element of bool NAT
{ b1 where b1 is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( 1 <= b1 & b1 <= len (<*> INT) ) } is set
K503((Seg (len (<*> INT))),a) is Relation-like non-empty empty-yielding NAT -defined RAT -valued V8() V10() V12() Function-like one-to-one functional empty trivial non proper V25( Seg (len (<*> INT)),{a}) ext-real non positive non negative complex V40() integer finite finite-yielding V48() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V55() V56() V57() V58() V59() V60() V61() V62() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V71() Element of bool [:(Seg (len (<*> INT))),{a}:]
{a} is non empty trivial finite 1 -element set
[:(Seg (len (<*> INT))),{a}:] is Relation-like non-empty empty-yielding RAT -valued V8() V12() functional empty trivial ext-real non positive non negative complex V40() integer finite finite-yielding V48() cardinal {} -element FinSequence-like FinSequence-membered V55() V56() V57() V58() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V71() set
bool [:(Seg (len (<*> INT))),{a}:] is non empty finite V48() set
((len (<*> INT)) |-> a) |^ (<*> INT) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Product (((len (<*> INT)) |-> a) |^ (<*> INT)) is Element of the carrier of n
the multF of n is Relation-like Function-like V25([: the carrier of n, the carrier of n:], the carrier of n) associative having_a_unity 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 non empty set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like non empty set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty set
the multF of n $$ (((len (<*> INT)) |-> a) |^ (<*> INT)) is Element of the carrier of n
a |^ ((<*> INT)) is Element of the carrier of n
b is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V55() V56() V57() FinSequence of INT
len b is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(len b) |-> a 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
Seg (len b) is finite len b -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
{ b1 where b1 is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( 1 <= b1 & b1 <= len b ) } is set
K503((Seg (len b)),a) is Relation-like NAT -defined Function-like V25( Seg (len b),{a}) finite FinSequence-like FinSubsequence-like Element of bool [:(Seg (len b)),{a}:]
[:(Seg (len b)),{a}:] is Relation-like finite set
bool [:(Seg (len b)),{a}:] is non empty finite V48() set
((len b) |-> a) |^ b is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Product (((len b) |-> a) |^ b) is Element of the carrier of n
the multF of n $$ (((len b) |-> a) |^ b) is Element of the carrier of n
(b) is ext-real complex V40() integer V43() Element of INT
addint $$ b is ext-real complex V40() integer V43() Element of INT
a |^ (b) is Element of the carrier of n
n is non empty unital Group-like associative multMagma
the carrier of n is non empty set
a is Element of the carrier of n
b is Element of the carrier of n
{b} is non empty trivial finite 1 -element Element of bool the carrier of n
bool the carrier of n is non empty set
gr {b} is non empty strict unital Group-like associative Subgroup of n
e is ext-real complex V40() integer set
b |^ e is Element of the carrier of n
j2 is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
- j2 is ext-real non positive complex V40() integer V43() Element of INT
j2 -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 = j2 } is set
j2 |-> b is Relation-like NAT -defined the carrier of n -valued Function-like finite j2 -element FinSequence-like FinSubsequence-like Element of j2 -tuples_on the carrier of n
Seg j2 is finite j2 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
{ b1 where b1 is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( 1 <= b1 & b1 <= j2 ) } is set
K503((Seg j2),b) is Relation-like NAT -defined Function-like V25( Seg j2,{b}) finite FinSequence-like FinSubsequence-like Element of bool [:(Seg j2),{b}:]
{b} is non empty trivial finite 1 -element set
[:(Seg j2),{b}:] is Relation-like finite set
bool [:(Seg j2),{b}:] is non empty finite V48() set
j3 is Relation-like NAT -defined the carrier of n -valued Function-like finite j2 -element FinSequence-like FinSubsequence-like Element of j2 -tuples_on the carrier of n
len j3 is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
rng j3 is finite set
j2 |-> (@ 1) is Relation-like NAT -defined INT -valued Function-like finite j2 -element FinSequence-like FinSubsequence-like V55() V56() V57() Element of j2 -tuples_on INT
j2 -tuples_on INT is functional non empty FinSequence-membered FinSequenceSet of INT
INT * is functional non empty FinSequence-membered FinSequenceSet of INT
{ b1 where b1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like Element of INT * : len b1 = j2 } is set
K503((Seg j2),(@ 1)) is Relation-like NAT -defined RAT -valued INT -valued Function-like V25( Seg j2,{(@ 1)}) finite FinSequence-like FinSubsequence-like V55() V56() V57() Element of bool [:(Seg j2),{(@ 1)}:]
{(@ 1)} is non empty trivial finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered set
[:(Seg j2),{(@ 1)}:] is Relation-like RAT -valued INT -valued finite V55() V56() V57() set
bool [:(Seg j2),{(@ 1)}:] is non empty finite V48() set
len (j2 |-> (@ 1)) is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
j3 |^ (j2 |-> (@ 1)) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Product (j3 |^ (j2 |-> (@ 1))) is Element of the carrier of n
the multF of n is Relation-like Function-like V25([: the carrier of n, the carrier of n:], the carrier of n) associative having_a_unity 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 non empty set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like non empty set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty set
the multF of n $$ (j3 |^ (j2 |-> (@ 1))) is Element of the carrier of n
(len j3) |-> (@ 1) is Relation-like NAT -defined INT -valued Function-like finite len j3 -element FinSequence-like FinSubsequence-like V55() V56() V57() Element of (len j3) -tuples_on INT
(len j3) -tuples_on INT is functional non empty FinSequence-membered FinSequenceSet of INT
{ b1 where b1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like Element of INT * : len b1 = len j3 } is set
Seg (len j3) is finite len j3 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
{ b1 where b1 is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( 1 <= b1 & b1 <= len j3 ) } is set
K503((Seg (len j3)),(@ 1)) is Relation-like NAT -defined RAT -valued INT -valued Function-like V25( Seg (len j3),{(@ 1)}) finite FinSequence-like FinSubsequence-like V55() V56() V57() Element of bool [:(Seg (len j3)),{(@ 1)}:]
[:(Seg (len j3)),{(@ 1)}:] is Relation-like RAT -valued INT -valued finite V55() V56() V57() set
bool [:(Seg (len j3)),{(@ 1)}:] is non empty finite V48() set
j3 |^ ((len j3) |-> (@ 1)) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Product (j3 |^ ((len j3) |-> (@ 1))) is Element of the carrier of n
the multF of n $$ (j3 |^ ((len j3) |-> (@ 1))) is Element of the carrier of n
Product (j2 |-> b) is Element of the carrier of n
the multF of n $$ (j2 |-> b) is Element of the carrier of n
j3 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len j3 is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
c7 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V55() V56() V57() FinSequence of INT
len c7 is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
rng j3 is finite set
j3 |^ c7 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Product (j3 |^ c7) is Element of the carrier of n
the multF of n is Relation-like Function-like V25([: the carrier of n, the carrier of n:], the carrier of n) associative having_a_unity 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 non empty set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like non empty set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty set
the multF of n $$ (j3 |^ c7) is Element of the carrier of n
a " is Element of the carrier of n
- (- j2) is ext-real non negative complex V40() integer V43() Element of INT
b |^ (- (- j2)) is Element of the carrier of n
b |^ j2 is Element of the carrier of n
power n is Relation-like Function-like V25([: the carrier of n,NAT:], the carrier of n) Element of bool [:[: the carrier of n,NAT:], the carrier of n:]
[: the carrier of n,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V55() V56() V57() V58() set
[:[: the carrier of n,NAT:], the carrier of n:] is Relation-like non empty non trivial non finite set
bool [:[: the carrier of n,NAT:], the carrier of n:] is non empty non trivial non finite set
(power n) . (b,j2) is set
[b,j2] is non empty set
{b,j2} is non empty finite set
{b} is non empty trivial finite 1 -element set
{{b,j2},{b}} is non empty finite V48() set
(power n) . [b,j2] is set
j2 -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 = j2 } is set
j2 |-> b is Relation-like NAT -defined the carrier of n -valued Function-like finite j2 -element FinSequence-like FinSubsequence-like Element of j2 -tuples_on the carrier of n
Seg j2 is finite j2 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
{ b1 where b1 is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( 1 <= b1 & b1 <= j2 ) } is set
K503((Seg j2),b) is Relation-like NAT -defined Function-like V25( Seg j2,{b}) finite FinSequence-like FinSubsequence-like Element of bool [:(Seg j2),{b}:]
[:(Seg j2),{b}:] is Relation-like finite set
bool [:(Seg j2),{b}:] is non empty finite V48() set
j3 is Relation-like NAT -defined the carrier of n -valued Function-like finite j2 -element FinSequence-like FinSubsequence-like Element of j2 -tuples_on the carrier of n
len j3 is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
rng j3 is finite set
j2 |-> (@ 1) is Relation-like NAT -defined INT -valued Function-like finite j2 -element FinSequence-like FinSubsequence-like V55() V56() V57() Element of j2 -tuples_on INT
j2 -tuples_on INT is functional non empty FinSequence-membered FinSequenceSet of INT
INT * is functional non empty FinSequence-membered FinSequenceSet of INT
{ b1 where b1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like Element of INT * : len b1 = j2 } is set
K503((Seg j2),(@ 1)) is Relation-like NAT -defined RAT -valued INT -valued Function-like V25( Seg j2,{(@ 1)}) finite FinSequence-like FinSubsequence-like V55() V56() V57() Element of bool [:(Seg j2),{(@ 1)}:]
{(@ 1)} is non empty trivial finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered set
[:(Seg j2),{(@ 1)}:] is Relation-like RAT -valued INT -valued finite V55() V56() V57() set
bool [:(Seg j2),{(@ 1)}:] is non empty finite V48() set
len (j2 |-> (@ 1)) is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
j3 |^ (j2 |-> (@ 1)) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Product (j3 |^ (j2 |-> (@ 1))) is Element of the carrier of n
the multF of n is Relation-like Function-like V25([: the carrier of n, the carrier of n:], the carrier of n) associative having_a_unity 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 non empty set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like non empty set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty set
the multF of n $$ (j3 |^ (j2 |-> (@ 1))) is Element of the carrier of n
(len j3) |-> (@ 1) is Relation-like NAT -defined INT -valued Function-like finite len j3 -element FinSequence-like FinSubsequence-like V55() V56() V57() Element of (len j3) -tuples_on INT
(len j3) -tuples_on INT is functional non empty FinSequence-membered FinSequenceSet of INT
{ b1 where b1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like Element of INT * : len b1 = len j3 } is set
Seg (len j3) is finite len j3 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
{ b1 where b1 is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( 1 <= b1 & b1 <= len j3 ) } is set
K503((Seg (len j3)),(@ 1)) is Relation-like NAT -defined RAT -valued INT -valued Function-like V25( Seg (len j3),{(@ 1)}) finite FinSequence-like FinSubsequence-like V55() V56() V57() Element of bool [:(Seg (len j3)),{(@ 1)}:]
[:(Seg (len j3)),{(@ 1)}:] is Relation-like RAT -valued INT -valued finite V55() V56() V57() set
bool [:(Seg (len j3)),{(@ 1)}:] is non empty finite V48() set
j3 |^ ((len j3) |-> (@ 1)) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Product (j3 |^ ((len j3) |-> (@ 1))) is Element of the carrier of n
the multF of n $$ (j3 |^ ((len j3) |-> (@ 1))) is Element of the carrier of n
Product (j2 |-> b) is Element of the carrier of n
the multF of n $$ (j2 |-> b) is Element of the carrier of n
j3 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len j3 is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
c7 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V55() V56() V57() FinSequence of INT
len c7 is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
rng j3 is finite set
j3 |^ c7 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Product (j3 |^ c7) is Element of the carrier of n
the multF of n is Relation-like Function-like V25([: the carrier of n, the carrier of n:], the carrier of n) associative having_a_unity 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 non empty set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like non empty set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty set
the multF of n $$ (j3 |^ c7) is Element of the carrier of n
(a ") " is Element of the carrier of n
e is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len e is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
j2 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V55() V56() V57() FinSequence of INT
len j2 is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
rng e is finite set
e |^ j2 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Product (e |^ j2) is Element of the carrier of n
the multF of n is Relation-like Function-like V25([: the carrier of n, the carrier of n:], the carrier of n) associative having_a_unity 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 non empty set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like non empty set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty set
the multF of n $$ (e |^ j2) is Element of the carrier of n
(j2) is ext-real complex V40() integer V43() Element of INT
addint $$ j2 is ext-real complex V40() integer V43() Element of INT
b |^ (j2) is Element of the carrier of n
dom e is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
(len e) |-> b is Relation-like NAT -defined the carrier of n -valued Function-like finite len e -element FinSequence-like FinSubsequence-like Element of (len e) -tuples_on the carrier of n
(len e) -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 e } is set
Seg (len e) is finite len e -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
{ b1 where b1 is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( 1 <= b1 & b1 <= len e ) } is set
K503((Seg (len e)),b) is Relation-like NAT -defined Function-like V25( Seg (len e),{b}) finite FinSequence-like FinSubsequence-like Element of bool [:(Seg (len e)),{b}:]
{b} is non empty trivial finite 1 -element set
[:(Seg (len e)),{b}:] is Relation-like finite set
bool [:(Seg (len e)),{b}:] is non empty finite V48() set
j3 is V8() V12() ext-real non negative complex V40() integer finite cardinal set
e . j3 is set
((len e) |-> b) . j3 is set
dom ((len e) |-> b) is finite len e -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
(len j2) |-> b is Relation-like NAT -defined the carrier of n -valued Function-like finite len j2 -element FinSequence-like FinSubsequence-like Element of (len j2) -tuples_on the carrier of n
(len j2) -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 j2 } is set
Seg (len j2) is finite len j2 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
{ b1 where b1 is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( 1 <= b1 & b1 <= len j2 ) } is set
K503((Seg (len j2)),b) is Relation-like NAT -defined Function-like V25( Seg (len j2),{b}) finite FinSequence-like FinSubsequence-like Element of bool [:(Seg (len j2)),{b}:]
[:(Seg (len j2)),{b}:] is Relation-like finite set
bool [:(Seg (len j2)),{b}:] is non empty finite V48() set
((len j2) |-> b) |^ j2 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Product (((len j2) |-> b) |^ j2) is Element of the carrier of n
the multF of n $$ (((len j2) |-> b) |^ j2) is Element of the carrier of n
e is ext-real complex V40() integer set
b |^ e is Element of the carrier of n
j2 is ext-real complex V40() integer set
b |^ j2 is Element of the carrier of n
n is non empty finite unital Group-like associative multMagma
the carrier of n is non empty finite set
a is Element of the carrier of n
1_ n is non being_of_order_0 Element of the carrier of n
card n is V8() V12() non empty ext-real positive non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
card the carrier of n is V8() V12() non empty ext-real positive non negative complex V40() integer finite cardinal set
(card n) + 1 is V8() V12() non empty ext-real positive non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
b is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len b is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
dom b is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
Seg ((card n) + 1) is non empty