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 finite (card n) + 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 <= (card n) + 1 ) } is set
rng b is finite set
e is set
j2 is set
b . j2 is set
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
a |^ j3 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) . (a,j3) is set
[a,j3] is non empty set
{a,j3} is non empty finite set
{a} is non empty trivial finite 1 -element set
{{a,j3},{a}} is non empty finite V48() set
(power n) . [a,j3] is set
e is set
j2 is V8() V12() ext-real non negative complex V40() integer finite cardinal set
a |^ 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) . (a,j2) is set
[a,j2] is non empty set
{a,j2} is non empty finite set
{a} is non empty trivial finite 1 -element set
{{a,j2},{a}} is non empty finite V48() set
(power n) . [a,j2] is set
[:(Seg ((card n) + 1)), the carrier of n:] is Relation-like non empty finite set
bool [:(Seg ((card n) + 1)), the carrier of n:] is non empty finite V48() set
card (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 V43() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
card (Seg ((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
card ((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
e is Relation-like Function-like V25( Seg ((card n) + 1), the carrier of n) finite Element of bool [:(Seg ((card n) + 1)), the carrier of n:]
j2 is set
j3 is set
e . j2 is set
e . j3 is set
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
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
b - c7 is ext-real complex V40() integer V43() Element of INT
p 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 |^ p 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) . (a,p) is set
[a,p] is non empty set
{a,p} is non empty finite set
{a} is non empty trivial finite 1 -element set
{{a,p},{a}} is non empty finite V48() set
(power n) . [a,p] is set
e . c7 is set
a |^ c7 is Element of the carrier of n
(power n) . (a,c7) is set
[a,c7] is non empty set
{a,c7} is non empty finite set
{{a,c7},{a}} is non empty finite V48() set
(power n) . [a,c7] is set
a |^ b is Element of the carrier of n
(power n) . (a,b) is set
[a,b] is non empty set
{a,b} is non empty finite set
{{a,b},{a}} is non empty finite V48() set
(power n) . [a,b] is set
- c7 is ext-real non positive complex V40() integer V43() Element of INT
b + (- c7) is ext-real complex V40() integer V43() Element of INT
a |^ (b + (- c7)) is Element of the carrier of n
a |^ (- c7) is Element of the carrier of n
(a |^ c7) * (a |^ (- 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 finite 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 finite set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like non empty finite set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty finite V48() set
the multF of n . ((a |^ c7),(a |^ (- c7))) is Element of the carrier of n
[(a |^ c7),(a |^ (- c7))] is non empty set
{(a |^ c7),(a |^ (- c7))} is non empty finite set
{(a |^ c7)} is non empty trivial finite 1 -element set
{{(a |^ c7),(a |^ (- c7))},{(a |^ c7)}} is non empty finite V48() set
the multF of n . [(a |^ c7),(a |^ (- c7))] is set
c7 + (- c7) is ext-real complex V40() integer V43() Element of INT
a |^ (c7 + (- c7)) is Element of the carrier of n
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
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
c7 - b is ext-real complex V40() integer V43() Element of INT
p 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 |^ p 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) . (a,p) is set
[a,p] is non empty set
{a,p} is non empty finite set
{a} is non empty trivial finite 1 -element set
{{a,p},{a}} is non empty finite V48() set
(power n) . [a,p] is set
e . c7 is set
a |^ c7 is Element of the carrier of n
(power n) . (a,c7) is set
[a,c7] is non empty set
{a,c7} is non empty finite set
{{a,c7},{a}} is non empty finite V48() set
(power n) . [a,c7] is set
a |^ b is Element of the carrier of n
(power n) . (a,b) is set
[a,b] is non empty set
{a,b} is non empty finite set
{{a,b},{a}} is non empty finite V48() set
(power n) . [a,b] is set
- b is ext-real non positive complex V40() integer V43() Element of INT
c7 + (- b) is ext-real complex V40() integer V43() Element of INT
a |^ (c7 + (- b)) is Element of the carrier of n
a |^ (- b) is Element of the carrier of n
(a |^ 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 finite 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 finite set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like non empty finite set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty finite V48() set
the multF of n . ((a |^ b),(a |^ (- b))) is Element of the carrier of n
[(a |^ b),(a |^ (- b))] is non empty set
{(a |^ b),(a |^ (- b))} is non empty finite set
{(a |^ b)} is non empty trivial finite 1 -element set
{{(a |^ b),(a |^ (- b))},{(a |^ b)}} is non empty finite V48() set
the multF of n . [(a |^ b),(a |^ (- b))] is set
b + (- b) is ext-real complex V40() integer V43() Element of INT
a |^ (b + (- b)) is Element of the carrier of n
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
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
b is V8() V12() ext-real non negative complex V40() integer finite cardinal set
a |^ b 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) . (a,b) is set
[a,b] is non empty set
{a,b} is non empty finite set
{a} is non empty trivial finite 1 -element set
{{a,b},{a}} is non empty finite V48() set
(power n) . [a,b] is set
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
ord 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 non empty trivial finite 1 -element Element of bool the carrier of n
bool the carrier of n is non empty finite V48() set
gr {a} is non empty finite strict unital Group-like associative Subgroup of n
card (gr {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
the carrier of (gr {a}) is non empty finite set
card the carrier of (gr {a}) is V8() V12() non empty ext-real positive non negative complex V40() integer finite cardinal set
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 (ord a) is finite ord a -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 <= ord a ) } is set
rng b is finite set
e is set
j2 is set
b . j2 is set
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
a |^ j3 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) . (a,j3) is set
[a,j3] is non empty set
{a,j3} is non empty finite set
{a} is non empty trivial finite 1 -element set
{{a,j3},{a}} is non empty finite V48() set
(power n) . [a,j3] is set
e is set
j2 is V8() V12() ext-real non negative complex V40() integer finite cardinal set
a |^ 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) . (a,j2) is set
[a,j2] is non empty set
{a,j2} is non empty finite set
{a} is non empty trivial finite 1 -element set
{{a,j2},{a}} is non empty finite V48() set
(power n) . [a,j2] is set
(ord a) + 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
0 + 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 . 1 is set
a |^ 1 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) . (a,1) is set
[a,1] is non empty set
{a,1} is non empty finite set
{a} is non empty trivial finite 1 -element set
{{a,1},{a}} is non empty finite V48() set
(power n) . [a,1] is set
e is set
b . e is set
j2 is set
b . j2 is set
e is non empty set
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 finite 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 finite set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like non empty finite set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty finite V48() set
dom the multF of n is finite set
the multF of n || e is Relation-like Function-like set
[:e,e:] is Relation-like non empty set
the multF of n | [:e,e:] is Relation-like finite set
dom ( the multF of n || e) is set
rng ( the multF of n || e) is set
j2 is set
c7 is set
( the multF of n || e) . c7 is set
b is set
p is set
[b,p] is non empty set
{b,p} is non empty finite set
{b} is non empty trivial finite 1 -element set
{{b,p},{b}} is non empty finite V48() set
s is V8() V12() ext-real non negative complex V40() integer finite cardinal set
a |^ s 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) . (a,s) is set
[a,s] is non empty set
{a,s} is non empty finite set
{a} is non empty trivial finite 1 -element set
{{a,s},{a}} is non empty finite V48() set
(power n) . [a,s] is set
r is V8() V12() ext-real non negative complex V40() integer finite cardinal set
a |^ r is Element of the carrier of n
(power n) . (a,r) is set
[a,r] is non empty set
{a,r} is non empty finite set
{{a,r},{a}} is non empty finite V48() set
(power n) . [a,r] is set
r + s 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 |^ (r + s) is Element of the carrier of n
(power n) . (a,(r + s)) is set
[a,(r + s)] is non empty set
{a,(r + s)} is non empty finite set
{{a,(r + s)},{a}} is non empty finite V48() set
(power n) . [a,(r + s)] is set
(r + s) mod (ord 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
b . (ord a) is set
(r + s) div (ord 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
(ord a) * ((r + s) div (ord 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
((ord a) * ((r + s) div (ord a))) + ((r + s) mod (ord 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 |^ (((ord a) * ((r + s) div (ord a))) + ((r + s) mod (ord a))) is Element of the carrier of n
(power n) . (a,(((ord a) * ((r + s) div (ord a))) + ((r + s) mod (ord a)))) is set
[a,(((ord a) * ((r + s) div (ord a))) + ((r + s) mod (ord a)))] is non empty set
{a,(((ord a) * ((r + s) div (ord a))) + ((r + s) mod (ord a)))} is non empty finite set
{{a,(((ord a) * ((r + s) div (ord a))) + ((r + s) mod (ord a)))},{a}} is non empty finite V48() set
(power n) . [a,(((ord a) * ((r + s) div (ord a))) + ((r + s) mod (ord a)))] is set
a |^ ((ord a) * ((r + s) div (ord a))) is Element of the carrier of n
(power n) . (a,((ord a) * ((r + s) div (ord a)))) is set
[a,((ord a) * ((r + s) div (ord a)))] is non empty set
{a,((ord a) * ((r + s) div (ord a)))} is non empty finite set
{{a,((ord a) * ((r + s) div (ord a)))},{a}} is non empty finite V48() set
(power n) . [a,((ord a) * ((r + s) div (ord a)))] is set
a |^ ((r + s) mod (ord a)) is Element of the carrier of n
(power n) . (a,((r + s) mod (ord a))) is set
[a,((r + s) mod (ord a))] is non empty set
{a,((r + s) mod (ord a))} is non empty finite set
{{a,((r + s) mod (ord a))},{a}} is non empty finite V48() set
(power n) . [a,((r + s) mod (ord a))] is set
(a |^ ((ord a) * ((r + s) div (ord a)))) * (a |^ ((r + s) mod (ord a))) is Element of the carrier of n
the multF of n . ((a |^ ((ord a) * ((r + s) div (ord a)))),(a |^ ((r + s) mod (ord a)))) is Element of the carrier of n
[(a |^ ((ord a) * ((r + s) div (ord a)))),(a |^ ((r + s) mod (ord a)))] is non empty set
{(a |^ ((ord a) * ((r + s) div (ord a)))),(a |^ ((r + s) mod (ord a)))} is non empty finite set
{(a |^ ((ord a) * ((r + s) div (ord a))))} is non empty trivial finite 1 -element set
{{(a |^ ((ord a) * ((r + s) div (ord a)))),(a |^ ((r + s) mod (ord a)))},{(a |^ ((ord a) * ((r + s) div (ord a))))}} is non empty finite V48() set
the multF of n . [(a |^ ((ord a) * ((r + s) div (ord a)))),(a |^ ((r + s) mod (ord a)))] is set
a |^ (ord a) is Element of the carrier of n
(power n) . (a,(ord a)) is set
[a,(ord a)] is non empty set
{a,(ord a)} is non empty finite set
{{a,(ord a)},{a}} is non empty finite V48() set
(power n) . [a,(ord a)] is set
(a |^ (ord a)) |^ ((r + s) div (ord a)) is Element of the carrier of n
(power n) . ((a |^ (ord a)),((r + s) div (ord a))) is set
[(a |^ (ord a)),((r + s) div (ord a))] is non empty set
{(a |^ (ord a)),((r + s) div (ord a))} is non empty finite set
{(a |^ (ord a))} is non empty trivial finite 1 -element set
{{(a |^ (ord a)),((r + s) div (ord a))},{(a |^ (ord a))}} is non empty finite V48() set
(power n) . [(a |^ (ord a)),((r + s) div (ord a))] is set
((a |^ (ord a)) |^ ((r + s) div (ord a))) * (a |^ ((r + s) mod (ord a))) is Element of the carrier of n
the multF of n . (((a |^ (ord a)) |^ ((r + s) div (ord a))),(a |^ ((r + s) mod (ord a)))) is Element of the carrier of n
[((a |^ (ord a)) |^ ((r + s) div (ord a))),(a |^ ((r + s) mod (ord a)))] is non empty set
{((a |^ (ord a)) |^ ((r + s) div (ord a))),(a |^ ((r + s) mod (ord a)))} is non empty finite set
{((a |^ (ord a)) |^ ((r + s) div (ord a)))} is non empty trivial finite 1 -element set
{{((a |^ (ord a)) |^ ((r + s) div (ord a))),(a |^ ((r + s) mod (ord a)))},{((a |^ (ord a)) |^ ((r + s) div (ord a)))}} is non empty finite V48() set
the multF of n . [((a |^ (ord a)) |^ ((r + s) div (ord a))),(a |^ ((r + s) mod (ord a)))] is set
1_ n is non being_of_order_0 Element of the carrier of n
(1_ n) |^ ((r + s) div (ord a)) is Element of the carrier of n
(power n) . ((1_ n),((r + s) div (ord a))) is set
[(1_ n),((r + s) div (ord a))] is non empty set
{(1_ n),((r + s) div (ord a))} is non empty finite set
{(1_ n)} is non empty trivial finite 1 -element set
{{(1_ n),((r + s) div (ord a))},{(1_ n)}} is non empty finite V48() set
(power n) . [(1_ n),((r + s) div (ord a))] is set
((1_ n) |^ ((r + s) div (ord a))) * (a |^ ((r + s) mod (ord a))) is Element of the carrier of n
the multF of n . (((1_ n) |^ ((r + s) div (ord a))),(a |^ ((r + s) mod (ord a)))) is Element of the carrier of n
[((1_ n) |^ ((r + s) div (ord a))),(a |^ ((r + s) mod (ord a)))] is non empty set
{((1_ n) |^ ((r + s) div (ord a))),(a |^ ((r + s) mod (ord a)))} is non empty finite set
{((1_ n) |^ ((r + s) div (ord a)))} is non empty trivial finite 1 -element set
{{((1_ n) |^ ((r + s) div (ord a))),(a |^ ((r + s) mod (ord a)))},{((1_ n) |^ ((r + s) div (ord a)))}} is non empty finite V48() set
the multF of n . [((1_ n) |^ ((r + s) div (ord a))),(a |^ ((r + s) mod (ord a)))] is set
(1_ n) * (a |^ ((r + s) mod (ord a))) is Element of the carrier of n
the multF of n . ((1_ n),(a |^ ((r + s) mod (ord a)))) is Element of the carrier of n
[(1_ n),(a |^ ((r + s) mod (ord a)))] is non empty set
{(1_ n),(a |^ ((r + s) mod (ord a)))} is non empty finite set
{{(1_ n),(a |^ ((r + s) mod (ord a)))},{(1_ n)}} is non empty finite V48() set
the multF of n . [(1_ n),(a |^ ((r + s) mod (ord a)))] is set
a |^ 0 is Element of the carrier of n
(power n) . (a,0) is set
[a,0] is non empty set
{a,0} is non empty finite set
{{a,0},{a}} is non empty finite V48() set
(power n) . [a,0] is set
((r + s) mod (ord a)) + 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
0 + 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 . ((r + s) mod (ord a)) is set
(r + s) div (ord 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
(ord a) * ((r + s) div (ord 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
((ord a) * ((r + s) div (ord a))) + ((r + s) mod (ord 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 |^ (((ord a) * ((r + s) div (ord a))) + ((r + s) mod (ord a))) is Element of the carrier of n
(power n) . (a,(((ord a) * ((r + s) div (ord a))) + ((r + s) mod (ord a)))) is set
[a,(((ord a) * ((r + s) div (ord a))) + ((r + s) mod (ord a)))] is non empty set
{a,(((ord a) * ((r + s) div (ord a))) + ((r + s) mod (ord a)))} is non empty finite set
{{a,(((ord a) * ((r + s) div (ord a))) + ((r + s) mod (ord a)))},{a}} is non empty finite V48() set
(power n) . [a,(((ord a) * ((r + s) div (ord a))) + ((r + s) mod (ord a)))] is set
a |^ ((ord a) * ((r + s) div (ord a))) is Element of the carrier of n
(power n) . (a,((ord a) * ((r + s) div (ord a)))) is set
[a,((ord a) * ((r + s) div (ord a)))] is non empty set
{a,((ord a) * ((r + s) div (ord a)))} is non empty finite set
{{a,((ord a) * ((r + s) div (ord a)))},{a}} is non empty finite V48() set
(power n) . [a,((ord a) * ((r + s) div (ord a)))] is set
a |^ ((r + s) mod (ord a)) is Element of the carrier of n
(power n) . (a,((r + s) mod (ord a))) is set
[a,((r + s) mod (ord a))] is non empty set
{a,((r + s) mod (ord a))} is non empty finite set
{{a,((r + s) mod (ord a))},{a}} is non empty finite V48() set
(power n) . [a,((r + s) mod (ord a))] is set
(a |^ ((ord a) * ((r + s) div (ord a)))) * (a |^ ((r + s) mod (ord a))) is Element of the carrier of n
the multF of n . ((a |^ ((ord a) * ((r + s) div (ord a)))),(a |^ ((r + s) mod (ord a)))) is Element of the carrier of n
[(a |^ ((ord a) * ((r + s) div (ord a)))),(a |^ ((r + s) mod (ord a)))] is non empty set
{(a |^ ((ord a) * ((r + s) div (ord a)))),(a |^ ((r + s) mod (ord a)))} is non empty finite set
{(a |^ ((ord a) * ((r + s) div (ord a))))} is non empty trivial finite 1 -element set
{{(a |^ ((ord a) * ((r + s) div (ord a)))),(a |^ ((r + s) mod (ord a)))},{(a |^ ((ord a) * ((r + s) div (ord a))))}} is non empty finite V48() set
the multF of n . [(a |^ ((ord a) * ((r + s) div (ord a)))),(a |^ ((r + s) mod (ord a)))] is set
a |^ (ord a) is Element of the carrier of n
(power n) . (a,(ord a)) is set
[a,(ord a)] is non empty set
{a,(ord a)} is non empty finite set
{{a,(ord a)},{a}} is non empty finite V48() set
(power n) . [a,(ord a)] is set
(a |^ (ord a)) |^ ((r + s) div (ord a)) is Element of the carrier of n
(power n) . ((a |^ (ord a)),((r + s) div (ord a))) is set
[(a |^ (ord a)),((r + s) div (ord a))] is non empty set
{(a |^ (ord a)),((r + s) div (ord a))} is non empty finite set
{(a |^ (ord a))} is non empty trivial finite 1 -element set
{{(a |^ (ord a)),((r + s) div (ord a))},{(a |^ (ord a))}} is non empty finite V48() set
(power n) . [(a |^ (ord a)),((r + s) div (ord a))] is set
((a |^ (ord a)) |^ ((r + s) div (ord a))) * (a |^ ((r + s) mod (ord a))) is Element of the carrier of n
the multF of n . (((a |^ (ord a)) |^ ((r + s) div (ord a))),(a |^ ((r + s) mod (ord a)))) is Element of the carrier of n
[((a |^ (ord a)) |^ ((r + s) div (ord a))),(a |^ ((r + s) mod (ord a)))] is non empty set
{((a |^ (ord a)) |^ ((r + s) div (ord a))),(a |^ ((r + s) mod (ord a)))} is non empty finite set
{((a |^ (ord a)) |^ ((r + s) div (ord a)))} is non empty trivial finite 1 -element set
{{((a |^ (ord a)) |^ ((r + s) div (ord a))),(a |^ ((r + s) mod (ord a)))},{((a |^ (ord a)) |^ ((r + s) div (ord a)))}} is non empty finite V48() set
the multF of n . [((a |^ (ord a)) |^ ((r + s) div (ord a))),(a |^ ((r + s) mod (ord a)))] is set
1_ n is non being_of_order_0 Element of the carrier of n
(1_ n) |^ ((r + s) div (ord a)) is Element of the carrier of n
(power n) . ((1_ n),((r + s) div (ord a))) is set
[(1_ n),((r + s) div (ord a))] is non empty set
{(1_ n),((r + s) div (ord a))} is non empty finite set
{(1_ n)} is non empty trivial finite 1 -element set
{{(1_ n),((r + s) div (ord a))},{(1_ n)}} is non empty finite V48() set
(power n) . [(1_ n),((r + s) div (ord a))] is set
((1_ n) |^ ((r + s) div (ord a))) * (a |^ ((r + s) mod (ord a))) is Element of the carrier of n
the multF of n . (((1_ n) |^ ((r + s) div (ord a))),(a |^ ((r + s) mod (ord a)))) is Element of the carrier of n
[((1_ n) |^ ((r + s) div (ord a))),(a |^ ((r + s) mod (ord a)))] is non empty set
{((1_ n) |^ ((r + s) div (ord a))),(a |^ ((r + s) mod (ord a)))} is non empty finite set
{((1_ n) |^ ((r + s) div (ord a)))} is non empty trivial finite 1 -element set
{{((1_ n) |^ ((r + s) div (ord a))),(a |^ ((r + s) mod (ord a)))},{((1_ n) |^ ((r + s) div (ord a)))}} is non empty finite V48() set
the multF of n . [((1_ n) |^ ((r + s) div (ord a))),(a |^ ((r + s) mod (ord a)))] is set
(1_ n) * (a |^ ((r + s) mod (ord a))) is Element of the carrier of n
the multF of n . ((1_ n),(a |^ ((r + s) mod (ord a)))) is Element of the carrier of n
[(1_ n),(a |^ ((r + s) mod (ord a)))] is non empty set
{(1_ n),(a |^ ((r + s) mod (ord a)))} is non empty finite set
{{(1_ n),(a |^ ((r + s) mod (ord a)))},{(1_ n)}} is non empty finite V48() set
the multF of n . [(1_ n),(a |^ ((r + s) mod (ord a)))] is set
(a |^ r) * (a |^ s) is Element of the carrier of n
the multF of n . ((a |^ r),(a |^ s)) is Element of the carrier of n
[(a |^ r),(a |^ s)] is non empty set
{(a |^ r),(a |^ s)} is non empty finite set
{(a |^ r)} is non empty trivial finite 1 -element set
{{(a |^ r),(a |^ s)},{(a |^ r)}} is non empty finite V48() set
the multF of n . [(a |^ r),(a |^ s)] is set
s is set
b . s is set
[:[:e,e:],e:] is Relation-like non empty set
bool [:[:e,e:],e:] is non empty set
j2 is Relation-like Function-like V25([:e,e:],e) Element of bool [:[:e,e:],e:]
multMagma(# e,j2 #) is non empty strict multMagma
the carrier of multMagma(# e,j2 #) is non empty set
c7 is Element of the carrier of multMagma(# e,j2 #)
b is Element of the carrier of multMagma(# e,j2 #)
c7 * b is Element of the carrier of multMagma(# e,j2 #)
the multF of multMagma(# e,j2 #) is Relation-like Function-like V25([: the carrier of multMagma(# e,j2 #), the carrier of multMagma(# e,j2 #):], the carrier of multMagma(# e,j2 #)) Element of bool [:[: the carrier of multMagma(# e,j2 #), the carrier of multMagma(# e,j2 #):], the carrier of multMagma(# e,j2 #):]
[: the carrier of multMagma(# e,j2 #), the carrier of multMagma(# e,j2 #):] is Relation-like non empty set
[:[: the carrier of multMagma(# e,j2 #), the carrier of multMagma(# e,j2 #):], the carrier of multMagma(# e,j2 #):] is Relation-like non empty set
bool [:[: the carrier of multMagma(# e,j2 #), the carrier of multMagma(# e,j2 #):], the carrier of multMagma(# e,j2 #):] is non empty set
the multF of multMagma(# e,j2 #) . (c7,b) is Element of the carrier of multMagma(# e,j2 #)
[c7,b] is non empty set
{c7,b} is non empty finite set
{c7} is non empty trivial finite 1 -element set
{{c7,b},{c7}} is non empty finite V48() set
the multF of multMagma(# e,j2 #) . [c7,b] is set
p is Element of the carrier of n
s is Element of the carrier of n
p * s is Element of the carrier of n
the multF of n . (p,s) is Element of the carrier of n
[p,s] is non empty set
{p,s} is non empty finite set
{p} is non empty trivial finite 1 -element set
{{p,s},{p}} is non empty finite V48() set
the multF of n . [p,s] is set
[c7,b] is non empty Element of [: the carrier of multMagma(# e,j2 #), the carrier of multMagma(# e,j2 #):]
( the multF of n || e) . [c7,b] is set
a |^ (ord a) 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) . (a,(ord a)) is set
[a,(ord a)] is non empty set
{a,(ord a)} is non empty finite set
{a} is non empty trivial finite 1 -element set
{{a,(ord a)},{a}} is non empty finite V48() set
(power n) . [a,(ord a)] is set
b . (ord a) is set
c7 is set
b . c7 is set
1_ n is non being_of_order_0 Element of the carrier of n
c7 is Element of the carrier of multMagma(# e,j2 #)
b is Element of the carrier of multMagma(# e,j2 #)
b * c7 is Element of the carrier of multMagma(# e,j2 #)
the multF of multMagma(# e,j2 #) is Relation-like Function-like V25([: the carrier of multMagma(# e,j2 #), the carrier of multMagma(# e,j2 #):], the carrier of multMagma(# e,j2 #)) Element of bool [:[: the carrier of multMagma(# e,j2 #), the carrier of multMagma(# e,j2 #):], the carrier of multMagma(# e,j2 #):]
[: the carrier of multMagma(# e,j2 #), the carrier of multMagma(# e,j2 #):] is Relation-like non empty set
[:[: the carrier of multMagma(# e,j2 #), the carrier of multMagma(# e,j2 #):], the carrier of multMagma(# e,j2 #):] is Relation-like non empty set
bool [:[: the carrier of multMagma(# e,j2 #), the carrier of multMagma(# e,j2 #):], the carrier of multMagma(# e,j2 #):] is non empty set
the multF of multMagma(# e,j2 #) . (b,c7) is Element of the carrier of multMagma(# e,j2 #)
[b,c7] is non empty set
{b,c7} is non empty finite set
{b} is non empty trivial finite 1 -element set
{{b,c7},{b}} is non empty finite V48() set
the multF of multMagma(# e,j2 #) . [b,c7] is set
c7 * b is Element of the carrier of multMagma(# e,j2 #)
the multF of multMagma(# e,j2 #) . (c7,b) is Element of the carrier of multMagma(# e,j2 #)
[c7,b] is non empty set
{c7,b} is non empty finite set
{c7} is non empty trivial finite 1 -element set
{{c7,b},{c7}} is non empty finite V48() set
the multF of multMagma(# e,j2 #) . [c7,b] is set
p is Element of the carrier of n
p * (1_ n) is Element of the carrier of n
the multF of n . (p,(1_ n)) is Element of the carrier of n
[p,(1_ n)] is non empty set
{p,(1_ n)} is non empty finite set
{p} is non empty trivial finite 1 -element set
{{p,(1_ n)},{p}} is non empty finite V48() set
the multF of n . [p,(1_ n)] is set
(1_ n) * p is Element of the carrier of n
the multF of n . ((1_ n),p) is Element of the carrier of n
[(1_ n),p] is non empty set
{(1_ n),p} is non empty finite set
{(1_ n)} is non empty trivial finite 1 -element set
{{(1_ n),p},{(1_ n)}} is non empty finite V48() set
the multF of n . [(1_ n),p] is set
s is set
b . s is set
r 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 |^ r is Element of the carrier of n
(power n) . (a,r) is set
[a,r] is non empty set
{a,r} is non empty finite set
{{a,r},{a}} is non empty finite V48() set
(power n) . [a,r] is set
s is V8() V12() ext-real non negative complex V40() integer finite cardinal set
a |^ s is Element of the carrier of n
(power n) . (a,s) is set
[a,s] is non empty set
{a,s} is non empty finite set
{{a,s},{a}} is non empty finite V48() set
(power n) . [a,s] is set
s is V8() V12() ext-real non negative complex V40() integer finite cardinal set
a |^ s is Element of the carrier of n
(power n) . (a,s) is set
[a,s] is non empty set
{a,s} is non empty finite set
{{a,s},{a}} is non empty finite V48() set
(power n) . [a,s] is set
(ord a) - s is ext-real complex V40() integer V43() Element of INT
a |^ ((ord a) - s) is Element of the carrier of n
b . (ord a) is set
r 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
b . r is set
(ord a) + s 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
s - s is ext-real complex V40() integer V43() Element of INT
0 + 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
s is set
b . s is set
s + ((ord a) - s) is ext-real complex V40() integer V43() Element of INT
r is Element of the carrier of multMagma(# e,j2 #)
r * b is Element of the carrier of multMagma(# e,j2 #)
the multF of multMagma(# e,j2 #) . (r,b) is Element of the carrier of multMagma(# e,j2 #)
[r,b] is non empty set
{r,b} is non empty finite set
{r} is non empty trivial finite 1 -element set
{{r,b},{r}} is non empty finite V48() set
the multF of multMagma(# e,j2 #) . [r,b] is set
(a |^ ((ord a) - s)) * (a |^ s) is Element of the carrier of n
the multF of n . ((a |^ ((ord a) - s)),(a |^ s)) is Element of the carrier of n
[(a |^ ((ord a) - s)),(a |^ s)] is non empty set
{(a |^ ((ord a) - s)),(a |^ s)} is non empty finite set
{(a |^ ((ord a) - s))} is non empty trivial finite 1 -element set
{{(a |^ ((ord a) - s)),(a |^ s)},{(a |^ ((ord a) - s))}} is non empty finite V48() set
the multF of n . [(a |^ ((ord a) - s)),(a |^ s)] is set
b * r is Element of the carrier of multMagma(# e,j2 #)
the multF of multMagma(# e,j2 #) . (b,r) is Element of the carrier of multMagma(# e,j2 #)
[b,r] is non empty set
{b,r} is non empty finite set
{{b,r},{b}} is non empty finite V48() set
the multF of multMagma(# e,j2 #) . [b,r] is set
(a |^ s) * (a |^ ((ord a) - s)) is Element of the carrier of n
the multF of n . ((a |^ s),(a |^ ((ord a) - s))) is Element of the carrier of n
[(a |^ s),(a |^ ((ord a) - s))] is non empty set
{(a |^ s),(a |^ ((ord a) - s))} is non empty finite set
{(a |^ s)} is non empty trivial finite 1 -element set
{{(a |^ s),(a |^ ((ord a) - s))},{(a |^ s)}} is non empty finite V48() set
the multF of n . [(a |^ s),(a |^ ((ord a) - s))] is set
b is Element of the carrier of multMagma(# e,j2 #)
b * c7 is Element of the carrier of multMagma(# e,j2 #)
the multF of multMagma(# e,j2 #) is Relation-like Function-like V25([: the carrier of multMagma(# e,j2 #), the carrier of multMagma(# e,j2 #):], the carrier of multMagma(# e,j2 #)) Element of bool [:[: the carrier of multMagma(# e,j2 #), the carrier of multMagma(# e,j2 #):], the carrier of multMagma(# e,j2 #):]
[: the carrier of multMagma(# e,j2 #), the carrier of multMagma(# e,j2 #):] is Relation-like non empty set
[:[: the carrier of multMagma(# e,j2 #), the carrier of multMagma(# e,j2 #):], the carrier of multMagma(# e,j2 #):] is Relation-like non empty set
bool [:[: the carrier of multMagma(# e,j2 #), the carrier of multMagma(# e,j2 #):], the carrier of multMagma(# e,j2 #):] is non empty set
the multF of multMagma(# e,j2 #) . (b,c7) is Element of the carrier of multMagma(# e,j2 #)
[b,c7] is non empty set
{b,c7} is non empty finite set
{b} is non empty trivial finite 1 -element set
{{b,c7},{b}} is non empty finite V48() set
the multF of multMagma(# e,j2 #) . [b,c7] is set
p is Element of the carrier of multMagma(# e,j2 #)
c7 * p is Element of the carrier of multMagma(# e,j2 #)
the multF of multMagma(# e,j2 #) . (c7,p) is Element of the carrier of multMagma(# e,j2 #)
[c7,p] is non empty set
{c7,p} is non empty finite set
{c7} is non empty trivial finite 1 -element set
{{c7,p},{c7}} is non empty finite V48() set
the multF of multMagma(# e,j2 #) . [c7,p] is set
s is Element of the carrier of multMagma(# e,j2 #)
c7 is Element of the carrier of multMagma(# e,j2 #)
b is Element of the carrier of multMagma(# e,j2 #)
c7 * b is Element of the carrier of multMagma(# e,j2 #)
the multF of multMagma(# e,j2 #) is Relation-like Function-like V25([: the carrier of multMagma(# e,j2 #), the carrier of multMagma(# e,j2 #):], the carrier of multMagma(# e,j2 #)) Element of bool [:[: the carrier of multMagma(# e,j2 #), the carrier of multMagma(# e,j2 #):], the carrier of multMagma(# e,j2 #):]
[: the carrier of multMagma(# e,j2 #), the carrier of multMagma(# e,j2 #):] is Relation-like non empty set
[:[: the carrier of multMagma(# e,j2 #), the carrier of multMagma(# e,j2 #):], the carrier of multMagma(# e,j2 #):] is Relation-like non empty set
bool [:[: the carrier of multMagma(# e,j2 #), the carrier of multMagma(# e,j2 #):], the carrier of multMagma(# e,j2 #):] is non empty set
the multF of multMagma(# e,j2 #) . (c7,b) is Element of the carrier of multMagma(# e,j2 #)
[c7,b] is non empty set
{c7,b} is non empty finite set
{c7} is non empty trivial finite 1 -element set
{{c7,b},{c7}} is non empty finite V48() set
the multF of multMagma(# e,j2 #) . [c7,b] is set
p is Element of the carrier of multMagma(# e,j2 #)
(c7 * b) * p is Element of the carrier of multMagma(# e,j2 #)
the multF of multMagma(# e,j2 #) . ((c7 * b),p) is Element of the carrier of multMagma(# e,j2 #)
[(c7 * b),p] is non empty set
{(c7 * b),p} is non empty finite set
{(c7 * b)} is non empty trivial finite 1 -element set
{{(c7 * b),p},{(c7 * b)}} is non empty finite V48() set
the multF of multMagma(# e,j2 #) . [(c7 * b),p] is set
b * p is Element of the carrier of multMagma(# e,j2 #)
the multF of multMagma(# e,j2 #) . (b,p) is Element of the carrier of multMagma(# e,j2 #)
[b,p] is non empty set
{b,p} is non empty finite set
{b} is non empty trivial finite 1 -element set
{{b,p},{b}} is non empty finite V48() set
the multF of multMagma(# e,j2 #) . [b,p] is set
c7 * (b * p) is Element of the carrier of multMagma(# e,j2 #)
the multF of multMagma(# e,j2 #) . (c7,(b * p)) is Element of the carrier of multMagma(# e,j2 #)
[c7,(b * p)] is non empty set
{c7,(b * p)} is non empty finite set
{{c7,(b * p)},{c7}} is non empty finite V48() set
the multF of multMagma(# e,j2 #) . [c7,(b * p)] is set
r is Element of the carrier of n
s is Element of the carrier of n
r * s is Element of the carrier of n
the multF of n . (r,s) is Element of the carrier of n
[r,s] is non empty set
{r,s} is non empty finite set
{r} is non empty trivial finite 1 -element set
{{r,s},{r}} is non empty finite V48() set
the multF of n . [r,s] is set
s is Element of the carrier of n
s * r is Element of the carrier of n
the multF of n . (s,r) is Element of the carrier of n
[s,r] is non empty set
{s,r} is non empty finite set
{s} is non empty trivial finite 1 -element set
{{s,r},{s}} is non empty finite V48() set
the multF of n . [s,r] is set
(s * r) * s is Element of the carrier of n
the multF of n . ((s * r),s) is Element of the carrier of n
[(s * r),s] is non empty set
{(s * r),s} is non empty finite set
{(s * r)} is non empty trivial finite 1 -element set
{{(s * r),s},{(s * r)}} is non empty finite V48() set
the multF of n . [(s * r),s] is set
s * (r * s) is Element of the carrier of n
the multF of n . (s,(r * s)) is Element of the carrier of n
[s,(r * s)] is non empty set
{s,(r * s)} is non empty finite set
{{s,(r * s)},{s}} is non empty finite V48() set
the multF of n . [s,(r * s)] is set
b is Element of the carrier of multMagma(# e,j2 #)
c7 is non empty unital Group-like associative multMagma
the carrier of c7 is non empty set
e is non empty finite strict unital Group-like associative Subgroup of n
the carrier of e is non empty finite set
e is non empty finite strict unital Group-like associative Subgroup of n
the carrier of e is non empty finite set
j3 is set
dom b is finite set
b . j3 is set
c7 is set
b . c7 is set
p 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
b . p is set
a |^ p 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) . (a,p) is set
[a,p] is non empty set
{a,p} is non empty finite set
{a} is non empty trivial finite 1 -element set
{{a,p},{a}} is non empty finite V48() set
(power n) . [a,p] is set
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
b . b is set
a |^ b is Element of the carrier of n
(power n) . (a,b) is set
[a,b] is non empty set
{a,b} is non empty finite set
{{a,b},{a}} is non empty finite V48() set
(power n) . [a,b] is set
b - p is ext-real complex V40() integer V43() Element of INT
s is ext-real complex V40() Element of REAL
r is ext-real complex V40() Element of REAL
s + r is ext-real complex V40() Element of REAL
s is ext-real complex V40() Element of REAL
(s + r) - r is ext-real complex V40() Element of REAL
s - r is ext-real complex V40() Element of REAL
1_ n is non being_of_order_0 Element of the carrier of n
(a |^ p) " is Element of the carrier of n
(a |^ b) * ((a |^ p) ") 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 finite 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 finite set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like non empty finite set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty finite V48() set
the multF of n . ((a |^ b),((a |^ p) ")) is Element of the carrier of n
[(a |^ b),((a |^ p) ")] is non empty set
{(a |^ b),((a |^ p) ")} is non empty finite set
{(a |^ b)} is non empty trivial finite 1 -element set
{{(a |^ b),((a |^ p) ")},{(a |^ b)}} is non empty finite V48() set
the multF of n . [(a |^ b),((a |^ p) ")] is set
a |^ 0 is Element of the carrier of n
(power n) . (a,0) is set
[a,0] is non empty set
{a,0} is non empty finite set
{{a,0},{a}} is non empty finite V48() set
(power n) . [a,0] is set
- p is ext-real non positive complex V40() integer V43() Element of INT
a |^ (- p) is Element of the carrier of n
(a |^ b) * (a |^ (- p)) is Element of the carrier of n
the multF of n . ((a |^ b),(a |^ (- p))) is Element of the carrier of n
[(a |^ b),(a |^ (- p))] is non empty set
{(a |^ b),(a |^ (- p))} is non empty finite set
{{(a |^ b),(a |^ (- p))},{(a |^ b)}} is non empty finite V48() set
the multF of n . [(a |^ b),(a |^ (- p))] is set
b + (- p) is ext-real complex V40() integer V43() Element of INT
a |^ (b + (- p)) is Element of the carrier of n
r 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 |^ r is Element of the carrier of n
(power n) . (a,r) is set
[a,r] is non empty set
{a,r} is non empty finite set
{{a,r},{a}} is non empty finite V48() set
(power n) . [a,r] is set
p - b is ext-real complex V40() integer V43() Element of INT
s is ext-real complex V40() Element of REAL
s is ext-real complex V40() Element of REAL
s + s is ext-real complex V40() Element of REAL
r is ext-real complex V40() Element of REAL
(s + s) - s is ext-real complex V40() Element of REAL
r - s is ext-real complex V40() Element of REAL
1_ n is non being_of_order_0 Element of the carrier of n
(a |^ b) " is Element of the carrier of n
(a |^ p) * ((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 finite 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 finite set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like non empty finite set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty finite V48() set
the multF of n . ((a |^ p),((a |^ b) ")) is Element of the carrier of n
[(a |^ p),((a |^ b) ")] is non empty set
{(a |^ p),((a |^ b) ")} is non empty finite set
{(a |^ p)} is non empty trivial finite 1 -element set
{{(a |^ p),((a |^ b) ")},{(a |^ p)}} is non empty finite V48() set
the multF of n . [(a |^ p),((a |^ b) ")] is set
a |^ 0 is Element of the carrier of n
(power n) . (a,0) is set
[a,0] is non empty set
{a,0} is non empty finite set
{{a,0},{a}} is non empty finite V48() set
(power n) . [a,0] is set
- b is ext-real non positive complex V40() integer V43() Element of INT
a |^ (- b) is Element of the carrier of n
(a |^ p) * (a |^ (- b)) is Element of the carrier of n
the multF of n . ((a |^ p),(a |^ (- b))) is Element of the carrier of n
[(a |^ p),(a |^ (- b))] is non empty set
{(a |^ p),(a |^ (- b))} is non empty finite set
{{(a |^ p),(a |^ (- b))},{(a |^ p)}} is non empty finite V48() set
the multF of n . [(a |^ p),(a |^ (- b))] is set
p + (- b) is ext-real complex V40() integer V43() Element of INT
a |^ (p + (- b)) is Element of the carrier of n
r 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 |^ r is Element of the carrier of n
(power n) . (a,r) is set
[a,r] is non empty set
{a,r} is non empty finite set
{{a,r},{a}} is non empty finite V48() set
(power n) . [a,r] is set
e is finite set
card 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
card the carrier of (gr {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
n is non empty finite unital Group-like associative multMagma
the carrier of n is non empty finite set
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
a is Element of the carrier of n
ord 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 non empty trivial finite 1 -element Element of bool the carrier of n
bool the carrier of n is non empty finite V48() set
gr {a} is non empty finite strict unital Group-like associative Subgroup of n
card (gr {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
the carrier of (gr {a}) is non empty finite set
card the carrier of (gr {a}) is V8() V12() non empty ext-real positive non negative complex V40() integer finite cardinal set
n is non empty finite unital Group-like associative multMagma
the carrier of n is non empty finite set
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
1_ n is non being_of_order_0 Element of the carrier of n
a is Element of the carrier of n
a |^ (card n) 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) . (a,(card n)) is set
[a,(card n)] is non empty set
{a,(card n)} is non empty finite set
{a} is non empty trivial finite 1 -element set
{{a,(card n)},{a}} is non empty finite V48() set
(power n) . [a,(card n)] is set
ord 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
b is V8() V12() ext-real non negative complex V40() integer finite cardinal set
(ord a) * 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
a |^ (ord a) is Element of the carrier of n
(power n) . (a,(ord a)) is set
[a,(ord a)] is non empty set
{a,(ord a)} is non empty finite set
{{a,(ord a)},{a}} is non empty finite V48() set
(power n) . [a,(ord a)] is set
(a |^ (ord a)) |^ b is Element of the carrier of n
(power n) . ((a |^ (ord a)),b) is set
[(a |^ (ord a)),b] is non empty set
{(a |^ (ord a)),b} is non empty finite set
{(a |^ (ord a))} is non empty trivial finite 1 -element set
{{(a |^ (ord a)),b},{(a |^ (ord a))}} is non empty finite V48() set
(power n) . [(a |^ (ord a)),b] is set
(1_ n) |^ b is Element of the carrier of n
(power n) . ((1_ n),b) is set
[(1_ n),b] is non empty set
{(1_ n),b} is non empty finite set
{(1_ n)} is non empty trivial finite 1 -element set
{{(1_ n),b},{(1_ n)}} is non empty finite V48() set
(power n) . [(1_ n),b] is set
n is V8() V12() ext-real non negative complex V40() integer finite cardinal set
a is non empty finite unital Group-like associative multMagma
the carrier of a is non empty finite set
card 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
card the carrier of a is V8() V12() non empty ext-real positive non negative complex V40() integer finite cardinal set
n mod (card 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
(card a) - (n mod (card a)) is ext-real complex V40() integer V43() Element of INT
b is Element of the carrier of a
b |^ n is Element of the carrier of a
power a is Relation-like Function-like V25([: the carrier of a,NAT:], the carrier of a) Element of bool [:[: the carrier of a,NAT:], the carrier of a:]
[: the carrier of a,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V55() V56() V57() V58() set
[:[: the carrier of a,NAT:], the carrier of a:] is Relation-like non empty non trivial non finite set
bool [:[: the carrier of a,NAT:], the carrier of a:] is non empty non trivial non finite set
(power a) . (b,n) is set
[b,n] is non empty set
{b,n} is non empty finite set
{b} is non empty trivial finite 1 -element set
{{b,n},{b}} is non empty finite V48() set
(power a) . [b,n] is set
(b |^ n) " is Element of the carrier of a
b |^ ((card a) - (n mod (card a))) is Element of the carrier of a
(b |^ n) * (b |^ ((card a) - (n mod (card a)))) is Element of the carrier of a
the multF of a is Relation-like Function-like V25([: the carrier of a, the carrier of a:], the carrier of a) associative having_a_unity finite Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]
[: the carrier of a, the carrier of a:] is Relation-like non empty finite set
[:[: the carrier of a, the carrier of a:], the carrier of a:] is Relation-like non empty finite set
bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty finite V48() set
the multF of a . ((b |^ n),(b |^ ((card a) - (n mod (card a))))) is Element of the carrier of a
[(b |^ n),(b |^ ((card a) - (n mod (card a))))] is non empty set
{(b |^ n),(b |^ ((card a) - (n mod (card a))))} is non empty finite set
{(b |^ n)} is non empty trivial finite 1 -element set
{{(b |^ n),(b |^ ((card a) - (n mod (card a))))},{(b |^ n)}} is non empty finite V48() set
the multF of a . [(b |^ n),(b |^ ((card a) - (n mod (card a))))] is set
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
n + 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
b |^ (n + j3) is Element of the carrier of a
(power a) . (b,(n + j3)) is set
[b,(n + j3)] is non empty set
{b,(n + j3)} is non empty finite set
{{b,(n + j3)},{b}} is non empty finite V48() set
(power a) . [b,(n + j3)] is set
n div (card 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
(card a) * (n div (card 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
((card a) * (n div (card a))) + (n mod (card 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
(((card a) * (n div (card a))) + (n mod (card a))) + 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
b |^ ((((card a) * (n div (card a))) + (n mod (card a))) + j3) is Element of the carrier of a
(power a) . (b,((((card a) * (n div (card a))) + (n mod (card a))) + j3)) is set
[b,((((card a) * (n div (card a))) + (n mod (card a))) + j3)] is non empty set
{b,((((card a) * (n div (card a))) + (n mod (card a))) + j3)} is non empty finite set
{{b,((((card a) * (n div (card a))) + (n mod (card a))) + j3)},{b}} is non empty finite V48() set
(power a) . [b,((((card a) * (n div (card a))) + (n mod (card a))) + j3)] is set
((card a) * (n div (card a))) + (card 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
- (n mod (card a)) is ext-real non positive complex V40() integer V43() Element of INT
(- (n mod (card a))) + (n mod (card a)) is ext-real complex V40() integer V43() Element of INT
(((card a) * (n div (card a))) + (card a)) + ((- (n mod (card a))) + (n mod (card a))) is ext-real complex V40() integer V43() Element of INT
b |^ ((((card a) * (n div (card a))) + (card a)) + ((- (n mod (card a))) + (n mod (card a)))) is Element of the carrier of a
b |^ (((card a) * (n div (card a))) + (card a)) is Element of the carrier of a
(power a) . (b,(((card a) * (n div (card a))) + (card a))) is set
[b,(((card a) * (n div (card a))) + (card a))] is non empty set
{b,(((card a) * (n div (card a))) + (card a))} is non empty finite set
{{b,(((card a) * (n div (card a))) + (card a))},{b}} is non empty finite V48() set
(power a) . [b,(((card a) * (n div (card a))) + (card a))] is set
b |^ ((- (n mod (card a))) + (n mod (card a))) is Element of the carrier of a
(b |^ (((card a) * (n div (card a))) + (card a))) * (b |^ ((- (n mod (card a))) + (n mod (card a)))) is Element of the carrier of a
the multF of a . ((b |^ (((card a) * (n div (card a))) + (card a))),(b |^ ((- (n mod (card a))) + (n mod (card a))))) is Element of the carrier of a
[(b |^ (((card a) * (n div (card a))) + (card a))),(b |^ ((- (n mod (card a))) + (n mod (card a))))] is non empty set
{(b |^ (((card a) * (n div (card a))) + (card a))),(b |^ ((- (n mod (card a))) + (n mod (card a))))} is non empty finite set
{(b |^ (((card a) * (n div (card a))) + (card a)))} is non empty trivial finite 1 -element set
{{(b |^ (((card a) * (n div (card a))) + (card a))),(b |^ ((- (n mod (card a))) + (n mod (card a))))},{(b |^ (((card a) * (n div (card a))) + (card a)))}} is non empty finite V48() set
the multF of a . [(b |^ (((card a) * (n div (card a))) + (card a))),(b |^ ((- (n mod (card a))) + (n mod (card a))))] is set
b |^ (- (n mod (card a))) is Element of the carrier of a
b |^ (n mod (card a)) is Element of the carrier of a
(power a) . (b,(n mod (card a))) is set
[b,(n mod (card a))] is non empty set
{b,(n mod (card a))} is non empty finite set
{{b,(n mod (card a))},{b}} is non empty finite V48() set
(power a) . [b,(n mod (card a))] is set
(b |^ (- (n mod (card a)))) * (b |^ (n mod (card a))) is Element of the carrier of a
the multF of a . ((b |^ (- (n mod (card a)))),(b |^ (n mod (card a)))) is Element of the carrier of a
[(b |^ (- (n mod (card a)))),(b |^ (n mod (card a)))] is non empty set
{(b |^ (- (n mod (card a)))),(b |^ (n mod (card a)))} is non empty finite set
{(b |^ (- (n mod (card a))))} is non empty trivial finite 1 -element set
{{(b |^ (- (n mod (card a)))),(b |^ (n mod (card a)))},{(b |^ (- (n mod (card a))))}} is non empty finite V48() set
the multF of a . [(b |^ (- (n mod (card a)))),(b |^ (n mod (card a)))] is set
(b |^ (((card a) * (n div (card a))) + (card a))) * ((b |^ (- (n mod (card a)))) * (b |^ (n mod (card a)))) is Element of the carrier of a
the multF of a . ((b |^ (((card a) * (n div (card a))) + (card a))),((b |^ (- (n mod (card a)))) * (b |^ (n mod (card a))))) is Element of the carrier of a
[(b |^ (((card a) * (n div (card a))) + (card a))),((b |^ (- (n mod (card a)))) * (b |^ (n mod (card a))))] is non empty set
{(b |^ (((card a) * (n div (card a))) + (card a))),((b |^ (- (n mod (card a)))) * (b |^ (n mod (card a))))} is non empty finite set
{{(b |^ (((card a) * (n div (card a))) + (card a))),((b |^ (- (n mod (card a)))) * (b |^ (n mod (card a))))},{(b |^ (((card a) * (n div (card a))) + (card a)))}} is non empty finite V48() set
the multF of a . [(b |^ (((card a) * (n div (card a))) + (card a))),((b |^ (- (n mod (card a)))) * (b |^ (n mod (card a))))] is set
(b |^ (n mod (card a))) " is Element of the carrier of a
((b |^ (n mod (card a))) ") * (b |^ (n mod (card a))) is Element of the carrier of a
the multF of a . (((b |^ (n mod (card a))) "),(b |^ (n mod (card a)))) is Element of the carrier of a
[((b |^ (n mod (card a))) "),(b |^ (n mod (card a)))] is non empty set
{((b |^ (n mod (card a))) "),(b |^ (n mod (card a)))} is non empty finite set
{((b |^ (n mod (card a))) ")} is non empty trivial finite 1 -element set
{{((b |^ (n mod (card a))) "),(b |^ (n mod (card a)))},{((b |^ (n mod (card a))) ")}} is non empty finite V48() set
the multF of a . [((b |^ (n mod (card a))) "),(b |^ (n mod (card a)))] is set
(b |^ (((card a) * (n div (card a))) + (card a))) * (((b |^ (n mod (card a))) ") * (b |^ (n mod (card a)))) is Element of the carrier of a
the multF of a . ((b |^ (((card a) * (n div (card a))) + (card a))),(((b |^ (n mod (card a))) ") * (b |^ (n mod (card a))))) is Element of the carrier of a
[(b |^ (((card a) * (n div (card a))) + (card a))),(((b |^ (n mod (card a))) ") * (b |^ (n mod (card a))))] is non empty set
{(b |^ (((card a) * (n div (card a))) + (card a))),(((b |^ (n mod (card a))) ") * (b |^ (n mod (card a))))} is non empty finite set
{{(b |^ (((card a) * (n div (card a))) + (card a))),(((b |^ (n mod (card a))) ") * (b |^ (n mod (card a))))},{(b |^ (((card a) * (n div (card a))) + (card a)))}} is non empty finite V48() set
the multF of a . [(b |^ (((card a) * (n div (card a))) + (card a))),(((b |^ (n mod (card a))) ") * (b |^ (n mod (card a))))] is set
1_ a is non being_of_order_0 Element of the carrier of a
(b |^ (((card a) * (n div (card a))) + (card a))) * (1_ a) is Element of the carrier of a
the multF of a . ((b |^ (((card a) * (n div (card a))) + (card a))),(1_ a)) is Element of the carrier of a
[(b |^ (((card a) * (n div (card a))) + (card a))),(1_ a)] is non empty set
{(b |^ (((card a) * (n div (card a))) + (card a))),(1_ a)} is non empty finite set
{{(b |^ (((card a) * (n div (card a))) + (card a))),(1_ a)},{(b |^ (((card a) * (n div (card a))) + (card a)))}} is non empty finite V48() set
the multF of a . [(b |^ (((card a) * (n div (card a))) + (card a))),(1_ a)] is set
(n div (card a)) + 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
(card a) * ((n div (card a)) + 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
b |^ ((card a) * ((n div (card a)) + 1)) is Element of the carrier of a
(power a) . (b,((card a) * ((n div (card a)) + 1))) is set
[b,((card a) * ((n div (card a)) + 1))] is non empty set
{b,((card a) * ((n div (card a)) + 1))} is non empty finite set
{{b,((card a) * ((n div (card a)) + 1))},{b}} is non empty finite V48() set
(power a) . [b,((card a) * ((n div (card a)) + 1))] is set
b |^ (card a) is Element of the carrier of a
(power a) . (b,(card a)) is set
[b,(card a)] is non empty set
{b,(card a)} is non empty finite set
{{b,(card a)},{b}} is non empty finite V48() set
(power a) . [b,(card a)] is set
(b |^ (card a)) |^ ((n div (card a)) + 1) is Element of the carrier of a
(power a) . ((b |^ (card a)),((n div (card a)) + 1)) is set
[(b |^ (card a)),((n div (card a)) + 1)] is non empty set
{(b |^ (card a)),((n div (card a)) + 1)} is non empty finite set
{(b |^ (card a))} is non empty trivial finite 1 -element set
{{(b |^ (card a)),((n div (card a)) + 1)},{(b |^ (card a))}} is non empty finite V48() set
(power a) . [(b |^ (card a)),((n div (card a)) + 1)] is set
(1_ a) |^ ((n div (card a)) + 1) is Element of the carrier of a
(power a) . ((1_ a),((n div (card a)) + 1)) is set
[(1_ a),((n div (card a)) + 1)] is non empty set
{(1_ a),((n div (card a)) + 1)} is non empty finite set
{(1_ a)} is non empty trivial finite 1 -element set
{{(1_ a),((n div (card a)) + 1)},{(1_ a)}} is non empty finite V48() set
(power a) . [(1_ a),((n div (card a)) + 1)] is set
n is non empty associative multMagma
the carrier of n is non empty set
the multF of n is Relation-like Function-like V25([: the carrier of n, the carrier of n:], the carrier of n) associative 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
multMagma(# the carrier of n, the multF of n #) is non empty strict multMagma
the carrier of multMagma(# the carrier of n, the multF of n #) is non empty set
b is Element of the carrier of multMagma(# the carrier of n, the multF of n #)
e is Element of the carrier of multMagma(# the carrier of n, the multF of n #)
b * e is Element of the carrier of multMagma(# the carrier of n, the multF of n #)
the multF of multMagma(# the carrier of n, the multF of n #) is Relation-like Function-like V25([: the carrier of multMagma(# the carrier of n, the multF of n #), the carrier of multMagma(# the carrier of n, the multF of n #):], the carrier of multMagma(# the carrier of n, the multF of n #)) Element of bool [:[: the carrier of multMagma(# the carrier of n, the multF of n #), the carrier of multMagma(# the carrier of n, the multF of n #):], the carrier of multMagma(# the carrier of n, the multF of n #):]
[: the carrier of multMagma(# the carrier of n, the multF of n #), the carrier of multMagma(# the carrier of n, the multF of n #):] is Relation-like non empty set
[:[: the carrier of multMagma(# the carrier of n, the multF of n #), the carrier of multMagma(# the carrier of n, the multF of n #):], the carrier of multMagma(# the carrier of n, the multF of n #):] is Relation-like non empty set
bool [:[: the carrier of multMagma(# the carrier of n, the multF of n #), the carrier of multMagma(# the carrier of n, the multF of n #):], the carrier of multMagma(# the carrier of n, the multF of n #):] is non empty set
the multF of multMagma(# the carrier of n, the multF of n #) . (b,e) is Element of the carrier of multMagma(# the carrier of n, the multF of n #)
[b,e] is non empty set
{b,e} is non empty finite set
{b} is non empty trivial finite 1 -element set
{{b,e},{b}} is non empty finite V48() set
the multF of multMagma(# the carrier of n, the multF of n #) . [b,e] is set
j2 is Element of the carrier of multMagma(# the carrier of n, the multF of n #)
(b * e) * j2 is Element of the carrier of multMagma(# the carrier of n, the multF of n #)
the multF of multMagma(# the carrier of n, the multF of n #) . ((b * e),j2) is Element of the carrier of multMagma(# the carrier of n, the multF of n #)
[(b * e),j2] is non empty set
{(b * e),j2} is non empty finite set
{(b * e)} is non empty trivial finite 1 -element set
{{(b * e),j2},{(b * e)}} is non empty finite V48() set
the multF of multMagma(# the carrier of n, the multF of n #) . [(b * e),j2] is set
e * j2 is Element of the carrier of multMagma(# the carrier of n, the multF of n #)
the multF of multMagma(# the carrier of n, the multF of n #) . (e,j2) is Element of the carrier of multMagma(# the carrier of n, the multF of n #)
[e,j2] is non empty set
{e,j2} is non empty finite set
{e} is non empty trivial finite 1 -element set
{{e,j2},{e}} is non empty finite V48() set
the multF of multMagma(# the carrier of n, the multF of n #) . [e,j2] is set
b * (e * j2) is Element of the carrier of multMagma(# the carrier of n, the multF of n #)
the multF of multMagma(# the carrier of n, the multF of n #) . (b,(e * j2)) is Element of the carrier of multMagma(# the carrier of n, the multF of n #)
[b,(e * j2)] is non empty set
{b,(e * j2)} is non empty finite set
{{b,(e * j2)},{b}} is non empty finite V48() set
the multF of multMagma(# the carrier of n, the multF of n #) . [b,(e * j2)] is set
n is non empty unital Group-like associative multMagma
the carrier of n is non empty set
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
multMagma(# the carrier of n, the multF of n #) is non empty strict associative multMagma
the carrier of multMagma(# the carrier of n, the multF of n #) is non empty set
1_ n is non being_of_order_0 Element of the carrier of n
b is Element of the carrier of multMagma(# the carrier of n, the multF of n #)
e is Element of the carrier of multMagma(# the carrier of n, the multF of n #)
e * b is Element of the carrier of multMagma(# the carrier of n, the multF of n #)
the multF of multMagma(# the carrier of n, the multF of n #) is Relation-like Function-like V25([: the carrier of multMagma(# the carrier of n, the multF of n #), the carrier of multMagma(# the carrier of n, the multF of n #):], the carrier of multMagma(# the carrier of n, the multF of n #)) associative Element of bool [:[: the carrier of multMagma(# the carrier of n, the multF of n #), the carrier of multMagma(# the carrier of n, the multF of n #):], the carrier of multMagma(# the carrier of n, the multF of n #):]
[: the carrier of multMagma(# the carrier of n, the multF of n #), the carrier of multMagma(# the carrier of n, the multF of n #):] is Relation-like non empty set
[:[: the carrier of multMagma(# the carrier of n, the multF of n #), the carrier of multMagma(# the carrier of n, the multF of n #):], the carrier of multMagma(# the carrier of n, the multF of n #):] is Relation-like non empty set
bool [:[: the carrier of multMagma(# the carrier of n, the multF of n #), the carrier of multMagma(# the carrier of n, the multF of n #):], the carrier of multMagma(# the carrier of n, the multF of n #):] is non empty set
the multF of multMagma(# the carrier of n, the multF of n #) . (e,b) is Element of the carrier of multMagma(# the carrier of n, the multF of n #)
[e,b] is non empty set
{e,b} is non empty finite set
{e} is non empty trivial finite 1 -element set
{{e,b},{e}} is non empty finite V48() set
the multF of multMagma(# the carrier of n, the multF of n #) . [e,b] is set
b * e is Element of the carrier of multMagma(# the carrier of n, the multF of n #)
the multF of multMagma(# the carrier of n, the multF of n #) . (b,e) is Element of the carrier of multMagma(# the carrier of n, the multF of n #)
[b,e] is non empty set
{b,e} is non empty finite set
{b} is non empty trivial finite 1 -element set
{{b,e},{b}} is non empty finite V48() set
the multF of multMagma(# the carrier of n, the multF of n #) . [b,e] is set
j2 is Element of the carrier of n
j2 * (1_ n) is Element of the carrier of n
the multF of n . (j2,(1_ n)) is Element of the carrier of n
[j2,(1_ n)] is non empty set
{j2,(1_ n)} is non empty finite set
{j2} is non empty trivial finite 1 -element set
{{j2,(1_ n)},{j2}} is non empty finite V48() set
the multF of n . [j2,(1_ n)] is set
(1_ n) * j2 is Element of the carrier of n
the multF of n . ((1_ n),j2) is Element of the carrier of n
[(1_ n),j2] is non empty set
{(1_ n),j2} is non empty finite set
{(1_ n)} is non empty trivial finite 1 -element set
{{(1_ n),j2},{(1_ n)}} is non empty finite V48() set
the multF of n . [(1_ n),j2] is set
j2 " is Element of the carrier of n
j3 is Element of the carrier of multMagma(# the carrier of n, the multF of n #)
e * j3 is Element of the carrier of multMagma(# the carrier of n, the multF of n #)
the multF of multMagma(# the carrier of n, the multF of n #) . (e,j3) is Element of the carrier of multMagma(# the carrier of n, the multF of n #)
[e,j3] is non empty set
{e,j3} is non empty finite set
{{e,j3},{e}} is non empty finite V48() set
the multF of multMagma(# the carrier of n, the multF of n #) . [e,j3] is set
j3 * e is Element of the carrier of multMagma(# the carrier of n, the multF of n #)
the multF of multMagma(# the carrier of n, the multF of n #) . (j3,e) is Element of the carrier of multMagma(# the carrier of n, the multF of n #)
[j3,e] is non empty set
{j3,e} is non empty finite set
{j3} is non empty trivial finite 1 -element set
{{j3,e},{j3}} is non empty finite V48() set
the multF of multMagma(# the carrier of n, the multF of n #) . [j3,e] is set
j2 * (j2 ") is Element of the carrier of n
the multF of n . (j2,(j2 ")) is Element of the carrier of n
[j2,(j2 ")] is non empty set
{j2,(j2 ")} is non empty finite set
{{j2,(j2 ")},{j2}} is non empty finite V48() set
the multF of n . [j2,(j2 ")] is set
(j2 ") * j2 is Element of the carrier of n
the multF of n . ((j2 "),j2) is Element of the carrier of n
[(j2 "),j2] is non empty set
{(j2 "),j2} is non empty finite set
{(j2 ")} is non empty trivial finite 1 -element set
{{(j2 "),j2},{(j2 ")}} is non empty finite V48() set
the multF of n . [(j2 "),j2] is set
n is non empty finite strict unital Group-like associative multMagma
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
the carrier of n is non empty finite set
card the carrier of n is V8() V12() non empty ext-real positive non negative complex V40() integer finite cardinal set
1_ n is non being_of_order_0 Element of the carrier of n
(1). n is non empty finite strict unital Group-like associative Subgroup of n
a is Element of the carrier of n
{(1_ n)} is non empty trivial finite 1 -element Element of bool the carrier of n
bool the carrier of n is non empty finite V48() set
the carrier of ((1). n) is non empty finite set
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 finite 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 finite set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like non empty finite set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty finite V48() set
multMagma(# the carrier of n, the multF of n #) is non empty strict unital Group-like associative multMagma
n is V8() V12() ext-real non negative complex V40() integer finite cardinal set
a is non empty finite strict unital Group-like associative multMagma
card 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
the carrier of a is non empty finite set
card the carrier of a is V8() V12() non empty ext-real positive non negative complex V40() integer finite cardinal set
(1). a is non empty finite strict unital Group-like associative Subgroup of a
b is non empty finite strict unital Group-like associative Subgroup of a
card b 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
the carrier of b is non empty finite set
card the carrier of b is V8() V12() non empty ext-real positive non negative complex V40() integer finite cardinal set
multMagma(# INT,addint #) is non empty non trivial strict multMagma
() is non empty strict multMagma
the carrier of () is non empty set
b is Element of the carrier of ()
e is Element of the carrier of ()
b * e is Element of the carrier of ()
the multF of () is Relation-like Function-like V25([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is Relation-like non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is Relation-like non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the multF of () . (b,e) is Element of the carrier of ()
[b,e] is non empty set
{b,e} is non empty finite set
{b} is non empty trivial finite 1 -element set
{{b,e},{b}} is non empty finite V48() set
the multF of () . [b,e] is set
j2 is Element of the carrier of ()
(b * e) * j2 is Element of the carrier of ()
the multF of () . ((b * e),j2) is Element of the carrier of ()
[(b * e),j2] is non empty set
{(b * e),j2} is non empty finite set
{(b * e)} is non empty trivial finite 1 -element set
{{(b * e),j2},{(b * e)}} is non empty finite V48() set
the multF of () . [(b * e),j2] is set
e * j2 is Element of the carrier of ()
the multF of () . (e,j2) is Element of the carrier of ()
[e,j2] is non empty set
{e,j2} is non empty finite set
{e} is non empty trivial finite 1 -element set
{{e,j2},{e}} is non empty finite V48() set
the multF of () . [e,j2] is set
b * (e * j2) is Element of the carrier of ()
the multF of () . (b,(e * j2)) is Element of the carrier of ()
[b,(e * j2)] is non empty set
{b,(e * j2)} is non empty finite set
{{b,(e * j2)},{b}} is non empty finite V48() set
the multF of () . [b,(e * j2)] is set
c7 is ext-real complex V40() integer set
b is ext-real complex V40() integer set
c7 + b is ext-real complex V40() integer V43() Element of INT
j3 is ext-real complex V40() integer set
j3 + c7 is ext-real complex V40() integer V43() Element of INT
(j3 + c7) + b is ext-real complex V40() integer V43() Element of INT
j3 + (c7 + b) is ext-real complex V40() integer V43() Element of INT
a is Element of the carrier of ()
b is Element of the carrier of ()
b * a is Element of the carrier of ()
the multF of () is Relation-like Function-like V25([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is Relation-like non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is Relation-like non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the multF of () . (b,a) is Element of the carrier of ()
[b,a] is non empty set
{b,a} is non empty finite set
{b} is non empty trivial finite 1 -element set
{{b,a},{b}} is non empty finite V48() set
the multF of () . [b,a] is set
a * b is Element of the carrier of ()
the multF of () . (a,b) is Element of the carrier of ()
[a,b] is non empty set
{a,b} is non empty finite set
{a} is non empty trivial finite 1 -element set
{{a,b},{a}} is non empty finite V48() set
the multF of () . [a,b] is set
e is ext-real complex V40() integer set
- e is ext-real complex V40() integer V43() Element of INT
e + 0 is ext-real complex V40() integer V43() Element of INT
0 + e is ext-real complex V40() integer V43() Element of INT
j2 is Element of the carrier of ()
b * j2 is Element of the carrier of ()
the multF of () . (b,j2) is Element of the carrier of ()
[b,j2] is non empty set
{b,j2} is non empty finite set
{{b,j2},{b}} is non empty finite V48() set
the multF of () . [b,j2] is set
j2 * b is Element of the carrier of ()
the multF of () . (j2,b) is Element of the carrier of ()
[j2,b] is non empty set
{j2,b} is non empty finite set
{j2} is non empty trivial finite 1 -element set
{{j2,b},{j2}} is non empty finite V48() set
the multF of () . [j2,b] is set
e + (- e) is ext-real complex V40() integer V43() Element of INT
(- e) + e is ext-real complex V40() integer V43() Element of INT
the carrier of () is non empty set
n is ext-real complex V40() integer V43() Element of the carrier of ()
a is ext-real complex V40() integer V43() Element of the carrier of ()
n * a is ext-real complex V40() integer V43() Element of the carrier of ()
the multF of () is Relation-like INT -valued Function-like V25([: the carrier of (), the carrier of ():], the carrier of ()) associative having_a_unity V55() V56() V57() Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is Relation-like RAT -valued INT -valued non empty V55() V56() V57() set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is Relation-like RAT -valued INT -valued non empty V55() V56() V57() set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the multF of () . (n,a) is ext-real complex V40() integer V43() Element of the carrier of ()
[n,a] is non empty set
{n,a} is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{n} is non empty trivial finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered set
{{n,a},{n}} is non empty finite V48() set
the multF of () . [n,a] is ext-real complex V40() integer set
n + a is ext-real complex V40() integer V43() Element of INT
n is V8() V12() ext-real 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 V8() V12() ext-real 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
[:(Segm n),(Segm n):] is Relation-like RAT -valued INT -valued V55() V56() V57() V58() set
[:[:(Segm n),(Segm n):],(Segm n):] is Relation-like RAT -valued INT -valued V55() V56() V57() V58() set
bool [:[:(Segm n),(Segm n):],(Segm n):] is non empty set
a is V8() V12() non empty ext-real positive non negative complex V40() integer finite cardinal set
Segm a is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
b is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal Element of Segm a
e is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal Element of Segm a
b + 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
(b + e) mod 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
b + 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
(b + e) mod 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
j2 is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal Element of Segm a
[:(Segm a),(Segm a):] is Relation-like RAT -valued INT -valued non empty V55() V56() V57() V58() set
[:[:(Segm a),(Segm a):],(Segm a):] is Relation-like RAT -valued INT -valued non empty V55() V56() V57() V58() set
bool [:[:(Segm a),(Segm a):],(Segm a):] is non empty set
b is Relation-like INT -valued Function-like V25([:(Segm a),(Segm a):], Segm a) V55() V56() V57() V58() Element of bool [:[:(Segm a),(Segm a):],(Segm a):]
a is Relation-like INT -valued Function-like V25([:(Segm n),(Segm n):], Segm n) V55() V56() V57() V58() Element of bool [:[:(Segm n),(Segm n):],(Segm n):]
b is Relation-like INT -valued Function-like V25([:(Segm n),(Segm n):], Segm n) V55() V56() V57() V58() Element of bool [:[:(Segm n),(Segm n):],(Segm n):]
e is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal Element of Segm n
j2 is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal Element of Segm n
a . (e,j2) is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal Element of Segm n
[e,j2] is non empty set
{e,j2} is non empty finite V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{e} is non empty trivial finite V48() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{e,j2},{e}} is non empty finite V48() set
a . [e,j2] is V8() V12() ext-real non negative complex V40() integer finite cardinal set
b . (e,j2) is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal Element of Segm n
b . [e,j2] is V8() V12() ext-real non negative complex V40() integer finite cardinal set
e + 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
(e + j2) mod n 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
n is V8() V12() non empty ext-real positive non negative complex V40() integer finite cardinal set
Segm n is non empty 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([:(Segm n),(Segm n):], Segm n) V55() V56() V57() V58() Element of bool [:[:(Segm n),(Segm n):],(Segm n):]
[:(Segm n),(Segm n):] is Relation-like RAT -valued INT -valued non empty V55() V56() V57() V58() set
[:[:(Segm n),(Segm n):],(Segm n):] is Relation-like RAT -valued INT -valued non empty V55() V56() V57() V58() set
bool [:[:(Segm n),(Segm n):],(Segm n):] is non empty set
multMagma(# (Segm n),(n) #) is non empty strict multMagma
n is V8() V12() non empty ext-real positive non negative complex V40() integer finite cardinal set
(n) is non empty strict multMagma
Segm n is non empty 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([:(Segm n),(Segm n):], Segm n) V55() V56() V57() V58() Element of bool [:[:(Segm n),(Segm n):],(Segm n):]
[:(Segm n),(Segm n):] is Relation-like RAT -valued INT -valued non empty V55() V56() V57() V58() set
[:[:(Segm n),(Segm n):],(Segm n):] is Relation-like RAT -valued INT -valued non empty V55() V56() V57() V58() set
bool [:[:(Segm n),(Segm n):],(Segm n):] is non empty set
multMagma(# (Segm n),(n) #) is non empty strict multMagma
the carrier of (n) is non empty set
e is Element of the carrier of (n)
j2 is Element of the carrier of (n)
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)) 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)
[e,j2] is non empty set
{e,j2} is non empty finite set
{e} is non empty trivial finite 1 -element set
{{e,j2},{e}} is non empty finite V48() set
the multF of (n) . [e,j2] is set
j3 is Element of the carrier of (n)
(e * j2) * j3 is Element of the carrier of (n)
the multF of (n) . ((e * j2),j3) is Element of the carrier of (n)
[(e * j2),j3] is non empty set
{(e * j2),j3} is non empty finite set
{(e * j2)} is non empty trivial finite 1 -element set
{{(e * j2),j3},{(e * j2)}} is non empty finite V48() set
the multF of (n) . [(e * j2),j3] is set
j2 * j3 is Element of the carrier of (n)
the multF of (n) . (j2,j3) is Element of the carrier of (n)
[j2,j3] is non empty set
{j2,j3} is non empty finite set
{j2} is non empty trivial finite 1 -element set
{{j2,j3},{j2}} is non empty finite V48() set
the multF of (n) . [j2,j3] is set
e * (j2 * j3) is Element of the carrier of (n)
the multF of (n) . (e,(j2 * j3)) is Element of the carrier of (n)
[e,(j2 * j3)] is non empty set
{e,(j2 * j3)} is non empty finite set
{{e,(j2 * j3)},{e}} is non empty finite V48() set
the multF of (n) . [e,(j2 * j3)] is set
b is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal Element of Segm n
p is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal Element of Segm n
b + p 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
(b + p) mod n 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 V8() V12() ext-real non negative complex V40() integer V43() finite cardinal Element of Segm n
c7 + 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
(c7 + b) mod n 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 + b) mod n) + p 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 + b) mod n) + p) mod n 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 + b) + p 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 + b) + p) mod n 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 + (b + p) 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 + (b + p)) mod n 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 + ((b + p) mod n) 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 + ((b + p) mod n)) mod n 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
b is Element of the carrier of (n)
e is Element of the carrier of (n)
e * 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)) 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,b) is Element of the carrier of (n)
[e,b] is non empty set
{e,b} is non empty finite set
{e} is non empty trivial finite 1 -element set
{{e,b},{e}} is non empty finite V48() set
the multF of (n) . [e,b] is set
b * e is Element of the carrier of (n)
the multF of (n) . (b,e) is Element of the carrier of (n)
[b,e] is non empty set
{b,e} is non empty finite set
{b} is non empty trivial finite 1 -element set
{{b,e},{b}} is non empty finite V48() set
the multF of (n) . [b,e] is set
j2 is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal Element of Segm n
j3 is V8() V12() ext-real non negative complex V40() integer finite cardinal set
j2 + 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
j2 + 0 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 + 0) mod n 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
0 + 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
(0 + j2) mod n 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 mod n 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 Element of the carrier of (n)
e * c7 is Element of the carrier of (n)
the multF of (n) . (e,c7) is Element of the carrier of (n)
[e,c7] is non empty set
{e,c7} is non empty finite set
{{e,c7},{e}} is non empty finite V48() set
the multF of (n) . [e,c7] is set
c7 * e is Element of the carrier of (n)
the multF of (n) . (c7,e) is Element of the carrier of (n)
[c7,e] is non empty set
{c7,e} is non empty finite set
{c7} is non empty trivial finite 1 -element set
{{c7,e},{c7}} is non empty finite V48() set
the multF of (n) . [c7,e] is set
b is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal Element of Segm n
j2 + 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
(j2 + b) mod n 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
0 * n 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
(0 * n) mod n 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
b is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal Element of Segm n
j2 + 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
(j2 + b) mod n 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
n mod n 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
n mod n 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
(n mod n) + 0 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
((n mod n) + 0) mod n 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
0 * n 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
(0 * n) mod n 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
b is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal Element of Segm n
j2 + 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
(j2 + b) mod n 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
n mod n 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_ () is ext-real complex V40() integer V43() non being_of_order_0 Element of the carrier of ()
n is ext-real complex V40() integer V43() Element of the carrier of ()
a is ext-real complex V40() integer V43() Element of the carrier of ()
a * n is ext-real complex V40() integer V43() Element of the carrier of ()
the multF of () . (a,n) is ext-real complex V40() integer V43() Element of the carrier of ()
[a,n] is non empty set
{a,n} 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,n},{a}} is non empty finite V48() set
the multF of () . [a,n] is ext-real complex V40() integer set
a + n is ext-real complex V40() integer V43() Element of INT
b is ext-real complex V40() integer V43() Element of the carrier of ()
n * b is ext-real complex V40() integer V43() Element of the carrier of ()
the multF of () . (n,b) is ext-real complex V40() integer V43() Element of the carrier of ()
[n,b] is non empty set
{n,b} is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{n} is non empty trivial finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered set
{{n,b},{n}} is non empty finite V48() set
the multF of () . [n,b] is ext-real complex V40() integer set
n + b 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
(n) is non empty finite strict unital Group-like associative multMagma
Segm n is non empty 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([:(Segm n),(Segm n):], Segm n) V55() V56() V57() V58() Element of bool [:[:(Segm n),(Segm n):],(Segm n):]
[:(Segm n),(Segm n):] is Relation-like RAT -valued INT -valued non empty V55() V56() V57() V58() set
[:[:(Segm n),(Segm n):],(Segm n):] is Relation-like RAT -valued INT -valued non empty V55() V56() V57() V58() set
bool [:[:(Segm n),(Segm n):],(Segm n):] is non empty set
multMagma(# (Segm n),(n) #) is non empty strict multMagma
1_ (n) is non being_of_order_0 Element of the carrier of (n)
the carrier of (n) is non empty finite set
a is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal Element of Segm n
b is Element of the carrier of (n)
e is Element of the carrier of (n)
e * 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 finite 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 finite set
[:[: the carrier of (n), the carrier of (n):], the carrier of (n):] is Relation-like non empty finite set
bool [:[: the carrier of (n), the carrier of (n):], the carrier of (n):] is non empty finite V48() set
the multF of (n) . (e,b) is Element of the carrier of (n)
[e,b] is non empty set
{e,b} is non empty finite set
{e} is non empty trivial finite 1 -element set
{{e,b},{e}} is non empty finite V48() set
the multF of (n) . [e,b] is set
b * e is Element of the carrier of (n)
the multF of (n) . (b,e) is Element of the carrier of (n)
[b,e] is non empty set
{b,e} is non empty finite set
{b} is non empty trivial finite 1 -element set
{{b,e},{b}} is non empty finite V48() set
the multF of (n) . [b,e] is set
j2 is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal Element of Segm n
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
0 + 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
(0 + j3) mod n 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 + 0 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 + 0) mod n 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
n is ext-real complex V40() integer set
n is ext-real complex V40() integer V43() Element of the carrier of ()
n " is ext-real complex V40() integer V43() Element of the carrier of ()
- n is ext-real complex V40() integer V43() Element of INT
a is ext-real complex V40() integer V43() Element of the carrier of ()
n * a is ext-real complex V40() integer V43() Element of the carrier of ()
the multF of () . (n,a) is ext-real complex V40() integer V43() Element of the carrier of ()
[n,a] is non empty set
{n,a} is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{n} is non empty trivial finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered set
{{n,a},{n}} is non empty finite V48() set
the multF of () . [n,a] is ext-real complex V40() integer set
n + a is ext-real complex V40() integer V43() Element of INT
(1) is ext-real complex V40() integer V43() Element of the carrier of ()
n is V8() V12() ext-real non negative complex V40() integer finite cardinal set
(1) |^ n is ext-real complex V40() integer V43() Element of the carrier of ()
power () is Relation-like INT -valued Function-like V25([: the carrier of (),NAT:], the carrier of ()) V55() V56() V57() Element of bool [:[: the carrier of (),NAT:], the carrier of ():]
[: the carrier of (),NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V55() V56() V57() V58() set
[:[: the carrier of (),NAT:], the carrier of ():] is Relation-like RAT -valued INT -valued non empty non trivial non finite V55() V56() V57() set
bool [:[: the carrier of (),NAT:], the carrier of ():] is non empty non trivial non finite set
(power ()) . ((1),n) is set
[(1),n] is non empty set
{(1),n} is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{(1)} is non empty trivial finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered set
{{(1),n},{(1)}} is non empty finite V48() set
(power ()) . [(1),n] is ext-real complex V40() integer set
a is V8() V12() ext-real non negative complex V40() integer finite cardinal set
(1) |^ a is ext-real complex V40() integer V43() Element of the carrier of ()
(power ()) . ((1),a) is set
[(1),a] is non empty set
{(1),a} is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{{(1),a},{(1)}} is non empty finite V48() set
(power ()) . [(1),a] is ext-real complex V40() integer set
a + 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
(1) |^ (a + 1) is ext-real complex V40() integer V43() Element of the carrier of ()
(power ()) . ((1),(a + 1)) is set
[(1),(a + 1)] is non empty set
{(1),(a + 1)} is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{{(1),(a + 1)},{(1)}} is non empty finite V48() set
(power ()) . [(1),(a + 1)] is ext-real complex V40() integer set
((1) |^ a) * (1) is ext-real complex V40() integer V43() Element of the carrier of ()
the multF of () . (((1) |^ a),(1)) is ext-real complex V40() integer V43() Element of the carrier of ()
[((1) |^ a),(1)] is non empty set
{((1) |^ a),(1)} is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{((1) |^ a)} is non empty trivial finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered set
{{((1) |^ a),(1)},{((1) |^ a)}} is non empty finite V48() set
the multF of () . [((1) |^ a),(1)] is ext-real complex V40() integer set
((1) |^ a) + (1) is ext-real complex V40() integer V43() Element of INT
(1) |^ 0 is ext-real complex V40() integer V43() Element of the carrier of ()
(power ()) . ((1),0) is set
[(1),0] is non empty set
{(1),0} is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{{(1),0},{(1)}} is non empty finite V48() set
(power ()) . [(1),0] is ext-real complex V40() integer set
n is ext-real complex V40() integer set
(1) |^ n is ext-real complex V40() integer V43() Element of the carrier of ()
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 ext-real non positive complex V40() integer V43() Element of INT
b is ext-real complex V40() integer set
(1) |^ a is ext-real complex V40() integer V43() Element of the carrier of ()
power () is Relation-like INT -valued Function-like V25([: the carrier of (),NAT:], the carrier of ()) V55() V56() V57() Element of bool [:[: the carrier of (),NAT:], the carrier of ():]
[: the carrier of (),NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V55() V56() V57() V58() set
[:[: the carrier of (),NAT:], the carrier of ():] is Relation-like RAT -valued INT -valued non empty non trivial non finite V55() V56() V57() set
bool [:[: the carrier of (),NAT:], the carrier of ():] is non empty non trivial non finite set
(power ()) . ((1),a) is set
[(1),a] is non empty set
{(1),a} is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{(1)} is non empty trivial finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered set
{{(1),a},{(1)}} is non empty finite V48() set
(power ()) . [(1),a] is ext-real complex V40() integer set
((1) |^ a) " is ext-real complex V40() integer V43() Element of the carrier of ()
e is ext-real complex V40() integer V43() Element of the carrier of ()
e " is ext-real complex V40() integer V43() Element of the carrier of ()
{(1)} is non empty trivial finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered Element of bool the carrier of ()
bool the carrier of () is non empty set
gr {(1)} is non empty strict unital Group-like associative Subgroup of ()
n is ext-real complex V40() integer V43() Element of INT
a is ext-real complex V40() integer V43() Element of the carrier of ()
{a} is non empty trivial finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered Element of bool the carrier of ()
(Omega). () is non empty strict unital Group-like associative Subgroup of ()
multMagma(# the carrier of (), the multF of () #) is non empty strict unital Group-like associative multMagma
b is non empty unital Group-like associative Subgroup of ()
the carrier of b is non empty set
the carrier of ((Omega). ()) is non empty set
j2 is set
j3 is ext-real complex V40() integer set
e is Element of the carrier of b
e |^ j3 is Element of the carrier of b
a |^ j3 is ext-real complex V40() integer V43() Element of the carrier of ()
b is non empty strict unital Group-like associative Subgroup of ()
the carrier of b is non empty set
n is non empty unital Group-like associative multMagma
(1). n is non empty finite strict unital Group-like associative Subgroup of n
1_ n is non being_of_order_0 Element of the carrier of n
the carrier of n is non empty set
{(1_ n)} is non empty trivial finite 1 -element Element of bool the carrier of n
bool the carrier of n is non empty set
the carrier of ((1). n) is non empty finite set
a is Element of the carrier of ((1). n)
the multF of ((1). n) is Relation-like Function-like V25([: the carrier of ((1). n), the carrier of ((1). n):], the carrier of ((1). n)) associative having_a_unity finite Element of bool [:[: the carrier of ((1). n), the carrier of ((1). n):], the carrier of ((1). n):]
[: the carrier of ((1). n), the carrier of ((1). n):] is Relation-like non empty finite set
[:[: the carrier of ((1). n), the carrier of ((1). n):], the carrier of ((1). n):] is Relation-like non empty finite set
bool [:[: the carrier of ((1). n), the carrier of ((1). n):], the carrier of ((1). n):] is non empty finite V48() set
multMagma(# the carrier of ((1). n), the multF of ((1). n) #) is non empty strict unital Group-like associative multMagma
{a} is non empty trivial finite 1 -element Element of bool the carrier of ((1). n)
bool the carrier of ((1). n) is non empty finite V48() set
gr {a} is non empty finite strict unital Group-like associative Subgroup of (1). n
(Omega). ((1). n) is non empty finite strict unital Group-like associative Subgroup of (1). n
b is non empty finite unital Group-like associative Subgroup of (1). n
the carrier of b is non empty finite set
the carrier of ((Omega). ((1). n)) is non empty finite set
b is non empty finite strict unital Group-like associative Subgroup of (1). n
the carrier of b is non empty finite set
the non empty unital Group-like associative multMagma is non empty unital Group-like associative multMagma
(1). the non empty unital Group-like associative multMagma is non empty finite strict unital Group-like associative () Subgroup of the non empty unital Group-like associative multMagma
n is non empty unital Group-like associative multMagma
the carrier of n is non empty set
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
multMagma(# the carrier of n, the multF of n #) is non empty strict unital Group-like associative multMagma
a is Element of the carrier of n
{a} is non empty trivial finite 1 -element Element of bool the carrier of n
bool the carrier of n is non empty set
gr {a} is non empty strict unital Group-like associative Subgroup of n
b is Element of the carrier of n
b is Element of the carrier of n
a is Element of the carrier of n
{a} is non empty trivial finite 1 -element Element of bool the carrier of n
bool the carrier of n is non empty set
gr {a} is non empty strict unital Group-like associative Subgroup of n
b is Element of the carrier of n
e is ext-real complex V40() integer set
a |^ e 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
multMagma(# the carrier of n, the multF of n #) is non empty strict unital Group-like associative multMagma
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
b is Element of the carrier of n
e is ext-real complex V40() integer set
a |^ 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
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
j2 mod (card n) 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
(card n) - (j2 mod (card n)) is ext-real complex V40() integer V43() Element of INT
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
a |^ j3 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) . (a,j3) is set
[a,j3] is non empty set
{a,j3} is non empty finite set
{a} is non empty trivial finite 1 -element set
{{a,j3},{a}} is non empty finite V48() set
(power n) . [a,j3] is set
a |^ j2 is Element of the carrier of n
(power n) . (a,j2) is set
[a,j2] is non empty set
{a,j2} is non empty finite set
{{a,j2},{a}} is non empty finite V48() set
(power n) . [a,j2] is set
(a |^ j2) " is Element of the carrier of n
a is Element of the carrier of n
b is Element of the carrier of n
e is V8() V12() ext-real non negative complex V40() integer finite cardinal set
a |^ e 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) . (a,e) is set
[a,e] is non empty set
{a,e} is non empty finite set
{a} is non empty trivial finite 1 -element set
{{a,e},{a}} is non empty finite V48() set
(power n) . [a,e] is set
j2 is ext-real complex V40() integer set
a |^ 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
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
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 finite 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 finite set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like non empty finite set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty finite V48() set
multMagma(# the carrier of n, the multF of n #) is non empty strict unital Group-like associative multMagma
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 finite V48() set
gr {b} is non empty finite strict unital Group-like associative Subgroup of n
ord 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
a is non empty unital Group-like associative multMagma
card a is V8() cardinal set
the carrier of a is non empty set
card the carrier of a is V8() non empty cardinal set
a is Element of the carrier of n
ord 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
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 finite 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 finite set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like non empty finite set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty finite V48() set
multMagma(# the carrier of n, the multF of n #) is non empty strict unital Group-like associative multMagma
b is Element of the carrier of n
ord 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
{b} is non empty trivial finite 1 -element Element of bool the carrier of n
bool the carrier of n is non empty finite V48() set
gr {b} is non empty finite strict unital Group-like associative Subgroup of n
card (gr {b}) 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
the carrier of (gr {b}) is non empty finite set
card the carrier of (gr {b}) is V8() V12() non empty ext-real positive non negative complex V40() integer finite cardinal set
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 finite V48() set
gr {b} is non empty finite strict unital Group-like associative Subgroup of n
n is non empty finite unital Group-like associative multMagma
a is non empty finite strict unital Group-like associative Subgroup of n
card 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
the carrier of a is non empty finite set
card the carrier of a is V8() V12() non empty ext-real positive non negative complex V40() integer finite cardinal set
the carrier of n is non empty finite set
b is Element of the carrier of n
(1). n is non empty finite strict unital Group-like associative () Subgroup of n
1_ a is non being_of_order_0 Element of the carrier of a
e is Element of the carrier of a
j2 is V8() V12() ext-real non negative complex V40() integer finite cardinal set
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
1_ n is non being_of_order_0 Element of the carrier of n
j3 is V8() V12() ext-real non negative complex V40() integer finite cardinal set
b |^ j3 is Element of the carrier of n
(power n) . (b,j3) is set
[b,j3] is non empty set
{b,j3} is non empty finite set
{{b,j3},{b}} is non empty finite V48() set
(power n) . [b,j3] is set
j3 is V8() V12() ext-real non negative complex V40() integer finite cardinal set
b |^ j3 is Element of the carrier of n
(power n) . (b,j3) is set
[b,j3] is non empty set
{b,j3} is non empty finite set
{{b,j3},{b}} is non empty finite V48() set
(power n) . [b,j3] is set
c7 is Element of the carrier of a
b is Element of the carrier of a
p is V8() V12() ext-real non negative complex V40() integer finite cardinal set
b |^ p is Element of the carrier of n
(power n) . (b,p) is set
[b,p] is non empty set
{b,p} is non empty finite set
{{b,p},{b}} is non empty finite V48() set
(power n) . [b,p] is set
s is V8() V12() ext-real non negative complex V40() integer finite cardinal set
j3 * s 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
r is V8() V12() ext-real non negative complex V40() integer finite cardinal set
(j3 * s) + r 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
s 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 |^ s is Element of the carrier of a
power a is Relation-like Function-like V25([: the carrier of a,NAT:], the carrier of a) Element of bool [:[: the carrier of a,NAT:], the carrier of a:]
[: the carrier of a,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V55() V56() V57() V58() set
[:[: the carrier of a,NAT:], the carrier of a:] is Relation-like non empty non trivial non finite set
bool [:[: the carrier of a,NAT:], the carrier of a:] is non empty non trivial non finite set
(power a) . (c7,s) is set
[c7,s] is non empty set
{c7,s} is non empty finite set
{c7} is non empty trivial finite 1 -element set
{{c7,s},{c7}} is non empty finite V48() set
(power a) . [c7,s] is set
r 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
(b |^ j3) |^ s is Element of the carrier of n
(power n) . ((b |^ j3),s) is set
[(b |^ j3),s] is non empty set
{(b |^ j3),s} is non empty finite set
{(b |^ j3)} is non empty trivial finite 1 -element set
{{(b |^ j3),s},{(b |^ j3)}} is non empty finite V48() set
(power n) . [(b |^ j3),s] is set
(c7 |^ s) " is Element of the carrier of a
((b |^ j3) |^ s) " is Element of the carrier of n
j3 * s 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
b |^ (j3 * s) is Element of the carrier of n
(power n) . (b,(j3 * s)) is set
[b,(j3 * s)] is non empty set
{b,(j3 * s)} is non empty finite set
{{b,(j3 * s)},{b}} is non empty finite V48() set
(power n) . [b,(j3 * s)] is set
(b |^ (j3 * s)) " is Element of the carrier of n
b |^ r is Element of the carrier of n
(power n) . (b,r) is set
[b,r] is non empty set
{b,r} is non empty finite set
{{b,r},{b}} is non empty finite V48() set
(power n) . [b,r] is set
(b |^ (j3 * s)) * (b |^ r) 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 finite 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 finite set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like non empty finite set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty finite V48() set
the multF of n . ((b |^ (j3 * s)),(b |^ r)) is Element of the carrier of n
[(b |^ (j3 * s)),(b |^ r)] is non empty set
{(b |^ (j3 * s)),(b |^ r)} is non empty finite set
{(b |^ (j3 * s))} is non empty trivial finite 1 -element set
{{(b |^ (j3 * s)),(b |^ r)},{(b |^ (j3 * s))}} is non empty finite V48() set
the multF of n . [(b |^ (j3 * s)),(b |^ r)] is set
((b |^ (j3 * s)) ") * (b |^ p) is Element of the carrier of n
the multF of n . (((b |^ (j3 * s)) "),(b |^ p)) is Element of the carrier of n
[((b |^ (j3 * s)) "),(b |^ p)] is non empty set
{((b |^ (j3 * s)) "),(b |^ p)} is non empty finite set
{((b |^ (j3 * s)) ")} is non empty trivial finite 1 -element set
{{((b |^ (j3 * s)) "),(b |^ p)},{((b |^ (j3 * s)) ")}} is non empty finite V48() set
the multF of n . [((b |^ (j3 * s)) "),(b |^ p)] is set
((b |^ (j3 * s)) ") * (b |^ (j3 * s)) is Element of the carrier of n
the multF of n . (((b |^ (j3 * s)) "),(b |^ (j3 * s))) is Element of the carrier of n
[((b |^ (j3 * s)) "),(b |^ (j3 * s))] is non empty set
{((b |^ (j3 * s)) "),(b |^ (j3 * s))} is non empty finite set
{{((b |^ (j3 * s)) "),(b |^ (j3 * s))},{((b |^ (j3 * s)) ")}} is non empty finite V48() set
the multF of n . [((b |^ (j3 * s)) "),(b |^ (j3 * s))] is set
(((b |^ (j3 * s)) ") * (b |^ (j3 * s))) * (b |^ r) is Element of the carrier of n
the multF of n . ((((b |^ (j3 * s)) ") * (b |^ (j3 * s))),(b |^ r)) is Element of the carrier of n
[(((b |^ (j3 * s)) ") * (b |^ (j3 * s))),(b |^ r)] is non empty set
{(((b |^ (j3 * s)) ") * (b |^ (j3 * s))),(b |^ r)} is non empty finite set
{(((b |^ (j3 * s)) ") * (b |^ (j3 * s)))} is non empty trivial finite 1 -element set
{{(((b |^ (j3 * s)) ") * (b |^ (j3 * s))),(b |^ r)},{(((b |^ (j3 * s)) ") * (b |^ (j3 * s)))}} is non empty finite V48() set
the multF of n . [(((b |^ (j3 * s)) ") * (b |^ (j3 * s))),(b |^ r)] is set
1_ n is non being_of_order_0 Element of the carrier of n
(1_ n) * (b |^ r) is Element of the carrier of n
the multF of n . ((1_ n),(b |^ r)) is Element of the carrier of n
[(1_ n),(b |^ r)] is non empty set
{(1_ n),(b |^ r)} is non empty finite set
{(1_ n)} is non empty trivial finite 1 -element set
{{(1_ n),(b |^ r)},{(1_ n)}} is non empty finite V48() set
the multF of n . [(1_ n),(b |^ r)] is set
g is Element of the carrier of a
b is Element of the carrier of a
g * b is Element of the carrier of a
the multF of a is Relation-like Function-like V25([: the carrier of a, the carrier of a:], the carrier of a) associative having_a_unity finite Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]
[: the carrier of a, the carrier of a:] is Relation-like non empty finite set
[:[: the carrier of a, the carrier of a:], the carrier of a:] is Relation-like non empty finite set
bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty finite V48() set
the multF of a . (g,b) is Element of the carrier of a
[g,b] is non empty set
{g,b} is non empty finite set
{g} is non empty trivial finite 1 -element set
{{g,b},{g}} is non empty finite V48() set
the multF of a . [g,b] is set
(b |^ j3) |^ s is Element of the carrier of n
(power n) . ((b |^ j3),s) is set
[(b |^ j3),s] is non empty set
{(b |^ j3),s} is non empty finite set
{(b |^ j3)} is non empty trivial finite 1 -element set
{{(b |^ j3),s},{(b |^ j3)}} is non empty finite V48() set
(power n) . [(b |^ j3),s] is set
b is Element of the carrier of a
j3 is Element of the carrier of a
n is non empty finite strict unital Group-like associative multMagma
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
the carrier of n is non empty finite set
card the carrier of n is V8() V12() non empty ext-real positive non negative complex V40() integer finite cardinal set
b is Element of the carrier of n
ord 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
(1). n is non empty finite strict unital Group-like associative () Subgroup of n
the carrier of ((1). n) is non empty finite set
b is set
e is Element of the carrier of n
ord 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
1_ n is non being_of_order_0 Element of the carrier of n
{(1_ n)} is non empty trivial finite 1 -element Element of bool the carrier of n
bool the carrier of n is non empty finite V48() set
b is Element of the carrier of n
ord 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
n is V8() V12() non empty ext-real positive non negative complex V40() integer finite cardinal set
(n) is non empty finite strict unital Group-like associative multMagma
Segm n is non empty 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([:(Segm n),(Segm n):], Segm n) V55() V56() V57() V58() Element of bool [:[:(Segm n),(Segm n):],(Segm n):]
[:(Segm n),(Segm n):] is Relation-like RAT -valued INT -valued non empty V55() V56() V57() V58() set
[:[:(Segm n),(Segm n):],(Segm n):] is Relation-like RAT -valued INT -valued non empty V55() V56() V57() V58() set
bool [:[:(Segm n),(Segm n):],(Segm n):] is non empty set
multMagma(# (Segm n),(n) #) is non empty strict multMagma
the carrier of (n) is non empty finite set
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
0 + 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
1_ (n) is non being_of_order_0 Element of the carrier of (n)
{(1_ (n))} is non empty trivial finite 1 -element Element of bool the carrier of (n)
bool the carrier of (n) is non empty finite V48() set
(1). (n) is non empty finite strict unital Group-like associative () Subgroup of (n)
the carrier of ((1). (n)) is non empty finite set
a is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal Element of Segm n
b is Element of the carrier of (n)
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
j3 is V8() V12() ext-real non negative complex V40() integer finite cardinal set
b |^ j3 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,j3) is set
[b,j3] is non empty set
{b,j3} is non empty finite set
{b} is non empty trivial finite 1 -element set
{{b,j3},{b}} is non empty finite V48() set
(power (n)) . [b,j3] is set
j3 mod n 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 + 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 |^ (j3 + 1) is Element of the carrier of (n)
(power (n)) . (b,(j3 + 1)) is set
[b,(j3 + 1)] is non empty set
{b,(j3 + 1)} is non empty finite set
{{b,(j3 + 1)},{b}} is non empty finite V48() set
(power (n)) . [b,(j3 + 1)] is set
(j3 + 1) mod n 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
b |^ 1 is Element of the carrier of (n)
(power (n)) . (b,1) is set
[b,1] is non empty set
{b,1} is non empty finite set
{{b,1},{b}} is non empty finite V48() set
(power (n)) . [b,1] is set
(b |^ j3) * (b |^ 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 finite 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 finite set
[:[: the carrier of (n), the carrier of (n):], the carrier of (n):] is Relation-like non empty finite set
bool [:[: the carrier of (n), the carrier of (n):], the carrier of (n):] is non empty finite V48() set
the multF of (n) . ((b |^ j3),(b |^ 1)) is Element of the carrier of (n)
[(b |^ j3),(b |^ 1)] is non empty set
{(b |^ j3),(b |^ 1)} is non empty finite set
{(b |^ j3)} is non empty trivial finite 1 -element set
{{(b |^ j3),(b |^ 1)},{(b |^ j3)}} is non empty finite V48() set
the multF of (n) . [(b |^ j3),(b |^ 1)] is set
(b |^ j3) * b is Element of the carrier of (n)
the multF of (n) . ((b |^ j3),b) is Element of the carrier of (n)
[(b |^ j3),b] is non empty set
{(b |^ j3),b} is non empty finite set
{{(b |^ j3),b},{(b |^ j3)}} is non empty finite V48() set
the multF of (n) . [(b |^ j3),b] is set
c7 is V8() V12() ext-real non negative complex V40() integer V43() finite cardinal Element of Segm n
c7 + 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
(c7 + a) mod n 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
b |^ 0 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,0) is set
[b,0] is non empty set
{b,0} is non empty finite set
{b} is non empty trivial finite 1 -element set
{{b,0},{b}} is non empty finite V48() set
(power (n)) . [b,0] is set
1_ (n) is non being_of_order_0 Element of the carrier of (n)
0 mod n 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
b |^ j2 is Element of the carrier of (n)
(power (n)) . (b,j2) is set
[b,j2] is non empty set
{b,j2} is non empty finite set
{{b,j2},{b}} is non empty finite V48() set
(power (n)) . [b,j2] is set
j2 mod n 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 is ext-real complex V40() integer set
b |^ j3 is Element of the carrier of (n)
a 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
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 . (a,b) is Element of the carrier of n
[a,b] is non empty set
{a,b} is non empty finite set
{a} is non empty trivial finite 1 -element set
{{a,b},{a}} is non empty finite V48() set
the multF of n . [a,b] is set
b * a is Element of the carrier of n
the multF of n . (b,a) is Element of the carrier of n
[b,a] is non empty set
{b,a} is non empty finite set
{b} is non empty trivial finite 1 -element set
{{b,a},{b}} is non empty finite V48() set
the multF of n . [b,a] is set
e is Element of the carrier of n
j2 is ext-real complex V40() integer set
e |^ j2 is Element of the carrier of n
j3 is ext-real complex V40() integer set
e |^ j3 is Element of the carrier of n
j2 is ext-real complex V40() integer set
e is Element of the carrier of n
e |^ j2 is Element of the carrier of n
j3 is ext-real complex V40() integer set
e |^ j3 is Element of the carrier of n
j2 is ext-real complex V40() integer set
e is Element of the carrier of n
e |^ j2 is Element of the carrier of n
j3 is ext-real complex V40() integer set
e |^ j3 is Element of the carrier of n
j3 + j2 is ext-real complex V40() integer V43() Element of INT
e |^ (j3 + j2) is Element of the carrier of n
multMagma(# the carrier of (), the multF of () #) is non empty strict unital Group-like associative multMagma
n is V8() V12() non empty ext-real positive non negative complex V40() integer finite cardinal set
(n) is non empty finite strict unital Group-like associative multMagma
Segm n is non empty 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([:(Segm n),(Segm n):], Segm n) V55() V56() V57() V58() Element of bool [:[:(Segm n),(Segm n):],(Segm n):]
[:(Segm n),(Segm n):] is Relation-like RAT -valued INT -valued non empty V55() V56() V57() V58() set
[:[:(Segm n),(Segm n):],(Segm n):] is Relation-like RAT -valued INT -valued non empty V55() V56() V57() V58() set
bool [:[:(Segm n),(Segm n):],(Segm n):] is non empty set
multMagma(# (Segm n),(n) #) is non empty strict multMagma
the carrier of (n) is non empty finite set
a is Element of the carrier of (n)