:: GR_CY_1 semantic presentation

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

c

Seg c

{ b

finSeg c

addint $$ ((finSeg c

addcomplex $$ j2 is complex Element of COMPLEX

addcomplex $$ ((finSeg c

b is V8() V12() ext-real non negative complex V40() integer finite cardinal set

finSeg b is finite b -element Element of K107(NAT)

{ b

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)

{ b

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

{ b

{}. 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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

c

len c

rng j3 is finite set

j3 |^ c

Product (j3 |^ c

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

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

c

len c

rng j3 is finite set

j3 |^ c

Product (j3 |^ c

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

(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

{ b

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

{ b

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

{ b

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

{ b

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