:: GR_CY_1 semantic presentation

bool REAL is non empty non trivial non finite set

COMPLEX is non empty non trivial non finite complex-membered V71() set

is Relation-like non empty non trivial non finite V55() set
bool is non empty non trivial non finite set

bool is non empty non trivial non finite set
is Relation-like non empty non trivial non finite V55() V56() V57() set
bool is non empty non trivial non finite set
is Relation-like non empty non trivial non finite V55() V56() V57() set
bool is non empty non trivial non finite set
is Relation-like RAT -valued non empty non trivial non finite V55() V56() V57() set
bool is non empty non trivial non finite set
is Relation-like RAT -valued non empty non trivial non finite V55() V56() V57() set
bool is non empty non trivial non finite set

bool is non empty non trivial non finite set

bool is non empty non trivial non finite set
is Relation-like RAT -valued INT -valued non empty non trivial non finite V55() V56() V57() V58() set
is Relation-like RAT -valued INT -valued non empty non trivial non finite V55() V56() V57() V58() set
bool is non empty non trivial non finite 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 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 set

n . (a,b) is ext-real complex V40() integer V43() Element of INT
[a,b] is non empty 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

n . (a,b) is ext-real complex V40() integer V43() Element of INT
[a,b] is non empty 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
addint . (a,b) is ext-real complex V40() integer V43() Element of INT

bool is non empty non trivial non finite set

is Relation-like non empty non trivial non finite V55() set
bool is non empty non trivial non finite set

{ } is set
finSeg c7 is finite c7 -element Element of K107(NAT)
addint \$\$ ((finSeg c7),([#] (n,))) is ext-real complex V40() integer V43() Element of INT

addcomplex \$\$ ((finSeg c7),([#] (j2,))) is complex Element of COMPLEX

{ } is set
addint \$\$ ((),([#] (n,))) is ext-real complex V40() integer V43() Element of INT
addcomplex \$\$ ((),([#] (j2,))) is complex Element of COMPLEX

finSeg (b + 1) is non empty finite b + 1 -element Element of K107(NAT)
{ } is set
addint \$\$ ((finSeg (b + 1)),([#] (n,))) is ext-real complex V40() integer V43() Element of INT
addcomplex \$\$ ((finSeg (b + 1)),([#] (j2,))) is complex Element of COMPLEX
([#] (n,)) . (b + 1) is ext-real complex V40() integer V43() Element of INT

() \/ {.(b + 1).} is non empty finite Element of K107(NAT)
addint \$\$ ((() \/ {.(b + 1).}),([#] (n,))) is ext-real complex V40() integer V43() Element of INT
addint . ((addint \$\$ ((),([#] (n,)))),(([#] (n,)) . (b + 1))) is ext-real complex V40() integer V43() Element of INT
[(addint \$\$ ((),([#] (n,)))),(([#] (n,)) . (b + 1))] is non empty set
{(addint \$\$ ((),([#] (n,)))),(([#] (n,)) . (b + 1))} is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered set

{{(addint \$\$ ((),([#] (n,)))),(([#] (n,)) . (b + 1))},{(addint \$\$ ((),([#] (n,))))}} is non empty finite V48() set
addint . [(addint \$\$ ((),([#] (n,)))),(([#] (n,)) . (b + 1))] is ext-real complex V40() integer set
(addint \$\$ ((),([#] (n,)))) + (([#] (n,)) . (b + 1)) is ext-real complex V40() integer V43() Element of INT
([#] (j2,)) . (b + 1) is complex Element of COMPLEX
addcomplex . ((addcomplex \$\$ ((),([#] (j2,)))),(([#] (j2,)) . (b + 1))) is complex Element of COMPLEX
[(addcomplex \$\$ ((),([#] (j2,)))),(([#] (j2,)) . (b + 1))] is non empty set
{(addcomplex \$\$ ((),([#] (j2,)))),(([#] (j2,)) . (b + 1))} is non empty finite complex-membered set
{(addcomplex \$\$ ((),([#] (j2,))))} is non empty trivial finite 1 -element complex-membered set
{{(addcomplex \$\$ ((),([#] (j2,)))),(([#] (j2,)) . (b + 1))},{(addcomplex \$\$ ((),([#] (j2,))))}} is non empty finite V48() set
addcomplex . [(addcomplex \$\$ ((),([#] (j2,)))),(([#] (j2,)) . (b + 1))] is complex set
addcomplex \$\$ ((() \/ {.(b + 1).}),([#] (j2,))) is complex Element of COMPLEX

{ } is set

addint \$\$ ((),([#] (n,))) is ext-real complex V40() integer V43() Element of INT
addcomplex \$\$ ((),([#] (j2,))) is complex Element of COMPLEX

(()) is ext-real complex V40() integer V43() Element of INT

the carrier of n is non empty set
a is Element of the carrier of n

(len ()) -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 () } is set

{ } is set

{a} is non empty trivial finite 1 -element set

bool [:(Seg (len ())),{a}:] is non empty finite V48() set

Product (((len ()) |-> a) |^ ()) 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 ()) |-> a) |^ ()) is Element of the carrier of n
a |^ (()) is Element of the carrier of n

[:NAT, the carrier of n:] is Relation-like non empty non trivial non finite set
(<*> the carrier of n) |^ () 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

the carrier of n is non empty set
a is Element of the carrier of n

(len b) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b1 where b1 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of n * : len b1 = len b } is set

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

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

a |^ (b) is Element of the carrier of n

[1,e] is non empty set

{{1,e},{1}} is non empty finite V48() set

(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

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

[1,a] is non empty set
{1,a} is non empty finite set
{{1,a},{1}} is non empty finite V48() set

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

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

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

@ (@ e) is ext-real complex V40() integer V43() Element of INT

[1,(@ (@ e))] is non empty set

{{1,(@ (@ e))},{1}} is non empty finite V48() set
{[1,(@ (@ 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))} 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

[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

the carrier of n is non empty set
a is Element of the carrier of n

(len b) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b1 where b1 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of n * : len b1 = len b } is set

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

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

a |^ (b) is Element of the carrier of n

[1,e] is non empty set

{{1,e},{1}} is non empty finite V48() set

(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

{ } 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 ()) -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 () } is set

{ } is set

{a} is non empty trivial finite 1 -element set

bool [:(Seg (len ())),{a}:] is non empty finite V48() set

Product (((len ()) |-> a) |^ ()) 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 ()) |-> a) |^ ()) is Element of the carrier of n
a |^ (()) is Element of the carrier of n

(len b) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ 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

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

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

a |^ (b) is Element of the carrier of n

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

b |^ e is Element of the carrier of n

- 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

{ } is set

{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

rng j3 is finite set

{ } 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)}:]

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

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

{ } is set

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

rng j3 is finite set

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
() . (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
() . [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

{ } is set

[:(Seg j2),{b}:] is Relation-like finite set
bool [:(Seg j2),{b}:] is non empty finite V48() set

rng j3 is finite set

{ } 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)}:]

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

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

{ } is set

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

rng j3 is finite set

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

rng e is finite set

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

b |^ (j2) is Element of 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

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

e . j3 is set
((len e) |-> b) . j3 is set

(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

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

b |^ e is Element of the carrier of n

b |^ j2 is Element of the carrier of n

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 the carrier of n is V8() V12() non empty ext-real positive non negative complex V40() integer finite cardinal set

Seg ((card n) + 1) is non empty