:: GROUP_4 semantic presentation

REAL is non empty V46() set

NAT is non empty V35() V36() V37() V46() V51() V52() Element of bool REAL

bool REAL is non empty V46() set

{} is V1() non-empty empty-yielding V4( NAT ) Function-like one-to-one constant functional empty ext-real V35() V36() V37() V39() V40() V41() V42() V43() integer V46() V51() V53( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set

the V1() non-empty empty-yielding V4( NAT ) Function-like one-to-one constant functional empty ext-real V35() V36() V37() V39() V40() V41() V42() V43() integer V46() V51() V53( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set is V1() non-empty empty-yielding V4( NAT ) Function-like one-to-one constant functional empty ext-real V35() V36() V37() V39() V40() V41() V42() V43() integer V46() V51() V53( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set

COMPLEX is non empty V46() set

NAT is non empty V35() V36() V37() V46() V51() V52() set

bool NAT is non empty V46() set

bool NAT is non empty V46() set

K110(NAT) is V30() set

RAT is non empty V46() set

INT is non empty V46() set

[:COMPLEX,COMPLEX:] is V1() non empty V46() set

bool [:COMPLEX,COMPLEX:] is non empty V46() set

[:[:COMPLEX,COMPLEX:],COMPLEX:] is V1() non empty V46() set

bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty V46() set

[:REAL,REAL:] is V1() non empty V46() set

bool [:REAL,REAL:] is non empty V46() set

[:[:REAL,REAL:],REAL:] is V1() non empty V46() set

bool [:[:REAL,REAL:],REAL:] is non empty V46() set

[:RAT,RAT:] is V1() non empty V46() set

bool [:RAT,RAT:] is non empty V46() set

[:[:RAT,RAT:],RAT:] is V1() non empty V46() set

bool [:[:RAT,RAT:],RAT:] is non empty V46() set

[:INT,INT:] is V1() non empty V46() set

bool [:INT,INT:] is non empty V46() set

[:[:INT,INT:],INT:] is V1() non empty V46() set

bool [:[:INT,INT:],INT:] is non empty V46() set

[:NAT,NAT:] is V1() non empty V46() set

[:[:NAT,NAT:],NAT:] is V1() non empty V46() set

bool [:[:NAT,NAT:],NAT:] is non empty V46() set

1 is non empty ext-real positive V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

2 is non empty ext-real positive V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

3 is non empty ext-real positive V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

0 is V1() non-empty empty-yielding V4( NAT ) Function-like one-to-one constant functional empty ext-real V35() V36() V37() V39() V40() V41() V42() V43() integer V46() V51() V53( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT

Seg 1 is non empty trivial V46() V53(1) Element of bool NAT

{1} is non empty trivial V53(1) set

Seg 2 is non empty V46() V53(2) Element of bool NAT

{1,2} is non empty set

G is non empty set

L is V1() V4( NAT ) V5(G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of G

E is set

L - E is V1() V4( NAT ) Function-like V46() FinSequence-like FinSubsequence-like set

F

the carrier of F

bool the carrier of F

{ b

( b

meet { b

( b

L is non empty strict unital Group-like associative Subgroup of F

L is non empty strict unital Group-like associative Subgroup of F

carr L is Element of bool the carrier of F

the carrier of L is non empty set

A is Element of the carrier of F

E is Element of bool the carrier of F

H is set

A is Element of bool the carrier of F

H is non empty strict unital Group-like associative Subgroup of F

the carrier of H is non empty set

H is non empty unital Group-like associative Subgroup of F

the carrier of H is non empty set

A " is Element of the carrier of F

A is Element of the carrier of F

H is Element of the carrier of F

A is set

H is Element of bool the carrier of F

H3 is non empty strict unital Group-like associative Subgroup of F

the carrier of H3 is non empty set

H3 is non empty unital Group-like associative Subgroup of F

the carrier of H3 is non empty set

A * H is Element of the carrier of F

the multF of F

[: the carrier of F

[:[: the carrier of F

bool [:[: the carrier of F

the multF of F

A is set

H is Element of bool the carrier of F

A is non empty strict unital Group-like associative Subgroup of F

the carrier of A is non empty set

A is non empty unital Group-like associative Subgroup of F

the carrier of A is non empty set

1_ F

F

Subgroups F

G is set

L is set

L is non empty strict unital Group-like associative Subgroup of F

E is non empty unital Group-like associative Subgroup of F

G is ext-real V42() V43() integer set

G is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

L is non empty unital Group-like associative multMagma

the carrier of L is non empty set

E is Element of the carrier of L

E |^ G is Element of the carrier of L

A is non empty unital Group-like associative Subgroup of L

the carrier of A is non empty set

H is Element of the carrier of A

H |^ G is Element of the carrier of A

A is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

E |^ A is Element of the carrier of L

H |^ A is Element of the carrier of A

A + 1 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

E |^ (A + 1) is Element of the carrier of L

(E |^ A) * E is Element of the carrier of L

the multF of L is V1() Function-like quasi_total associative having_a_unity Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]

[: the carrier of L, the carrier of L:] is V1() non empty set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is V1() non empty set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set

the multF of L . ((E |^ A),E) is Element of the carrier of L

(H |^ A) * H is Element of the carrier of A

the multF of A is V1() Function-like quasi_total associative having_a_unity Element of bool [:[: the carrier of A, the carrier of A:], the carrier of A:]

[: the carrier of A, the carrier of A:] is V1() non empty set

[:[: the carrier of A, the carrier of A:], the carrier of A:] is V1() non empty set

bool [:[: the carrier of A, the carrier of A:], the carrier of A:] is non empty set

the multF of A . ((H |^ A),H) is Element of the carrier of A

H |^ (A + 1) is Element of the carrier of A

E |^ 0 is Element of the carrier of L

1_ L is non being_of_order_0 Element of the carrier of L

1_ A is non being_of_order_0 Element of the carrier of A

H |^ 0 is Element of the carrier of A

G is ext-real V42() V43() integer set

L is non empty unital Group-like associative multMagma

the carrier of L is non empty set

E is Element of the carrier of L

E |^ G is Element of the carrier of L

A is non empty unital Group-like associative Subgroup of L

the carrier of A is non empty set

H is Element of the carrier of A

H |^ G is Element of the carrier of A

abs G is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

E |^ (abs G) is Element of the carrier of L

H |^ (abs G) is Element of the carrier of A

abs G is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

E |^ (abs G) is Element of the carrier of L

H |^ (abs G) is Element of the carrier of A

(E |^ (abs G)) " is Element of the carrier of L

(H |^ (abs G)) " is Element of the carrier of A

G is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

L is non empty unital Group-like associative multMagma

the carrier of L is non empty set

E is Element of the carrier of L

E |^ G is Element of the carrier of L

A is non empty unital Group-like associative Subgroup of L

H is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

H + 1 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

E |^ (H + 1) is Element of the carrier of L

E |^ H is Element of the carrier of L

(E |^ H) * E is Element of the carrier of L

the multF of L is V1() Function-like quasi_total associative having_a_unity Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]

[: the carrier of L, the carrier of L:] is V1() non empty set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is V1() non empty set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set

the multF of L . ((E |^ H),E) is Element of the carrier of L

E |^ 0 is Element of the carrier of L

1_ L is non being_of_order_0 Element of the carrier of L

G is ext-real V42() V43() integer set

L is non empty unital Group-like associative multMagma

the carrier of L is non empty set

E is Element of the carrier of L

E |^ G is Element of the carrier of L

A is non empty unital Group-like associative Subgroup of L

abs G is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

E |^ (abs G) is Element of the carrier of L

abs G is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

E |^ (abs G) is Element of the carrier of L

(E |^ (abs G)) " is Element of the carrier of L

G is non empty multMagma

the carrier of G is non empty set

L is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

the multF of G is V1() Function-like quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is V1() non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is V1() non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

the multF of G "**" L is Element of the carrier of G

G is non empty unital associative multMagma

the carrier of G is non empty set

L is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

E is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

L ^ E is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

(G,(L ^ E)) is Element of the carrier of G

the multF of G is V1() Function-like quasi_total associative having_a_unity Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is V1() non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is V1() non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

the multF of G "**" (L ^ E) is Element of the carrier of G

(G,L) is Element of the carrier of G

the multF of G "**" L is Element of the carrier of G

(G,E) is Element of the carrier of G

the multF of G "**" E is Element of the carrier of G

(G,L) * (G,E) is Element of the carrier of G

the multF of G . ((G,L),(G,E)) is Element of the carrier of G

G is non empty unital multMagma

the carrier of G is non empty set

L is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

E is Element of the carrier of G

<*E*> is V1() V4( NAT ) V5( the carrier of G) Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of G

L ^ <*E*> is V1() V4( NAT ) V5( the carrier of G) Function-like non empty V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

(G,(L ^ <*E*>)) is Element of the carrier of G

the multF of G is V1() Function-like quasi_total having_a_unity Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is V1() non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is V1() non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

the multF of G "**" (L ^ <*E*>) is Element of the carrier of G

(G,L) is Element of the carrier of G

the multF of G "**" L is Element of the carrier of G

(G,L) * E is Element of the carrier of G

the multF of G . ((G,L),E) is Element of the carrier of G

G is non empty unital associative multMagma

the carrier of G is non empty set

E is Element of the carrier of G

<*E*> is V1() V4( NAT ) V5( the carrier of G) Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of G

L is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

<*E*> ^ L is V1() V4( NAT ) V5( the carrier of G) Function-like non empty V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

(G,(<*E*> ^ L)) is Element of the carrier of G

the multF of G is V1() Function-like quasi_total associative having_a_unity Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is V1() non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is V1() non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

the multF of G "**" (<*E*> ^ L) is Element of the carrier of G

(G,L) is Element of the carrier of G

the multF of G "**" L is Element of the carrier of G

E * (G,L) is Element of the carrier of G

the multF of G . (E,(G,L)) is Element of the carrier of G

G is non empty unital multMagma

the carrier of G is non empty set

<*> the carrier of G is V1() non-empty empty-yielding V4( NAT ) V5( the carrier of G) Function-like one-to-one constant functional empty proper ext-real V35() V36() V37() V39() V40() V41() V42() V43() integer V46() V51() V53( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of the carrier of G

[:NAT, the carrier of G:] is V1() non empty V46() set

(G,(<*> the carrier of G)) is Element of the carrier of G

the multF of G is V1() Function-like quasi_total having_a_unity Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is V1() non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is V1() non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

the multF of G "**" (<*> the carrier of G) is Element of the carrier of G

1_ G is Element of the carrier of G

len (<*> the carrier of G) is V1() non-empty empty-yielding V4( NAT ) Function-like one-to-one constant functional empty ext-real V35() V36() V37() V39() V40() V41() V42() V43() integer V46() V51() V53( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT

the_unity_wrt the multF of G is Element of the carrier of G

G is non empty multMagma

the carrier of G is non empty set

L is Element of the carrier of G

<*L*> is V1() V4( NAT ) V5( the carrier of G) Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of G

(G,<*L*>) is Element of the carrier of G

the multF of G is V1() Function-like quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is V1() non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is V1() non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

the multF of G "**" <*L*> is Element of the carrier of G

G is non empty multMagma

the carrier of G is non empty set

L is Element of the carrier of G

E is Element of the carrier of G

<*L,E*> is V1() V4( NAT ) V5( the carrier of G) Function-like non empty V46() V53(2) FinSequence-like FinSubsequence-like FinSequence of the carrier of G

(G,<*L,E*>) is Element of the carrier of G

the multF of G is V1() Function-like quasi_total Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is V1() non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is V1() non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

the multF of G "**" <*L,E*> is Element of the carrier of G

L * E is Element of the carrier of G

the multF of G . (L,E) is Element of the carrier of G

G is non empty unital Group-like associative multMagma

the carrier of G is non empty set

L is Element of the carrier of G

E is Element of the carrier of G

L * E is Element of the carrier of G

the multF of G is V1() Function-like quasi_total associative having_a_unity Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is V1() non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is V1() non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

the multF of G . (L,E) is Element of the carrier of G

A is Element of the carrier of G

<*L,E,A*> is V1() V4( NAT ) V5( the carrier of G) Function-like non empty V46() V53(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of G

(G,<*L,E,A*>) is Element of the carrier of G

the multF of G "**" <*L,E,A*> is Element of the carrier of G

(L * E) * A is Element of the carrier of G

the multF of G . ((L * E),A) is Element of the carrier of G

E * A is Element of the carrier of G

the multF of G . (E,A) is Element of the carrier of G

L * (E * A) is Element of the carrier of G

the multF of G . (L,(E * A)) is Element of the carrier of G

<*L*> is V1() V4( NAT ) V5( the carrier of G) Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of G

(G,<*L*>) is Element of the carrier of G

the multF of G "**" <*L*> is Element of the carrier of G

<*A*> is V1() V4( NAT ) V5( the carrier of G) Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of G

(G,<*A*>) is Element of the carrier of G

the multF of G "**" <*A*> is Element of the carrier of G

<*L,E*> is V1() V4( NAT ) V5( the carrier of G) Function-like non empty V46() V53(2) FinSequence-like FinSubsequence-like FinSequence of the carrier of G

(G,<*L,E*>) is Element of the carrier of G

the multF of G "**" <*L,E*> is Element of the carrier of G

<*E,A*> is V1() V4( NAT ) V5( the carrier of G) Function-like non empty V46() V53(2) FinSequence-like FinSubsequence-like FinSequence of the carrier of G

(G,<*E,A*>) is Element of the carrier of G

the multF of G "**" <*E,A*> is Element of the carrier of G

<*L*> ^ <*E,A*> is V1() V4( NAT ) V5( the carrier of G) Function-like non empty V46() V53(1 + 2) FinSequence-like FinSubsequence-like FinSequence of the carrier of G

1 + 2 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

<*L,E*> ^ <*A*> is V1() V4( NAT ) V5( the carrier of G) Function-like non empty V46() V53(2 + 1) FinSequence-like FinSubsequence-like FinSequence of the carrier of G

2 + 1 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

G is non empty unital Group-like associative multMagma

the carrier of G is non empty set

L is Element of the carrier of G

0 |-> L is V1() non-empty empty-yielding V4( NAT ) V5( the carrier of G) Function-like one-to-one constant functional empty ext-real V35() V36() V37() V39() V40() V41() V42() V43() integer V46() V51() V53( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered Element of 0 -tuples_on the carrier of G

0 -tuples_on the carrier of G is functional non empty FinSequence-membered FinSequenceSet of the carrier of G

(G,(0 |-> L)) is Element of the carrier of G

the multF of G is V1() Function-like quasi_total associative having_a_unity Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is V1() non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is V1() non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

the multF of G "**" (0 |-> L) is Element of the carrier of G

<*> the carrier of G is V1() non-empty empty-yielding V4( NAT ) V5( the carrier of G) Function-like one-to-one constant functional empty proper ext-real V35() V36() V37() V39() V40() V41() V42() V43() integer V46() V51() V53( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of the carrier of G

[:NAT, the carrier of G:] is V1() non empty V46() set

(G,(<*> the carrier of G)) is Element of the carrier of G

the multF of G "**" (<*> the carrier of G) is Element of the carrier of G

1_ G is non being_of_order_0 Element of the carrier of G

L |^ 0 is Element of the carrier of G

G is non empty unital Group-like associative multMagma

the carrier of G is non empty set

E is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

L is Element of the carrier of G

E |-> L is V1() V4( NAT ) V5( the carrier of G) Function-like V46() V53(E) FinSequence-like FinSubsequence-like Element of E -tuples_on the carrier of G

E -tuples_on the carrier of G is functional non empty FinSequence-membered FinSequenceSet of the carrier of G

(G,(E |-> L)) is Element of the carrier of G

the multF of G is V1() Function-like quasi_total associative having_a_unity Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is V1() non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is V1() non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

the multF of G "**" (E |-> L) is Element of the carrier of G

L |^ E is Element of the carrier of G

E + 1 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

(E + 1) |-> L is V1() V4( NAT ) V5( the carrier of G) Function-like V46() V53(E + 1) FinSequence-like FinSubsequence-like Element of (E + 1) -tuples_on the carrier of G

(E + 1) -tuples_on the carrier of G is functional non empty FinSequence-membered FinSequenceSet of the carrier of G

(G,((E + 1) |-> L)) is Element of the carrier of G

the multF of G "**" ((E + 1) |-> L) is Element of the carrier of G

<*L*> is V1() V4( NAT ) V5( the carrier of G) Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of G

(E |-> L) ^ <*L*> is V1() V4( NAT ) V5( the carrier of G) Function-like non empty V46() V53(E + 1) FinSequence-like FinSubsequence-like FinSequence of the carrier of G

E + 1 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

(G,((E |-> L) ^ <*L*>)) is Element of the carrier of G

the multF of G "**" ((E |-> L) ^ <*L*>) is Element of the carrier of G

(G,<*L*>) is Element of the carrier of G

the multF of G "**" <*L*> is Element of the carrier of G

(G,(E |-> L)) * (G,<*L*>) is Element of the carrier of G

the multF of G . ((G,(E |-> L)),(G,<*L*>)) is Element of the carrier of G

(L |^ E) * L is Element of the carrier of G

the multF of G . ((L |^ E),L) is Element of the carrier of G

L |^ (E + 1) is Element of the carrier of G

G is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

L is non empty unital Group-like associative multMagma

the carrier of L is non empty set

E is Element of the carrier of L

G |-> E is V1() V4( NAT ) V5( the carrier of L) Function-like V46() V53(G) FinSequence-like FinSubsequence-like Element of G -tuples_on the carrier of L

G -tuples_on the carrier of L is functional non empty FinSequence-membered FinSequenceSet of the carrier of L

(L,(G |-> E)) is Element of the carrier of L

the multF of L is V1() Function-like quasi_total associative having_a_unity Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]

[: the carrier of L, the carrier of L:] is V1() non empty set

[:[: the carrier of L, the carrier of L:], the carrier of L:] is V1() non empty set

bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set

the multF of L "**" (G |-> E) is Element of the carrier of L

E |^ G is Element of the carrier of L

A is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

A |-> E is V1() V4( NAT ) V5( the carrier of L) Function-like V46() V53(A) FinSequence-like FinSubsequence-like Element of A -tuples_on the carrier of L

A -tuples_on the carrier of L is functional non empty FinSequence-membered FinSequenceSet of the carrier of L

(L,(A |-> E)) is Element of the carrier of L

the multF of L "**" (A |-> E) is Element of the carrier of L

E |^ A is Element of the carrier of L

A + 1 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

(A + 1) |-> E is V1() V4( NAT ) V5( the carrier of L) Function-like V46() V53(A + 1) FinSequence-like FinSubsequence-like Element of (A + 1) -tuples_on the carrier of L

(A + 1) -tuples_on the carrier of L is functional non empty FinSequence-membered FinSequenceSet of the carrier of L

(L,((A + 1) |-> E)) is Element of the carrier of L

the multF of L "**" ((A + 1) |-> E) is Element of the carrier of L

E |^ (A + 1) is Element of the carrier of L

0 |-> E is V1() non-empty empty-yielding V4( NAT ) V5( the carrier of L) Function-like one-to-one constant functional empty ext-real V35() V36() V37() V39() V40() V41() V42() V43() integer V46() V51() V53( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered Element of 0 -tuples_on the carrier of L

0 -tuples_on the carrier of L is functional non empty FinSequence-membered FinSequenceSet of the carrier of L

(L,(0 |-> E)) is Element of the carrier of L

the multF of L "**" (0 |-> E) is Element of the carrier of L

E |^ 0 is Element of the carrier of L

G is non empty unital Group-like associative multMagma

the carrier of G is non empty set

1_ G is non being_of_order_0 Element of the carrier of G

{(1_ G)} is non empty trivial V53(1) Element of bool the carrier of G

bool the carrier of G is non empty set

L is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

( the carrier of G,L,{(1_ G)}) is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

(G,( the carrier of G,L,{(1_ G)})) is Element of the carrier of G

the multF of G is V1() Function-like quasi_total associative having_a_unity Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is V1() non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is V1() non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

the multF of G "**" ( the carrier of G,L,{(1_ G)}) is Element of the carrier of G

(G,L) is Element of the carrier of G

the multF of G "**" L is Element of the carrier of G

E is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

( the carrier of G,E,{(1_ G)}) is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

(G,( the carrier of G,E,{(1_ G)})) is Element of the carrier of G

the multF of G "**" ( the carrier of G,E,{(1_ G)}) is Element of the carrier of G

(G,E) is Element of the carrier of G

the multF of G "**" E is Element of the carrier of G

A is Element of the carrier of G

<*A*> is V1() V4( NAT ) V5( the carrier of G) Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of G

E ^ <*A*> is V1() V4( NAT ) V5( the carrier of G) Function-like non empty V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

( the carrier of G,(E ^ <*A*>),{(1_ G)}) is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

(G,( the carrier of G,(E ^ <*A*>),{(1_ G)})) is Element of the carrier of G

the multF of G "**" ( the carrier of G,(E ^ <*A*>),{(1_ G)}) is Element of the carrier of G

(G,(E ^ <*A*>)) is Element of the carrier of G

the multF of G "**" (E ^ <*A*>) is Element of the carrier of G

( the carrier of G,<*A*>,{(1_ G)}) is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

( the carrier of G,E,{(1_ G)}) ^ ( the carrier of G,<*A*>,{(1_ G)}) is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

(G,(( the carrier of G,E,{(1_ G)}) ^ ( the carrier of G,<*A*>,{(1_ G)}))) is Element of the carrier of G

the multF of G "**" (( the carrier of G,E,{(1_ G)}) ^ ( the carrier of G,<*A*>,{(1_ G)})) is Element of the carrier of G

(G,( the carrier of G,<*A*>,{(1_ G)})) is Element of the carrier of G

the multF of G "**" ( the carrier of G,<*A*>,{(1_ G)}) is Element of the carrier of G

(G,E) * (G,( the carrier of G,<*A*>,{(1_ G)})) is Element of the carrier of G

the multF of G . ((G,E),(G,( the carrier of G,<*A*>,{(1_ G)}))) is Element of the carrier of G

<*> the carrier of G is V1() non-empty empty-yielding V4( NAT ) V5( the carrier of G) Function-like one-to-one constant functional empty proper ext-real V35() V36() V37() V39() V40() V41() V42() V43() integer V46() V51() V53( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of the carrier of G

[:NAT, the carrier of G:] is V1() non empty V46() set

<*> the carrier of G is V1() non-empty empty-yielding V4( NAT ) V5( the carrier of G) Function-like one-to-one constant functional empty proper ext-real V35() V36() V37() V39() V40() V41() V42() V43() integer V46() V51() V53( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of the carrier of G

[:NAT, the carrier of G:] is V1() non empty V46() set

( the carrier of G,(<*> the carrier of G),{(1_ G)}) is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

(G,( the carrier of G,(<*> the carrier of G),{(1_ G)})) is Element of the carrier of G

the multF of G "**" ( the carrier of G,(<*> the carrier of G),{(1_ G)}) is Element of the carrier of G

(G,(<*> the carrier of G)) is Element of the carrier of G

the multF of G "**" (<*> the carrier of G) is Element of the carrier of G

G is V1() V4( NAT ) Function-like V46() FinSequence-like FinSubsequence-like set

dom G is Element of bool NAT

len G is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

L is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

(len G) - L is ext-real V42() V43() integer set

((len G) - L) + 1 is ext-real V42() V43() integer set

0 - ((len G) - L) is ext-real V42() V43() integer set

L - (len G) is ext-real V42() V43() integer set

(len G) + 1 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

E is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

E - 1 is ext-real V42() V43() integer set

(E - 1) - L is ext-real V42() V43() integer set

((len G) - L) - 1 is ext-real V42() V43() integer set

L + 1 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

E - (L + 1) is ext-real V42() V43() integer set

(len G) - (L + 1) is ext-real V42() V43() integer set

L + 0 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

0 + 1 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

G is non empty unital Group-like associative multMagma

the carrier of G is non empty set

L is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

len L is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

dom L is Element of bool NAT

(G,L) is Element of the carrier of G

the multF of G is V1() Function-like quasi_total associative having_a_unity Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is V1() non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is V1() non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

the multF of G "**" L is Element of the carrier of G

E is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

len E is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

(G,E) is Element of the carrier of G

the multF of G "**" E is Element of the carrier of G

(G,E) " is Element of the carrier of G

A is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

A + 1 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

H is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

len H is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

dom H is Element of bool NAT

(G,H) is Element of the carrier of G

the multF of G "**" H is Element of the carrier of G

A is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

len A is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

(G,A) is Element of the carrier of G

the multF of G "**" A is Element of the carrier of G

(G,A) " is Element of the carrier of G

Seg A is V46() V53(A) Element of bool NAT

H | (Seg A) is V1() V4( NAT ) V4( Seg A) V4( NAT ) V5( the carrier of G) Function-like FinSubsequence-like Element of bool [:NAT, the carrier of G:]

[:NAT, the carrier of G:] is V1() non empty V46() set

bool [:NAT, the carrier of G:] is non empty V46() set

H is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

len H is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

H3 is V1() V4( NAT ) Function-like V46() FinSequence-like FinSubsequence-like set

len H3 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

dom H3 is Element of bool NAT

dom H is Element of bool NAT

rng H3 is set

H2 is set

F1 is set

H3 . F1 is set

I1 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

I1 + 1 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

dom A is Element of bool NAT

A . (I1 + 1) is set

rng A is set

rng H is set

H . (A + 1) is set

H2 is Element of the carrier of G

<*H2*> is V1() V4( NAT ) V5( the carrier of G) Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of G

H ^ <*H2*> is V1() V4( NAT ) V5( the carrier of G) Function-like non empty V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

F1 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

H2 " is Element of the carrier of G

<*(H2 ")*> is V1() V4( NAT ) V5( the carrier of G) Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of G

dom <*(H2 ")*> is non empty trivial V53(1) Element of bool NAT

{1} is non empty trivial V53(1) Element of bool NAT

(len H) - (len H) is ext-real V42() V43() integer set

((len H) - (len H)) + 1 is ext-real V42() V43() integer set

A . (((len H) - (len H)) + 1) is set

H /. (len H) is Element of the carrier of G

(H /. (len H)) " is Element of the carrier of G

A . F1 is set

<*(H2 ")*> . F1 is set

I1 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

(len H) - I1 is ext-real V42() V43() integer set

((len H) - I1) + 1 is ext-real V42() V43() integer set

i is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

i + 1 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

(len H) - I1 is ext-real V42() V43() integer set

((len H) - I1) + 1 is ext-real V42() V43() integer set

F1 is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

F1 . i is set

A . (i + 1) is set

H /. I1 is Element of the carrier of G

H . I1 is set

H . I1 is set

H /. I1 is Element of the carrier of G

F1 . (((len H) - I1) + 1) is set

(H /. I1) " is Element of the carrier of G

(G,H) is Element of the carrier of G

the multF of G "**" H is Element of the carrier of G

(G,F1) is Element of the carrier of G

the multF of G "**" F1 is Element of the carrier of G

(G,F1) " is Element of the carrier of G

len <*(H2 ")*> is non empty ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

I1 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

dom F1 is Element of bool NAT

(len <*(H2 ")*>) + I1 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

A . ((len <*(H2 ")*>) + I1) is set

F1 . I1 is set

len F1 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

(len <*(H2 ")*>) + (len F1) is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

<*(H2 ")*> ^ F1 is V1() V4( NAT ) V5( the carrier of G) Function-like non empty V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

(H2 ") * (G,F1) is Element of the carrier of G

the multF of G . ((H2 "),(G,F1)) is Element of the carrier of G

(G,H) " is Element of the carrier of G

(H2 ") * ((G,H) ") is Element of the carrier of G

the multF of G . ((H2 "),((G,H) ")) is Element of the carrier of G

(G,H) * H2 is Element of the carrier of G

the multF of G . ((G,H),H2) is Element of the carrier of G

((G,H) * H2) " is Element of the carrier of G

A is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

len A is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

dom A is Element of bool NAT

(G,A) is Element of the carrier of G

the multF of G "**" A is Element of the carrier of G

H is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

len H is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

(G,H) is Element of the carrier of G

the multF of G "**" H is Element of the carrier of G

(G,H) " is Element of the carrier of G

<*> the carrier of G is V1() non-empty empty-yielding V4( NAT ) V5( the carrier of G) Function-like one-to-one constant functional empty proper ext-real V35() V36() V37() V39() V40() V41() V42() V43() integer V46() V51() V53( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of the carrier of G

[:NAT, the carrier of G:] is V1() non empty V46() set

1_ G is non being_of_order_0 Element of the carrier of G

G is non empty unital Group-like associative multMagma

the carrier of G is non empty set

L is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

dom L is Element of bool NAT

[:(dom L),(dom L):] is V1() set

bool [:(dom L),(dom L):] is non empty set

(G,L) is Element of the carrier of G

the multF of G is V1() Function-like quasi_total associative having_a_unity Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is V1() non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is V1() non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

the multF of G "**" L is Element of the carrier of G

E is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

(G,E) is Element of the carrier of G

the multF of G "**" E is Element of the carrier of G

H is V1() Function-like quasi_total bijective Element of bool [:(dom L),(dom L):]

L * H is V1() V5( the carrier of G) Function-like Element of bool [:(dom L), the carrier of G:]

[:(dom L), the carrier of G:] is V1() set

bool [:(dom L), the carrier of G:] is non empty set

G is non empty unital Group-like associative multMagma

the carrier of G is non empty set

L is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

rng L is set

(G,L) is Element of the carrier of G

the multF of G is V1() Function-like quasi_total associative having_a_unity Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is V1() non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is V1() non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

the multF of G "**" L is Element of the carrier of G

E is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

rng E is set

(G,E) is Element of the carrier of G

the multF of G "**" E is Element of the carrier of G

G is non empty unital Group-like associative multMagma

the carrier of G is non empty set

L is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

len L is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

dom L is Element of bool NAT

(G,L) is Element of the carrier of G

the multF of G is V1() Function-like quasi_total associative having_a_unity Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is V1() non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is V1() non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

the multF of G "**" L is Element of the carrier of G

E is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

len E is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

(G,E) is Element of the carrier of G

the multF of G "**" E is Element of the carrier of G

A is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

len A is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

(G,A) is Element of the carrier of G

the multF of G "**" A is Element of the carrier of G

(G,E) * (G,A) is Element of the carrier of G

the multF of G . ((G,E),(G,A)) is Element of the carrier of G

dom A is Element of bool NAT

Seg (len A) is V46() V53( len A) Element of bool NAT

dom E is Element of bool NAT

Seg (len E) is V46() V53( len E) Element of bool NAT

Seg (len L) is V46() V53( len L) Element of bool NAT

A is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

L . A is set

E /. A is Element of the carrier of G

A /. A is Element of the carrier of G

(E /. A) * (A /. A) is Element of the carrier of G

the multF of G . ((E /. A),(A /. A)) is Element of the carrier of G

E . A is set

the multF of G . ((E . A),(A /. A)) is set

A . A is set

the multF of G . ((E . A),(A . A)) is set

G is non empty unital Group-like associative multMagma

the carrier of G is non empty set

L is non empty unital Group-like associative Subgroup of G

carr L is Element of bool the carrier of G

bool the carrier of G is non empty set

the carrier of L is non empty set

E is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

rng E is set

(G,E) is Element of the carrier of G

the multF of G is V1() Function-like quasi_total associative having_a_unity Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is V1() non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is V1() non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

the multF of G "**" E is Element of the carrier of G

A is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

rng A is set

(G,A) is Element of the carrier of G

the multF of G "**" A is Element of the carrier of G

H is Element of the carrier of G

<*H*> is V1() V4( NAT ) V5( the carrier of G) Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of G

A ^ <*H*> is V1() V4( NAT ) V5( the carrier of G) Function-like non empty V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

rng (A ^ <*H*>) is non empty set

(G,(A ^ <*H*>)) is Element of the carrier of G

the multF of G "**" (A ^ <*H*>) is Element of the carrier of G

(G,A) * H is Element of the carrier of G

the multF of G . ((G,A),H) is Element of the carrier of G

rng <*H*> is non empty trivial V53(1) set

{H} is non empty trivial V53(1) Element of bool the carrier of G

<*> the carrier of G is V1() non-empty empty-yielding V4( NAT ) V5( the carrier of G) Function-like one-to-one constant functional empty proper ext-real V35() V36() V37() V39() V40() V41() V42() V43() integer V46() V51() V53( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of the carrier of G

[:NAT, the carrier of G:] is V1() non empty V46() set

rng (<*> the carrier of G) is V1() non-empty empty-yielding V4( NAT ) Function-like one-to-one constant functional empty trivial with_non-empty_elements ext-real V35() V36() V37() V39() V40() V41() V42() V43() integer V46() V51() V53( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set

(G,(<*> the carrier of G)) is Element of the carrier of G

the multF of G "**" (<*> the carrier of G) is Element of the carrier of G

1_ G is non being_of_order_0 Element of the carrier of G

G is non empty unital Group-like associative multMagma

the carrier of G is non empty set

E is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

len E is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

dom E is Element of bool NAT

L is V1() V4( NAT ) V5( INT ) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of INT

A is V1() V4( NAT ) Function-like V46() FinSequence-like FinSubsequence-like set

len A is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

dom A is Element of bool NAT

rng A is set

H is set

A is set

A . A is set

H is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

L /. H is ext-real V42() V43() integer Element of INT

((L /. H)) is ext-real V42() V43() integer Element of INT

E /. H is Element of the carrier of G

(E /. H) |^ ((L /. H)) is Element of the carrier of G

H is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

len H is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

A is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

H . A is set

L /. A is ext-real V42() V43() integer Element of INT

((L /. A)) is ext-real V42() V43() integer Element of INT

E /. A is Element of the carrier of G

(E /. A) |^ ((L /. A)) is Element of the carrier of G

A is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

len A is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

H is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

len H is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

dom A is Element of bool NAT

Seg (len E) is V46() V53( len E) Element of bool NAT

A is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() set

A . A is set

L /. A is ext-real V42() V43() integer Element of INT

((L /. A)) is ext-real V42() V43() integer Element of INT

E /. A is Element of the carrier of G

(E /. A) |^ ((L /. A)) is Element of the carrier of G

H . A is set

G is non empty unital Group-like associative multMagma

the carrier of G is non empty set

L is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

len L is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

E is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

len E is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

L ^ E is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

A is V1() V4( NAT ) V5( INT ) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of INT

len A is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

(G,A,L) is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

H is V1() V4( NAT ) V5( INT ) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of INT

len H is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

A ^ H is V1() V4( NAT ) V5( INT ) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of INT

(G,(A ^ H),(L ^ E)) is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

(G,H,E) is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

(G,A,L) ^ (G,H,E) is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

len (L ^ E) is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

(len L) + (len E) is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

len (A ^ H) is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

dom (L ^ E) is Element of bool NAT

dom (A ^ H) is Element of bool NAT

H3 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

dom L is Element of bool NAT

len (G,A,L) is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

dom (G,A,L) is Element of bool NAT

((G,A,L) ^ (G,H,E)) . H3 is set

(G,A,L) . H3 is set

A /. H3 is ext-real V42() V43() integer Element of INT

((A /. H3)) is ext-real V42() V43() integer Element of INT

L /. H3 is Element of the carrier of G

(L /. H3) |^ ((A /. H3)) is Element of the carrier of G

(A ^ H) . H3 is set

(A ^ H) /. H3 is ext-real V42() V43() integer Element of INT

L . H3 is set

(L ^ E) . H3 is set

(L ^ E) /. H3 is Element of the carrier of G

dom A is Element of bool NAT

A . H3 is set

(((A ^ H) /. H3)) is ext-real V42() V43() integer Element of INT

((L ^ E) /. H3) |^ (((A ^ H) /. H3)) is Element of the carrier of G

dom E is Element of bool NAT

H2 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() set

(len L) + H2 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

H2 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

(len L) + H2 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

(L ^ E) . H3 is set

E . H2 is set

E /. H2 is Element of the carrier of G

len (G,A,L) is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

len (G,H,E) is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

dom (G,H,E) is Element of bool NAT

((G,A,L) ^ (G,H,E)) . H3 is set

(G,H,E) . H2 is set

(L ^ E) /. H3 is Element of the carrier of G

(A ^ H) /. H3 is ext-real V42() V43() integer Element of INT

(A ^ H) . H3 is set

dom H is Element of bool NAT

H /. H2 is ext-real V42() V43() integer Element of INT

H . H2 is set

(((A ^ H) /. H3)) is ext-real V42() V43() integer Element of INT

((L ^ E) /. H3) |^ (((A ^ H) /. H3)) is Element of the carrier of G

dom L is Element of bool NAT

dom E is Element of bool NAT

((G,A,L) ^ (G,H,E)) . H3 is set

(A ^ H) /. H3 is ext-real V42() V43() integer Element of INT

(((A ^ H) /. H3)) is ext-real V42() V43() integer Element of INT

(L ^ E) /. H3 is Element of the carrier of G

((L ^ E) /. H3) |^ (((A ^ H) /. H3)) is Element of the carrier of G

((G,A,L) ^ (G,H,E)) . H3 is set

(A ^ H) /. H3 is ext-real V42() V43() integer Element of INT

(((A ^ H) /. H3)) is ext-real V42() V43() integer Element of INT

(L ^ E) /. H3 is Element of the carrier of G

((L ^ E) /. H3) |^ (((A ^ H) /. H3)) is Element of the carrier of G

len ((G,A,L) ^ (G,H,E)) is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

len (G,A,L) is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

len (G,H,E) is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

(len (G,A,L)) + (len (G,H,E)) is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

(len L) + (len (G,H,E)) is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

G is non empty unital Group-like associative multMagma

the carrier of G is non empty set

L is non empty unital Group-like associative Subgroup of G

carr L is Element of bool the carrier of G

bool the carrier of G is non empty set

the carrier of L is non empty set

E is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

rng E is set

A is V1() V4( NAT ) V5( INT ) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of INT

(G,A,E) is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

(G,(G,A,E)) is Element of the carrier of G

the multF of G is V1() Function-like quasi_total associative having_a_unity Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is V1() non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is V1() non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

the multF of G "**" (G,A,E) is Element of the carrier of G

rng (G,A,E) is set

H is set

dom (G,A,E) is Element of bool NAT

A is set

(G,A,E) . A is set

len (G,A,E) is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

len E is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

H is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

dom E is Element of bool NAT

E . H is set

E /. H is Element of the carrier of G

A /. H is ext-real V42() V43() integer Element of INT

((A /. H)) is ext-real V42() V43() integer Element of INT

(E /. H) |^ ((A /. H)) is Element of the carrier of G

<*> INT is V1() non-empty empty-yielding V4( NAT ) V5( INT ) Function-like one-to-one constant functional empty proper ext-real V35() V36() V37() V39() V40() V41() V42() V43() integer V46() V51() V53( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of INT

[:NAT,INT:] is V1() non empty V46() set

G is non empty unital Group-like associative multMagma

the carrier of G is non empty set

<*> the carrier of G is V1() non-empty empty-yielding V4( NAT ) V5( the carrier of G) Function-like one-to-one constant functional empty proper ext-real V35() V36() V37() V39() V40() V41() V42() V43() integer V46() V51() V53( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of the carrier of G

[:NAT, the carrier of G:] is V1() non empty V46() set

(G,(<*> INT),(<*> the carrier of G)) is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G

len (<*> the carrier of G) is V1() non-empty empty-yielding V4( NAT ) Function-like one-to-one constant functional empty ext-real V35() V36() V37() V39() V40() V41() V42() V43() integer V46() V51() V53( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT

len (G,(<*> INT),(<*> the carrier of G)) is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

G is ext-real V42() V43() integer set

(G) is ext-real V42() V43() integer Element of INT

<*(G)*> is V1() V4( NAT ) V5( INT ) Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of INT

L is non empty unital Group-like associative multMagma

the carrier of L is non empty set

E is Element of the carrier of L

<*E*> is V1() V4( NAT ) V5( the carrier of L) Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of L

(L,<*(G)*>,<*E*>) is V1() V4( NAT ) V5( the carrier of L) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of L

E |^ G is Element of the carrier of L

<*(E |^ G)*> is V1() V4( NAT ) V5( the carrier of L) Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of L

len <*E*> is non empty ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

<*(G)*> /. 1 is ext-real V42() V43() integer Element of INT

dom <*E*> is non empty trivial V53(1) Element of bool NAT

Seg (len <*E*>) is non empty V46() V53( len <*E*>) Element of bool NAT

A is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

<*(E |^ G)*> . A is set

<*(G)*> /. A is ext-real V42() V43() integer Element of INT

((<*(G)*> /. A)) is ext-real V42() V43() integer Element of INT

<*E*> /. A is Element of the carrier of L

(<*E*> /. A) |^ ((<*(G)*> /. A)) is Element of the carrier of L

len <*(E |^ G)*> is non empty ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

G is ext-real V42() V43() integer set

(G) is ext-real V42() V43() integer Element of INT

L is ext-real V42() V43() integer set

(L) is ext-real V42() V43() integer Element of INT

<*(G),(L)*> is V1() V4( NAT ) V5( INT ) Function-like non empty V46() V53(2) FinSequence-like FinSubsequence-like FinSequence of INT

E is non empty unital Group-like associative multMagma

the carrier of E is non empty set

A is Element of the carrier of E

A |^ G is Element of the carrier of E

H is Element of the carrier of E

<*A,H*> is V1() V4( NAT ) V5( the carrier of E) Function-like non empty V46() V53(2) FinSequence-like FinSubsequence-like FinSequence of the carrier of E

(E,<*(G),(L)*>,<*A,H*>) is V1() V4( NAT ) V5( the carrier of E) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of E

H |^ L is Element of the carrier of E

<*(A |^ G),(H |^ L)*> is V1() V4( NAT ) V5( the carrier of E) Function-like non empty V46() V53(2) FinSequence-like FinSubsequence-like FinSequence of the carrier of E

<*(G)*> is V1() V4( NAT ) V5( INT ) Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of INT

len <*(G)*> is non empty ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

<*(L)*> is V1() V4( NAT ) V5( INT ) Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of INT

len <*(L)*> is non empty ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

<*A*> is V1() V4( NAT ) V5( the carrier of E) Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of E

<*H*> is V1() V4( NAT ) V5( the carrier of E) Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of E

<*A*> ^ <*H*> is V1() V4( NAT ) V5( the carrier of E) Function-like non empty V46() V53(1 + 1) FinSequence-like FinSubsequence-like FinSequence of the carrier of E

1 + 1 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

<*(G)*> ^ <*(L)*> is V1() V4( NAT ) V5( INT ) Function-like non empty V46() V53(1 + 1) FinSequence-like FinSubsequence-like FinSequence of INT

len <*A*> is non empty ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

len <*H*> is non empty ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

(E,<*(G)*>,<*A*>) is V1() V4( NAT ) V5( the carrier of E) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of E

(E,<*(L)*>,<*H*>) is V1() V4( NAT ) V5( the carrier of E) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of E

(E,<*(G)*>,<*A*>) ^ (E,<*(L)*>,<*H*>) is V1() V4( NAT ) V5( the carrier of E) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of E

<*(A |^ G)*> is V1() V4( NAT ) V5( the carrier of E) Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of E

<*(A |^ G)*> ^ (E,<*(L)*>,<*H*>) is V1() V4( NAT ) V5( the carrier of E) Function-like non empty V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of E

<*(H |^ L)*> is V1() V4( NAT ) V5( the carrier of E) Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of E

<*(A |^ G)*> ^ <*(H |^ L)*> is V1() V4( NAT ) V5( the carrier of E) Function-like non empty V46() V53(1 + 1) FinSequence-like FinSubsequence-like FinSequence of the carrier of E

G is ext-real V42() V43() integer set

(G) is ext-real V42() V43() integer Element of INT

L is ext-real V42() V43() integer set

(L) is ext-real V42() V43() integer Element of INT

E is ext-real V42() V43() integer set

(E) is ext-real V42() V43() integer Element of INT

<*(G),(L),(E)*> is V1() V4( NAT ) V5( INT ) Function-like non empty V46() V53(3) FinSequence-like FinSubsequence-like FinSequence of INT

A is non empty unital Group-like associative multMagma

the carrier of A is non empty set

H is Element of the carrier of A

H |^ G is Element of the carrier of A

A is Element of the carrier of A

A |^ L is Element of the carrier of A

H is Element of the carrier of A

<*H,A,H*> is V1() V4( NAT ) V5( the carrier of A) Function-like non empty V46() V53(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of A

(A,<*(G),(L),(E)*>,<*H,A,H*>) is V1() V4( NAT ) V5( the carrier of A) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of A

H |^ E is Element of the carrier of A

<*(H |^ G),(A |^ L),(H |^ E)*> is V1() V4( NAT ) V5( the carrier of A) Function-like non empty V46() V53(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of A

<*(G)*> is V1() V4( NAT ) V5( INT ) Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of INT

len <*(G)*> is non empty ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

<*(L),(E)*> is V1() V4( NAT ) V5( INT ) Function-like non empty V46() V53(2) FinSequence-like FinSubsequence-like FinSequence of INT

len <*(L),(E)*> is non empty ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

<*H*> is V1() V4( NAT ) V5( the carrier of A) Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of A

<*A,H*> is V1() V4( NAT ) V5( the carrier of A) Function-like non empty V46() V53(2) FinSequence-like FinSubsequence-like FinSequence of the carrier of A

<*H*> ^ <*A,H*> is V1() V4( NAT ) V5( the carrier of A) Function-like non empty V46() V53(1 + 2) FinSequence-like FinSubsequence-like FinSequence of the carrier of A

1 + 2 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

<*(G)*> ^ <*(L),(E)*> is V1() V4( NAT ) V5( INT ) Function-like non empty V46() V53(1 + 2) FinSequence-like FinSubsequence-like FinSequence of INT

len <*H*> is non empty ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

len <*A,H*> is non empty ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT

(A,<*(G)*>,<*H*>) is V1() V4( NAT ) V5( the carrier of A) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of A

(A,<*(L),(E)*>,<*A,H*>) is V1() V4( NAT ) V5( the carrier of A) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of A

(A,<*(G)*>,<*H*>) ^ (A,<*(L),(E)*>,<*A,H*>) is V1() V4( NAT ) V5( the carrier of A) Function-like V46() FinSequence-like