:: 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₁() is non empty unital Group-like associative multMagma
the carrier of F₁() is non empty set
bool the carrier of F₁() is non empty set
{ b₁ where b₁ is Element of bool the carrier of F₁() : ex b₂ being non empty strict unital Group-like associative Subgroup of F₁() st
( b₁ = the carrier of b₂ & P₁[b₂] ) } is set
meet { b₁ where b₁ is Element of bool the carrier of F₁() : ex b₂ being non empty strict unital Group-like associative Subgroup of F₁() st
( b₁ = the carrier of b₂ & P₁[b₂] ) } is set
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₁() is V1() Function-like quasi_total associative having_a_unity Element of bool [:[: the carrier of F₁(), the carrier of F₁():], the carrier of F₁():]
[: the carrier of F₁(), the carrier of F₁():] is V1() non empty set
[:[: the carrier of F₁(), the carrier of F₁():], the carrier of F₁():] is V1() non empty set
bool [:[: the carrier of F₁(), the carrier of F₁():], the carrier of F₁():] is non empty set
the multF of F₁() . (A,H) is Element of the carrier 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₁() is non being_of_order_0 Element of the carrier of F₁()
F₁() is non empty unital Group-like associative multMagma
Subgroups F₁() is non empty set
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