:: 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 FinSubsequence-like FinSequence of the carrier of A
<*(H |^ G)*> 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
<*(H |^ G)*> ^ (A,<*(L),(E)*>,<*A,H*>) is V1() V4( NAT ) V5( the carrier of A) Function-like non empty V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of A
<*(A |^ L),(H |^ E)*> 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 |^ G)*> ^ <*(A |^ L),(H |^ E)*> 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) is ext-real V42() V43() integer Element of INT
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
(len L) |-> (1) is V1() V4( NAT ) V5( INT ) Function-like V46() V53( len L) FinSequence-like FinSubsequence-like Element of (len L) -tuples_on INT
(len L) -tuples_on INT is functional non empty FinSequence-membered FinSequenceSet of INT
(G,((len L) |-> (1)),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
len E is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
(len E) |-> (1) is V1() V4( NAT ) V5( INT ) Function-like V46() V53( len E) FinSequence-like FinSubsequence-like Element of (len E) -tuples_on INT
(len E) -tuples_on INT is functional non empty FinSequence-membered FinSequenceSet of INT
(G,((len E) |-> (1)),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 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
len (E ^ <*A*>) is non empty ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
(len (E ^ <*A*>)) |-> (1) is V1() V4( NAT ) V5( INT ) Function-like V46() V53( len (E ^ <*A*>)) FinSequence-like FinSubsequence-like Element of (len (E ^ <*A*>)) -tuples_on INT
(len (E ^ <*A*>)) -tuples_on INT is functional non empty FinSequence-membered FinSequenceSet of INT
(G,((len (E ^ <*A*>)) |-> (1)),(E ^ <*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 non empty ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
<*(1)*> is V1() V4( NAT ) V5( INT ) Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of INT
len <*(1)*> is non empty ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
len ((len E) |-> (1)) is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
(len E) + (len <*A*>) is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
((len E) |-> (1)) ^ <*(1)*> is V1() V4( NAT ) V5( INT ) Function-like non empty V46() V53((len E) + 1) FinSequence-like FinSubsequence-like FinSequence of INT
(len E) + 1 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
(G,(((len E) |-> (1)) ^ <*(1)*>),(E ^ <*A*>)) is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,<*(1)*>,<*A*>) is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,((len E) |-> (1)),E) ^ (G,<*(1)*>,<*A*>) is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G
A |^ 1 is Element of the carrier of G
<*(A |^ 1)*> 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 |^ 1)*> 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 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
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 (<*> the carrier of G)) |-> (1) is V1() V4( NAT ) V5( INT ) Function-like V46() V53( len (<*> the carrier of G)) FinSequence-like FinSubsequence-like Element of (len (<*> the carrier of G)) -tuples_on INT
(len (<*> the carrier of G)) -tuples_on INT is functional non empty FinSequence-membered FinSequenceSet of INT
(G,((len (<*> the carrier of G)) |-> (1)),(<*> 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
0 |-> (1) is V1() non-empty empty-yielding V4( NAT ) V5( INT ) 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 INT
0 -tuples_on INT is functional non empty FinSequence-membered FinSequenceSet of INT
(G,(0 |-> (1)),(<*> 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
(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
(0) is ext-real V42() V43() integer Element of INT
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
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
(len L) |-> (0) is V1() V4( NAT ) V5( INT ) Function-like V46() V53( len L) FinSequence-like FinSubsequence-like Element of (len L) -tuples_on INT
(len L) -tuples_on INT is functional non empty FinSequence-membered FinSequenceSet of INT
(G,((len L) |-> (0)),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) |-> (1_ G) is V1() V4( NAT ) V5( the carrier of G) Function-like V46() V53( len L) FinSequence-like FinSubsequence-like Element of (len L) -tuples_on the carrier of G
(len L) -tuples_on the carrier of G is functional non empty FinSequence-membered FinSequenceSet 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
(len E) |-> (0) is V1() V4( NAT ) V5( INT ) Function-like V46() V53( len E) FinSequence-like FinSubsequence-like Element of (len E) -tuples_on INT
(len E) -tuples_on INT is functional non empty FinSequence-membered FinSequenceSet of INT
(G,((len E) |-> (0)),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) |-> (1_ G) is V1() V4( NAT ) V5( the carrier of G) Function-like V46() V53( len E) FinSequence-like FinSubsequence-like Element of (len E) -tuples_on the carrier of G
(len E) -tuples_on the carrier of G is functional non empty FinSequence-membered FinSequenceSet 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
len (E ^ <*A*>) is non empty ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
(len (E ^ <*A*>)) |-> (0) is V1() V4( NAT ) V5( INT ) Function-like V46() V53( len (E ^ <*A*>)) FinSequence-like FinSubsequence-like Element of (len (E ^ <*A*>)) -tuples_on INT
(len (E ^ <*A*>)) -tuples_on INT is functional non empty FinSequence-membered FinSequenceSet of INT
(G,((len (E ^ <*A*>)) |-> (0)),(E ^ <*A*>)) is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(len (E ^ <*A*>)) |-> (1_ G) is V1() V4( NAT ) V5( the carrier of G) Function-like V46() V53( len (E ^ <*A*>)) FinSequence-like FinSubsequence-like Element of (len (E ^ <*A*>)) -tuples_on the carrier of G
(len (E ^ <*A*>)) -tuples_on the carrier of G is functional non empty FinSequence-membered FinSequenceSet of the carrier of G
len <*A*> is non empty ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
<*(0)*> is V1() V4( NAT ) V5( INT ) Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of INT
len <*(0)*> is non empty ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
len ((len E) |-> (0)) is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
(len E) + (len <*A*>) is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
((len E) |-> (0)) ^ <*(0)*> is V1() V4( NAT ) V5( INT ) Function-like non empty V46() V53((len E) + 1) FinSequence-like FinSubsequence-like FinSequence of INT
(len E) + 1 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
(G,(((len E) |-> (0)) ^ <*(0)*>),(E ^ <*A*>)) is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,<*(0)*>,<*A*>) is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,((len E) |-> (0)),E) ^ (G,<*(0)*>,<*A*>) is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G
A |^ 0 is Element of the carrier of G
<*(A |^ 0)*> 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
((len E) |-> (1_ G)) ^ <*(A |^ 0)*> is V1() V4( NAT ) V5( the carrier of G) Function-like non empty V46() V53((len E) + 1) FinSequence-like FinSubsequence-like FinSequence of the carrier of G
<*(1_ G)*> 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
((len E) |-> (1_ G)) ^ <*(1_ G)*> is V1() V4( NAT ) V5( the carrier of G) Function-like non empty V46() V53((len E) + 1) FinSequence-like FinSubsequence-like FinSequence 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
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 (<*> the carrier of G)) |-> (0) is V1() V4( NAT ) V5( INT ) Function-like V46() V53( len (<*> the carrier of G)) FinSequence-like FinSubsequence-like Element of (len (<*> the carrier of G)) -tuples_on INT
(len (<*> the carrier of G)) -tuples_on INT is functional non empty FinSequence-membered FinSequenceSet of INT
(G,((len (<*> the carrier of G)) |-> (0)),(<*> 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)) |-> (1_ G) is V1() V4( NAT ) V5( the carrier of G) Function-like V46() V53( len (<*> the carrier of G)) FinSequence-like FinSubsequence-like Element of (len (<*> the carrier of G)) -tuples_on the carrier of G
(len (<*> the carrier of G)) -tuples_on the carrier of G is functional non empty FinSequence-membered FinSequenceSet of the carrier of G
0 |-> (0) is V1() non-empty empty-yielding V4( NAT ) V5( INT ) 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 INT
0 -tuples_on INT is functional non empty FinSequence-membered FinSequenceSet of INT
(G,(0 |-> (0)),(<*> 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
(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
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
1_ L is non being_of_order_0 Element of the carrier of L
G |-> (1_ L) 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
E is V1() V4( NAT ) V5( INT ) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of INT
len E is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
(L,E,(G |-> (1_ L))) is V1() V4( NAT ) V5( the carrier of L) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of L
A is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
A |-> (1_ L) 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
A + 1 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
(A + 1) |-> (1_ L) 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
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
(L,H,((A + 1) |-> (1_ L))) is V1() V4( NAT ) V5( the carrier of L) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of L
Seg A is V46() V53(A) Element of bool NAT
H | (Seg A) is V1() V4( NAT ) V4( Seg A) V4( NAT ) V5( INT ) Function-like FinSubsequence-like Element of bool [:NAT,INT:]
bool [:NAT,INT:] is non empty V46() set
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
(L,A,(A |-> (1_ L))) is V1() V4( NAT ) V5( the carrier of L) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of L
rng H is set
dom H is Element of bool NAT
H . (A + 1) is set
<*(1_ L)*> 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 <*(1_ L)*> is non empty ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
H is ext-real V42() V43() integer set
(H) is ext-real V42() V43() integer Element of INT
<*(H)*> is V1() V4( NAT ) V5( INT ) Function-like constant non empty trivial V46() V53(1) 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
(A |-> (1_ L)) ^ <*(1_ L)*> is V1() V4( NAT ) V5( the carrier of L) Function-like non empty V46() V53(A + 1) FinSequence-like FinSubsequence-like FinSequence of the carrier of L
A + 1 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
len (A |-> (1_ L)) 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 non empty V46() FinSequence-like FinSubsequence-like FinSequence of INT
(L,<*(H)*>,<*(1_ L)*>) is V1() V4( NAT ) V5( the carrier of L) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of L
(L,A,(A |-> (1_ L))) ^ (L,<*(H)*>,<*(1_ L)*>) is V1() V4( NAT ) V5( the carrier of L) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of L
(1_ L) |^ H is Element of the carrier of L
<*((1_ L) |^ H)*> 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
(A |-> (1_ L)) ^ <*((1_ L) |^ H)*> is V1() V4( NAT ) V5( the carrier of L) Function-like non empty V46() V53(A + 1) FinSequence-like FinSubsequence-like FinSequence of the carrier of L
0 |-> (1_ L) 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
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
(L,A,(0 |-> (1_ L))) is V1() V4( NAT ) V5( the carrier of L) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of L
<*> the carrier of L is V1() non-empty empty-yielding V4( NAT ) V5( the carrier of L) 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 L
[:NAT, the carrier of L:] is V1() non empty V46() set
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
bool the carrier of G is non empty set
L is Element of bool the carrier of G
bool the carrier of G is non empty Element of bool (bool the carrier of G)
bool (bool the carrier of G) is non empty set
E is set
meet E is set
(Omega). G is non empty strict unital Group-like associative Subgroup 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
multMagma(# the carrier of G, the multF of G #) is strict multMagma
carr ((Omega). G) is Element of bool the carrier of G
the carrier of ((Omega). G) is non empty set
H is set
A is set
H is non empty unital Group-like associative Subgroup of G
carr H is Element of bool the carrier of G
the carrier of H is non empty set
H is set
A is non empty unital Group-like associative Subgroup of G
carr A is Element of bool the carrier of G
the carrier of A is non empty set
1_ G is non being_of_order_0 Element of the carrier of G
A is Element of the carrier of G
H is Element of bool the carrier of G
H is Element of the carrier of G
H3 is set
H2 is non empty unital Group-like associative Subgroup of G
carr H2 is Element of bool the carrier of G
the carrier of H2 is non empty set
A * H is Element of the carrier of G
the multF of G . (A,H) is Element of the carrier of G
A is Element of the carrier of G
H is set
H3 is non empty unital Group-like associative Subgroup of G
carr H3 is Element of bool the carrier of G
the carrier of H3 is non empty set
A " is Element of the carrier of G
A is non empty strict unital Group-like associative Subgroup of G
the carrier of A is non empty set
H is set
H3 is non empty unital Group-like associative Subgroup of G
carr H3 is Element of bool the carrier of G
the carrier of H3 is non empty set
H is non empty strict unital Group-like associative Subgroup of G
the carrier of H is non empty set
carr H is Element of bool the carrier of G
E is non empty strict unital Group-like associative Subgroup of G
the carrier of E is non empty set
A is non empty strict unital Group-like associative Subgroup of G
the carrier of A is non empty set
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
bool the carrier of G is non empty set
L is Element of the carrier of G
E is Element of bool the carrier of G
(G,E) is non empty strict unital Group-like associative Subgroup of G
{ b₁ where b₁ is Element of the carrier of G : S₁[b₁] } is set
H is Element of the carrier of G
A is Element of bool the carrier of G
A is Element of the carrier of G
H is Element of the carrier of G
H2 is V1() V4( NAT ) V5( INT ) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of INT
H3 is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,H2,H3) is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,(G,H2,H3)) 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,H2,H3) is Element of the carrier of G
len H3 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
len H2 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
rng H3 is set
H3 is V1() V4( NAT ) V5( INT ) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of INT
H is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,H3,H) is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,(G,H3,H)) 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,H3,H) is Element of the carrier of G
len H is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
len H3 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
rng H is set
H2 is Element of the carrier of G
I1 is V1() V4( NAT ) V5( INT ) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of INT
F1 is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,I1,F1) is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,(G,I1,F1)) is Element of the carrier of G
the multF of G "**" (G,I1,F1) is Element of the carrier of G
len F1 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
len I1 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
rng F1 is set
F1 is V1() V4( NAT ) V5( INT ) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of INT
H2 is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,F1,H2) is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,(G,F1,H2)) is Element of the carrier of G
the multF of G "**" (G,F1,H2) is Element of the carrier of G
len H2 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
len F1 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
rng H2 is set
H ^ H2 is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len (H ^ H2) is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
(len H3) + (len F1) is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
H3 ^ F1 is V1() V4( NAT ) V5( INT ) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of INT
len (H3 ^ F1) is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
rng (H ^ H2) is set
(rng H) \/ (rng H2) is set
H * A is Element of the carrier of G
the multF of G . (H,A) is Element of the carrier of G
(G,H3,H) ^ (G,F1,H2) is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,((G,H3,H) ^ (G,F1,H2))) is Element of the carrier of G
the multF of G "**" ((G,H3,H) ^ (G,F1,H2)) is Element of the carrier of G
(G,(H3 ^ F1),(H ^ H2)) is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,(G,(H3 ^ F1),(H ^ H2))) is Element of the carrier of G
the multF of G "**" (G,(H3 ^ F1),(H ^ H2)) is Element of the carrier of G
H is Element of the carrier of G
A is Element of the carrier of G
H3 is V1() V4( NAT ) V5( INT ) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of INT
H is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,H3,H) is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,(G,H3,H)) is Element of the carrier of G
the multF of G "**" (G,H3,H) is Element of the carrier of G
len H is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
len H3 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
rng H is set
H is V1() V4( NAT ) V5( INT ) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of INT
A is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,H,A) is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,(G,H,A)) is Element of the carrier of G
the multF of G "**" (G,H,A) is Element of the carrier of G
len A is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
len H is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
rng A is set
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
Seg (len H) is V46() V53( len H) 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
(len A) - I1 is ext-real V42() V43() integer set
((len A) - 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
dom A is Element of bool NAT
A . (((len A) - I1) + 1) is set
H2 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() set
(len H) - H2 is ext-real V42() V43() integer set
((len H) - H2) + 1 is ext-real V42() V43() integer set
H . (((len H) - H2) + 1) is set
F1 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
H . F1 is set
rng H is set
I1 is ext-real V42() V43() integer Element of INT
i is ext-real V42() V43() integer set
- i is ext-real V42() V43() integer set
b is set
H2 is V1() V4( NAT ) Function-like V46() FinSequence-like FinSubsequence-like set
dom H2 is Element of bool NAT
len H2 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
rng H2 is set
F1 is set
I1 is set
H2 . I1 is set
i is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
(len H) - i is ext-real V42() V43() integer set
((len H) - i) + 1 is ext-real V42() V43() integer set
H . (((len H) - i) + 1) is set
b is ext-real V42() V43() integer set
- b is ext-real V42() V43() integer set
Seg (len A) is V46() V53( len A) Element of bool NAT
dom A is Element of bool NAT
len (G,H,A) is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
I1 is V1() V4( NAT ) V5( INT ) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of INT
i is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,I1,i) is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len (G,I1,i) is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
len i is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
dom (G,I1,i) is Element of bool NAT
dom i is Element of bool NAT
c is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
I1 /. c is ext-real V42() V43() integer Element of INT
((I1 /. c)) is ext-real V42() V43() integer Element of INT
(len (G,H,A)) - c is ext-real V42() V43() integer set
((len (G,H,A)) - c) + 1 is ext-real V42() V43() integer set
n is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
H /. n is ext-real V42() V43() integer Element of INT
((H /. n)) is ext-real V42() V43() integer Element of INT
(G,I1,i) /. c is Element of the carrier of G
(G,I1,i) . c is set
H . n is set
I1 . c is set
p is ext-real V42() V43() integer set
- p is ext-real V42() V43() integer set
i /. c is Element of the carrier of G
(i /. c) |^ (- p) is Element of the carrier of G
i . c is set
A . n is set
dom I1 is Element of bool NAT
A /. n is Element of the carrier of G
(A /. n) |^ p is Element of the carrier of G
((A /. n) |^ p) " is Element of the carrier of G
((G,I1,i) /. c) " is Element of the carrier of G
(G,H,A) . (((len (G,H,A)) - c) + 1) is set
(G,(G,H,A)) " is Element of the carrier of G
(G,(G,I1,i)) is Element of the carrier of G
the multF of G "**" (G,I1,i) is Element of the carrier of G
H " is Element of the carrier of G
len {} 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 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
1_ G is non being_of_order_0 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,(<*> 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
H is non empty strict unital Group-like associative Subgroup of G
the carrier of H is non empty set
H is set
H3 is Element of the carrier of G
<*H3*> 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
rng <*H3*> is non empty trivial V53(1) set
{H3} is non empty trivial V53(1) Element of bool the carrier of G
len <*H3*> is non empty ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
A is ext-real V42() V43() integer set
(A) is ext-real V42() V43() integer Element of INT
<*(A)*> is V1() V4( NAT ) V5( INT ) Function-like constant non empty trivial V46() V53(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
(G,<*(A)*>,<*H3*>) 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)*>,<*H3*>)) is Element of the carrier of G
the multF of G "**" (G,<*(A)*>,<*H3*>) is Element of the carrier of G
H3 |^ 1 is Element of the carrier of G
<*(H3 |^ 1)*> 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,<*(H3 |^ 1)*>) is Element of the carrier of G
the multF of G "**" <*(H3 |^ 1)*> is Element of the carrier of G
A is Element of the carrier of G
H3 is V1() V4( NAT ) V5( INT ) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of INT
H is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,H3,H) is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,(G,H3,H)) is Element of the carrier of G
the multF of G "**" (G,H3,H) is Element of the carrier of G
len H is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
len H3 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
rng H is set
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( 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
rng A is set
(G,H,A) is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,(G,H,A)) 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,H,A) is Element of the carrier of G
the carrier of (G,E) is non empty set
carr (G,E) is Element of bool the carrier of G
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
bool the carrier of G is non empty set
L is Element of the carrier of G
E is Element of bool the carrier of G
(G,E) is non empty strict unital Group-like associative Subgroup of G
the carrier of (G,E) is non empty 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 ) 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 Element of bool the carrier of G
bool the carrier of G is non empty set
(G,({} the carrier of G)) is non empty strict unital Group-like associative Subgroup of G
(1). G is non empty V73() strict unital Group-like associative Subgroup of G
the carrier of ((1). G) is non empty V46() set
L is non empty strict unital Group-like associative Subgroup of G
the carrier of L is non empty set
G is non empty unital Group-like associative multMagma
L is non empty strict unital Group-like associative Subgroup of G
carr L is Element of bool the carrier of G
the carrier of G is non empty set
bool the carrier of G is non empty set
the carrier of L is non empty set
(G,(carr L)) is non empty strict unital Group-like associative Subgroup of G
E is non empty strict unital Group-like associative Subgroup of G
the carrier of E is non empty set
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
bool the carrier of G is non empty set
L is Element of bool the carrier of G
(G,L) is non empty strict unital Group-like associative Subgroup of G
E is Element of bool the carrier of G
(G,E) is non empty strict unital Group-like associative Subgroup 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
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
rng H is set
(G,A,H) 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,H)) 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,H) is Element of the carrier of G
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
bool the carrier of G is non empty set
L is Element of bool the carrier of G
(G,L) is non empty strict unital Group-like associative Subgroup of G
E is Element of bool the carrier of G
L /\ E is Element of bool the carrier of G
(G,(L /\ E)) is non empty strict unital Group-like associative Subgroup of G
(G,E) is non empty strict unital Group-like associative Subgroup of G
(G,L) /\ (G,E) is non empty strict unital Group-like associative Subgroup 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
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
rng H is set
(G,A,H) 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,H)) 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,H) is Element of the carrier of G
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
bool the carrier of G is non empty set
L is Element of bool the carrier of G
(G,L) is non empty strict unital Group-like associative Subgroup of G
the carrier of (G,L) is non empty set
{ b₁ where b₁ is Element of bool the carrier of G : ex b₂ being non empty strict unital Group-like associative Subgroup of G st
( b₁ = the carrier of b₂ & L c= carr b₂ ) } is set
meet { b₁ where b₁ is Element of bool the carrier of G : ex b₂ being non empty strict unital Group-like associative Subgroup of G st
( b₁ = the carrier of b₂ & L c= carr b₂ ) } is set
A is set
H is Element of bool the carrier of G
A is non empty strict unital Group-like associative Subgroup of G
the carrier of A is non empty set
carr A is Element of bool the carrier of G
(Omega). G is non empty strict unital Group-like associative Subgroup 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
multMagma(# the carrier of G, the multF of G #) is strict multMagma
the carrier of ((Omega). G) is non empty set
carr ((Omega). G) is Element of bool the carrier of G
{ b₁ where b₁ is Element of bool the carrier of G : ex b₂ being non empty strict unital Group-like associative Subgroup of G st
( b₁ = the carrier of b₂ & S₁[b₂] ) } is set
meet { b₁ where b₁ is Element of bool the carrier of G : ex b₂ being non empty strict unital Group-like associative Subgroup of G st
( b₁ = the carrier of b₂ & S₁[b₂] ) } is set
A is non empty strict unital Group-like associative Subgroup of G
the carrier of A is non empty set
H is non empty strict unital Group-like associative Subgroup of G
the carrier of H is non empty set
carr H is Element of bool the carrier of G
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
bool 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
L is Element of bool the carrier of G
(G,L) is non empty strict unital Group-like associative Subgroup of G
L \ {(1_ G)} is Element of bool the carrier of G
(G,(L \ {(1_ G)})) is non empty strict unital Group-like associative Subgroup of G
{ b₁ where b₁ is Element of bool the carrier of G : ex b₂ being non empty strict unital Group-like associative Subgroup of G st
( b₁ = the carrier of b₂ & L c= carr b₂ ) } is set
{ b₁ where b₁ is Element of bool the carrier of G : ex b₂ being non empty strict unital Group-like associative Subgroup of G st
( b₁ = the carrier of b₂ & L \ {(1_ G)} c= carr b₂ ) } is set
H is set
A is Element of bool the carrier of G
H is non empty strict unital Group-like associative Subgroup of G
the carrier of H is non empty set
carr H is Element of bool the carrier of G
H is non empty strict unital Group-like associative Subgroup of G
the carrier of H is non empty set
carr H is Element of bool the carrier of G
H is set
A is Element of bool the carrier of G
H is non empty strict unital Group-like associative Subgroup of G
the carrier of H is non empty set
carr H is Element of bool the carrier of G
H is non empty strict unital Group-like associative Subgroup of G
the carrier of H is non empty set
carr H is Element of bool the carrier of G
(L \ {(1_ G)}) \/ {(1_ G)} is non empty Element of bool the carrier of G
the carrier of (G,L) is non empty set
meet { b₁ where b₁ is Element of bool the carrier of G : ex b₂ being non empty strict unital Group-like associative Subgroup of G st
( b₁ = the carrier of b₂ & L c= carr b₂ ) } is set
the carrier of (G,(L \ {(1_ G)})) is non empty set
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
G is non empty unital Group-like associative multMagma
1_ G is non being_of_order_0 Element of the carrier of G
the carrier of G is non empty set
bool the carrier of G is non empty set
L is Element of bool the carrier of G
(G,L) is non empty strict unital Group-like associative Subgroup 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
multMagma(# the carrier of G, the multF of G #) is strict multMagma
{(1_ G)} is non empty trivial V53(1) Element of bool the carrier of G
L \ {(1_ G)} is Element of bool the carrier of G
(G,(L \ {(1_ G)})) is non empty strict unital Group-like associative Subgroup of G
G is non empty unital Group-like associative multMagma
G is non empty strict unital Group-like associative multMagma
the carrier of G is non empty set
L is non empty strict 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 Element of the carrier of G
{E} is non empty trivial V53(1) Element of bool the carrier of G
(carr L) \/ {E} is non empty Element of bool the carrier of G
(G,((carr L) \/ {E})) is non empty strict unital Group-like associative Subgroup of G
(G,(carr L)) is non empty strict unital Group-like associative Subgroup of G
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
bool the carrier of G is non empty set
{ b₁ where b₁ is Element of bool the carrier of G : ex b₂ being non empty strict unital Group-like associative Subgroup of G st
( b₁ = the carrier of b₂ & b₂ is (G) ) } is set
meet { b₁ where b₁ is Element of bool the carrier of G : ex b₂ being non empty strict unital Group-like associative Subgroup of G st
( b₁ = the carrier of b₂ & b₂ is (G) ) } is set
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
multMagma(# the carrier of G, the multF of G #) is strict multMagma
{ b₁ where b₁ is Element of bool the carrier of G : ex b₂ being non empty strict unital Group-like associative Subgroup of G st
( b₁ = the carrier of b₂ & S₁[b₂] ) } is set
meet { b₁ where b₁ is Element of bool the carrier of G : ex b₂ being non empty strict unital Group-like associative Subgroup of G st
( b₁ = the carrier of b₂ & S₁[b₂] ) } is set
L is non empty strict unital Group-like associative Subgroup of G
E is non empty strict unital Group-like associative Subgroup of G
the carrier of E is non empty set
A is non empty strict unital Group-like associative Subgroup of G
(Omega). G is non empty strict unital Group-like associative Subgroup of G
L is non empty strict unital Group-like associative Subgroup of G
L is non empty strict unital Group-like associative Subgroup of G
L is non empty strict unital Group-like associative Subgroup of G
E is non empty strict unital Group-like associative Subgroup of G
the carrier of E is non empty set
A is non empty strict unital Group-like associative Subgroup of G
H is non empty strict unital Group-like associative Subgroup of G
A is non empty strict unital Group-like associative Subgroup of G
L is non empty strict unital Group-like associative Subgroup of G
the carrier of L is non empty set
E is non empty strict unital Group-like associative Subgroup of G
the carrier of E is non empty set
H is non empty strict unital Group-like associative Subgroup of G
A is non empty strict unital Group-like associative Subgroup 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 non empty unital Group-like associative multMagma
(E) is non empty strict unital Group-like associative Subgroup of E
the carrier of E is non empty set
bool the carrier of E is non empty set
{ b₁ where b₁ is Element of bool the carrier of E : ex b₂ being non empty strict unital Group-like associative Subgroup of E st
( b₁ = the carrier of b₂ & b₂ is (E) ) } is set
H is non empty strict unital Group-like associative Subgroup of E
H is non empty strict unital Group-like associative Subgroup of E
the carrier of (E) is non empty set
meet { b₁ where b₁ is Element of bool the carrier of E : ex b₂ being non empty strict unital Group-like associative Subgroup of E st
( b₁ = the carrier of b₂ & b₂ is (E) ) } is set
A is non empty strict unital Group-like associative Subgroup of E
A is non empty strict unital Group-like associative Subgroup of E
carr A is Element of bool the carrier of E
the carrier of A is non empty set
A is set
H is Element of bool the carrier of E
H3 is non empty strict unital Group-like associative Subgroup of E
the carrier of H3 is non empty set
H3 is non empty strict unital Group-like associative Subgroup of E
the carrier of H3 is non empty set
carr H is Element of bool the carrier of E
the carrier of H is non empty set
meet { b₁ where b₁ is Element of bool the carrier of E : ex b₂ being non empty strict unital Group-like associative Subgroup of E st
( b₁ = the carrier of b₂ & b₂ is (E) ) } is set
the carrier of (E) is non empty set
A is non empty strict unital Group-like associative Subgroup of E
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
(G) is non empty strict unital Group-like associative Subgroup of 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
multMagma(# the carrier of G, the multF of G #) is strict multMagma
G is non empty unital Group-like associative multMagma
(G) is non empty strict unital Group-like associative Subgroup of G
L is non empty strict unital Group-like associative Subgroup of G
the carrier of G is non empty set
E is Element of the carrier of G
G is non empty strict unital Group-like associative multMagma
(G) is non empty strict unital Group-like associative Subgroup of G
the carrier of (G) is non empty set
the carrier of G is non empty set
{ b₁ where b₁ is Element of the carrier of G : b₁ is (G) } is set
E is set
A is Element of the carrier of G
bool the carrier of G is non empty set
{A} is non empty trivial V53(1) Element of bool the carrier of G
H is Element of bool the carrier of G
(G,H) is non empty strict unital Group-like associative Subgroup of G
H \ {A} is Element of bool the carrier of G
(G,(H \ {A})) is non empty strict unital Group-like associative Subgroup of G
H is Element of the carrier of G
H2 is V1() V4( NAT ) V5( INT ) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of INT
len H2 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
H3 is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len H3 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
rng H3 is set
(G,H2,H3) is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,(G,H2,H3)) 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,H2,H3) is Element of the carrier of G
rng (G,H2,H3) is set
carr (G,(H \ {A})) is Element of bool the carrier of G
the carrier of (G,(H \ {A})) is non empty set
F1 is set
dom (G,H2,H3) is Element of bool NAT
I1 is set
(G,H2,H3) . I1 is set
len (G,H2,H3) is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
i is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
dom H3 is Element of bool NAT
H2 /. i is ext-real V42() V43() integer Element of INT
((H2 /. i)) is ext-real V42() V43() integer Element of INT
H3 /. i is Element of the carrier of G
(H3 /. i) |^ ((H2 /. i)) is Element of the carrier of G
H3 . i is set
Subgroups G is non empty set
H is set
H3 is non empty set
H2 is Element of H3
F1 is Element of H3
I1 is Element of H3
i is non empty strict unital Group-like associative Subgroup of G
b is non empty strict unital Group-like associative Subgroup of G
c is non empty strict unital Group-like associative Subgroup of G
n is non empty strict unital Group-like associative Subgroup of G
H2 is set
{ b₁ where b₁ is Element of bool the carrier of G : ex b₂ being non empty strict unital Group-like associative Subgroup of G st
( b₂ in H2 & b₁ = carr b₂ ) } is set
I1 is set
i is Element of bool the carrier of G
b is non empty strict unital Group-like associative Subgroup of G
carr b is Element of bool the carrier of G
the carrier of b is non empty set
union { b₁ where b₁ is Element of bool the carrier of G : ex b₂ being non empty strict unital Group-like associative Subgroup of G st
( b₂ in H2 & b₁ = carr b₂ ) } is set
the Element of H3 is Element of H3
c is Element of H3
b is Element of H3
i is Element of the carrier of G
I1 is Element of bool the carrier of G
b is Element of the carrier of G
c is set
n is set
p is Element of bool the carrier of G
p is Element of bool the carrier of G
k is non empty strict unital Group-like associative Subgroup of G
carr k is Element of bool the carrier of G
the carrier of k is non empty set
k is non empty unital Group-like associative Subgroup of G
carr k is Element of bool the carrier of G
the carrier of k is non empty set
F1 is non empty strict unital Group-like associative Subgroup of G
carr F1 is Element of bool the carrier of G
the carrier of F1 is non empty set
F1 is non empty unital Group-like associative Subgroup of G
carr F1 is Element of bool the carrier of G
the carrier of F1 is non empty set
m is non empty strict unital Group-like associative Subgroup of G
q is non empty strict unital Group-like associative Subgroup of G
i * b is Element of the carrier of G
the multF of G . (i,b) is Element of the carrier of G
m is non empty strict unital Group-like associative Subgroup of G
q is non empty strict unital Group-like associative Subgroup of G
i * b is Element of the carrier of G
the multF of G . (i,b) is Element of the carrier of G
i * b is Element of the carrier of G
the multF of G . (i,b) is Element of the carrier of G
i * b is Element of the carrier of G
the multF of G . (i,b) is Element of the carrier of G
i is Element of the carrier of G
b is set
c is Element of bool the carrier of G
n is non empty strict unital Group-like associative Subgroup of G
carr n is Element of bool the carrier of G
the carrier of n is non empty set
n is non empty unital Group-like associative Subgroup of G
carr n is Element of bool the carrier of G
the carrier of n is non empty set
i " is Element of the carrier of G
the Element of H2 is Element of H2
b is non empty strict unital Group-like associative Subgroup of G
carr b is Element of bool the carrier of G
the carrier of b is non empty set
c is non empty strict unital Group-like associative Subgroup of G
the carrier of c is non empty set
n is set
p is Element of bool the carrier of G
p is non empty strict unital Group-like associative Subgroup of G
carr p is Element of bool the carrier of G
the carrier of p is non empty set
p is non empty strict unital Group-like associative Subgroup of G
carr p is Element of bool the carrier of G
the carrier of p is non empty set
carr c is Element of bool the carrier of G
n is Element of H3
p is Element of H3
k is non empty strict unital Group-like associative Subgroup of G
F1 is non empty strict unital Group-like associative Subgroup of G
p is Element of H3
m is non empty strict unital Group-like associative Subgroup of G
carr F1 is Element of bool the carrier of G
the carrier of F1 is non empty set
i is Element of H3
H2 is Element of H3
H2 is Element of H3
F1 is non empty strict unital Group-like associative Subgroup of G
H2 is Element of H3
I1 is non empty strict unital Group-like associative Subgroup of G
F1 is Element of H3
i is non empty strict unital Group-like associative Subgroup of G
b is non empty strict unital Group-like associative Subgroup of G
c is non empty strict unital Group-like associative Subgroup of G
H2 is Element of H3
F1 is non empty strict unital Group-like associative Subgroup of G
the carrier of F1 is non empty set
the multF of F1 is V1() Function-like quasi_total associative having_a_unity Element of bool [:[: the carrier of F1, the carrier of F1:], the carrier of F1:]
[: the carrier of F1, the carrier of F1:] is V1() non empty set
[:[: the carrier of F1, the carrier of F1:], the carrier of F1:] is V1() non empty set
bool [:[: the carrier of F1, the carrier of F1:], the carrier of F1:] is non empty set
multMagma(# the carrier of F1, the multF of F1 #) is strict multMagma
multMagma(# the carrier of G, the multF of G #) is strict multMagma
I1 is non empty strict unital Group-like associative Subgroup of G
carr F1 is Element of bool the carrier of G
the carrier of I1 is non empty set
carr I1 is Element of bool the carrier of G
(H \ {A}) \/ {A} is non empty Element of bool the carrier of G
i is set
(G,(carr I1)) is non empty strict unital Group-like associative Subgroup of G
i is Element of H3
b is non empty strict unital Group-like associative Subgroup of G
c is non empty strict unital Group-like associative Subgroup of G
the carrier of F1 is non empty set
E is set
A is Element of the carrier of G
H is non empty strict unital Group-like associative Subgroup of G
carr H is Element of bool the carrier of G
bool the carrier of G is non empty set
the carrier of H is non empty set
{A} is non empty trivial V53(1) Element of bool the carrier of G
(carr H) /\ {A} is Element of bool the carrier of G
A is set
(carr H) \/ {A} is non empty Element of bool the carrier of G
((carr H) \/ {A}) \ {A} is Element of bool the carrier of G
(carr H) \ {A} is Element of bool the carrier of G
(G,(((carr H) \/ {A}) \ {A})) is non empty strict unital Group-like associative Subgroup of G
(G,((carr H) \/ {A})) is non empty strict unital Group-like associative Subgroup of G
H is non empty strict unital Group-like associative Subgroup of G
H is non empty strict unital Group-like associative Subgroup of G
G is non empty strict unital Group-like associative multMagma
the carrier of G is non empty set
(G) is non empty strict unital Group-like associative Subgroup of G
L is Element of the carrier of G
the carrier of (G) is non empty set
{ b₁ where b₁ is Element of the carrier of G : b₁ is (G) } is set
E is Element of the carrier of G
{ b₁ where b₁ is Element of the carrier of G : b₁ is (G) } is set
the carrier of (G) is non empty set
G is non empty unital Group-like associative multMagma
L is non empty unital Group-like associative Subgroup of G
carr L is Element of bool the carrier of G
the carrier of G is non empty set
bool the carrier of G is non empty set
the carrier of L is non empty set
E is non empty unital Group-like associative Subgroup of G
carr E is Element of bool the carrier of G
the carrier of E is non empty set
(carr L) * (carr E) is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr L & b₂ in carr E ) } is set
G is non empty unital Group-like associative multMagma
A is non empty unital Group-like associative multMagma
H is non empty unital Group-like associative multMagma
L is non empty unital Group-like associative Subgroup of G
E is non empty unital Group-like associative Subgroup of G
(G,L,E) is Element of bool the carrier of G
the carrier of G is non empty set
bool the carrier of G is non empty set
carr L is Element of bool the carrier of G
the carrier of L is non empty set
carr E is Element of bool the carrier of G
the carrier of E is non empty set
(carr L) * (carr E) is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr L & b₂ in carr E ) } is set
H is non empty unital Group-like associative Subgroup of A
A is non empty unital Group-like associative Subgroup of A
(A,H,A) is Element of bool the carrier of A
the carrier of A is non empty set
bool the carrier of A is non empty set
carr H is Element of bool the carrier of A
the carrier of H is non empty set
carr A is Element of bool the carrier of A
the carrier of A is non empty set
(carr H) * (carr A) is Element of bool the carrier of A
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of A : ( b₁ in carr H & b₂ in carr A ) } is set
H * (carr A) is Element of bool the carrier of A
H3 is non empty unital Group-like associative Subgroup of H
H2 is non empty unital Group-like associative Subgroup of H
(H,H3,H2) is Element of bool the carrier of H
the carrier of H is non empty set
bool the carrier of H is non empty set
carr H3 is Element of bool the carrier of H
the carrier of H3 is non empty set
carr H2 is Element of bool the carrier of H
the carrier of H2 is non empty set
(carr H3) * (carr H2) is Element of bool the carrier of H
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of H : ( b₁ in carr H3 & b₂ in carr H2 ) } is set
(carr H3) * H2 is Element of bool the carrier of H
G is non empty unital Group-like associative multMagma
L is non empty unital Group-like associative Subgroup of G
E is non empty unital Group-like associative Subgroup of G
(G,L,E) is Element of bool the carrier of G
the carrier of G is non empty set
bool the carrier of G is non empty set
carr L is Element of bool the carrier of G
the carrier of L is non empty set
carr E is Element of bool the carrier of G
the carrier of E is non empty set
(carr L) * (carr E) is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr L & b₂ in carr E ) } is set
A is non empty unital Group-like associative Subgroup of G
(G,L,E) * A is Element of bool the carrier of G
carr A is Element of bool the carrier of G
the carrier of A is non empty set
(G,L,E) * (carr A) is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in (G,L,E) & b₂ in carr A ) } is set
(G,E,A) is Element of bool the carrier of G
(carr E) * (carr A) is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr E & b₂ in carr A ) } is set
L * (G,E,A) is Element of bool the carrier of G
(carr L) * (G,E,A) is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr L & b₂ in (G,E,A) ) } is set
(carr E) * A is Element of bool the carrier of G
(carr L) * ((carr E) * A) is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr L & b₂ in (carr E) * A ) } is set
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 non empty unital Group-like associative Subgroup of G
L * E is Element of bool the carrier of G
bool the carrier of G is non empty set
carr E is Element of bool the carrier of G
the carrier of E is non empty set
L * (carr E) is Element of bool the carrier of G
{L} is non empty trivial V53(1) Element of bool the carrier of G
{L} * (carr E) is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in {L} & b₂ in carr E ) } is set
A is non empty unital Group-like associative Subgroup of G
(L * E) * A is Element of bool the carrier of G
carr A is Element of bool the carrier of G
the carrier of A is non empty set
(L * E) * (carr A) is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in L * E & b₂ in carr A ) } is set
(G,E,A) is Element of bool the carrier of G
(carr E) * (carr A) is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr E & b₂ in carr A ) } is set
L * (G,E,A) is Element of bool the carrier of G
{L} * (G,E,A) is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in {L} & b₂ in (G,E,A) ) } is set
(carr E) * A is Element of bool the carrier of G
L * ((carr E) * A) is Element of bool the carrier of G
{L} * ((carr E) * A) is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in {L} & b₂ in (carr E) * A ) } is set
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 non empty unital Group-like associative Subgroup of G
A is non empty unital Group-like associative Subgroup of G
(G,E,A) is Element of bool the carrier of G
bool the carrier of G is non empty set
carr E is Element of bool the carrier of G
the carrier of E is non empty set
carr A is Element of bool the carrier of G
the carrier of A is non empty set
(carr E) * (carr A) is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr E & b₂ in carr A ) } is set
(G,E,A) * L is Element of bool the carrier of G
{L} is non empty trivial V53(1) Element of bool the carrier of G
(G,E,A) * {L} is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in (G,E,A) & b₂ in {L} ) } is set
A * L is Element of bool the carrier of G
(carr A) * L is Element of bool the carrier of G
(carr A) * {L} is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr A & b₂ in {L} ) } is set
E * (A * L) is Element of bool the carrier of G
(carr E) * (A * L) is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr E & b₂ in A * L ) } is set
E * (carr A) is Element of bool the carrier of G
(E * (carr A)) * L is Element of bool the carrier of G
(E * (carr A)) * {L} is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in E * (carr A) & b₂ in {L} ) } is set
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
bool the carrier of G is non empty set
L is Element of bool the carrier of G
E is non empty unital Group-like associative Subgroup of G
L * E is Element of bool the carrier of G
carr E is Element of bool the carrier of G
the carrier of E is non empty set
L * (carr E) is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in L & b₂ in carr E ) } is set
A is non empty unital Group-like associative Subgroup of G
(L * E) * A is Element of bool the carrier of G
carr A is Element of bool the carrier of G
the carrier of A is non empty set
(L * E) * (carr A) is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in L * E & b₂ in carr A ) } is set
(G,E,A) is Element of bool the carrier of G
(carr E) * (carr A) is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr E & b₂ in carr A ) } is set
L * (G,E,A) is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in L & b₂ in (G,E,A) ) } is set
E * (carr A) is Element of bool the carrier of G
L * (E * (carr A)) is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in L & b₂ in E * (carr A) ) } is set
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
bool the carrier of G is non empty set
L is Element of bool the carrier of G
E is non empty unital Group-like associative Subgroup of G
A is non empty unital Group-like associative Subgroup of G
(G,E,A) is Element of bool the carrier of G
carr E is Element of bool the carrier of G
the carrier of E is non empty set
carr A is Element of bool the carrier of G
the carrier of A is non empty set
(carr E) * (carr A) is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr E & b₂ in carr A ) } is set
(G,E,A) * L is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in (G,E,A) & b₂ in L ) } is set
A * L is Element of bool the carrier of G
(carr A) * L is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr A & b₂ in L ) } is set
E * (A * L) is Element of bool the carrier of G
(carr E) * (A * L) is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr E & b₂ in A * L ) } is set
E * (carr A) is Element of bool the carrier of G
(E * (carr A)) * L is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in E * (carr A) & b₂ in L ) } 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 non empty unital Group-like associative Subgroup of G
carr E is Element of bool the carrier of G
the carrier of E is non empty set
(carr L) \/ (carr E) is Element of bool the carrier of G
(G,((carr L) \/ (carr E))) is non empty strict unital Group-like associative Subgroup of G
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
H is non empty unital Group-like associative multMagma
the carrier of H is non empty set
E is non empty unital Group-like associative Subgroup of G
A is non empty unital Group-like associative Subgroup of G
(G,E,A) is non empty strict unital Group-like associative Subgroup of G
carr E is Element of bool the carrier of G
bool the carrier of G is non empty set
the carrier of E is non empty set
carr A is Element of bool the carrier of G
the carrier of A is non empty set
(carr E) \/ (carr A) is Element of bool the carrier of G
(G,((carr E) \/ (carr A))) is non empty strict unital Group-like associative Subgroup of G
L is Element of the carrier of G
H2 is V1() V4( NAT ) V5( the carrier of H) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of H
len H2 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
F1 is V1() V4( NAT ) V5( INT ) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of INT
len F1 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
rng H2 is set
H is non empty unital Group-like associative Subgroup of H
carr H is Element of bool the carrier of H
bool the carrier of H is non empty set
the carrier of H is non empty set
H3 is non empty unital Group-like associative Subgroup of H
carr H3 is Element of bool the carrier of H
the carrier of H3 is non empty set
(carr H) \/ (carr H3) is Element of bool the carrier of H
A is Element of the carrier of H
(H,F1,H2) is V1() V4( NAT ) V5( the carrier of H) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of H
(H,(H,F1,H2)) is Element of the carrier of H
the multF of H is V1() Function-like quasi_total associative having_a_unity Element of bool [:[: the carrier of H, the carrier of H:], the carrier of H:]
[: the carrier of H, the carrier of H:] is V1() non empty set
[:[: the carrier of H, the carrier of H:], the carrier of H:] is V1() non empty set
bool [:[: the carrier of H, the carrier of H:], the carrier of H:] is non empty set
the multF of H "**" (H,F1,H2) is Element of the carrier of H
(H,H,H3) is non empty strict unital Group-like associative Subgroup of H
(H,((carr H) \/ (carr H3))) is non empty strict unital Group-like associative Subgroup of H
G is non empty unital Group-like associative multMagma
L is non empty unital Group-like associative Subgroup of G
E is non empty unital Group-like associative Subgroup of G
(G,L,E) is non empty strict unital Group-like associative Subgroup of G
the carrier of G is non empty set
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
carr E is Element of bool the carrier of G
the carrier of E is non empty set
(carr L) \/ (carr E) is Element of bool the carrier of G
(G,((carr L) \/ (carr E))) is non empty strict unital Group-like associative Subgroup of G
(G,L,E) is Element of bool the carrier of G
(carr L) * (carr E) is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr L & b₂ in carr E ) } is set
(G,(G,L,E)) is non empty strict unital Group-like associative Subgroup of G
(G,((carr L) * (carr E))) is non empty strict unital Group-like associative Subgroup 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
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
rng A is set
(G,H,A) is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,(G,H,A)) 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,H,A) is Element of the carrier of G
rng (G,H,A) is set
carr (G,L,E) is Element of bool the carrier of G
the carrier of (G,L,E) is non empty set
H2 is set
rng H is set
dom (G,H,A) is Element of bool NAT
F1 is set
(G,H,A) . F1 is set
len (G,H,A) is 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 H is Element of bool NAT
H /. I1 is ext-real V42() V43() integer Element of INT
H . I1 is set
((H /. I1)) is ext-real V42() V43() integer Element of INT
dom A is Element of bool NAT
A /. I1 is Element of the carrier of G
A . I1 is set
b is Element of the carrier of G
c is Element of the carrier of G
b * c is Element of the carrier of G
the multF of G . (b,c) is Element of the carrier of G
i is ext-real V42() V43() integer set
(A /. I1) |^ i is Element of the carrier of G
n is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
2 * n is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
Seg (2 * n) is V46() V53(2 * n) Element of bool NAT
p is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() set
p mod 2 is ext-real V42() V43() integer set
p is set
k is set
p is set
k is set
p is set
p is V1() V4( NAT ) Function-like V46() FinSequence-like FinSubsequence-like set
dom p is Element of bool NAT
len p is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
rng p is set
{b,c} is non empty Element of bool the carrier of G
p is set
k is set
p . k is set
F1 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
F1 mod 2 is ext-real V42() V43() integer set
F1 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
F1 mod 2 is ext-real V42() V43() integer set
F1 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
F1 mod 2 is ext-real V42() V43() integer set
the carrier of (G,((carr L) \/ (carr E))) is non empty set
carr (G,((carr L) \/ (carr E))) is Element of bool the carrier of G
p is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G
k is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() set
k mod 2 is ext-real V42() V43() integer set
Seg k is V46() V53(k) Element of bool NAT
p | (Seg k) is V1() V4( NAT ) V4( Seg k) 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
k div 2 is ext-real V42() V43() integer set
(A /. I1) |^ (k div 2) is Element of the carrier of G
F1 is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence 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
2 * 0 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
0 div 2 is ext-real V42() V43() integer 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
1_ G is non being_of_order_0 Element of the carrier of G
1 + 1 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
2 - 2 is ext-real V42() V43() integer set
k - 2 is ext-real V42() V43() integer set
m is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
Seg m is V46() V53(m) Element of bool NAT
p | (Seg m) is V1() V4( NAT ) V4( Seg m) V4( NAT ) V5( the carrier of G) Function-like FinSubsequence-like Element of bool [:NAT, the carrier of G:]
1 * 2 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
m mod 2 is ext-real V42() V43() integer set
m + 2 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
q is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len q 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() set
m + l is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
len F1 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() set
k + l is ext-real V42() V43() integer set
l is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
dom q is Element of bool NAT
dom F1 is Element of bool NAT
F1 . l is set
p . l is set
q . l is set
(G,q) is Element of the carrier of G
the multF of G "**" q is Element of the carrier of G
m div 2 is ext-real V42() V43() integer set
(A /. I1) |^ (m div 2) is Element of the carrier of G
l is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
<*b,c*> 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
dom <*b,c*> is non empty V53(2) Element of bool NAT
{1,2} is non empty Element of bool NAT
<*b,c*> . l is set
m + 1 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
(m + 1) mod 2 is ext-real V42() V43() integer set
dom p is Element of bool NAT
(len q) + l is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
F1 . ((len q) + l) is set
p . (m + 1) is set
<*b,c*> . l is set
dom p is Element of bool NAT
m + (1 + 1) is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
(len q) + l is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
F1 . ((len q) + l) is set
p . (m + 2) is set
(len q) + l is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
F1 . ((len q) + l) is set
<*b,c*> . l is set
(len q) + l is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
F1 . ((len q) + l) is set
<*b,c*> . l is set
2 * 1 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
m div (2 * 1) is ext-real V42() V43() integer set
(m div (2 * 1)) + 1 is ext-real V42() V43() integer set
2 div 2 is ext-real V42() V43() integer set
(m div 2) + (2 div 2) is ext-real V42() V43() integer set
len <*b,c*> is non empty ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
(len q) + (len <*b,c*>) 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() set
k + l is ext-real V42() V43() integer set
q ^ <*b,c*> 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,<*b,c*>) is Element of the carrier of G
the multF of G "**" <*b,c*> is Element of the carrier of G
(G,q) * (G,<*b,c*>) is Element of the carrier of G
the multF of G . ((G,q),(G,<*b,c*>)) is Element of the carrier of G
(G,q) * (A /. I1) is Element of the carrier of G
the multF of G . ((G,q),(A /. I1)) is Element of the carrier of G
(m div 2) + 1 is ext-real V42() V43() integer set
(A /. I1) |^ ((m div 2) + 1) is Element of the carrier of G
rng p is set
len p is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
p | (Seg (2 * n)) is V1() V4( NAT ) V4( Seg (2 * n)) 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
(2 * n) mod 2 is ext-real V42() V43() integer set
(2 * n) div 2 is ext-real V42() V43() integer set
(G,p) is Element of the carrier of G
the multF of G "**" p is Element of the carrier of G
c " is Element of the carrier of G
b " is Element of the carrier of G
abs i is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
2 * (abs i) is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
(2 * (abs i)) mod 2 is ext-real V42() V43() integer set
(2 * (abs i)) div 2 is ext-real V42() V43() integer set
Seg (2 * (abs i)) is V46() V53(2 * (abs i)) Element of bool NAT
p is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() set
p mod 2 is ext-real V42() V43() integer set
p is set
k is set
p is set
k is set
p is set
p is V1() V4( NAT ) Function-like V46() FinSequence-like FinSubsequence-like set
dom p is Element of bool NAT
len p is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
rng p is set
{(b "),(c ")} is non empty Element of bool the carrier of G
p is set
k is set
p . k is set
F1 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
F1 mod 2 is ext-real V42() V43() integer set
F1 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
F1 mod 2 is ext-real V42() V43() integer set
F1 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
F1 mod 2 is ext-real V42() V43() integer set
the carrier of (G,((carr L) \/ (carr E))) is non empty set
carr (G,((carr L) \/ (carr E))) is Element of bool the carrier of G
p is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G
k is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() set
k mod 2 is ext-real V42() V43() integer set
Seg k is V46() V53(k) Element of bool NAT
p | (Seg k) is V1() V4( NAT ) V4( Seg k) 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
k div 2 is ext-real V42() V43() integer set
(A /. I1) |^ (k div 2) is Element of the carrier of G
((A /. I1) |^ (k div 2)) " is Element of the carrier of G
F1 is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence 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
2 * 0 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
0 div 2 is ext-real V42() V43() integer set
1_ G is non being_of_order_0 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
1 + 1 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
2 - 2 is ext-real V42() V43() integer set
k - 2 is ext-real V42() V43() integer set
m is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
Seg m is V46() V53(m) Element of bool NAT
p | (Seg m) is V1() V4( NAT ) V4( Seg m) V4( NAT ) V5( the carrier of G) Function-like FinSubsequence-like Element of bool [:NAT, the carrier of G:]
1 * 2 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
m mod 2 is ext-real V42() V43() integer set
m + 2 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
q is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len q 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() set
m + l is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
len F1 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() set
k + l is ext-real V42() V43() integer set
l is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
dom q is Element of bool NAT
dom F1 is Element of bool NAT
F1 . l is set
p . l is set
q . l is set
(G,q) is Element of the carrier of G
the multF of G "**" q is Element of the carrier of G
m div 2 is ext-real V42() V43() integer set
(A /. I1) |^ (m div 2) is Element of the carrier of G
((A /. I1) |^ (m div 2)) " is Element of the carrier of G
l is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
<*(c "),(b ")*> 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
dom <*(c "),(b ")*> is non empty V53(2) Element of bool NAT
{1,2} is non empty Element of bool NAT
<*(c "),(b ")*> . l is set
m + 1 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
(m + 1) mod 2 is ext-real V42() V43() integer set
dom p is Element of bool NAT
(len q) + l is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
F1 . ((len q) + l) is set
p . (m + 1) is set
<*(c "),(b ")*> . l is set
dom p is Element of bool NAT
m + (1 + 1) is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
(len q) + l is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
F1 . ((len q) + l) is set
p . (m + 2) is set
(len q) + l is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
F1 . ((len q) + l) is set
<*(c "),(b ")*> . l is set
(len q) + l is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
F1 . ((len q) + l) is set
<*(c "),(b ")*> . l is set
2 * 1 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
m div (2 * 1) is ext-real V42() V43() integer set
(m div (2 * 1)) + 1 is ext-real V42() V43() integer set
2 div 2 is ext-real V42() V43() integer set
(m div 2) + (2 div 2) is ext-real V42() V43() integer set
len <*(c "),(b ")*> is non empty ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
(len q) + (len <*(c "),(b ")*>) 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() set
k + l is ext-real V42() V43() integer set
q ^ <*(c "),(b ")*> 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,<*(c "),(b ")*>) is Element of the carrier of G
the multF of G "**" <*(c "),(b ")*> is Element of the carrier of G
(G,q) * (G,<*(c "),(b ")*>) is Element of the carrier of G
the multF of G . ((G,q),(G,<*(c "),(b ")*>)) is Element of the carrier of G
(c ") * (b ") is Element of the carrier of G
the multF of G . ((c "),(b ")) is Element of the carrier of G
(G,q) * ((c ") * (b ")) is Element of the carrier of G
the multF of G . ((G,q),((c ") * (b "))) is Element of the carrier of G
(A /. I1) " is Element of the carrier of G
(G,q) * ((A /. I1) ") is Element of the carrier of G
the multF of G . ((G,q),((A /. I1) ")) is Element of the carrier of G
(A /. I1) * ((A /. I1) |^ (m div 2)) is Element of the carrier of G
the multF of G . ((A /. I1),((A /. I1) |^ (m div 2))) is Element of the carrier of G
((A /. I1) * ((A /. I1) |^ (m div 2))) " is Element of the carrier of G
(m div 2) + 1 is ext-real V42() V43() integer set
(A /. I1) |^ ((m div 2) + 1) is Element of the carrier of G
((A /. I1) |^ ((m div 2) + 1)) " is Element of the carrier of G
len p is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
p | (Seg (2 * (abs i))) is V1() V4( NAT ) V4( Seg (2 * (abs i))) 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
rng p is set
(A /. I1) |^ (abs i) is Element of the carrier of G
((A /. I1) |^ (abs i)) " is Element of the carrier of G
(G,p) is Element of the carrier of G
the multF of G "**" p is Element of the carrier of G
H is set
1_ G is non being_of_order_0 Element of the carrier of G
A is Element of the carrier of G
A * (1_ G) is Element of the carrier of G
the multF of G . (A,(1_ G)) is Element of the carrier of G
1_ G is non being_of_order_0 Element of the carrier of G
A is Element of the carrier of G
(1_ G) * A is Element of the carrier of G
the multF of G . ((1_ G),A) is Element of the carrier of G
G is non empty unital Group-like associative multMagma
L is non empty unital Group-like associative Subgroup of G
E is non empty unital Group-like associative Subgroup of G
(G,L,E) is Element of bool the carrier of G
the carrier of G is non empty set
bool the carrier of G is non empty set
carr L is Element of bool the carrier of G
the carrier of L is non empty set
carr E is Element of bool the carrier of G
the carrier of E is non empty set
(carr L) * (carr E) is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr L & b₂ in carr E ) } is set
(G,E,L) is Element of bool the carrier of G
(carr E) * (carr L) is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr E & b₂ in carr L ) } is set
(G,L,E) is non empty strict unital Group-like associative Subgroup of G
(carr L) \/ (carr E) is Element of bool the carrier of G
(G,((carr L) \/ (carr E))) is non empty strict unital Group-like associative Subgroup of G
the carrier of (G,L,E) is non empty set
A is non empty strict unital Group-like associative Subgroup of G
the carrier of A is non empty set
A is Element of the carrier of G
H is Element of the carrier of G
H3 is Element of the carrier of G
H * H3 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 . (H,H3) is Element of the carrier of G
<*H,H3*> 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
rng <*H,H3*> is non empty set
{H,H3} is non empty Element of bool the carrier of G
len <*H,H3*> is non empty ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
H is ext-real V42() V43() integer set
(H) is ext-real V42() V43() integer Element of INT
<*(H),(H)*> is V1() V4( NAT ) V5( INT ) Function-like non empty V46() V53(2) FinSequence-like FinSubsequence-like FinSequence of INT
len <*(H),(H)*> 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 G) Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence 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,<*H*>) * H3 is Element of the carrier of G
the multF of G . ((G,<*H*>),H3) is Element of the carrier of G
<*H3*> 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,<*H3*>) is Element of the carrier of G
the multF of G "**" <*H3*> is Element of the carrier of G
(G,<*H*>) * (G,<*H3*>) is Element of the carrier of G
the multF of G . ((G,<*H*>),(G,<*H3*>)) is Element of the carrier of G
<*H*> ^ <*H3*> is V1() V4( NAT ) V5( the carrier of G) Function-like non empty V46() V53(1 + 1) FinSequence-like FinSubsequence-like FinSequence of the carrier of G
1 + 1 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
(G,(<*H*> ^ <*H3*>)) is Element of the carrier of G
the multF of G "**" (<*H*> ^ <*H3*>) is Element of the carrier of G
(G,<*H,H3*>) is Element of the carrier of G
the multF of G "**" <*H,H3*> is Element of the carrier of G
H |^ H is Element of the carrier of G
<*(H |^ H),H3*> 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,<*(H |^ H),H3*>) is Element of the carrier of G
the multF of G "**" <*(H |^ H),H3*> is Element of the carrier of G
H3 |^ H is Element of the carrier of G
<*(H |^ H),(H3 |^ H)*> 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,<*(H |^ H),(H3 |^ H)*>) is Element of the carrier of G
the multF of G "**" <*(H |^ H),(H3 |^ H)*> is Element of the carrier of G
(G,<*(H),(H)*>,<*H,H3*>) is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,(G,<*(H),(H)*>,<*H,H3*>)) is Element of the carrier of G
the multF of G "**" (G,<*(H),(H)*>,<*H,H3*>) is Element of the carrier of G
H is set
1_ G is non being_of_order_0 Element of the carrier of G
A is Element of the carrier of G
A * (1_ G) is Element of the carrier of G
the multF of G . (A,(1_ G)) is Element of the carrier of G
1_ G is non being_of_order_0 Element of the carrier of G
A is Element of the carrier of G
(1_ G) * A is Element of the carrier of G
the multF of G . ((1_ G),A) is Element of the carrier of G
G is non empty unital Group-like associative multMagma
L is non empty unital Group-like associative Subgroup of G
E is non empty unital Group-like associative Subgroup of G
(G,L,E) is non empty strict unital Group-like associative Subgroup of G
the carrier of G is non empty set
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
carr E is Element of bool the carrier of G
the carrier of E is non empty set
(carr L) \/ (carr E) is Element of bool the carrier of G
(G,((carr L) \/ (carr E))) is non empty strict unital Group-like associative Subgroup of G
the carrier of (G,L,E) is non empty set
(G,L,E) is Element of bool the carrier of G
(carr L) * (carr E) is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr L & b₂ in carr E ) } is set
(G,E,L) is Element of bool the carrier of G
(carr E) * (carr L) is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr E & b₂ in carr L ) } is set
G is non empty unital Group-like associative multMagma
L is non empty strict unital Group-like associative normal Subgroup of G
E is non empty strict unital Group-like associative normal Subgroup of G
(G,L,E) is non empty strict unital Group-like associative Subgroup of G
the carrier of G is non empty set
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
carr E is Element of bool the carrier of G
the carrier of E is non empty set
(carr L) \/ (carr E) is Element of bool the carrier of G
(G,((carr L) \/ (carr E))) is non empty strict unital Group-like associative Subgroup of G
the carrier of (G,L,E) is non empty set
(G,L,E) is Element of bool the carrier of G
(carr L) * (carr E) is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr L & b₂ in carr E ) } is set
(G,E,L) is Element of bool the carrier of G
(carr E) * (carr L) is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr E & b₂ in carr L ) } is set
G is non empty unital Group-like associative multMagma
L is non empty strict unital Group-like associative normal Subgroup of G
E is non empty strict unital Group-like associative normal Subgroup of G
(G,L,E) is non empty strict unital Group-like associative Subgroup of G
the carrier of G is non empty set
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
carr E is Element of bool the carrier of G
the carrier of E is non empty set
(carr L) \/ (carr E) is Element of bool the carrier of G
(G,((carr L) \/ (carr E))) is non empty strict unital Group-like associative Subgroup of G
(carr L) * (carr E) is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr L & b₂ in carr E ) } is set
the carrier of (G,L,E) is non empty set
(G,L,E) is Element of bool the carrier of G
A is non empty strict unital Group-like associative normal Subgroup of G
the carrier of A is non empty set
G is non empty unital Group-like associative multMagma
L is non empty strict unital Group-like associative Subgroup of G
(G,L,L) is non empty strict unital Group-like associative Subgroup of G
the carrier of G is non empty set
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
(carr L) \/ (carr L) is Element of bool the carrier of G
(G,((carr L) \/ (carr L))) is non empty strict unital Group-like associative Subgroup of G
G is non empty unital Group-like associative multMagma
L is non empty unital Group-like associative Subgroup of G
E is non empty unital Group-like associative Subgroup of G
(G,L,E) is non empty strict unital Group-like associative Subgroup of G
the carrier of G is non empty set
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
carr E is Element of bool the carrier of G
the carrier of E is non empty set
(carr L) \/ (carr E) is Element of bool the carrier of G
(G,((carr L) \/ (carr E))) is non empty strict unital Group-like associative Subgroup of G
(G,E,L) is non empty strict unital Group-like associative Subgroup of G
(carr E) \/ (carr L) is Element of bool the carrier of G
(G,((carr E) \/ (carr L))) is non empty strict unital Group-like associative Subgroup of G
G is non empty unital Group-like associative multMagma
L is non empty unital Group-like associative Subgroup of G
E is non empty unital Group-like associative Subgroup of G
(G,L,E) is non empty strict unital Group-like associative Subgroup of G
the carrier of G is non empty set
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
carr E is Element of bool the carrier of G
the carrier of E is non empty set
(carr L) \/ (carr E) is Element of bool the carrier of G
(G,((carr L) \/ (carr E))) is non empty strict unital Group-like associative Subgroup of G
the carrier of (G,((carr L) \/ (carr E))) is non empty set
G is non empty unital Group-like associative multMagma
L is non empty unital Group-like associative Subgroup of G
E is non empty unital Group-like associative Subgroup of G
(G,L,E) is non empty strict unital Group-like associative Subgroup of G
the carrier of G is non empty set
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
carr E is Element of bool the carrier of G
the carrier of E is non empty set
(carr L) \/ (carr E) is Element of bool the carrier of G
(G,((carr L) \/ (carr E))) is non empty strict unital Group-like associative Subgroup of G
A is non empty unital Group-like associative Subgroup of G
(G,(G,L,E),A) is non empty strict unital Group-like associative Subgroup of G
carr (G,L,E) is Element of bool the carrier of G
the carrier of (G,L,E) is non empty set
carr A is Element of bool the carrier of G
the carrier of A is non empty set
(carr (G,L,E)) \/ (carr A) is Element of bool the carrier of G
(G,((carr (G,L,E)) \/ (carr A))) is non empty strict unital Group-like associative Subgroup of G
(G,E,A) is non empty strict unital Group-like associative Subgroup of G
(carr E) \/ (carr A) is Element of bool the carrier of G
(G,((carr E) \/ (carr A))) is non empty strict unital Group-like associative Subgroup of G
(G,L,(G,E,A)) is non empty strict unital Group-like associative Subgroup of G
carr (G,E,A) is Element of bool the carrier of G
the carrier of (G,E,A) is non empty set
(carr L) \/ (carr (G,E,A)) is Element of bool the carrier of G
(G,((carr L) \/ (carr (G,E,A)))) is non empty strict unital Group-like associative Subgroup 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
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
rng A is set
(G,H,A) is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,(G,H,A)) 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,H,A) is Element of the carrier of G
carr (G,((carr L) \/ (carr (G,E,A)))) is Element of bool the carrier of G
the carrier of (G,((carr L) \/ (carr (G,E,A)))) is non empty set
H3 is set
H2 is Element of the carrier of G
F1 is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len F1 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
I1 is V1() V4( NAT ) V5( INT ) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of INT
len I1 is ext-real V35() V36() V37() V41() V42() V43() integer V46() V51() Element of NAT
rng F1 is set
(G,I1,F1) is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,(G,I1,F1)) is Element of the carrier of G
the multF of G "**" (G,I1,F1) is Element of the carrier of G
(G,A,E) is non empty strict unital Group-like associative Subgroup of G
(carr A) \/ (carr E) is Element of bool the carrier of G
(G,((carr A) \/ (carr E))) is non empty strict unital Group-like associative Subgroup of G
(G,(carr (G,((carr L) \/ (carr (G,E,A)))))) is non empty strict unital Group-like associative Subgroup of G
G is non empty unital Group-like associative multMagma
L is non empty unital Group-like associative Subgroup of G
E is non empty unital Group-like associative Subgroup of G
(G,L,E) is non empty strict unital Group-like associative Subgroup of G
the carrier of G is non empty set
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
carr E is Element of bool the carrier of G
the carrier of E is non empty set
(carr L) \/ (carr E) is Element of bool the carrier of G
(G,((carr L) \/ (carr E))) is non empty strict unital Group-like associative Subgroup of G
A is non empty unital Group-like associative Subgroup of G
(G,(G,L,E),A) is non empty strict unital Group-like associative Subgroup of G
carr (G,L,E) is Element of bool the carrier of G
the carrier of (G,L,E) is non empty set
carr A is Element of bool the carrier of G
the carrier of A is non empty set
(carr (G,L,E)) \/ (carr A) is Element of bool the carrier of G
(G,((carr (G,L,E)) \/ (carr A))) is non empty strict unital Group-like associative Subgroup of G
(G,E,A) is non empty strict unital Group-like associative Subgroup of G
(carr E) \/ (carr A) is Element of bool the carrier of G
(G,((carr E) \/ (carr A))) is non empty strict unital Group-like associative Subgroup of G
(G,L,(G,E,A)) is non empty strict unital Group-like associative Subgroup of G
carr (G,E,A) is Element of bool the carrier of G
the carrier of (G,E,A) is non empty set
(carr L) \/ (carr (G,E,A)) is Element of bool the carrier of G
(G,((carr L) \/ (carr (G,E,A)))) is non empty strict unital Group-like associative Subgroup of G
(G,(G,E,A),L) is non empty strict unital Group-like associative Subgroup of G
(carr (G,E,A)) \/ (carr L) is Element of bool the carrier of G
(G,((carr (G,E,A)) \/ (carr L))) is non empty strict unital Group-like associative Subgroup of G
(G,A,L) is non empty strict unital Group-like associative Subgroup of G
(carr A) \/ (carr L) is Element of bool the carrier of G
(G,((carr A) \/ (carr L))) is non empty strict unital Group-like associative Subgroup of G
(G,E,(G,A,L)) is non empty strict unital Group-like associative Subgroup of G
carr (G,A,L) is Element of bool the carrier of G
the carrier of (G,A,L) is non empty set
(carr E) \/ (carr (G,A,L)) is Element of bool the carrier of G
(G,((carr E) \/ (carr (G,A,L)))) is non empty strict unital Group-like associative Subgroup of G
(G,(G,A,L),E) is non empty strict unital Group-like associative Subgroup of G
(carr (G,A,L)) \/ (carr E) is Element of bool the carrier of G
(G,((carr (G,A,L)) \/ (carr E))) is non empty strict unital Group-like associative Subgroup of G
(G,A,(G,L,E)) is non empty strict unital Group-like associative Subgroup of G
(carr A) \/ (carr (G,L,E)) is Element of bool the carrier of G
(G,((carr A) \/ (carr (G,L,E)))) is non empty strict unital Group-like associative Subgroup of G
G is non empty unital Group-like associative multMagma
(1). G is non empty V73() strict unital Group-like associative Subgroup of G
L is non empty strict unital Group-like associative Subgroup of G
(G,((1). G),L) is non empty strict unital Group-like associative Subgroup of G
the carrier of G is non empty set
carr ((1). G) is Element of bool the carrier of G
bool the carrier of G is non empty set
the carrier of ((1). G) is non empty V46() set
carr L is Element of bool the carrier of G
the carrier of L is non empty set
(carr ((1). G)) \/ (carr L) is Element of bool the carrier of G
(G,((carr ((1). G)) \/ (carr L))) is non empty strict unital Group-like associative Subgroup of G
(G,L,((1). G)) is non empty strict unital Group-like associative Subgroup of G
(carr L) \/ (carr ((1). G)) is Element of bool the carrier of G
(G,((carr L) \/ (carr ((1). G)))) is non empty strict unital Group-like associative Subgroup of G
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
{(1_ G)} \/ (carr L) is non empty Element of bool the carrier of G
G is non empty unital Group-like associative multMagma
(Omega). G is non empty strict unital Group-like associative Subgroup of G
the carrier of G is non empty set
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
multMagma(# the carrier of G, the multF of G #) is strict multMagma
L is non empty unital Group-like associative Subgroup of G
(G,((Omega). G),L) is non empty strict unital Group-like associative Subgroup of G
carr ((Omega). G) is Element of bool the carrier of G
bool the carrier of G is non empty set
the carrier of ((Omega). G) is non empty set
carr L is Element of bool the carrier of G
the carrier of L is non empty set
(carr ((Omega). G)) \/ (carr L) is Element of bool the carrier of G
(G,((carr ((Omega). G)) \/ (carr L))) is non empty strict unital Group-like associative Subgroup of G
(G,L,((Omega). G)) is non empty strict unital Group-like associative Subgroup of G
(carr L) \/ (carr ((Omega). G)) is Element of bool the carrier of G
(G,((carr L) \/ (carr ((Omega). G)))) is non empty strict unital Group-like associative Subgroup of G
the carrier of ((Omega). G) \/ (carr L) is non empty set
[#] the carrier of G is non empty non proper Element of bool the carrier of G
G is non empty unital Group-like associative multMagma
L is non empty unital Group-like associative Subgroup of G
E is non empty unital Group-like associative Subgroup of G
(G,L,E) is non empty strict unital Group-like associative Subgroup of G
the carrier of G is non empty set
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
carr E is Element of bool the carrier of G
the carrier of E is non empty set
(carr L) \/ (carr E) is Element of bool the carrier of G
(G,((carr L) \/ (carr E))) is non empty strict unital Group-like associative Subgroup of G
(G,E,L) is non empty strict unital Group-like associative Subgroup of G
(carr E) \/ (carr L) is Element of bool the carrier of G
(G,((carr E) \/ (carr L))) is non empty strict unital Group-like associative Subgroup of G
G is non empty unital Group-like associative multMagma
L is non empty unital Group-like associative Subgroup of G
E is non empty strict unital Group-like associative Subgroup of G
(G,L,E) is non empty strict unital Group-like associative Subgroup of G
the carrier of G is non empty set
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
carr E is Element of bool the carrier of G
the carrier of E is non empty set
(carr L) \/ (carr E) is Element of bool the carrier of G
(G,((carr L) \/ (carr E))) is non empty strict unital Group-like associative Subgroup of G
(G,(carr E)) is non empty strict unital Group-like associative Subgroup of G
G is non empty unital Group-like associative multMagma
L is non empty unital Group-like associative Subgroup of G
E is non empty unital Group-like associative Subgroup of G
A is non empty unital Group-like associative Subgroup of G
(G,E,A) is non empty strict unital Group-like associative Subgroup of G
the carrier of G is non empty set
carr E is Element of bool the carrier of G
bool the carrier of G is non empty set
the carrier of E is non empty set
carr A is Element of bool the carrier of G
the carrier of A is non empty set
(carr E) \/ (carr A) is Element of bool the carrier of G
(G,((carr E) \/ (carr A))) is non empty strict unital Group-like associative Subgroup of G
G is non empty unital Group-like associative multMagma
L is non empty unital Group-like associative Subgroup of G
E is non empty unital Group-like associative Subgroup of G
(G,L,E) is non empty strict unital Group-like associative Subgroup of G
the carrier of G is non empty set
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
carr E is Element of bool the carrier of G
the carrier of E is non empty set
(carr L) \/ (carr E) is Element of bool the carrier of G
(G,((carr L) \/ (carr E))) is non empty strict unital Group-like associative Subgroup of G
A is non empty strict unital Group-like associative Subgroup 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
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
rng A is set
(G,H,A) is V1() V4( NAT ) V5( the carrier of G) Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,(G,H,A)) 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,H,A) is Element of the carrier of G
the carrier of A is non empty set
carr A is Element of bool the carrier of G
(G,(carr A)) is non empty strict unital Group-like associative Subgroup of G
G is non empty unital Group-like associative multMagma
L is non empty unital Group-like associative Subgroup of G
A is non empty strict unital Group-like associative Subgroup of G
E is non empty strict unital Group-like associative Subgroup of G
(G,L,E) is non empty strict unital Group-like associative Subgroup of G
the carrier of G is non empty set
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
carr E is Element of bool the carrier of G
the carrier of E is non empty set
(carr L) \/ (carr E) is Element of bool the carrier of G
(G,((carr L) \/ (carr E))) is non empty strict unital Group-like associative Subgroup of G
(G,A,E) is non empty strict unital Group-like associative Subgroup of G
carr A is Element of bool the carrier of G
the carrier of A is non empty set
(carr A) \/ (carr E) is Element of bool the carrier of G
(G,((carr A) \/ (carr E))) is non empty strict unital Group-like associative Subgroup of G
(G,(G,L,E),(G,A,E)) is non empty strict unital Group-like associative Subgroup of G
carr (G,L,E) is Element of bool the carrier of G
the carrier of (G,L,E) is non empty set
carr (G,A,E) is Element of bool the carrier of G
the carrier of (G,A,E) is non empty set
(carr (G,L,E)) \/ (carr (G,A,E)) is Element of bool the carrier of G
(G,((carr (G,L,E)) \/ (carr (G,A,E)))) is non empty strict unital Group-like associative Subgroup of G
(G,(G,L,E),A) is non empty strict unital Group-like associative Subgroup of G
(carr (G,L,E)) \/ (carr A) is Element of bool the carrier of G
(G,((carr (G,L,E)) \/ (carr A))) is non empty strict unital Group-like associative Subgroup of G
(G,(G,(G,L,E),A),E) is non empty strict unital Group-like associative Subgroup of G
carr (G,(G,L,E),A) is Element of bool the carrier of G
the carrier of (G,(G,L,E),A) is non empty set
(carr (G,(G,L,E),A)) \/ (carr E) is Element of bool the carrier of G
(G,((carr (G,(G,L,E),A)) \/ (carr E))) is non empty strict unital Group-like associative Subgroup of G
(G,E,A) is non empty strict unital Group-like associative Subgroup of G
(carr E) \/ (carr A) is Element of bool the carrier of G
(G,((carr E) \/ (carr A))) is non empty strict unital Group-like associative Subgroup of G
(G,L,(G,E,A)) is non empty strict unital Group-like associative Subgroup of G
carr (G,E,A) is Element of bool the carrier of G
the carrier of (G,E,A) is non empty set
(carr L) \/ (carr (G,E,A)) is Element of bool the carrier of G
(G,((carr L) \/ (carr (G,E,A)))) is non empty strict unital Group-like associative Subgroup of G
(G,(G,L,(G,E,A)),E) is non empty strict unital Group-like associative Subgroup of G
carr (G,L,(G,E,A)) is Element of bool the carrier of G
the carrier of (G,L,(G,E,A)) is non empty set
(carr (G,L,(G,E,A))) \/ (carr E) is Element of bool the carrier of G
(G,((carr (G,L,(G,E,A))) \/ (carr E))) is non empty strict unital Group-like associative Subgroup of G
(G,L,(G,A,E)) is non empty strict unital Group-like associative Subgroup of G
(carr L) \/ (carr (G,A,E)) is Element of bool the carrier of G
(G,((carr L) \/ (carr (G,A,E)))) is non empty strict unital Group-like associative Subgroup of G
(G,(G,L,(G,A,E)),E) is non empty strict unital Group-like associative Subgroup of G
carr (G,L,(G,A,E)) is Element of bool the carrier of G
the carrier of (G,L,(G,A,E)) is non empty set
(carr (G,L,(G,A,E))) \/ (carr E) is Element of bool the carrier of G
(G,((carr (G,L,(G,A,E))) \/ (carr E))) is non empty strict unital Group-like associative Subgroup of G
(G,L,A) is non empty strict unital Group-like associative Subgroup of G
(carr L) \/ (carr A) is Element of bool the carrier of G
(G,((carr L) \/ (carr A))) is non empty strict unital Group-like associative Subgroup of G
(G,(G,L,A),E) is non empty strict unital Group-like associative Subgroup of G
carr (G,L,A) is Element of bool the carrier of G
the carrier of (G,L,A) is non empty set
(carr (G,L,A)) \/ (carr E) is Element of bool the carrier of G
(G,((carr (G,L,A)) \/ (carr E))) is non empty strict unital Group-like associative Subgroup of G
(G,(G,(G,L,A),E),E) is non empty strict unital Group-like associative Subgroup of G
carr (G,(G,L,A),E) is Element of bool the carrier of G
the carrier of (G,(G,L,A),E) is non empty set
(carr (G,(G,L,A),E)) \/ (carr E) is Element of bool the carrier of G
(G,((carr (G,(G,L,A),E)) \/ (carr E))) is non empty strict unital Group-like associative Subgroup of G
(G,(G,A,E),E) is non empty strict unital Group-like associative Subgroup of G
(carr (G,A,E)) \/ (carr E) is Element of bool the carrier of G
(G,((carr (G,A,E)) \/ (carr E))) is non empty strict unital Group-like associative Subgroup of G
(G,E,E) is non empty strict unital Group-like associative Subgroup of G
(carr E) \/ (carr E) is Element of bool the carrier of G
(G,((carr E) \/ (carr E))) is non empty strict unital Group-like associative Subgroup of G
(G,A,(G,E,E)) is non empty strict unital Group-like associative Subgroup of G
carr (G,E,E) is Element of bool the carrier of G
the carrier of (G,E,E) is non empty set
(carr A) \/ (carr (G,E,E)) is Element of bool the carrier of G
(G,((carr A) \/ (carr (G,E,E)))) is non empty strict unital Group-like associative Subgroup of G
G is non empty unital Group-like associative multMagma
L is non empty unital Group-like associative Subgroup of G
E is non empty unital Group-like associative Subgroup of G
L /\ E is non empty strict unital Group-like associative Subgroup of G
(G,L,E) is non empty strict unital Group-like associative Subgroup of G
the carrier of G is non empty set
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
carr E is Element of bool the carrier of G
the carrier of E is non empty set
(carr L) \/ (carr E) is Element of bool the carrier of G
(G,((carr L) \/ (carr E))) is non empty strict unital Group-like associative Subgroup of G
G is non empty unital Group-like associative multMagma
L is non empty unital Group-like associative Subgroup of G
E is non empty strict unital Group-like associative Subgroup of G
L /\ E is non empty strict unital Group-like associative Subgroup of G
(G,(L /\ E),E) is non empty strict unital Group-like associative Subgroup of G
the carrier of G is non empty set
carr (L /\ E) is Element of bool the carrier of G
bool the carrier of G is non empty set
the carrier of (L /\ E) is non empty set
carr E is Element of bool the carrier of G
the carrier of E is non empty set
(carr (L /\ E)) \/ (carr E) is Element of bool the carrier of G
(G,((carr (L /\ E)) \/ (carr E))) is non empty strict unital Group-like associative Subgroup of G
G is non empty unital Group-like associative multMagma
L is non empty unital Group-like associative Subgroup of G
E is non empty strict unital Group-like associative Subgroup of G
(G,E,L) is non empty strict unital Group-like associative Subgroup of G
the carrier of G is non empty set
carr E is Element of bool the carrier of G
bool the carrier of G is non empty set
the carrier of E is non empty set
carr L is Element of bool the carrier of G
the carrier of L is non empty set
(carr E) \/ (carr L) is Element of bool the carrier of G
(G,((carr E) \/ (carr L))) is non empty strict unital Group-like associative Subgroup of G
E /\ (G,E,L) is non empty strict unital Group-like associative Subgroup of G
G is non empty unital Group-like associative multMagma
L is non empty strict unital Group-like associative Subgroup of G
E is non empty strict unital Group-like associative Subgroup of G
(G,L,E) is non empty strict unital Group-like associative Subgroup of G
the carrier of G is non empty set
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
carr E is Element of bool the carrier of G
the carrier of E is non empty set
(carr L) \/ (carr E) is Element of bool the carrier of G
(G,((carr L) \/ (carr E))) is non empty strict unital Group-like associative Subgroup of G
L /\ E is non empty strict unital Group-like associative Subgroup of G
G is non empty unital Group-like associative multMagma
Subgroups G is non empty set
[:(Subgroups G),(Subgroups G):] is V1() non empty set
[:[:(Subgroups G),(Subgroups G):],(Subgroups G):] is V1() non empty set
bool [:[:(Subgroups G),(Subgroups G):],(Subgroups G):] is non empty set
L is Element of Subgroups G
E is Element of Subgroups G
A is non empty unital Group-like associative Subgroup of G
H is non empty unital Group-like associative Subgroup of G
(G,A,H) is non empty strict unital Group-like associative Subgroup of G
the carrier of G is non empty set
carr A is Element of bool the carrier of G
bool the carrier of G is non empty set
the carrier of A is non empty set
carr H is Element of bool the carrier of G
the carrier of H is non empty set
(carr A) \/ (carr H) is Element of bool the carrier of G
(G,((carr A) \/ (carr H))) is non empty strict unital Group-like associative Subgroup of G
A is Element of Subgroups G
H is non empty unital Group-like associative Subgroup of G
H3 is non empty unital Group-like associative Subgroup of G
(G,H,H3) is non empty strict unital Group-like associative Subgroup of G
carr H is Element of bool the carrier of G
the carrier of H is non empty set
carr H3 is Element of bool the carrier of G
the carrier of H3 is non empty set
(carr H) \/ (carr H3) is Element of bool the carrier of G
(G,((carr H) \/ (carr H3))) is non empty strict unital Group-like associative Subgroup of G
L is V1() Function-like quasi_total Element of bool [:[:(Subgroups G),(Subgroups G):],(Subgroups G):]
E is non empty strict unital Group-like associative Subgroup of G
A is non empty strict unital Group-like associative Subgroup of G
L . (E,A) is set
(G,E,A) is non empty strict unital Group-like associative Subgroup of G
the carrier of G is non empty set
carr E is Element of bool the carrier of G
bool the carrier of G is non empty set
the carrier of E is non empty set
carr A is Element of bool the carrier of G
the carrier of A is non empty set
(carr E) \/ (carr A) is Element of bool the carrier of G
(G,((carr E) \/ (carr A))) is non empty strict unital Group-like associative Subgroup of G
L is V1() Function-like quasi_total Element of bool [:[:(Subgroups G),(Subgroups G):],(Subgroups G):]
E is V1() Function-like quasi_total Element of bool [:[:(Subgroups G),(Subgroups G):],(Subgroups G):]
A is set
H is set
A is Element of Subgroups G
H is Element of Subgroups G
L . (A,H) is Element of Subgroups G
H3 is non empty strict unital Group-like associative Subgroup of G
H2 is non empty strict unital Group-like associative Subgroup of G
(G,H3,H2) is non empty strict unital Group-like associative Subgroup of G
the carrier of G is non empty set
carr H3 is Element of bool the carrier of G
bool the carrier of G is non empty set
the carrier of H3 is non empty set
carr H2 is Element of bool the carrier of G
the carrier of H2 is non empty set
(carr H3) \/ (carr H2) is Element of bool the carrier of G
(G,((carr H3) \/ (carr H2))) is non empty strict unital Group-like associative Subgroup of G
L . (A,H) is set
E . (A,H) is set
G is non empty unital Group-like associative multMagma
Subgroups G is non empty set
[:(Subgroups G),(Subgroups G):] is V1() non empty set
[:[:(Subgroups G),(Subgroups G):],(Subgroups G):] is V1() non empty set
bool [:[:(Subgroups G),(Subgroups G):],(Subgroups G):] is non empty set
L is Element of Subgroups G
E is Element of Subgroups G
A is non empty unital Group-like associative Subgroup of G
H is non empty unital Group-like associative Subgroup of G
A /\ H is non empty strict unital Group-like associative Subgroup of G
A is Element of Subgroups G
H is non empty unital Group-like associative Subgroup of G
H3 is non empty unital Group-like associative Subgroup of G
H /\ H3 is non empty strict unital Group-like associative Subgroup of G
L is V1() Function-like quasi_total Element of bool [:[:(Subgroups G),(Subgroups G):],(Subgroups G):]
E is non empty strict unital Group-like associative Subgroup of G
A is non empty strict unital Group-like associative Subgroup of G
L . (E,A) is set
E /\ A is non empty strict unital Group-like associative Subgroup of G
L is V1() Function-like quasi_total Element of bool [:[:(Subgroups G),(Subgroups G):],(Subgroups G):]
E is V1() Function-like quasi_total Element of bool [:[:(Subgroups G),(Subgroups G):],(Subgroups G):]
A is set
H is set
A is Element of Subgroups G
H is Element of Subgroups G
L . (A,H) is Element of Subgroups G
H3 is non empty strict unital Group-like associative Subgroup of G
H2 is non empty strict unital Group-like associative Subgroup of G
H3 /\ H2 is non empty strict unital Group-like associative Subgroup of G
L . (A,H) is set
E . (A,H) is set
G is non empty unital Group-like associative multMagma
Subgroups G is non empty set
(G) is V1() Function-like quasi_total Element of bool [:[:(Subgroups G),(Subgroups G):],(Subgroups G):]
[:(Subgroups G),(Subgroups G):] is V1() non empty set
[:[:(Subgroups G),(Subgroups G):],(Subgroups G):] is V1() non empty set
bool [:[:(Subgroups G),(Subgroups G):],(Subgroups G):] is non empty set
(G) is V1() Function-like quasi_total Element of bool [:[:(Subgroups G),(Subgroups G):],(Subgroups G):]
LattStr(# (Subgroups G),(G),(G) #) is non empty strict LattStr
the carrier of LattStr(# (Subgroups G),(G),(G) #) is non empty set
E is Element of the carrier of LattStr(# (Subgroups G),(G),(G) #)
H is non empty strict unital Group-like associative Subgroup of G
A is Element of the carrier of LattStr(# (Subgroups G),(G),(G) #)
A is non empty strict unital Group-like associative Subgroup of G
E "\/" A is Element of the carrier of LattStr(# (Subgroups G),(G),(G) #)
(G) . (E,A) is set
(G,H,A) is non empty strict unital Group-like associative Subgroup of G
the carrier of G is non empty set
carr H is Element of bool the carrier of G
bool the carrier of G is non empty set
the carrier of H is non empty set
carr A is Element of bool the carrier of G
the carrier of A is non empty set
(carr H) \/ (carr A) is Element of bool the carrier of G
(G,((carr H) \/ (carr A))) is non empty strict unital Group-like associative Subgroup of G
E is Element of the carrier of LattStr(# (Subgroups G),(G),(G) #)
H is non empty strict unital Group-like associative Subgroup of G
A is Element of the carrier of LattStr(# (Subgroups G),(G),(G) #)
A is non empty strict unital Group-like associative Subgroup of G
E "/\" A is Element of the carrier of LattStr(# (Subgroups G),(G),(G) #)
(G) . (E,A) is set
H /\ A is non empty strict unital Group-like associative Subgroup of G
E is Element of the carrier of LattStr(# (Subgroups G),(G),(G) #)
A is Element of the carrier of LattStr(# (Subgroups G),(G),(G) #)
H is Element of the carrier of LattStr(# (Subgroups G),(G),(G) #)
H is non empty strict unital Group-like associative Subgroup of G
H3 is non empty strict unital Group-like associative Subgroup of G
(G,H,H3) is non empty strict unital Group-like associative Subgroup of G
carr H is Element of bool the carrier of G
the carrier of H is non empty set
carr H3 is Element of bool the carrier of G
the carrier of H3 is non empty set
(carr H) \/ (carr H3) is Element of bool the carrier of G
(G,((carr H) \/ (carr H3))) is non empty strict unital Group-like associative Subgroup of G
A "\/" H is Element of the carrier of LattStr(# (Subgroups G),(G),(G) #)
E "\/" A is Element of the carrier of LattStr(# (Subgroups G),(G),(G) #)
A is non empty strict unital Group-like associative Subgroup of G
(G,A,H) is non empty strict unital Group-like associative Subgroup of G
carr A is Element of bool the carrier of G
the carrier of A is non empty set
(carr A) \/ (carr H) is Element of bool the carrier of G
(G,((carr A) \/ (carr H))) is non empty strict unital Group-like associative Subgroup of G
(G,H,A) is non empty strict unital Group-like associative Subgroup of G
(carr H) \/ (carr A) is Element of bool the carrier of G
(G,((carr H) \/ (carr A))) is non empty strict unital Group-like associative Subgroup of G
A "\/" E is Element of the carrier of LattStr(# (Subgroups G),(G),(G) #)
(E "\/" A) "\/" H is Element of the carrier of LattStr(# (Subgroups G),(G),(G) #)
(G,(G,A,H),H3) is non empty strict unital Group-like associative Subgroup of G
carr (G,A,H) is Element of bool the carrier of G
the carrier of (G,A,H) is non empty set
(carr (G,A,H)) \/ (carr H3) is Element of bool the carrier of G
(G,((carr (G,A,H)) \/ (carr H3))) is non empty strict unital Group-like associative Subgroup of G
(G,A,(G,H,H3)) is non empty strict unital Group-like associative Subgroup of G
carr (G,H,H3) is Element of bool the carrier of G
the carrier of (G,H,H3) is non empty set
(carr A) \/ (carr (G,H,H3)) is Element of bool the carrier of G
(G,((carr A) \/ (carr (G,H,H3)))) is non empty strict unital Group-like associative Subgroup of G
E "\/" (A "\/" H) is Element of the carrier of LattStr(# (Subgroups G),(G),(G) #)
A /\ H is non empty strict unital Group-like associative Subgroup of G
E "/\" A is Element of the carrier of LattStr(# (Subgroups G),(G),(G) #)
(E "/\" A) "\/" A is Element of the carrier of LattStr(# (Subgroups G),(G),(G) #)
(G,(A /\ H),H) is non empty strict unital Group-like associative Subgroup of G
carr (A /\ H) is Element of bool the carrier of G
the carrier of (A /\ H) is non empty set
(carr (A /\ H)) \/ (carr H) is Element of bool the carrier of G
(G,((carr (A /\ H)) \/ (carr H))) is non empty strict unital Group-like associative Subgroup of G
H /\ H3 is non empty strict unital Group-like associative Subgroup of G
A "/\" H is Element of the carrier of LattStr(# (Subgroups G),(G),(G) #)
H /\ A is non empty strict unital Group-like associative Subgroup of G
A "/\" E is Element of the carrier of LattStr(# (Subgroups G),(G),(G) #)
(E "/\" A) "/\" H is Element of the carrier of LattStr(# (Subgroups G),(G),(G) #)
(A /\ H) /\ H3 is non empty strict unital Group-like associative Subgroup of G
A /\ (H /\ H3) is non empty strict unital Group-like associative Subgroup of G
E "/\" (A "/\" H) is Element of the carrier of LattStr(# (Subgroups G),(G),(G) #)
E "/\" (E "\/" A) is Element of the carrier of LattStr(# (Subgroups G),(G),(G) #)
A /\ (G,A,H) is non empty strict unital Group-like associative Subgroup of G
E is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of E is non empty set
(1). G is non empty V73() strict unital Group-like associative Subgroup of G
H is Element of the carrier of E
A is Element of the carrier of E
A "/\" H is Element of the carrier of E
A is non empty strict unital Group-like associative Subgroup of G
((1). G) /\ A is non empty strict unital Group-like associative Subgroup of G
H "/\" A is Element of the carrier of E
(Omega). G is non empty strict unital Group-like associative Subgroup 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
multMagma(# the carrier of G, the multF of G #) is strict multMagma
A is Element of the carrier of E
H is Element of the carrier of E
H "\/" A is Element of the carrier of E
H is non empty strict unital Group-like associative Subgroup of G
(G,((Omega). G),H) is non empty strict unital Group-like associative Subgroup of G
carr ((Omega). G) is Element of bool the carrier of G
the carrier of ((Omega). G) is non empty set
carr H is Element of bool the carrier of G
the carrier of H is non empty set
(carr ((Omega). G)) \/ (carr H) is Element of bool the carrier of G
(G,((carr ((Omega). G)) \/ (carr H))) is non empty strict unital Group-like associative Subgroup of G
A "\/" H is Element of the carrier of E
G is non empty unital Group-like associative multMagma
Subgroups G is non empty set
(G) is V1() Function-like quasi_total Element of bool [:[:(Subgroups G),(Subgroups G):],(Subgroups G):]
[:(Subgroups G),(Subgroups G):] is V1() non empty set
[:[:(Subgroups G),(Subgroups G):],(Subgroups G):] is V1() non empty set
bool [:[:(Subgroups G),(Subgroups G):],(Subgroups G):] is non empty set
(G) is V1() Function-like quasi_total Element of bool [:[:(Subgroups G),(Subgroups G):],(Subgroups G):]
LattStr(# (Subgroups G),(G),(G) #) is non empty strict LattStr
G is non empty unital Group-like associative multMagma
(G) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
Subgroups G is non empty set
(G) is V1() Function-like quasi_total Element of bool [:[:(Subgroups G),(Subgroups G):],(Subgroups G):]
[:(Subgroups G),(Subgroups G):] is V1() non empty set
[:[:(Subgroups G),(Subgroups G):],(Subgroups G):] is V1() non empty set
bool [:[:(Subgroups G),(Subgroups G):],(Subgroups G):] is non empty set
(G) is V1() Function-like quasi_total Element of bool [:[:(Subgroups G),(Subgroups G):],(Subgroups G):]
LattStr(# (Subgroups G),(G),(G) #) is non empty strict LattStr
the carrier of (G) is non empty set
G is non empty unital Group-like associative multMagma
(G) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
Subgroups G is non empty set
(G) is V1() Function-like quasi_total Element of bool [:[:(Subgroups G),(Subgroups G):],(Subgroups G):]
[:(Subgroups G),(Subgroups G):] is V1() non empty set
[:[:(Subgroups G),(Subgroups G):],(Subgroups G):] is V1() non empty set
bool [:[:(Subgroups G),(Subgroups G):],(Subgroups G):] is non empty set
(G) is V1() Function-like quasi_total Element of bool [:[:(Subgroups G),(Subgroups G):],(Subgroups G):]
LattStr(# (Subgroups G),(G),(G) #) is non empty strict LattStr
the carrier of (G) is non empty set
[: the carrier of (G), the carrier of (G):] is V1() non empty set
the L_join 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):], 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
G is non empty unital Group-like associative multMagma
(G) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
Subgroups G is non empty set
(G) is V1() Function-like quasi_total Element of bool [:[:(Subgroups G),(Subgroups G):],(Subgroups G):]
[:(Subgroups G),(Subgroups G):] is V1() non empty set
[:[:(Subgroups G),(Subgroups G):],(Subgroups G):] is V1() non empty set
bool [:[:(Subgroups G),(Subgroups G):],(Subgroups G):] is non empty set
(G) is V1() Function-like quasi_total Element of bool [:[:(Subgroups G),(Subgroups G):],(Subgroups G):]
LattStr(# (Subgroups G),(G),(G) #) is non empty strict LattStr
the carrier of (G) is non empty set
[: the carrier of (G), the carrier of (G):] is V1() non empty set
the L_meet 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):], 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
G is non empty unital Group-like associative multMagma
(G) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
Subgroups G is non empty set
(G) is V1() Function-like quasi_total Element of bool [:[:(Subgroups G),(Subgroups G):],(Subgroups G):]
[:(Subgroups G),(Subgroups G):] is V1() non empty set
[:[:(Subgroups G),(Subgroups G):],(Subgroups G):] is V1() non empty set
bool [:[:(Subgroups G),(Subgroups G):],(Subgroups G):] is non empty set
(G) is V1() Function-like quasi_total Element of bool [:[:(Subgroups G),(Subgroups G):],(Subgroups G):]
LattStr(# (Subgroups G),(G),(G) #) is non empty strict LattStr
G is non empty unital Group-like associative multMagma
(G) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V95() LattStr
Subgroups G is non empty set
(G) is V1() Function-like quasi_total Element of bool [:[:(Subgroups G),(Subgroups G):],(Subgroups G):]
[:(Subgroups G),(Subgroups G):] is V1() non empty set
[:[:(Subgroups G),(Subgroups G):],(Subgroups G):] is V1() non empty set
bool [:[:(Subgroups G),(Subgroups G):],(Subgroups G):] is non empty set
(G) is V1() Function-like quasi_total Element of bool [:[:(Subgroups G),(Subgroups G):],(Subgroups G):]
LattStr(# (Subgroups G),(G),(G) #) is non empty strict LattStr
Bottom (G) is Element of the carrier of (G)
the carrier of (G) is non empty set
(1). G is non empty V73() strict unital Group-like associative Subgroup of G
A is Element of the carrier of (G)
E is Element of the carrier of (G)
A "/\" E is Element of the carrier of (G)
(G) . (A,E) is set
H is non empty strict unital Group-like associative Subgroup of G
H /\ ((1). G) is non empty strict unital Group-like associative Subgroup of G
G is non empty unital Group-like associative multMagma
(G) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V95() LattStr
Subgroups G is non empty set
(G) is V1() Function-like quasi_total Element of bool [:[:(Subgroups G),(Subgroups G):],(Subgroups G):]
[:(Subgroups G),(Subgroups G):] is V1() non empty set
[:[:(Subgroups G),(Subgroups G):],(Subgroups G):] is V1() non empty set
bool [:[:(Subgroups G),(Subgroups G):],(Subgroups G):] is non empty set
(G) is V1() Function-like quasi_total Element of bool [:[:(Subgroups G),(Subgroups G):],(Subgroups G):]
LattStr(# (Subgroups G),(G),(G) #) is non empty strict LattStr
Top (G) is Element of the carrier of (G)
the carrier of (G) is non empty set
(Omega). G is non empty strict unital Group-like associative Subgroup of G
the carrier of G is non empty set
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
multMagma(# the carrier of G, the multF of G #) is strict multMagma
A is Element of the carrier of (G)
E is Element of the carrier of (G)
A "\/" E is Element of the carrier of (G)
(G) . (A,E) is set
H is non empty strict unital Group-like associative Subgroup of G
(G,H,((Omega). G)) is non empty strict unital Group-like associative Subgroup of G
carr H is Element of bool the carrier of G
bool the carrier of G is non empty set
the carrier of H is non empty set
carr ((Omega). G) is Element of bool the carrier of G
the carrier of ((Omega). G) is non empty set
(carr H) \/ (carr ((Omega). G)) is Element of bool the carrier of G
(G,((carr H) \/ (carr ((Omega). G)))) is non empty strict unital Group-like associative Subgroup of G