:: GROUP_5 semantic presentation

REAL is non empty non finite set
NAT is non empty V18() V19() V20() non finite cardinal limit_cardinal Element of K19(REAL)
K19(REAL) is non empty non finite set
NAT is non empty V18() V19() V20() non finite cardinal limit_cardinal set
K19(NAT) is non empty non finite set
K19(NAT) is non empty non finite set
K172(NAT) is V49() set
INT is non empty non finite set
COMPLEX is non empty non finite set
RAT is non empty non finite set
K20(COMPLEX,COMPLEX) is non empty non finite set
K19(K20(COMPLEX,COMPLEX)) is non empty non finite set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is non empty non finite set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is non empty non finite set
K20(REAL,REAL) is non empty non finite set
K19(K20(REAL,REAL)) is non empty non finite set
K20(K20(REAL,REAL),REAL) is non empty non finite set
K19(K20(K20(REAL,REAL),REAL)) is non empty non finite set
K20(RAT,RAT) is non empty non finite set
K19(K20(RAT,RAT)) is non empty non finite set
K20(K20(RAT,RAT),RAT) is non empty non finite set
K19(K20(K20(RAT,RAT),RAT)) is non empty non finite set
K20(INT,INT) is non empty non finite set
K19(K20(INT,INT)) is non empty non finite set
K20(K20(INT,INT),INT) is non empty non finite set
K19(K20(K20(INT,INT),INT)) is non empty non finite set
K20(NAT,NAT) is non empty non finite set
K20(K20(NAT,NAT),NAT) is non empty non finite set
K19(K20(K20(NAT,NAT),NAT)) is non empty non finite set
{} is functional empty V18() V19() V20() V22() V23() V24() V25() V26() finite cardinal {} -element FinSequence-membered V50() integer set
the functional empty V18() V19() V20() V22() V23() V24() V25() V26() finite cardinal {} -element FinSequence-membered V50() integer set is functional empty V18() V19() V20() V22() V23() V24() V25() V26() finite cardinal {} -element FinSequence-membered V50() integer set
1 is non empty V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
2 is non empty V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
3 is non empty V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
Seg 1 is non empty V12() finite 1 -element Element of K19(NAT)
{1} is non empty V12() 1 -element set
Seg 2 is non empty finite 2 -element Element of K19(NAT)
{1,2} is non empty set
G is set
a is non empty unital Group-like associative L11()
(1). a is non empty finite strict unital Group-like associative Subgroup of a
1_ a is non being_of_order_0 Element of the carrier of a
the carrier of a is non empty set
the carrier of ((1). a) is non empty finite set
{(1_ a)} is non empty V12() 1 -element Element of K19( the carrier of a)
K19( the carrier of a) is non empty set
G is non empty unital Group-like associative L11()
the carrier of G is non empty set
a is Element of the carrier of G
b is Element of the carrier of G
a |^ b is Element of the carrier of G
b " is Element of the carrier of G
(b ") * a is Element of the carrier of G
((b ") * a) * b is Element of the carrier of G
b is non empty unital Group-like associative Subgroup of G
a * b is Element of the carrier of G
(b ") * (a * b) is Element of the carrier of G
G is non empty unital Group-like associative L11()
the carrier of G is non empty set
a is Element of the carrier of G
b is Element of the carrier of G
a |^ b is Element of the carrier of G
b " is Element of the carrier of G
(b ") * a is Element of the carrier of G
((b ") * a) * b is Element of the carrier of G
b is non empty strict unital Group-like associative normal Subgroup of G
b |^ b is non empty strict unital Group-like associative Subgroup of G
G is set
a is non empty unital Group-like associative L11()
the carrier of a is non empty set
b is non empty unital Group-like associative Subgroup of a
b is non empty unital Group-like associative Subgroup of a
b * b is Element of K19( the carrier of a)
K19( the carrier of a) is non empty set
carr b is Element of K19( the carrier of a)
the carrier of b is non empty set
carr b is Element of K19( the carrier of a)
the carrier of b is non empty set
(carr b) * (carr b) is Element of K19( the carrier of a)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of a : ( b₁ in carr b & b₂ in carr b ) } is set
(carr b) * b is Element of K19( the carrier of a)
c is Element of the carrier of a
d is Element of the carrier of a
c * d is Element of the carrier of a
c is Element of the carrier of a
d is Element of the carrier of a
c * d is Element of the carrier of a
b * (carr b) is Element of K19( the carrier of a)
G is set
a is non empty unital Group-like associative L11()
the carrier of a is non empty set
b is non empty unital Group-like associative Subgroup of a
b is non empty unital Group-like associative Subgroup of a
b * b is Element of K19( the carrier of a)
K19( the carrier of a) is non empty set
carr b is Element of K19( the carrier of a)
the carrier of b is non empty set
carr b is Element of K19( the carrier of a)
the carrier of b is non empty set
(carr b) * (carr b) is Element of K19( the carrier of a)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of a : ( b₁ in carr b & b₂ in carr b ) } is set
b * b is Element of K19( the carrier of a)
(carr b) * (carr b) is Element of K19( the carrier of a)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of a : ( b₁ in carr b & b₂ in carr b ) } is set
b "\/" b is non empty strict unital Group-like associative Subgroup of a
(carr b) \/ (carr b) is Element of K19( the carrier of a)
gr ((carr b) \/ (carr b)) is non empty strict unital Group-like associative Subgroup of a
the carrier of (b "\/" b) is non empty set
c is Element of the carrier of a
d is Element of the carrier of a
c * d is Element of the carrier of a
the carrier of (b "\/" b) is non empty set
G is set
a is non empty unital Group-like associative L11()
the carrier of a is non empty set
b is non empty unital Group-like associative Subgroup of a
b is non empty unital Group-like associative Subgroup of a
b "\/" b is non empty strict unital Group-like associative Subgroup of a
carr b is Element of K19( the carrier of a)
K19( the carrier of a) is non empty set
the carrier of b is non empty set
carr b is Element of K19( the carrier of a)
the carrier of b is non empty set
(carr b) \/ (carr b) is Element of K19( the carrier of a)
gr ((carr b) \/ (carr b)) is non empty strict unital Group-like associative Subgroup of a
b * b is Element of K19( the carrier of a)
(carr b) * (carr b) is Element of K19( the carrier of a)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of a : ( b₁ in carr b & b₂ in carr b ) } is set
b * b is Element of K19( the carrier of a)
(carr b) * (carr b) is Element of K19( the carrier of a)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of a : ( b₁ in carr b & b₂ in carr b ) } is set
c is Element of the carrier of a
d is Element of the carrier of a
c * d is Element of the carrier of a
G is set
a is non empty unital Group-like associative L11()
the carrier of a is non empty set
b is non empty strict unital Group-like associative normal Subgroup of a
b is non empty strict unital Group-like associative normal Subgroup of a
b "\/" b is non empty strict unital Group-like associative Subgroup of a
carr b is Element of K19( the carrier of a)
K19( the carrier of a) is non empty set
the carrier of b is non empty set
carr b is Element of K19( the carrier of a)
the carrier of b is non empty set
(carr b) \/ (carr b) is Element of K19( the carrier of a)
gr ((carr b) \/ (carr b)) is non empty strict unital Group-like associative Subgroup of a
b * b is Element of K19( the carrier of a)
(carr b) * (carr b) is Element of K19( the carrier of a)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of a : ( b₁ in carr b & b₂ in carr b ) } is set
b * b is Element of K19( the carrier of a)
(carr b) * (carr b) is Element of K19( the carrier of a)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of a : ( b₁ in carr b & b₂ in carr b ) } is set
c is Element of the carrier of a
d is Element of the carrier of a
c * d is Element of the carrier of a
G is non empty unital Group-like associative L11()
a is non empty unital Group-like associative Subgroup of G
b is non empty unital Group-like associative normal Subgroup of G
a * b is Element of K19( the carrier of G)
the carrier of G is non empty set
K19( the carrier of G) is non empty set
carr a is Element of K19( the carrier of G)
the carrier of a is non empty set
carr b is Element of K19( the carrier of G)
the carrier of b is non empty set
(carr a) * (carr b) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr a & b₂ in carr b ) } is set
b * a is Element of K19( the carrier of G)
(carr b) * (carr a) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr b & b₂ in carr a ) } is set
(carr a) * b is Element of K19( the carrier of G)
b * (carr a) is Element of K19( the carrier of G)
G is non empty unital Group-like associative L11()
the carrier of G is non empty set
a is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len a is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
dom a is Element of K19(NAT)
b is Element of the carrier of G
b is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len b is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
dom b is Element of K19(NAT)
b is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len b is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
c is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len c is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
dom b is Element of K19(NAT)
Seg (len a) is finite len a -element Element of K19(NAT)
d is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer set
b . d is set
a /. d is Element of the carrier of G
(a /. d) |^ b is Element of the carrier of G
b " is Element of the carrier of G
(b ") * (a /. d) is Element of the carrier of G
((b ") * (a /. d)) * b is Element of the carrier of G
c . d is set
G is non empty unital Group-like associative L11()
the carrier of G is non empty set
a is Element of the carrier of G
b is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,b,a) is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
b is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,b,a) is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,b,a) ^ (G,b,a) is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
b ^ b is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,(b ^ b),a) is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
c is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
dom (G,b,a) is Element of K19(NAT)
len (G,b,a) is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
Seg (len (G,b,a)) is finite len (G,b,a) -element Element of K19(NAT)
len b is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
Seg (len b) is finite len b -element Element of K19(NAT)
dom b is Element of K19(NAT)
b /. c is Element of the carrier of G
(b ^ b) /. c is Element of the carrier of G
dom (b ^ b) is Element of K19(NAT)
(G,b,a) . c is set
(b /. c) |^ a is Element of the carrier of G
a " is Element of the carrier of G
(a ") * (b /. c) is Element of the carrier of G
((a ") * (b /. c)) * a is Element of the carrier of G
(G,(b ^ b),a) . c is set
c is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
dom (G,b,a) is Element of K19(NAT)
len b is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
len (G,b,a) is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
dom b is Element of K19(NAT)
(len b) + c is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
(len (G,b,a)) + c is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
(G,(b ^ b),a) . ((len (G,b,a)) + c) is set
(b ^ b) /. ((len (G,b,a)) + c) is Element of the carrier of G
((b ^ b) /. ((len (G,b,a)) + c)) |^ a is Element of the carrier of G
(a ") * ((b ^ b) /. ((len (G,b,a)) + c)) is Element of the carrier of G
((a ") * ((b ^ b) /. ((len (G,b,a)) + c))) * a is Element of the carrier of G
(b ^ b) /. ((len b) + c) is Element of the carrier of G
((b ^ b) /. ((len b) + c)) |^ a is Element of the carrier of G
(a ") * ((b ^ b) /. ((len b) + c)) is Element of the carrier of G
((a ") * ((b ^ b) /. ((len b) + c))) * a is Element of the carrier of G
b /. c is Element of the carrier of G
(b /. c) |^ a is Element of the carrier of G
(a ") * (b /. c) is Element of the carrier of G
((a ") * (b /. c)) * a is Element of the carrier of G
(G,b,a) . c is set
(len (G,b,a)) + (len (G,b,a)) is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
(len b) + (len (G,b,a)) is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
(len b) + (len b) is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
len (b ^ b) is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
len (G,(b ^ b),a) is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
G is non empty unital Group-like associative L11()
the carrier of G is non empty set
<*> the carrier of G is V1() V4( NAT ) V5( the carrier of G) Function-like functional empty proper V18() V19() V20() V22() V23() V24() V25() V26() finite cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V50() integer FinSequence of the carrier of G
K20(NAT, the carrier of G) is non empty non finite set
a is Element of the carrier of G
(G,(<*> the carrier of G),a) is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len (G,(<*> the carrier of G),a) is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
len (<*> the carrier of G) is functional empty V18() V19() V20() V22() V23() V24() V25() V26() finite cardinal {} -element FinSequence-membered V50() integer Element of NAT
G is non empty unital Group-like associative L11()
the carrier of G is non empty set
a is Element of the carrier of G
<*a*> is V1() V4( NAT ) V5( the carrier of G) Function-like non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of G
b is Element of the carrier of G
(G,<*a*>,b) is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
a |^ b is Element of the carrier of G
b " is Element of the carrier of G
(b ") * a is Element of the carrier of G
((b ") * a) * b is Element of the carrier of G
<*(a |^ b)*> is V1() V4( NAT ) V5( the carrier of G) Function-like non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of G
b is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer set
dom <*a*> is non empty V12() 1 -element Element of K19(NAT)
{1} is non empty V12() 1 -element Element of K19(NAT)
<*(a |^ b)*> . b is set
<*a*> /. b is Element of the carrier of G
(<*a*> /. b) |^ b is Element of the carrier of G
(b ") * (<*a*> /. b) is Element of the carrier of G
((b ") * (<*a*> /. b)) * b is Element of the carrier of G
len <*(a |^ b)*> is non empty V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
len <*a*> is non empty V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
G is non empty unital Group-like associative L11()
the carrier of G is non empty set
a is Element of the carrier of G
b is Element of the carrier of G
<*a,b*> is V1() V4( NAT ) V5( the carrier of G) Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of G
b is Element of the carrier of G
(G,<*a,b*>,b) is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
a |^ b is Element of the carrier of G
b " is Element of the carrier of G
(b ") * a is Element of the carrier of G
((b ") * a) * b is Element of the carrier of G
b |^ b is Element of the carrier of G
(b ") * b is Element of the carrier of G
((b ") * b) * b is Element of the carrier of G
<*(a |^ b),(b |^ b)*> is V1() V4( NAT ) V5( the carrier of G) Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of G
<*a*> is V1() V4( NAT ) V5( the carrier of G) Function-like non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of G
<*b*> is V1() V4( NAT ) V5( the carrier of G) Function-like non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of G
<*a*> ^ <*b*> is V1() V4( NAT ) V5( the carrier of G) Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of G
1 + 1 is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
(G,(<*a*> ^ <*b*>),b) is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,<*a*>,b) is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,<*b*>,b) is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,<*a*>,b) ^ (G,<*b*>,b) is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
<*(a |^ b)*> is V1() V4( NAT ) V5( the carrier of G) Function-like non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of G
<*(a |^ b)*> ^ (G,<*b*>,b) is V1() V4( NAT ) V5( the carrier of G) Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
<*(b |^ b)*> is V1() V4( NAT ) V5( the carrier of G) Function-like non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of G
<*(a |^ b)*> ^ <*(b |^ b)*> is V1() V4( NAT ) V5( the carrier of G) Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of G
G is non empty unital Group-like associative L11()
the carrier of G is non empty set
a is Element of the carrier of G
b is Element of the carrier of G
b is Element of the carrier of G
<*a,b,b*> is V1() V4( NAT ) V5( the carrier of G) Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of G
c is Element of the carrier of G
(G,<*a,b,b*>,c) is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
a |^ c is Element of the carrier of G
c " is Element of the carrier of G
(c ") * a is Element of the carrier of G
((c ") * a) * c is Element of the carrier of G
b |^ c is Element of the carrier of G
(c ") * b is Element of the carrier of G
((c ") * b) * c is Element of the carrier of G
b |^ c is Element of the carrier of G
(c ") * b is Element of the carrier of G
((c ") * b) * c is Element of the carrier of G
<*(a |^ c),(b |^ c),(b |^ c)*> is V1() V4( NAT ) V5( the carrier of G) Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of G
<*a*> is V1() V4( NAT ) V5( the carrier of G) Function-like non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of G
<*b,b*> is V1() V4( NAT ) V5( the carrier of G) Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of G
<*a*> ^ <*b,b*> is V1() V4( NAT ) V5( the carrier of G) Function-like non empty finite 1 + 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of G
1 + 2 is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
(G,(<*a*> ^ <*b,b*>),c) is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,<*a*>,c) is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,<*b,b*>,c) is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,<*a*>,c) ^ (G,<*b,b*>,c) is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
<*(b |^ c),(b |^ c)*> is V1() V4( NAT ) V5( the carrier of G) Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,<*a*>,c) ^ <*(b |^ c),(b |^ c)*> is V1() V4( NAT ) V5( the carrier of G) Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
<*(a |^ c)*> is V1() V4( NAT ) V5( the carrier of G) Function-like non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of G
<*(a |^ c)*> ^ <*(b |^ c),(b |^ c)*> is V1() V4( NAT ) V5( the carrier of G) Function-like non empty finite 1 + 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of G
G is non empty unital Group-like associative L11()
the carrier of G is non empty set
a is Element of the carrier of G
b is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,b,a) is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
Product (G,b,a) is Element of the carrier of G
the U8 of G is V1() V4(K20( the carrier of G, the carrier of G)) V5( the carrier of G) Function-like V32(K20( the carrier of G, the carrier of G), the carrier of G) Element of K19(K20(K20( the carrier of G, the carrier of G), the carrier of G))
K20( the carrier of G, the carrier of G) is non empty set
K20(K20( the carrier of G, the carrier of G), the carrier of G) is non empty set
K19(K20(K20( the carrier of G, the carrier of G), the carrier of G)) is non empty set
K173( the carrier of G,(G,b,a), the U8 of G) is Element of the carrier of G
Product b is Element of the carrier of G
K173( the carrier of G,b, the U8 of G) is Element of the carrier of G
(Product b) |^ a is Element of the carrier of G
a " is Element of the carrier of G
(a ") * (Product b) is Element of the carrier of G
((a ") * (Product b)) * a is Element of the carrier of G
b is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,b,a) is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
Product (G,b,a) is Element of the carrier of G
K173( the carrier of G,(G,b,a), the U8 of G) is Element of the carrier of G
Product b is Element of the carrier of G
K173( the carrier of G,b, the U8 of G) is Element of the carrier of G
(Product b) |^ a is Element of the carrier of G
(a ") * (Product b) is Element of the carrier of G
((a ") * (Product b)) * a is Element of the carrier of G
c is Element of the carrier of G
<*c*> is V1() V4( NAT ) V5( the carrier of G) Function-like non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of G
b ^ <*c*> is V1() V4( NAT ) V5( the carrier of G) Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,(b ^ <*c*>),a) is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
Product (G,(b ^ <*c*>),a) is Element of the carrier of G
K173( the carrier of G,(G,(b ^ <*c*>),a), the U8 of G) is Element of the carrier of G
(G,<*c*>,a) is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,b,a) ^ (G,<*c*>,a) is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
Product ((G,b,a) ^ (G,<*c*>,a)) is Element of the carrier of G
K173( the carrier of G,((G,b,a) ^ (G,<*c*>,a)), the U8 of G) is Element of the carrier of G
Product (G,<*c*>,a) is Element of the carrier of G
K173( the carrier of G,(G,<*c*>,a), the U8 of G) is Element of the carrier of G
((Product b) |^ a) * (Product (G,<*c*>,a)) is Element of the carrier of G
c |^ a is Element of the carrier of G
(a ") * c is Element of the carrier of G
((a ") * c) * a is Element of the carrier of G
<*(c |^ a)*> is V1() V4( NAT ) V5( the carrier of G) Function-like non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of G
Product <*(c |^ a)*> is Element of the carrier of G
K173( the carrier of G,<*(c |^ a)*>, the U8 of G) is Element of the carrier of G
((Product b) |^ a) * (Product <*(c |^ a)*>) is Element of the carrier of G
((Product b) |^ a) * (c |^ a) is Element of the carrier of G
(Product b) * c is Element of the carrier of G
((Product b) * c) |^ a is Element of the carrier of G
(a ") * ((Product b) * c) is Element of the carrier of G
((a ") * ((Product b) * c)) * a is Element of the carrier of G
Product (b ^ <*c*>) is Element of the carrier of G
K173( the carrier of G,(b ^ <*c*>), the U8 of G) is Element of the carrier of G
(Product (b ^ <*c*>)) |^ a is Element of the carrier of G
(a ") * (Product (b ^ <*c*>)) is Element of the carrier of G
((a ") * (Product (b ^ <*c*>))) * a is Element of the carrier of G
<*> the carrier of G is V1() V4( NAT ) V5( the carrier of G) Function-like functional empty proper V18() V19() V20() V22() V23() V24() V25() V26() finite cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V50() integer FinSequence of the carrier of G
K20(NAT, the carrier of G) is non empty non finite set
(G,(<*> the carrier of G),a) is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
Product (G,(<*> the carrier of G),a) is Element of the carrier of G
K173( the carrier of G,(G,(<*> the carrier of G),a), the U8 of G) is Element of the carrier of G
Product (<*> the carrier of G) is Element of the carrier of G
K173( the carrier of G,(<*> the carrier of G), the U8 of G) is Element of the carrier of G
(Product (<*> the carrier of G)) |^ a is Element of the carrier of G
(a ") * (Product (<*> the carrier of G)) is Element of the carrier of G
((a ") * (Product (<*> the carrier of G))) * a is Element of the carrier of G
1_ G is non being_of_order_0 Element of the carrier of G
(1_ G) |^ a is Element of the carrier of G
(a ") * (1_ G) is Element of the carrier of G
((a ") * (1_ G)) * a is Element of the carrier of G
G is non empty unital Group-like associative L11()
the carrier of G is non empty set
a is Element of the carrier of G
b is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,b,a) is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
b is V1() V4( NAT ) V5( INT ) Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
(G,b,a) |^ b is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
b |^ b is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
(G,(b |^ b),a) is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len (b |^ b) is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
len b is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
dom (b |^ b) is Element of K19(NAT)
dom b is Element of K19(NAT)
len (G,b,a) is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
dom (G,b,a) is Element of K19(NAT)
len ((G,b,a) |^ b) is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
dom ((G,b,a) |^ b) is Element of K19(NAT)
Seg (len b) is finite len b -element Element of K19(NAT)
c is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer set
(G,b,a) /. c is Element of the carrier of G
(G,b,a) . c is set
(b |^ b) /. c is Element of the carrier of G
(b |^ b) . c is set
((G,b,a) |^ b) . c is set
b /. c is V25() V26() V50() integer Element of INT
@ (b /. c) is V25() V26() V50() integer Element of INT
((G,b,a) /. c) |^ (@ (b /. c)) is Element of the carrier of G
b /. c is Element of the carrier of G
(b /. c) |^ a is Element of the carrier of G
a " is Element of the carrier of G
(a ") * (b /. c) is Element of the carrier of G
((a ") * (b /. c)) * a is Element of the carrier of G
((b /. c) |^ a) |^ (@ (b /. c)) is Element of the carrier of G
(b /. c) |^ (@ (b /. c)) is Element of the carrier of G
((b /. c) |^ (@ (b /. c))) |^ a is Element of the carrier of G
(a ") * ((b /. c) |^ (@ (b /. c))) is Element of the carrier of G
((a ") * ((b /. c) |^ (@ (b /. c)))) * a is Element of the carrier of G
((b |^ b) /. c) |^ a is Element of the carrier of G
(a ") * ((b |^ b) /. c) is Element of the carrier of G
((a ") * ((b |^ b) /. c)) * a is Element of the carrier of G
(G,(b |^ b),a) . c is set
len (G,(b |^ b),a) is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
G is non empty unital Group-like associative L11()
the carrier of G is non empty set
a is Element of the carrier of G
a " is Element of the carrier of G
b is Element of the carrier of G
b " is Element of the carrier of G
(a ") * (b ") is Element of the carrier of G
((a ") * (b ")) * a is Element of the carrier of G
(((a ") * (b ")) * a) * b is Element of the carrier of G
G is non empty unital Group-like associative L11()
the carrier of G is non empty set
a is Element of the carrier of G
a " is Element of the carrier of G
b is Element of the carrier of G
(G,a,b) is Element of the carrier of G
b " is Element of the carrier of G
(a ") * (b ") is Element of the carrier of G
((a ") * (b ")) * a is Element of the carrier of G
(((a ") * (b ")) * a) * b is Element of the carrier of G
(b ") * a is Element of the carrier of G
(a ") * ((b ") * a) is Element of the carrier of G
((a ") * ((b ") * a)) * b is Element of the carrier of G
((b ") * a) * b is Element of the carrier of G
(a ") * (((b ") * a) * b) is Element of the carrier of G
a * b is Element of the carrier of G
(b ") * (a * b) is Element of the carrier of G
(a ") * ((b ") * (a * b)) is Element of the carrier of G
((a ") * (b ")) * (a * b) is Element of the carrier of G
G is non empty unital Group-like associative L11()
the carrier of G is non empty set
a is Element of the carrier of G
b is Element of the carrier of G
(G,a,b) is Element of the carrier of G
a " is Element of the carrier of G
b " is Element of the carrier of G
(a ") * (b ") is Element of the carrier of G
((a ") * (b ")) * a is Element of the carrier of G
(((a ") * (b ")) * a) * b is Element of the carrier of G
b * a is Element of the carrier of G
(b * a) " is Element of the carrier of G
a * b is Element of the carrier of G
((b * a) ") * (a * b) is Element of the carrier of G
((a ") * (b ")) * (a * b) is Element of the carrier of G
G is non empty unital Group-like associative L11()
the carrier of G is non empty set
b is non empty unital Group-like associative L11()
the carrier of b is non empty set
a is Element of the carrier of G
b is Element of the carrier of G
(G,a,b) is Element of the carrier of G
a " is Element of the carrier of G
b " is Element of the carrier of G
(a ") * (b ") is Element of the carrier of G
((a ") * (b ")) * a is Element of the carrier of G
(((a ") * (b ")) * a) * b is Element of the carrier of G
(b ") |^ a is Element of the carrier of G
((b ") |^ a) * b is Element of the carrier of G
c is Element of the carrier of b
d is Element of the carrier of b
(b,c,d) is Element of the carrier of b
c " is Element of the carrier of b
d " is Element of the carrier of b
(c ") * (d ") is Element of the carrier of b
((c ") * (d ")) * c is Element of the carrier of b
(((c ") * (d ")) * c) * d is Element of the carrier of b
c |^ d is Element of the carrier of b
(d ") * c is Element of the carrier of b
((d ") * c) * d is Element of the carrier of b
(c ") * (c |^ d) is Element of the carrier of b
G is non empty unital Group-like associative L11()
the carrier of G 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
(G,(1_ G),a) is Element of the carrier of G
(1_ G) " is Element of the carrier of G
a " is Element of the carrier of G
((1_ G) ") * (a ") is Element of the carrier of G
(((1_ G) ") * (a ")) * (1_ G) is Element of the carrier of G
((((1_ G) ") * (a ")) * (1_ G)) * a is Element of the carrier of G
(G,a,(1_ G)) is Element of the carrier of G
(a ") * ((1_ G) ") is Element of the carrier of G
((a ") * ((1_ G) ")) * a is Element of the carrier of G
(((a ") * ((1_ G) ")) * a) * (1_ G) is Element of the carrier of G
(((1_ G) ") * (a ")) * a is Element of the carrier of G
(1_ G) * (a ") is Element of the carrier of G
((1_ G) * (a ")) * a is Element of the carrier of G
(a ") * a is Element of the carrier of G
(a ") * (1_ G) is Element of the carrier of G
((a ") * (1_ G)) * a is Element of the carrier of G
G is non empty unital Group-like associative L11()
the carrier of G 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
(G,a,a) is Element of the carrier of G
a " is Element of the carrier of G
(a ") * (a ") is Element of the carrier of G
((a ") * (a ")) * a is Element of the carrier of G
(((a ") * (a ")) * a) * a is Element of the carrier of G
a * a is Element of the carrier of G
(a * a) " is Element of the carrier of G
((a * a) ") * (a * a) is Element of the carrier of G
G is non empty unital Group-like associative L11()
the carrier of G 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
a " is Element of the carrier of G
(G,a,(a ")) is Element of the carrier of G
(a ") " is Element of the carrier of G
(a ") * ((a ") ") is Element of the carrier of G
((a ") * ((a ") ")) * a is Element of the carrier of G
(((a ") * ((a ") ")) * a) * (a ") is Element of the carrier of G
(G,(a "),a) is Element of the carrier of G
((a ") ") * (a ") is Element of the carrier of G
(((a ") ") * (a ")) * (a ") is Element of the carrier of G
((((a ") ") * (a ")) * (a ")) * a is Element of the carrier of G
a * (a ") is Element of the carrier of G
((a ") * ((a ") ")) * (a * (a ")) is Element of the carrier of G
(1_ G) * (a * (a ")) is Element of the carrier of G
(a ") * a is Element of the carrier of G
(((a ") ") * (a ")) * ((a ") * a) is Element of the carrier of G
(((a ") ") * (a ")) * (1_ G) is Element of the carrier of G
G is non empty unital Group-like associative L11()
the carrier of G is non empty set
a is Element of the carrier of G
b is Element of the carrier of G
(G,a,b) is Element of the carrier of G
a " is Element of the carrier of G
b " is Element of the carrier of G
(a ") * (b ") is Element of the carrier of G
((a ") * (b ")) * a is Element of the carrier of G
(((a ") * (b ")) * a) * b is Element of the carrier of G
(G,a,b) " is Element of the carrier of G
(G,b,a) is Element of the carrier of G
(b ") * (a ") is Element of the carrier of G
((b ") * (a ")) * b is Element of the carrier of G
(((b ") * (a ")) * b) * a is Element of the carrier of G
a * b is Element of the carrier of G
((a ") * (b ")) * (a * b) is Element of the carrier of G
(((a ") * (b ")) * (a * b)) " is Element of the carrier of G
(a * b) " is Element of the carrier of G
((a ") * (b ")) " is Element of the carrier of G
((a * b) ") * (((a ") * (b ")) ") is Element of the carrier of G
((b ") * (a ")) * (((a ") * (b ")) ") is Element of the carrier of G
(b ") " is Element of the carrier of G
(a ") " is Element of the carrier of G
((b ") ") * ((a ") ") is Element of the carrier of G
((b ") * (a ")) * (((b ") ") * ((a ") ")) is Element of the carrier of G
((b ") ") * a is Element of the carrier of G
((b ") * (a ")) * (((b ") ") * a) is Element of the carrier of G
b * a is Element of the carrier of G
((b ") * (a ")) * (b * a) is Element of the carrier of G
G is non empty unital Group-like associative L11()
the carrier of G is non empty set
a is Element of the carrier of G
b is Element of the carrier of G
(G,a,b) is Element of the carrier of G
a " is Element of the carrier of G
b " is Element of the carrier of G
(a ") * (b ") is Element of the carrier of G
((a ") * (b ")) * a is Element of the carrier of G
(((a ") * (b ")) * a) * b is Element of the carrier of G
b is Element of the carrier of G
(G,a,b) |^ b is Element of the carrier of G
b " is Element of the carrier of G
(b ") * (G,a,b) is Element of the carrier of G
((b ") * (G,a,b)) * b is Element of the carrier of G
a |^ b is Element of the carrier of G
(b ") * a is Element of the carrier of G
((b ") * a) * b is Element of the carrier of G
b |^ b is Element of the carrier of G
(b ") * b is Element of the carrier of G
((b ") * b) * b is Element of the carrier of G
(G,(a |^ b),(b |^ b)) is Element of the carrier of G
(a |^ b) " is Element of the carrier of G
(b |^ b) " is Element of the carrier of G
((a |^ b) ") * ((b |^ b) ") is Element of the carrier of G
(((a |^ b) ") * ((b |^ b) ")) * (a |^ b) is Element of the carrier of G
((((a |^ b) ") * ((b |^ b) ")) * (a |^ b)) * (b |^ b) is Element of the carrier of G
1_ G is non being_of_order_0 Element of the carrier of G
(a ") * (1_ G) is Element of the carrier of G
((a ") * (1_ G)) * (b ") is Element of the carrier of G
(((a ") * (1_ G)) * (b ")) * a is Element of the carrier of G
((((a ") * (1_ G)) * (b ")) * a) * b is Element of the carrier of G
(b ") * (((((a ") * (1_ G)) * (b ")) * a) * b) is Element of the carrier of G
((b ") * (((((a ") * (1_ G)) * (b ")) * a) * b)) * b is Element of the carrier of G
b * (b ") is Element of the carrier of G
(a ") * (b * (b ")) is Element of the carrier of G
((a ") * (b * (b "))) * (b ") is Element of the carrier of G
(((a ") * (b * (b "))) * (b ")) * a is Element of the carrier of G
((((a ") * (b * (b "))) * (b ")) * a) * b is Element of the carrier of G
(b ") * (((((a ") * (b * (b "))) * (b ")) * a) * b) is Element of the carrier of G
((b ") * (((((a ") * (b * (b "))) * (b ")) * a) * b)) * b is Element of the carrier of G
a * b is Element of the carrier of G
(((a ") * (b * (b "))) * (b ")) * (a * b) is Element of the carrier of G
(b ") * ((((a ") * (b * (b "))) * (b ")) * (a * b)) is Element of the carrier of G
((b ") * ((((a ") * (b * (b "))) * (b ")) * (a * b))) * b is Element of the carrier of G
(b ") * (a * b) is Element of the carrier of G
((a ") * (b * (b "))) * ((b ") * (a * b)) is Element of the carrier of G
(b ") * (((a ") * (b * (b "))) * ((b ") * (a * b))) is Element of the carrier of G
((b ") * (((a ") * (b * (b "))) * ((b ") * (a * b)))) * b is Element of the carrier of G
(b * (b ")) * ((b ") * (a * b)) is Element of the carrier of G
(a ") * ((b * (b ")) * ((b ") * (a * b))) is Element of the carrier of G
(b ") * ((a ") * ((b * (b ")) * ((b ") * (a * b)))) is Element of the carrier of G
((b ") * ((a ") * ((b * (b ")) * ((b ") * (a * b))))) * b is Element of the carrier of G
(b ") * (a ") is Element of the carrier of G
((b ") * (a ")) * ((b * (b ")) * ((b ") * (a * b))) is Element of the carrier of G
(((b ") * (a ")) * ((b * (b ")) * ((b ") * (a * b)))) * b is Element of the carrier of G
(b ") * ((b ") * (a * b)) is Element of the carrier of G
b * ((b ") * ((b ") * (a * b))) is Element of the carrier of G
((b ") * (a ")) * (b * ((b ") * ((b ") * (a * b)))) is Element of the carrier of G
(((b ") * (a ")) * (b * ((b ") * ((b ") * (a * b))))) * b is Element of the carrier of G
(a ") |^ b is Element of the carrier of G
((b ") * (a ")) * b is Element of the carrier of G
((a ") |^ b) * ((b ") * ((b ") * (a * b))) is Element of the carrier of G
(((a ") |^ b) * ((b ") * ((b ") * (a * b)))) * b is Element of the carrier of G
((a |^ b) ") * ((b ") * ((b ") * (a * b))) is Element of the carrier of G
(((a |^ b) ") * ((b ") * ((b ") * (a * b)))) * b is Element of the carrier of G
(b ") * (1_ G) is Element of the carrier of G
((b ") * (1_ G)) * (a * b) is Element of the carrier of G
(b ") * (((b ") * (1_ G)) * (a * b)) is Element of the carrier of G
((a |^ b) ") * ((b ") * (((b ") * (1_ G)) * (a * b))) is Element of the carrier of G
(((a |^ b) ") * ((b ") * (((b ") * (1_ G)) * (a * b)))) * b is Element of the carrier of G
(b ") * (b * (b ")) is Element of the carrier of G
((b ") * (b * (b "))) * (a * b) is Element of the carrier of G
(b ") * (((b ") * (b * (b "))) * (a * b)) is Element of the carrier of G
((a |^ b) ") * ((b ") * (((b ") * (b * (b "))) * (a * b))) is Element of the carrier of G
(((a |^ b) ") * ((b ") * (((b ") * (b * (b "))) * (a * b)))) * b is Element of the carrier of G
(b * (b ")) * (a * b) is Element of the carrier of G
(b ") * ((b * (b ")) * (a * b)) is Element of the carrier of G
(b ") * ((b ") * ((b * (b ")) * (a * b))) is Element of the carrier of G
((a |^ b) ") * ((b ") * ((b ") * ((b * (b ")) * (a * b)))) is Element of the carrier of G
(((a |^ b) ") * ((b ") * ((b ") * ((b * (b ")) * (a * b))))) * b is Element of the carrier of G
(b ") * (b ") is Element of the carrier of G
((b ") * (b ")) * ((b * (b ")) * (a * b)) is Element of the carrier of G
((a |^ b) ") * (((b ") * (b ")) * ((b * (b ")) * (a * b))) is Element of the carrier of G
(((a |^ b) ") * (((b ") * (b ")) * ((b * (b ")) * (a * b)))) * b is Element of the carrier of G
(b ") * (a * b) is Element of the carrier of G
b * ((b ") * (a * b)) is Element of the carrier of G
((b ") * (b ")) * (b * ((b ") * (a * b))) is Element of the carrier of G
((a |^ b) ") * (((b ") * (b ")) * (b * ((b ") * (a * b)))) is Element of the carrier of G
(((a |^ b) ") * (((b ") * (b ")) * (b * ((b ") * (a * b))))) * b is Element of the carrier of G
(b ") |^ b is Element of the carrier of G
((b ") * (b ")) * b is Element of the carrier of G
((b ") |^ b) * ((b ") * (a * b)) is Element of the carrier of G
((a |^ b) ") * (((b ") |^ b) * ((b ") * (a * b))) is Element of the carrier of G
(((a |^ b) ") * (((b ") |^ b) * ((b ") * (a * b)))) * b is Element of the carrier of G
((b |^ b) ") * ((b ") * (a * b)) is Element of the carrier of G
((a |^ b) ") * (((b |^ b) ") * ((b ") * (a * b))) is Element of the carrier of G
(((a |^ b) ") * (((b |^ b) ") * ((b ") * (a * b)))) * b is Element of the carrier of G
a * (1_ G) is Element of the carrier of G
(a * (1_ G)) * b is Element of the carrier of G
(b ") * ((a * (1_ G)) * b) is Element of the carrier of G
((b |^ b) ") * ((b ") * ((a * (1_ G)) * b)) is Element of the carrier of G
((a |^ b) ") * (((b |^ b) ") * ((b ") * ((a * (1_ G)) * b))) is Element of the carrier of G
(((a |^ b) ") * (((b |^ b) ") * ((b ") * ((a * (1_ G)) * b)))) * b is Element of the carrier of G
a * (b * (b ")) is Element of the carrier of G
(a * (b * (b "))) * b is Element of the carrier of G
(b ") * ((a * (b * (b "))) * b) is Element of the carrier of G
((b |^ b) ") * ((b ") * ((a * (b * (b "))) * b)) is Element of the carrier of G
((a |^ b) ") * (((b |^ b) ") * ((b ") * ((a * (b * (b "))) * b))) is Element of the carrier of G
(((a |^ b) ") * (((b |^ b) ") * ((b ") * ((a * (b * (b "))) * b)))) * b is Element of the carrier of G
(b * (b ")) * b is Element of the carrier of G
a * ((b * (b ")) * b) is Element of the carrier of G
(b ") * (a * ((b * (b ")) * b)) is Element of the carrier of G
((b |^ b) ") * ((b ") * (a * ((b * (b ")) * b))) is Element of the carrier of G
((a |^ b) ") * (((b |^ b) ") * ((b ") * (a * ((b * (b ")) * b)))) is Element of the carrier of G
(((a |^ b) ") * (((b |^ b) ") * ((b ") * (a * ((b * (b ")) * b))))) * b is Element of the carrier of G
((b ") * a) * ((b * (b ")) * b) is Element of the carrier of G
((b |^ b) ") * (((b ") * a) * ((b * (b ")) * b)) is Element of the carrier of G
((a |^ b) ") * (((b |^ b) ") * (((b ") * a) * ((b * (b ")) * b))) is Element of the carrier of G
(((a |^ b) ") * (((b |^ b) ") * (((b ") * a) * ((b * (b ")) * b)))) * b is Element of the carrier of G
b * ((b ") * b) is Element of the carrier of G
((b ") * a) * (b * ((b ") * b)) is Element of the carrier of G
((b |^ b) ") * (((b ") * a) * (b * ((b ") * b))) is Element of the carrier of G
((a |^ b) ") * (((b |^ b) ") * (((b ") * a) * (b * ((b ") * b)))) is Element of the carrier of G
(((a |^ b) ") * (((b |^ b) ") * (((b ") * a) * (b * ((b ") * b))))) * b is Element of the carrier of G
(a |^ b) * ((b ") * b) is Element of the carrier of G
((b |^ b) ") * ((a |^ b) * ((b ") * b)) is Element of the carrier of G
((a |^ b) ") * (((b |^ b) ") * ((a |^ b) * ((b ") * b))) is Element of the carrier of G
(((a |^ b) ") * (((b |^ b) ") * ((a |^ b) * ((b ") * b)))) * b is Element of the carrier of G
(((b |^ b) ") * ((a |^ b) * ((b ") * b))) * b is Element of the carrier of G
((a |^ b) ") * ((((b |^ b) ") * ((a |^ b) * ((b ") * b))) * b) is Element of the carrier of G
((a |^ b) * ((b ") * b)) * b is Element of the carrier of G
((b |^ b) ") * (((a |^ b) * ((b ") * b)) * b) is Element of the carrier of G
((a |^ b) ") * (((b |^ b) ") * (((a |^ b) * ((b ") * b)) * b)) is Element of the carrier of G
(a |^ b) * (b |^ b) is Element of the carrier of G
((b |^ b) ") * ((a |^ b) * (b |^ b)) is Element of the carrier of G
((a |^ b) ") * (((b |^ b) ") * ((a |^ b) * (b |^ b))) is Element of the carrier of G
G is non empty unital Group-like associative L11()
the carrier of G is non empty set
a is Element of the carrier of G
a " is Element of the carrier of G
(a ") |^ 2 is Element of the carrier of G
b is Element of the carrier of G
(G,a,b) is Element of the carrier of G
b " is Element of the carrier of G
(a ") * (b ") is Element of the carrier of G
((a ") * (b ")) * a is Element of the carrier of G
(((a ") * (b ")) * a) * b is Element of the carrier of G
a * (b ") is Element of the carrier of G
(a * (b ")) |^ 2 is Element of the carrier of G
((a ") |^ 2) * ((a * (b ")) |^ 2) is Element of the carrier of G
b |^ 2 is Element of the carrier of G
(((a ") |^ 2) * ((a * (b ")) |^ 2)) * (b |^ 2) is Element of the carrier of G
a * b is Element of the carrier of G
((a ") * (b ")) * (a * b) is Element of the carrier of G
1_ G is non being_of_order_0 Element of the carrier of G
(a ") * (1_ G) is Element of the carrier of G
((a ") * (1_ G)) * (b ") is Element of the carrier of G
(((a ") * (1_ G)) * (b ")) * (a * b) is Element of the carrier of G
a * (1_ G) is Element of the carrier of G
(a * (1_ G)) * b is Element of the carrier of G
(((a ") * (1_ G)) * (b ")) * ((a * (1_ G)) * b) is Element of the carrier of G
(a ") * a is Element of the carrier of G
(a ") * ((a ") * a) is Element of the carrier of G
((a ") * ((a ") * a)) * (b ") is Element of the carrier of G
(((a ") * ((a ") * a)) * (b ")) * ((a * (1_ G)) * b) is Element of the carrier of G
(b ") * b is Element of the carrier of G
a * ((b ") * b) is Element of the carrier of G
(a * ((b ") * b)) * b is Element of the carrier of G
(((a ") * ((a ") * a)) * (b ")) * ((a * ((b ") * b)) * b) is Element of the carrier of G
(a ") * (a ") is Element of the carrier of G
((a ") * (a ")) * a is Element of the carrier of G
(((a ") * (a ")) * a) * (b ") is Element of the carrier of G
((((a ") * (a ")) * a) * (b ")) * ((a * ((b ") * b)) * b) is Element of the carrier of G
((a ") |^ 2) * a is Element of the carrier of G
(((a ") |^ 2) * a) * (b ") is Element of the carrier of G
((((a ") |^ 2) * a) * (b ")) * ((a * ((b ") * b)) * b) is Element of the carrier of G
((b ") * b) * b is Element of the carrier of G
a * (((b ") * b) * b) is Element of the carrier of G
((((a ") |^ 2) * a) * (b ")) * (a * (((b ") * b) * b)) is Element of the carrier of G
b * b is Element of the carrier of G
(b ") * (b * b) is Element of the carrier of G
a * ((b ") * (b * b)) is Element of the carrier of G
((((a ") |^ 2) * a) * (b ")) * (a * ((b ") * (b * b))) is Element of the carrier of G
(b ") * (b |^ 2) is Element of the carrier of G
a * ((b ") * (b |^ 2)) is Element of the carrier of G
((((a ") |^ 2) * a) * (b ")) * (a * ((b ") * (b |^ 2))) is Element of the carrier of G
((a ") |^ 2) * (a * (b ")) is Element of the carrier of G
(((a ") |^ 2) * (a * (b "))) * (a * ((b ") * (b |^ 2))) is Element of the carrier of G
(a * (b ")) * (a * ((b ") * (b |^ 2))) is Element of the carrier of G
((a ") |^ 2) * ((a * (b ")) * (a * ((b ") * (b |^ 2)))) is Element of the carrier of G
(a * (b ")) * (b |^ 2) is Element of the carrier of G
(a * (b ")) * ((a * (b ")) * (b |^ 2)) is Element of the carrier of G
((a ") |^ 2) * ((a * (b ")) * ((a * (b ")) * (b |^ 2))) is Element of the carrier of G
(a * (b ")) * (a * (b ")) is Element of the carrier of G
((a * (b ")) * (a * (b "))) * (b |^ 2) is Element of the carrier of G
((a ") |^ 2) * (((a * (b ")) * (a * (b "))) * (b |^ 2)) is Element of the carrier of G
((a ") |^ 2) * ((a * (b ")) * (a * (b "))) is Element of the carrier of G
(((a ") |^ 2) * ((a * (b ")) * (a * (b ")))) * (b |^ 2) is Element of the carrier of G
G is non empty unital Group-like associative L11()
the carrier of G is non empty set
a is Element of the carrier of G
b is Element of the carrier of G
a * b is Element of the carrier of G
b is Element of the carrier of G
(G,(a * b),b) is Element of the carrier of G
(a * b) " is Element of the carrier of G
b " is Element of the carrier of G
((a * b) ") * (b ") is Element of the carrier of G
(((a * b) ") * (b ")) * (a * b) is Element of the carrier of G
((((a * b) ") * (b ")) * (a * b)) * b is Element of the carrier of G
(G,a,b) is Element of the carrier of G
a " is Element of the carrier of G
(a ") * (b ") is Element of the carrier of G
((a ") * (b ")) * a is Element of the carrier of G
(((a ") * (b ")) * a) * b is Element of the carrier of G
(G,a,b) |^ b is Element of the carrier of G
b " is Element of the carrier of G
(b ") * (G,a,b) is Element of the carrier of G
((b ") * (G,a,b)) * b is Element of the carrier of G
(G,b,b) is Element of the carrier of G
(b ") * (b ") is Element of the carrier of G
((b ") * (b ")) * b is Element of the carrier of G
(((b ") * (b ")) * b) * b is Element of the carrier of G
((G,a,b) |^ b) * (G,b,b) is Element of the carrier of G
(a * b) * b is Element of the carrier of G
(((a * b) ") * (b ")) * ((a * b) * b) is Element of the carrier of G
(b ") * (a ") is Element of the carrier of G
((b ") * (a ")) * (b ") is Element of the carrier of G
(((b ") * (a ")) * (b ")) * ((a * b) * b) is Element of the carrier of G
1_ G is non being_of_order_0 Element of the carrier of G
a * (1_ G) is Element of the carrier of G
(a * (1_ G)) * b is Element of the carrier of G
((a * (1_ G)) * b) * b is Element of the carrier of G
(((b ") * (a ")) * (b ")) * (((a * (1_ G)) * b) * b) is Element of the carrier of G
b * (b ") is Element of the carrier of G
a * (b * (b ")) is Element of the carrier of G
(a * (b * (b "))) * b is Element of the carrier of G
((a * (b * (b "))) * b) * b is Element of the carrier of G
(((b ") * (a ")) * (b ")) * (((a * (b * (b "))) * b) * b) is Element of the carrier of G
b * (1_ G) is Element of the carrier of G
(b * (1_ G)) * (b ") is Element of the carrier of G
a * ((b * (1_ G)) * (b ")) is Element of the carrier of G
(a * ((b * (1_ G)) * (b "))) * b is Element of the carrier of G
((a * ((b * (1_ G)) * (b "))) * b) * b is Element of the carrier of G
(((b ") * (a ")) * (b ")) * (((a * ((b * (1_ G)) * (b "))) * b) * b) is Element of the carrier of G
b * (b ") is Element of the carrier of G
b * (b * (b ")) is Element of the carrier of G
(b * (b * (b "))) * (b ") is Element of the carrier of G
a * ((b * (b * (b "))) * (b ")) is Element of the carrier of G
(a * ((b * (b * (b "))) * (b "))) * b is Element of the carrier of G
((a * ((b * (b * (b "))) * (b "))) * b) * b is Element of the carrier of G
(((b ") * (a ")) * (b ")) * (((a * ((b * (b * (b "))) * (b "))) * b) * b) is Element of the carrier of G
(b ") * ((a ") * (b ")) is Element of the carrier of G
((b ") * ((a ") * (b "))) * (((a * ((b * (b * (b "))) * (b "))) * b) * b) is Element of the carrier of G
b * b is Element of the carrier of G
(a * ((b * (b * (b "))) * (b "))) * (b * b) is Element of the carrier of G
((b ") * ((a ") * (b "))) * ((a * ((b * (b * (b "))) * (b "))) * (b * b)) is Element of the carrier of G
b * b is Element of the carrier of G
(b * b) * (b ") is Element of the carrier of G
((b * b) * (b ")) * (b ") is Element of the carrier of G
a * (((b * b) * (b ")) * (b ")) is Element of the carrier of G
(a * (((b * b) * (b ")) * (b "))) * (b * b) is Element of the carrier of G
((b ") * ((a ") * (b "))) * ((a * (((b * b) * (b ")) * (b "))) * (b * b)) is Element of the carrier of G
(b * b) * ((b ") * (b ")) is Element of the carrier of G
a * ((b * b) * ((b ") * (b "))) is Element of the carrier of G
(a * ((b * b) * ((b ") * (b ")))) * (b * b) is Element of the carrier of G
((b ") * ((a ") * (b "))) * ((a * ((b * b) * ((b ") * (b ")))) * (b * b)) is Element of the carrier of G
b * ((b ") * (b ")) is Element of the carrier of G
b * (b * ((b ") * (b "))) is Element of the carrier of G
a * (b * (b * ((b ") * (b ")))) is Element of the carrier of G
(a * (b * (b * ((b ") * (b "))))) * (b * b) is Element of the carrier of G
((b ") * ((a ") * (b "))) * ((a * (b * (b * ((b ") * (b "))))) * (b * b)) is Element of the carrier of G
a * b is Element of the carrier of G
(a * b) * (b * ((b ") * (b "))) is Element of the carrier of G
((a * b) * (b * ((b ") * (b ")))) * (b * b) is Element of the carrier of G
((b ") * ((a ") * (b "))) * (((a * b) * (b * ((b ") * (b ")))) * (b * b)) is Element of the carrier of G
(b * ((b ") * (b "))) * (b * b) is Element of the carrier of G
(a * b) * ((b * ((b ") * (b "))) * (b * b)) is Element of the carrier of G
((b ") * ((a ") * (b "))) * ((a * b) * ((b * ((b ") * (b "))) * (b * b))) is Element of the carrier of G
((b ") * ((a ") * (b "))) * (a * b) is Element of the carrier of G
(((b ") * ((a ") * (b "))) * (a * b)) * ((b * ((b ") * (b "))) * (b * b)) is Element of the carrier of G
((a ") * (b ")) * (a * b) is Element of the carrier of G
(b ") * (((a ") * (b ")) * (a * b)) is Element of the carrier of G
((b ") * (((a ") * (b ")) * (a * b))) * ((b * ((b ") * (b "))) * (b * b)) is Element of the carrier of G
((b ") * (b ")) * (b * b) is Element of the carrier of G
b * (((b ") * (b ")) * (b * b)) is Element of the carrier of G
((b ") * (((a ") * (b ")) * (a * b))) * (b * (((b ") * (b ")) * (b * b))) is Element of the carrier of G
((b ") * (((a ") * (b ")) * (a * b))) * b is Element of the carrier of G
(((b ") * (((a ") * (b ")) * (a * b))) * b) * (((b ") * (b ")) * (b * b)) is Element of the carrier of G
((G,a,b) |^ b) * (((b ") * (b ")) * (b * b)) is Element of the carrier of G
G is non empty unital Group-like associative L11()
the carrier of G is non empty set
a is Element of the carrier of G
b is Element of the carrier of G
(G,a,b) is Element of the carrier of G
a " is Element of the carrier of G
b " is Element of the carrier of G
(a ") * (b ") is Element of the carrier of G
((a ") * (b ")) * a is Element of the carrier of G
(((a ") * (b ")) * a) * b is Element of the carrier of G
b is Element of the carrier of G
b * b is Element of the carrier of G
(G,a,(b * b)) is Element of the carrier of G
(b * b) " is Element of the carrier of G
(a ") * ((b * b) ") is Element of the carrier of G
((a ") * ((b * b) ")) * a is Element of the carrier of G
(((a ") * ((b * b) ")) * a) * (b * b) is Element of the carrier of G
(G,a,b) is Element of the carrier of G
b " is Element of the carrier of G
(a ") * (b ") is Element of the carrier of G
((a ") * (b ")) * a is Element of the carrier of G
(((a ") * (b ")) * a) * b is Element of the carrier of G
(G,a,b) |^ b is Element of the carrier of G
(b ") * (G,a,b) is Element of the carrier of G
((b ") * (G,a,b)) * b is Element of the carrier of G
(G,a,b) * ((G,a,b) |^ b) is Element of the carrier of G
a * (b * b) is Element of the carrier of G
((a ") * ((b * b) ")) * (a * (b * b)) is Element of the carrier of G
(b ") * (b ") is Element of the carrier of G
(a ") * ((b ") * (b ")) is Element of the carrier of G
((a ") * ((b ") * (b "))) * (a * (b * b)) is Element of the carrier of G
1_ G is non being_of_order_0 Element of the carrier of G
(b ") * (1_ G) is Element of the carrier of G
((b ") * (1_ G)) * (b ") is Element of the carrier of G
(a ") * (((b ") * (1_ G)) * (b ")) is Element of the carrier of G
((a ") * (((b ") * (1_ G)) * (b "))) * (a * (b * b)) is Element of the carrier of G
a * (a ") is Element of the carrier of G
(b ") * (a * (a ")) is Element of the carrier of G
((b ") * (a * (a "))) * (b ") is Element of the carrier of G
(a ") * (((b ") * (a * (a "))) * (b ")) is Element of the carrier of G
((a ") * (((b ") * (a * (a "))) * (b "))) * (a * (b * b)) is Element of the carrier of G
a * (1_ G) is Element of the carrier of G
(a * (1_ G)) * (a ") is Element of the carrier of G
(b ") * ((a * (1_ G)) * (a ")) is Element of the carrier of G
((b ") * ((a * (1_ G)) * (a "))) * (b ") is Element of the carrier of G
(a ") * (((b ") * ((a * (1_ G)) * (a "))) * (b ")) is Element of the carrier of G
((a ") * (((b ") * ((a * (1_ G)) * (a "))) * (b "))) * (a * (b * b)) is Element of the carrier of G
b * (b ") is Element of the carrier of G
a * (b * (b ")) is Element of the carrier of G
(a * (b * (b "))) * (a ") is Element of the carrier of G
(b ") * ((a * (b * (b "))) * (a ")) is Element of the carrier of G
((b ") * ((a * (b * (b "))) * (a "))) * (b ") is Element of the carrier of G
(a ") * (((b ") * ((a * (b * (b "))) * (a "))) * (b ")) is Element of the carrier of G
((a ") * (((b ") * ((a * (b * (b "))) * (a "))) * (b "))) * (a * (b * b)) is Element of the carrier of G
a * b is Element of the carrier of G
(a * b) * (b ") is Element of the carrier of G
((a * b) * (b ")) * (a ") is Element of the carrier of G
(b ") * (((a * b) * (b ")) * (a ")) is Element of the carrier of G
((b ") * (((a * b) * (b ")) * (a "))) * (b ") is Element of the carrier of G
(a ") * (((b ") * (((a * b) * (b ")) * (a "))) * (b ")) is Element of the carrier of G
((a ") * (((b ") * (((a * b) * (b ")) * (a "))) * (b "))) * (a * (b * b)) is Element of the carrier of G
(b ") * (a ") is Element of the carrier of G
(a * b) * ((b ") * (a ")) is Element of the carrier of G
(b ") * ((a * b) * ((b ") * (a "))) is Element of the carrier of G
((b ") * ((a * b) * ((b ") * (a ")))) * (b ") is Element of the carrier of G
(a ") * (((b ") * ((a * b) * ((b ") * (a ")))) * (b ")) is Element of the carrier of G
((a ") * (((b ") * ((a * b) * ((b ") * (a ")))) * (b "))) * (a * (b * b)) is Element of the carrier of G
((a * b) * ((b ") * (a "))) * (b ") is Element of the carrier of G
(b ") * (((a * b) * ((b ") * (a "))) * (b ")) is Element of the carrier of G
(a ") * ((b ") * (((a * b) * ((b ") * (a "))) * (b "))) is Element of the carrier of G
((a ") * ((b ") * (((a * b) * ((b ") * (a "))) * (b ")))) * (a * (b * b)) is Element of the carrier of G
((a ") * (b ")) * (((a * b) * ((b ") * (a "))) * (b ")) is Element of the carrier of G
(((a ") * (b ")) * (((a * b) * ((b ") * (a "))) * (b "))) * (a * (b * b)) is Element of the carrier of G
((a ") * (b ")) * ((a * b) * ((b ") * (a "))) is Element of the carrier of G
(((a ") * (b ")) * ((a * b) * ((b ") * (a ")))) * (b ") is Element of the carrier of G
((((a ") * (b ")) * ((a * b) * ((b ") * (a ")))) * (b ")) * (a * (b * b)) is Element of the carrier of G
((a ") * (b ")) * (a * b) is Element of the carrier of G
(((a ") * (b ")) * (a * b)) * ((b ") * (a ")) is Element of the carrier of G
((((a ") * (b ")) * (a * b)) * ((b ") * (a "))) * (b ") is Element of the carrier of G
(((((a ") * (b ")) * (a * b)) * ((b ") * (a "))) * (b ")) * (a * (b * b)) is Element of the carrier of G
((b ") * (a ")) * (b ") is Element of the carrier of G
(((a ") * (b ")) * (a * b)) * (((b ") * (a ")) * (b ")) is Element of the carrier of G
((((a ") * (b ")) * (a * b)) * (((b ") * (a ")) * (b "))) * (a * (b * b)) is Element of the carrier of G
(((b ") * (a ")) * (b ")) * (a * (b * b)) is Element of the carrier of G
(((a ") * (b ")) * (a * b)) * ((((b ") * (a ")) * (b ")) * (a * (b * b))) is Element of the carrier of G
a * b is Element of the carrier of G
(a * b) * b is Element of the carrier of G
(((b ") * (a ")) * (b ")) * ((a * b) * b) is Element of the carrier of G
(((a ") * (b ")) * (a * b)) * ((((b ") * (a ")) * (b ")) * ((a * b) * b)) is Element of the carrier of G
(b ") * ((a ") * (b ")) is Element of the carrier of G
((b ") * ((a ") * (b "))) * ((a * b) * b) is Element of the carrier of G
(((a ") * (b ")) * (a * b)) * (((b ") * ((a ") * (b "))) * ((a * b) * b)) is Element of the carrier of G
((a ") * (b ")) * ((a * b) * b) is Element of the carrier of G
(b ") * (((a ") * (b ")) * ((a * b) * b)) is Element of the carrier of G
(((a ") * (b ")) * (a * b)) * ((b ") * (((a ") * (b ")) * ((a * b) * b))) is Element of the carrier of G
((a ") * (b ")) * (a * b) is Element of the carrier of G
(((a ") * (b ")) * (a * b)) * b is Element of the carrier of G
(b ") * ((((a ") * (b ")) * (a * b)) * b) is Element of the carrier of G
(((a ") * (b ")) * (a * b)) * ((b ") * ((((a ") * (b ")) * (a * b)) * b)) is Element of the carrier of G
(b ") * (((a ") * (b ")) * (a * b)) is Element of the carrier of G
((b ") * (((a ") * (b ")) * (a * b))) * b is Element of the carrier of G
(((a ") * (b ")) * (a * b)) * (((b ") * (((a ") * (b ")) * (a * b))) * b) is Element of the carrier of G
(G,a,b) * (((b ") * (((a ") * (b ")) * (a * b))) * b) is Element of the carrier of G
G is non empty unital Group-like associative L11()
the carrier of G is non empty set
a is Element of the carrier of G
a " is Element of the carrier of G
b is Element of the carrier of G
(G,(a "),b) is Element of the carrier of G
(a ") " is Element of the carrier of G
b " is Element of the carrier of G
((a ") ") * (b ") is Element of the carrier of G
(((a ") ") * (b ")) * (a ") is Element of the carrier of G
((((a ") ") * (b ")) * (a ")) * b is Element of the carrier of G
(G,b,a) is Element of the carrier of G
(b ") * (a ") is Element of the carrier of G
((b ") * (a ")) * b is Element of the carrier of G
(((b ") * (a ")) * b) * a is Element of the carrier of G
(G,b,a) |^ (a ") is Element of the carrier of G
((a ") ") * (G,b,a) is Element of the carrier of G
(((a ") ") * (G,b,a)) * (a ") is Element of the carrier of G
(a ") * b is Element of the carrier of G
(b ") * ((a ") * b) is Element of the carrier of G
((a ") ") * ((b ") * ((a ") * b)) is Element of the carrier of G
1_ G is non being_of_order_0 Element of the carrier of G
(((a ") ") * ((b ") * ((a ") * b))) * (1_ G) is Element of the carrier of G
a * (a ") is Element of the carrier of G
(((a ") ") * ((b ") * ((a ") * b))) * (a * (a ")) is Element of the carrier of G
(((a ") ") * ((b ") * ((a ") * b))) * a is Element of the carrier of G
((((a ") ") * ((b ") * ((a ") * b))) * a) * (a ") is Element of the carrier of G
((b ") * ((a ") * b)) * a is Element of the carrier of G
((a ") ") * (((b ") * ((a ") * b)) * a) is Element of the carrier of G
(((a ") ") * (((b ") * ((a ") * b)) * a)) * (a ") is Element of the carrier of G
G is non empty unital Group-like associative L11()
the carrier of G is non empty set
a is Element of the carrier of G
b is Element of the carrier of G
b " is Element of the carrier of G
(G,a,(b ")) is Element of the carrier of G
a " is Element of the carrier of G
(b ") " is Element of the carrier of G
(a ") * ((b ") ") is Element of the carrier of G
((a ") * ((b ") ")) * a is Element of the carrier of G
(((a ") * ((b ") ")) * a) * (b ") is Element of the carrier of G
(G,b,a) is Element of the carrier of G
(b ") * (a ") is Element of the carrier of G
((b ") * (a ")) * b is Element of the carrier of G
(((b ") * (a ")) * b) * a is Element of the carrier of G
(G,b,a) |^ (b ") is Element of the carrier of G
((b ") ") * (G,b,a) is Element of the carrier of G
(((b ") ") * (G,b,a)) * (b ") is Element of the carrier of G
(a ") * b is Element of the carrier of G
((a ") * b) * a is Element of the carrier of G
(((a ") * b) * a) * (b ") is Element of the carrier of G
1_ G is non being_of_order_0 Element of the carrier of G
(1_ G) * ((((a ") * b) * a) * (b ")) is Element of the carrier of G
((b ") ") * (b ") is Element of the carrier of G
(((b ") ") * (b ")) * ((((a ") * b) * a) * (b ")) is Element of the carrier of G
(((b ") ") * (b ")) * (((a ") * b) * a) is Element of the carrier of G
((((b ") ") * (b ")) * (((a ") * b) * a)) * (b ") is Element of the carrier of G
(b ") * (((a ") * b) * a) is Element of the carrier of G
((b ") ") * ((b ") * (((a ") * b) * a)) is Element of the carrier of G
(((b ") ") * ((b ") * (((a ") * b) * a))) * (b ") is Element of the carrier of G
G is non empty unital Group-like associative L11()
the carrier of G is non empty set
a is Element of the carrier of G
a " is Element of the carrier of G
b is Element of the carrier of G
b " is Element of the carrier of G
(G,(a "),(b ")) is Element of the carrier of G
(a ") " is Element of the carrier of G
(b ") " is Element of the carrier of G
((a ") ") * ((b ") ") is Element of the carrier of G
(((a ") ") * ((b ") ")) * (a ") is Element of the carrier of G
((((a ") ") * ((b ") ")) * (a ")) * (b ") is Element of the carrier of G
(G,a,b) is Element of the carrier of G
(a ") * (b ") is Element of the carrier of G
((a ") * (b ")) * a is Element of the carrier of G
(((a ") * (b ")) * a) * b is Element of the carrier of G
a * b is Element of the carrier of G
(a * b) " is Element of the carrier of G
(G,a,b) |^ ((a * b) ") is Element of the carrier of G
((a * b) ") " is Element of the carrier of G
(((a * b) ") ") * (G,a,b) is Element of the carrier of G
((((a * b) ") ") * (G,a,b)) * ((a * b) ") is Element of the carrier of G
b * a is Element of the carrier of G
(b * a) " is Element of the carrier of G
(G,a,b) |^ ((b * a) ") is Element of the carrier of G
((b * a) ") " is Element of the carrier of G
(((b * a) ") ") * (G,a,b) is Element of the carrier of G
((((b * a) ") ") * (G,a,b)) * ((b * a) ") is Element of the carrier of G
(G,(b "),a) is Element of the carrier of G
((b ") ") * (a ") is Element of the carrier of G
(((b ") ") * (a ")) * (b ") is Element of the carrier of G
((((b ") ") * (a ")) * (b ")) * a is Element of the carrier of G
(G,(b "),a) |^ (a ") is Element of the carrier of G
((a ") ") * (G,(b "),a) is Element of the carrier of G
(((a ") ") * (G,(b "),a)) * (a ") is Element of the carrier of G
(G,a,b) |^ (b ") is Element of the carrier of G
((b ") ") * (G,a,b) is Element of the carrier of G
(((b ") ") * (G,a,b)) * (b ") is Element of the carrier of G
((G,a,b) |^ (b ")) |^ (a ") is Element of the carrier of G
((a ") ") * ((G,a,b) |^ (b ")) is Element of the carrier of G
(((a ") ") * ((G,a,b) |^ (b "))) * (a ") is Element of the carrier of G
(b ") * (a ") is Element of the carrier of G
(G,a,b) |^ ((b ") * (a ")) is Element of the carrier of G
((b ") * (a ")) " is Element of the carrier of G
(((b ") * (a ")) ") * (G,a,b) is Element of the carrier of G
((((b ") * (a ")) ") * (G,a,b)) * ((b ") * (a ")) is Element of the carrier of G
(G,b,(a ")) is Element of the carrier of G
(b ") * ((a ") ") is Element of the carrier of G
((b ") * ((a ") ")) * b is Element of the carrier of G
(((b ") * ((a ") ")) * b) * (a ") is Element of the carrier of G
(G,b,(a ")) |^ (b ") is Element of the carrier of G
((b ") ") * (G,b,(a ")) is Element of the carrier of G
(((b ") ") * (G,b,(a "))) * (b ") is Element of the carrier of G
(G,a,b) |^ (a ") is Element of the carrier of G
((a ") ") * (G,a,b) is Element of the carrier of G
(((a ") ") * (G,a,b)) * (a ") is Element of the carrier of G
((G,a,b) |^ (a ")) |^ (b ") is Element of the carrier of G
((b ") ") * ((G,a,b) |^ (a ")) is Element of the carrier of G
(((b ") ") * ((G,a,b) |^ (a "))) * (b ") is Element of the carrier of G
(G,a,b) |^ ((a ") * (b ")) is Element of the carrier of G
((a ") * (b ")) " is Element of the carrier of G
(((a ") * (b ")) ") * (G,a,b) is Element of the carrier of G
((((a ") * (b ")) ") * (G,a,b)) * ((a ") * (b ")) is Element of the carrier of G
G is non empty unital Group-like associative L11()
the carrier of G is non empty set
a is Element of the carrier of G
a " is Element of the carrier of G
b is Element of the carrier of G
b |^ (a ") is Element of the carrier of G
(a ") " is Element of the carrier of G
((a ") ") * b is Element of the carrier of G
(((a ") ") * b) * (a ") is Element of the carrier of G
(G,a,(b |^ (a "))) is Element of the carrier of G
(b |^ (a ")) " is Element of the carrier of G
(a ") * ((b |^ (a ")) ") is Element of the carrier of G
((a ") * ((b |^ (a ")) ")) * a is Element of the carrier of G
(((a ") * ((b |^ (a ")) ")) * a) * (b |^ (a ")) is Element of the carrier of G
(G,b,(a ")) is Element of the carrier of G
b " is Element of the carrier of G
(b ") * ((a ") ") is Element of the carrier of G
((b ") * ((a ") ")) * b is Element of the carrier of G
(((b ") * ((a ") ")) * b) * (a ") is Element of the carrier of G
(b ") |^ (a ") is Element of the carrier of G
((a ") ") * (b ") is Element of the carrier of G
(((a ") ") * (b ")) * (a ") is Element of the carrier of G
(a ") * ((b ") |^ (a ")) is Element of the carrier of G
((a ") * ((b ") |^ (a "))) * a is Element of the carrier of G
(((a ") * ((b ") |^ (a "))) * a) * (b |^ (a ")) is Element of the carrier of G
(b ") * (a ") is Element of the carrier of G
((a ") ") * ((b ") * (a ")) is Element of the carrier of G
(a ") * (((a ") ") * ((b ") * (a "))) is Element of the carrier of G
((a ") * (((a ") ") * ((b ") * (a ")))) * a is Element of the carrier of G
(((a ") * (((a ") ") * ((b ") * (a ")))) * a) * (b |^ (a ")) is Element of the carrier of G
((b ") * (a ")) * a is Element of the carrier of G
(((b ") * (a ")) * a) * (b |^ (a ")) is Element of the carrier of G
(b ") * ((((a ") ") * b) * (a ")) is Element of the carrier of G
G is non empty unital Group-like associative L11()
the carrier of G is non empty set
a is Element of the carrier of G
b is Element of the carrier of G
b " is Element of the carrier of G
a |^ (b ") is Element of the carrier of G
(b ") " is Element of the carrier of G
((b ") ") * a is Element of the carrier of G
(((b ") ") * a) * (b ") is Element of the carrier of G
(G,(a |^ (b ")),b) is Element of the carrier of G
(a |^ (b ")) " is Element of the carrier of G
((a |^ (b ")) ") * (b ") is Element of the carrier of G
(((a |^ (b ")) ") * (b ")) * (a |^ (b ")) is Element of the carrier of G
((((a |^ (b ")) ") * (b ")) * (a |^ (b "))) * b is Element of the carrier of G
(G,(b "),a) is Element of the carrier of G
a " is Element of the carrier of G
((b ") ") * (a ") is Element of the carrier of G
(((b ") ") * (a ")) * (b ") is Element of the carrier of G
((((b ") ") * (a ")) * (b ")) * a is Element of the carrier of G
(a ") |^ (b ") is Element of the carrier of G
((a ") |^ (b ")) * (b ") is Element of the carrier of G
(((a ") |^ (b ")) * (b ")) * (a |^ (b ")) is Element of the carrier of G
((((a ") |^ (b ")) * (b ")) * (a |^ (b "))) * b is Element of the carrier of G
(b ") * ((((b ") ") * a) * (b ")) is Element of the carrier of G
((a ") |^ (b ")) * ((b ") * ((((b ") ") * a) * (b "))) is Element of the carrier of G
(((a ") |^ (b ")) * ((b ") * ((((b ") ") * a) * (b ")))) * b is Element of the carrier of G
a * (b ") is Element of the carrier of G
((b ") ") * (a * (b ")) is Element of the carrier of G
(b ") * (((b ") ") * (a * (b "))) is Element of the carrier of G
((a ") |^ (b ")) * ((b ") * (((b ") ") * (a * (b ")))) is Element of the carrier of G
(((a ") |^ (b ")) * ((b ") * (((b ") ") * (a * (b "))))) * b is Element of the carrier of G
((a ") |^ (b ")) * (a * (b ")) is Element of the carrier of G
(((a ") |^ (b ")) * (a * (b "))) * b is Element of the carrier of G
(a * (b ")) * b is Element of the carrier of G
((a ") |^ (b ")) * ((a * (b ")) * b) is Element of the carrier of G
G is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
- G is V25() V26() V50() integer set
a is non empty unital Group-like associative L11()
the carrier of a is non empty set
b is Element of the carrier of a
b |^ G is Element of the carrier of a
b |^ (- G) is Element of the carrier of a
b is Element of the carrier of a
(a,(b |^ G),b) is Element of the carrier of a
(b |^ G) " is Element of the carrier of a
b " is Element of the carrier of a
((b |^ G) ") * (b ") is Element of the carrier of a
(((b |^ G) ") * (b ")) * (b |^ G) is Element of the carrier of a
((((b |^ G) ") * (b ")) * (b |^ G)) * b is Element of the carrier of a
b |^ b is Element of the carrier of a
(b ") * b is Element of the carrier of a
((b ") * b) * b is Element of the carrier of a
(b |^ b) |^ G is Element of the carrier of a
(b |^ (- G)) * ((b |^ b) |^ G) is Element of the carrier of a
(b ") * (b |^ G) is Element of the carrier of a
((b ") * (b |^ G)) * b is Element of the carrier of a
((b |^ G) ") * (((b ") * (b |^ G)) * b) is Element of the carrier of a
(b |^ G) |^ b is Element of the carrier of a
(b |^ (- G)) * ((b |^ G) |^ b) is Element of the carrier of a
G is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
- G is V25() V26() V50() integer set
a is non empty unital Group-like associative L11()
the carrier of a is non empty set
b is Element of the carrier of a
b is Element of the carrier of a
b |^ G is Element of the carrier of a
(a,b,(b |^ G)) is Element of the carrier of a
b " is Element of the carrier of a
(b |^ G) " is Element of the carrier of a
(b ") * ((b |^ G) ") is Element of the carrier of a
((b ") * ((b |^ G) ")) * b is Element of the carrier of a
(((b ") * ((b |^ G) ")) * b) * (b |^ G) is Element of the carrier of a
b |^ b is Element of the carrier of a
(b ") * b is Element of the carrier of a
((b ") * b) * b is Element of the carrier of a
(b |^ b) |^ (- G) is Element of the carrier of a
((b |^ b) |^ (- G)) * (b |^ G) is Element of the carrier of a
b |^ (- G) is Element of the carrier of a
(b |^ (- G)) |^ b is Element of the carrier of a
(b ") * (b |^ (- G)) is Element of the carrier of a
((b ") * (b |^ (- G))) * b is Element of the carrier of a
((b |^ (- G)) |^ b) * (b |^ G) is Element of the carrier of a
G is V25() V26() V50() integer set
- G is V25() V26() V50() integer set
a is non empty unital Group-like associative L11()
the carrier of a is non empty set
b is Element of the carrier of a
b |^ G is Element of the carrier of a
b |^ (- G) is Element of the carrier of a
b is Element of the carrier of a
(a,(b |^ G),b) is Element of the carrier of a
(b |^ G) " is Element of the carrier of a
b " is Element of the carrier of a
((b |^ G) ") * (b ") is Element of the carrier of a
(((b |^ G) ") * (b ")) * (b |^ G) is Element of the carrier of a
((((b |^ G) ") * (b ")) * (b |^ G)) * b is Element of the carrier of a
b |^ b is Element of the carrier of a
(b ") * b is Element of the carrier of a
((b ") * b) * b is Element of the carrier of a
(b |^ b) |^ G is Element of the carrier of a
(b |^ (- G)) * ((b |^ b) |^ G) is Element of the carrier of a
(b ") * (b |^ G) is Element of the carrier of a
((b ") * (b |^ G)) * b is Element of the carrier of a
((b |^ G) ") * (((b ") * (b |^ G)) * b) is Element of the carrier of a
(b |^ G) |^ b is Element of the carrier of a
(b |^ (- G)) * ((b |^ G) |^ b) is Element of the carrier of a
G is V25() V26() V50() integer set
- G is V25() V26() V50() integer set
a is non empty unital Group-like associative L11()
the carrier of a is non empty set
b is Element of the carrier of a
b is Element of the carrier of a
b |^ G is Element of the carrier of a
(a,b,(b |^ G)) is Element of the carrier of a
b " is Element of the carrier of a
(b |^ G) " is Element of the carrier of a
(b ") * ((b |^ G) ") is Element of the carrier of a
((b ") * ((b |^ G) ")) * b is Element of the carrier of a
(((b ") * ((b |^ G) ")) * b) * (b |^ G) is Element of the carrier of a
b |^ b is Element of the carrier of a
(b ") * b is Element of the carrier of a
((b ") * b) * b is Element of the carrier of a
(b |^ b) |^ (- G) is Element of the carrier of a
((b |^ b) |^ (- G)) * (b |^ G) is Element of the carrier of a
b |^ (- G) is Element of the carrier of a
(b |^ (- G)) |^ b is Element of the carrier of a
(b ") * (b |^ (- G)) is Element of the carrier of a
((b ") * (b |^ (- G))) * b is Element of the carrier of a
((b |^ (- G)) |^ b) * (b |^ G) is Element of the carrier of a
G is non empty unital Group-like associative L11()
the carrier of G 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
b is Element of the carrier of G
(G,a,b) is Element of the carrier of G
a " is Element of the carrier of G
b " is Element of the carrier of G
(a ") * (b ") is Element of the carrier of G
((a ") * (b ")) * a is Element of the carrier of G
(((a ") * (b ")) * a) * b is Element of the carrier of G
a * b is Element of the carrier of G
b * a is Element of the carrier of G
(b * a) " is Element of the carrier of G
((b * a) ") * (a * b) is Element of the carrier of G
((b * a) ") " is Element of the carrier of G
(b * a) " is Element of the carrier of G
(b ") * (a ") is Element of the carrier of G
((b * a) ") * (a * b) is Element of the carrier of G
((b ") * (a ")) * a is Element of the carrier of G
(((b ") * (a ")) * a) * b is Element of the carrier of G
(b ") * b is Element of the carrier of G
G is non empty unital Group-like associative commutative L11()
the carrier of G is non empty set
a is Element of the carrier of G
b is Element of the carrier of G
a * b is Element of the carrier of G
b * a is Element of the carrier of G
G is non empty unital Group-like associative L11()
the carrier of G 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
b is Element of the carrier of G
(G,a,b) is Element of the carrier of G
a " is Element of the carrier of G
b " is Element of the carrier of G
(a ") * (b ") is Element of the carrier of G
((a ") * (b ")) * a is Element of the carrier of G
(((a ") * (b ")) * a) * b is Element of the carrier of G
a * b is Element of the carrier of G
b * a is Element of the carrier of G
a is Element of the carrier of G
b is Element of the carrier of G
a * b is Element of the carrier of G
b * a is Element of the carrier of G
(G,a,b) is Element of the carrier of G
a " is Element of the carrier of G
b " is Element of the carrier of G
(a ") * (b ") is Element of the carrier of G
((a ") * (b ")) * a is Element of the carrier of G
(((a ") * (b ")) * a) * b is Element of the carrier of G
G is non empty unital Group-like associative L11()
the carrier of G is non empty set
a is Element of the carrier of G
b is Element of the carrier of G
(G,a,b) is Element of the carrier of G
a " is Element of the carrier of G
b " is Element of the carrier of G
(a ") * (b ") is Element of the carrier of G
((a ") * (b ")) * a is Element of the carrier of G
(((a ") * (b ")) * a) * b is Element of the carrier of G
b is non empty unital Group-like associative Subgroup of G
a * b is Element of the carrier of G
((a ") * (b ")) * (a * b) is Element of the carrier of G
G is non empty unital Group-like associative L11()
the carrier of G is non empty set
a is Element of the carrier of G
b is Element of the carrier of G
(G,a,b) is Element of the carrier of G
a " is Element of the carrier of G
b " is Element of the carrier of G
(a ") * (b ") is Element of the carrier of G
((a ") * (b ")) * a is Element of the carrier of G
(((a ") * (b ")) * a) * b is Element of the carrier of G
b is Element of the carrier of G
(G,(G,a,b),b) is Element of the carrier of G
(G,a,b) " is Element of the carrier of G
b " is Element of the carrier of G
((G,a,b) ") * (b ") is Element of the carrier of G
(((G,a,b) ") * (b ")) * (G,a,b) is Element of the carrier of G
((((G,a,b) ") * (b ")) * (G,a,b)) * b is Element of the carrier of G
G is non empty unital Group-like associative L11()
the carrier of G 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
b is Element of the carrier of G
(G,a,b,(1_ G)) is Element of the carrier of G
(G,a,b) is Element of the carrier of G
a " is Element of the carrier of G
b " is Element of the carrier of G
(a ") * (b ") is Element of the carrier of G
((a ") * (b ")) * a is Element of the carrier of G
(((a ") * (b ")) * a) * b is Element of the carrier of G
(G,(G,a,b),(1_ G)) is Element of the carrier of G
(G,a,b) " is Element of the carrier of G
(1_ G) " is Element of the carrier of G
((G,a,b) ") * ((1_ G) ") is Element of the carrier of G
(((G,a,b) ") * ((1_ G) ")) * (G,a,b) is Element of the carrier of G
((((G,a,b) ") * ((1_ G) ")) * (G,a,b)) * (1_ G) is Element of the carrier of G
(G,a,(1_ G),b) is Element of the carrier of G
(G,a,(1_ G)) is Element of the carrier of G
(a ") * ((1_ G) ") is Element of the carrier of G
((a ") * ((1_ G) ")) * a is Element of the carrier of G
(((a ") * ((1_ G) ")) * a) * (1_ G) is Element of the carrier of G
(G,(G,a,(1_ G)),b) is Element of the carrier of G
(G,a,(1_ G)) " is Element of the carrier of G
((G,a,(1_ G)) ") * (b ") is Element of the carrier of G
(((G,a,(1_ G)) ") * (b ")) * (G,a,(1_ G)) is Element of the carrier of G
((((G,a,(1_ G)) ") * (b ")) * (G,a,(1_ G))) * b is Element of the carrier of G
(G,(1_ G),a,b) is Element of the carrier of G
(G,(1_ G),a) is Element of the carrier of G
((1_ G) ") * (a ") is Element of the carrier of G
(((1_ G) ") * (a ")) * (1_ G) is Element of the carrier of G
((((1_ G) ") * (a ")) * (1_ G)) * a is Element of the carrier of G
(G,(G,(1_ G),a),b) is Element of the carrier of G
(G,(1_ G),a) " is Element of the carrier of G
((G,(1_ G),a) ") * (b ") is Element of the carrier of G
(((G,(1_ G),a) ") * (b ")) * (G,(1_ G),a) is Element of the carrier of G
((((G,(1_ G),a) ") * (b ")) * (G,(1_ G),a)) * b is Element of the carrier of G
(G,(1_ G),b) is Element of the carrier of G
((1_ G) ") * (b ") is Element of the carrier of G
(((1_ G) ") * (b ")) * (1_ G) is Element of the carrier of G
((((1_ G) ") * (b ")) * (1_ G)) * b is Element of the carrier of G
G is non empty unital Group-like associative L11()
the carrier of G 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
b is Element of the carrier of G
(G,a,a,b) is Element of the carrier of G
(G,a,a) is Element of the carrier of G
a " is Element of the carrier of G
(a ") * (a ") is Element of the carrier of G
((a ") * (a ")) * a is Element of the carrier of G
(((a ") * (a ")) * a) * a is Element of the carrier of G
(G,(G,a,a),b) is Element of the carrier of G
(G,a,a) " is Element of the carrier of G
b " is Element of the carrier of G
((G,a,a) ") * (b ") is Element of the carrier of G
(((G,a,a) ") * (b ")) * (G,a,a) is Element of the carrier of G
((((G,a,a) ") * (b ")) * (G,a,a)) * b is Element of the carrier of G
(G,(1_ G),b) is Element of the carrier of G
(1_ G) " is Element of the carrier of G
((1_ G) ") * (b ") is Element of the carrier of G
(((1_ G) ") * (b ")) * (1_ G) is Element of the carrier of G
((((1_ G) ") * (b ")) * (1_ G)) * b is Element of the carrier of G
G is non empty unital Group-like associative L11()
the carrier of G is non empty set
a is Element of the carrier of G
b is Element of the carrier of G
(G,a,b,a) is Element of the carrier of G
(G,a,b) is Element of the carrier of G
a " is Element of the carrier of G
b " is Element of the carrier of G
(a ") * (b ") is Element of the carrier of G
((a ") * (b ")) * a is Element of the carrier of G
(((a ") * (b ")) * a) * b is Element of the carrier of G
(G,(G,a,b),a) is Element of the carrier of G
(G,a,b) " is Element of the carrier of G
((G,a,b) ") * (a ") is Element of the carrier of G
(((G,a,b) ") * (a ")) * (G,a,b) is Element of the carrier of G
((((G,a,b) ") * (a ")) * (G,a,b)) * a is Element of the carrier of G
a |^ b is Element of the carrier of G
(b ") * a is Element of the carrier of G
((b ") * a) * b is Element of the carrier of G
(G,(a |^ b),a) is Element of the carrier of G
(a |^ b) " is Element of the carrier of G
((a |^ b) ") * (a ") is Element of the carrier of G
(((a |^ b) ") * (a ")) * (a |^ b) is Element of the carrier of G
((((a |^ b) ") * (a ")) * (a |^ b)) * a is Element of the carrier of G
(G,b,a) is Element of the carrier of G
(b ") * (a ") is Element of the carrier of G
((b ") * (a ")) * b is Element of the carrier of G
(((b ") * (a ")) * b) * a is Element of the carrier of G
(G,b,a) * (a ") is Element of the carrier of G
((G,b,a) * (a ")) * (G,a,b) is Element of the carrier of G
(((G,b,a) * (a ")) * (G,a,b)) * a is Element of the carrier of G
(a ") |^ b is Element of the carrier of G
((a ") |^ b) * ((((a ") * (b ")) * a) * b) is Element of the carrier of G
(((a ") |^ b) * ((((a ") * (b ")) * a) * b)) * a is Element of the carrier of G
((a |^ b) ") * ((((a ") * (b ")) * a) * b) is Element of the carrier of G
(((a |^ b) ") * ((((a ") * (b ")) * a) * b)) * a is Element of the carrier of G
a * b is Element of the carrier of G
((a ") * (b ")) * (a * b) is Element of the carrier of G
((a |^ b) ") * (((a ") * (b ")) * (a * b)) is Element of the carrier of G
(((a |^ b) ") * (((a ") * (b ")) * (a * b))) * a is Element of the carrier of G
(b ") * (a * b) is Element of the carrier of G
(a ") * ((b ") * (a * b)) is Element of the carrier of G
((a |^ b) ") * ((a ") * ((b ") * (a * b))) is Element of the carrier of G
(((a |^ b) ") * ((a ") * ((b ") * (a * b)))) * a is Element of the carrier of G
(a ") * (a |^ b) is Element of the carrier of G
((a |^ b) ") * ((a ") * (a |^ b)) is Element of the carrier of G
(((a |^ b) ") * ((a ") * (a |^ b))) * a is Element of the carrier of G
G is non empty unital Group-like associative L11()
the carrier of G is non empty set
a is Element of the carrier of G
b is Element of the carrier of G
(G,a,b,b) is Element of the carrier of G
(G,a,b) is Element of the carrier of G
a " is Element of the carrier of G
b " is Element of the carrier of G
(a ") * (b ") is Element of the carrier of G
((a ") * (b ")) * a is Element of the carrier of G
(((a ") * (b ")) * a) * b is Element of the carrier of G
(G,(G,a,b),b) is Element of the carrier of G
(G,a,b) " is Element of the carrier of G
((G,a,b) ") * (b ") is Element of the carrier of G
(((G,a,b) ") * (b ")) * (G,a,b) is Element of the carrier of G
((((G,a,b) ") * (b ")) * (G,a,b)) * b is Element of the carrier of G
(G,a,(b ")) is Element of the carrier of G
(b ") " is Element of the carrier of G
(a ") * ((b ") ") is Element of the carrier of G
((a ") * ((b ") ")) * a is Element of the carrier of G
(((a ") * ((b ") ")) * a) * (b ") is Element of the carrier of G
(G,a,(b ")) * (G,a,b) is Element of the carrier of G
((G,a,(b ")) * (G,a,b)) |^ b is Element of the carrier of G
(b ") * ((G,a,(b ")) * (G,a,b)) is Element of the carrier of G
((b ") * ((G,a,(b ")) * (G,a,b))) * b is Element of the carrier of G
(G,b,a) is Element of the carrier of G
(b ") * (a ") is Element of the carrier of G
((b ") * (a ")) * b is Element of the carrier of G
(((b ") * (a ")) * b) * a is Element of the carrier of G
(G,b,a) * (b ") is Element of the carrier of G
((G,b,a) * (b ")) * (G,a,b) is Element of the carrier of G
(((G,b,a) * (b ")) * (G,a,b)) * b is Element of the carrier of G
b * a is Element of the carrier of G
(a ") * (b * a) is Element of the carrier of G
(b ") * ((a ") * (b * a)) is Element of the carrier of G
((b ") * ((a ") * (b * a))) * (b ") is Element of the carrier of G
(((b ") * ((a ") * (b * a))) * (b ")) * (G,a,b) is Element of the carrier of G
((((b ") * ((a ") * (b * a))) * (b ")) * (G,a,b)) * b is Element of the carrier of G
((b ") ") * a is Element of the carrier of G
(a ") * (((b ") ") * a) is Element of the carrier of G
(b ") * ((a ") * (((b ") ") * a)) is Element of the carrier of G
((b ") * ((a ") * (((b ") ") * a))) * (b ") is Element of the carrier of G
(((b ") * ((a ") * (((b ") ") * a))) * (b ")) * (G,a,b) is Element of the carrier of G
((((b ") * ((a ") * (((b ") ") * a))) * (b ")) * (G,a,b)) * b is Element of the carrier of G
((a ") * (((b ") ") * a)) * (b ") is Element of the carrier of G
(b ") * (((a ") * (((b ") ") * a)) * (b ")) is Element of the carrier of G
((b ") * (((a ") * (((b ") ") * a)) * (b "))) * (G,a,b) is Element of the carrier of G
(((b ") * (((a ") * (((b ") ") * a)) * (b "))) * (G,a,b)) * b is Element of the carrier of G
(b ") * (G,a,(b ")) is Element of the carrier of G
((b ") * (G,a,(b "))) * (G,a,b) is Element of the carrier of G
(((b ") * (G,a,(b "))) * (G,a,b)) * b is Element of the carrier of G
G is non empty unital Group-like associative L11()
the carrier of G is non empty set
a is Element of the carrier of G
b is Element of the carrier of G
b |^ a is Element of the carrier of G
a " is Element of the carrier of G
(a ") * b is Element of the carrier of G
((a ") * b) * a is Element of the carrier of G
(G,a,b,(b |^ a)) is Element of the carrier of G
(G,a,b) is Element of the carrier of G
b " is Element of the carrier of G
(a ") * (b ") is Element of the carrier of G
((a ") * (b ")) * a is Element of the carrier of G
(((a ") * (b ")) * a) * b is Element of the carrier of G
(G,(G,a,b),(b |^ a)) is Element of the carrier of G
(G,a,b) " is Element of the carrier of G
(b |^ a) " is Element of the carrier of G
((G,a,b) ") * ((b |^ a) ") is Element of the carrier of G
(((G,a,b) ") * ((b |^ a) ")) * (G,a,b) is Element of the carrier of G
((((G,a,b) ") * ((b |^ a) ")) * (G,a,b)) * (b |^ a) is Element of the carrier of G
(G,b,a) is Element of the carrier of G
(b ") * (a ") is Element of the carrier of G
((b ") * (a ")) * b is Element of the carrier of G
(((b ") * (a ")) * b) * a is Element of the carrier of G
(G,b,(G,b,a)) is Element of the carrier of G
(G,b,a) " is Element of the carrier of G
(b ") * ((G,b,a) ") is Element of the carrier of G
((b ") * ((G,b,a) ")) * b is Element of the carrier of G
(((b ") * ((G,b,a) ")) * b) * (G,b,a) is Element of the carrier of G
(G,b,a) * ((b |^ a) ") is Element of the carrier of G
((G,b,a) * ((b |^ a) ")) * (G,a,b) is Element of the carrier of G
(((G,b,a) * ((b |^ a) ")) * (G,a,b)) * (b |^ a) is Element of the carrier of G
(b ") |^ a is Element of the carrier of G
((((b ") * (a ")) * b) * a) * ((b ") |^ a) is Element of the carrier of G
(((((b ") * (a ")) * b) * a) * ((b ") |^ a)) * (G,a,b) is Element of the carrier of G
((((((b ") * (a ")) * b) * a) * ((b ") |^ a)) * (G,a,b)) * (b |^ a) is Element of the carrier of G
(b ") * a is Element of the carrier of G
(a ") * ((b ") * a) is Element of the carrier of G
((((b ") * (a ")) * b) * a) * ((a ") * ((b ") * a)) is Element of the carrier of G
(((((b ") * (a ")) * b) * a) * ((a ") * ((b ") * a))) * (G,a,b) is Element of the carrier of G
((((((b ") * (a ")) * b) * a) * ((a ") * ((b ") * a))) * (G,a,b)) * (b |^ a) is Element of the carrier of G
((((b ") * (a ")) * b) * a) * (a ") is Element of the carrier of G
(((((b ") * (a ")) * b) * a) * (a ")) * ((b ") * a) is Element of the carrier of G
((((((b ") * (a ")) * b) * a) * (a ")) * ((b ") * a)) * (G,a,b) is Element of the carrier of G
(((((((b ") * (a ")) * b) * a) * (a ")) * ((b ") * a)) * (G,a,b)) * (b |^ a) is Element of the carrier of G
(((b ") * (a ")) * b) * ((b ") * a) is Element of the carrier of G
((((b ") * (a ")) * b) * ((b ") * a)) * (G,a,b) is Element of the carrier of G
(((((b ") * (a ")) * b) * ((b ") * a)) * (G,a,b)) * (b |^ a) is Element of the carrier of G
b * ((b ") * a) is Element of the carrier of G
((b ") * (a ")) * (b * ((b ") * a)) is Element of the carrier of G
(((b ") * (a ")) * (b * ((b ") * a))) * (G,a,b) is Element of the carrier of G
((((b ") * (a ")) * (b * ((b ") * a))) * (G,a,b)) * (b |^ a) is Element of the carrier of G
((b ") * (a ")) * a is Element of the carrier of G
(((b ") * (a ")) * a) * (G,a,b) is Element of the carrier of G
((((b ") * (a ")) * a) * (G,a,b)) * (b |^ a) is Element of the carrier of G
(b ") * ((((a ") * (b ")) * a) * b) is Element of the carrier of G
((b ") * ((((a ") * (b ")) * a) * b)) * (b |^ a) is Element of the carrier of G
1_ G is non being_of_order_0 Element of the carrier of G
((b ") * ((((a ") * (b ")) * a) * b)) * (1_ G) is Element of the carrier of G
(((b ") * ((((a ") * (b ")) * a) * b)) * (1_ G)) * (((a ") * b) * a) is Element of the carrier of G
(b ") * (G,a,b) is Element of the carrier of G
b * (b ") is Element of the carrier of G
((b ") * (G,a,b)) * (b * (b ")) is Element of the carrier of G
(((b ") * (G,a,b)) * (b * (b "))) * (((a ") * b) * a) is Element of the carrier of G
(b * (b ")) * (((a ") * b) * a) is Element of the carrier of G
((b ") * (G,a,b)) * ((b * (b ")) * (((a ") * b) * a)) is Element of the carrier of G
(b ") * (((a ") * b) * a) is Element of the carrier of G
b * ((b ") * (((a ") * b) * a)) is Element of the carrier of G
((b ") * (G,a,b)) * (b * ((b ") * (((a ") * b) * a))) is Element of the carrier of G
b * (G,b,a) is Element of the carrier of G
((b ") * (G,a,b)) * (b * (G,b,a)) is Element of the carrier of G
((b ") * ((G,b,a) ")) * (b * (G,b,a)) is Element of the carrier of G
G is non empty unital Group-like associative L11()
the carrier of G is non empty set
a is Element of the carrier of G
b is Element of the carrier of G
a * b is Element of the carrier of G
b is Element of the carrier of G
(G,(a * b),b) is Element of the carrier of G
(a * b) " is Element of the carrier of G
b " is Element of the carrier of G
((a * b) ") * (b ") is Element of the carrier of G
(((a * b) ") * (b ")) * (a * b) is Element of the carrier of G
((((a * b) ") * (b ")) * (a * b)) * b is Element of the carrier of G
(G,a,b) is Element of the carrier of G
a " is Element of the carrier of G
(a ") * (b ") is Element of the carrier of G
((a ") * (b ")) * a is Element of the carrier of G
(((a ") * (b ")) * a) * b is Element of the carrier of G
(G,a,b,b) is Element of the carrier of G
(G,(G,a,b),b) is Element of the carrier of G
(G,a,b) " is Element of the carrier of G
b " is Element of the carrier of G
((G,a,b) ") * (b ") is Element of the carrier of G
(((G,a,b) ") * (b ")) * (G,a,b) is Element of the carrier of G
((((G,a,b) ") * (b ")) * (G,a,b)) * b is Element of the carrier of G
(G,a,b) * (G,a,b,b) is Element of the carrier of G
(G,b,b) is Element of the carrier of G
(b ") * (b ") is Element of the carrier of G
((b ") * (b ")) * b is Element of the carrier of G
(((b ") * (b ")) * b) * b is Element of the carrier of G
((G,a,b) * (G,a,b,b)) * (G,b,b) is Element of the carrier of G
(G,b,a) is Element of the carrier of G
(b ") * (a ") is Element of the carrier of G
((b ") * (a ")) * b is Element of the carrier of G
(((b ") * (a ")) * b) * a is Element of the carrier of G
(G,b,a) * (b ") is Element of the carrier of G
((G,b,a) * (b ")) * (G,a,b) is Element of the carrier of G
(((G,b,a) * (b ")) * (G,a,b)) * b is Element of the carrier of G
((((a ") * (b ")) * a) * b) * ((((G,b,a) * (b ")) * (G,a,b)) * b) is Element of the carrier of G
(((((a ") * (b ")) * a) * b) * ((((G,b,a) * (b ")) * (G,a,b)) * b)) * (G,b,b) is Element of the carrier of G
b * a is Element of the carrier of G
((b ") * (a ")) * (b * a) is Element of the carrier of G
(((b ") * (a ")) * (b * a)) * (b ") is Element of the carrier of G
((((b ") * (a ")) * (b * a)) * (b ")) * (G,a,b) is Element of the carrier of G
(((((b ") * (a ")) * (b * a)) * (b ")) * (G,a,b)) * b is Element of the carrier of G
((((a ") * (b ")) * a) * b) * ((((((b ") * (a ")) * (b * a)) * (b ")) * (G,a,b)) * b) is Element of the carrier of G
(((((a ") * (b ")) * a) * b) * ((((((b ") * (a ")) * (b * a)) * (b ")) * (G,a,b)) * b)) * (G,b,b) is Element of the carrier of G
a * b is Element of the carrier of G
(a * b) " is Element of the carrier of G
((a * b) ") * (b * a) is Element of the carrier of G
(((a * b) ") * (b * a)) * (b ") is Element of the carrier of G
((((a * b) ") * (b * a)) * (b ")) * (G,a,b) is Element of the carrier of G
(((((a * b) ") * (b * a)) * (b ")) * (G,a,b)) * b is Element of the carrier of G
((((a ") * (b ")) * a) * b) * ((((((a * b) ") * (b * a)) * (b ")) * (G,a,b)) * b) is Element of the carrier of G
(((((a ") * (b ")) * a) * b) * ((((((a * b) ") * (b * a)) * (b ")) * (G,a,b)) * b)) * (G,b,b) is Element of the carrier of G
((a ") * (b ")) * (a * b) is Element of the carrier of G
(((a ") * (b ")) * (a * b)) * ((((((a * b) ") * (b * a)) * (b ")) * (G,a,b)) * b) is Element of the carrier of G
((((a ") * (b ")) * (a * b)) * ((((((a * b) ") * (b * a)) * (b ")) * (G,a,b)) * b)) * (G,b,b) is Element of the carrier of G
(a * b) * ((((((a * b) ") * (b * a)) * (b ")) * (G,a,b)) * b) is Element of the carrier of G
((a ") * (b ")) * ((a * b) * ((((((a * b) ") * (b * a)) * (b ")) * (G,a,b)) * b)) is Element of the carrier of G
(((a ") * (b ")) * ((a * b) * ((((((a * b) ") * (b * a)) * (b ")) * (G,a,b)) * b))) * (G,b,b) is Element of the carrier of G
(G,a,b) * b is Element of the carrier of G
((((a * b) ") * (b * a)) * (b ")) * ((G,a,b) * b) is Element of the carrier of G
(a * b) * (((((a * b) ") * (b * a)) * (b ")) * ((G,a,b) * b)) is Element of the carrier of G
((a ") * (b ")) * ((a * b) * (((((a * b) ") * (b * a)) * (b ")) * ((G,a,b) * b))) is Element of the carrier of G
(((a ") * (b ")) * ((a * b) * (((((a * b) ") * (b * a)) * (b ")) * ((G,a,b) * b)))) * (G,b,b) is Element of the carrier of G
(b ") * ((G,a,b) * b) is Element of the carrier of G
(((a * b) ") * (b * a)) * ((b ") * ((G,a,b) * b)) is Element of the carrier of G
(a * b) * ((((a * b) ") * (b * a)) * ((b ") * ((G,a,b) * b))) is Element of the carrier of G
((a ") * (b ")) * ((a * b) * ((((a * b) ") * (b * a)) * ((b ") * ((G,a,b) * b)))) is Element of the carrier of G
(((a ") * (b ")) * ((a * b) * ((((a * b) ") * (b * a)) * ((b ") * ((G,a,b) * b))))) * (G,b,b) is Element of the carrier of G
(b * a) * ((b ") * ((G,a,b) * b)) is Element of the carrier of G
((a * b) ") * ((b * a) * ((b ") * ((G,a,b) * b))) is Element of the carrier of G
(a * b) * (((a * b) ") * ((b * a) * ((b ") * ((G,a,b) * b)))) is Element of the carrier of G
((a ") * (b ")) * ((a * b) * (((a * b) ") * ((b * a) * ((b ") * ((G,a,b) * b))))) is Element of the carrier of G
(((a ") * (b ")) * ((a * b) * (((a * b) ") * ((b * a) * ((b ") * ((G,a,b) * b)))))) * (G,b,b) is Element of the carrier of G
(a * b) * ((a * b) ") is Element of the carrier of G
((a * b) * ((a * b) ")) * ((b * a) * ((b ") * ((G,a,b) * b))) is Element of the carrier of G
((a ") * (b ")) * (((a * b) * ((a * b) ")) * ((b * a) * ((b ") * ((G,a,b) * b)))) is Element of the carrier of G
(((a ") * (b ")) * (((a * b) * ((a * b) ")) * ((b * a) * ((b ") * ((G,a,b) * b))))) * (G,b,b) is Element of the carrier of G
1_ G is non being_of_order_0 Element of the carrier of G
(1_ G) * ((b * a) * ((b ") * ((G,a,b) * b))) is Element of the carrier of G
((a ") * (b ")) * ((1_ G) * ((b * a) * ((b ") * ((G,a,b) * b)))) is Element of the carrier of G
(((a ") * (b ")) * ((1_ G) * ((b * a) * ((b ") * ((G,a,b) * b))))) * (G,b,b) is Element of the carrier of G
((a ") * (b ")) * ((b * a) * ((b ") * ((G,a,b) * b))) is Element of the carrier of G
(((a ") * (b ")) * ((b * a) * ((b ") * ((G,a,b) * b)))) * (G,b,b) is Element of the carrier of G
((a ") * (b ")) * (b * a) is Element of the carrier of G
(((a ") * (b ")) * (b * a)) * ((b ") * ((G,a,b) * b)) is Element of the carrier of G
((((a ") * (b ")) * (b * a)) * ((b ") * ((G,a,b) * b))) * (G,b,b) is Element of the carrier of G
(b * a) " is Element of the carrier of G
((b * a) ") * (b * a) is Element of the carrier of G
(((b * a) ") * (b * a)) * ((b ") * ((G,a,b) * b)) is Element of the carrier of G
((((b * a) ") * (b * a)) * ((b ") * ((G,a,b) * b))) * (G,b,b) is Element of the carrier of G
(1_ G) * ((b ") * ((G,a,b) * b)) is Element of the carrier of G
((1_ G) * ((b ") * ((G,a,b) * b))) * (G,b,b) is Element of the carrier of G
((b ") * ((G,a,b) * b)) * (G,b,b) is Element of the carrier of G
((((a ") * (b ")) * a) * b) * b is Element of the carrier of G
(b ") * (((((a ") * (b ")) * a) * b) * b) is Element of the carrier of G
b * b is Element of the carrier of G
((b ") * (b ")) * (b * b) is Element of the carrier of G
((b ") * (((((a ") * (b ")) * a) * b) * b)) * (((b ") * (b ")) * (b * b)) is Element of the carrier of G
(b ") * ((((a ") * (b ")) * a) * b) is Element of the carrier of G
((b ") * ((((a ") * (b ")) * a) * b)) * b is Element of the carrier of G
(((b ") * ((((a ") * (b ")) * a) * b)) * b) * (((b ") * (b ")) * (b * b)) is Element of the carrier of G
(b ") * (((a ") * (b ")) * (a * b)) is Element of the carrier of G
((b ") * (((a ") * (b ")) * (a * b))) * b is Element of the carrier of G
(((b ") * (((a ") * (b ")) * (a * b))) * b) * (((b ") * (b ")) * (b * b)) is Element of the carrier of G
(b ") * (a * b) is Element of the carrier of G
(a ") * ((b ") * (a * b)) is Element of the carrier of G
(b ") * ((a ") * ((b ") * (a * b))) is Element of the carrier of G
((b ") * ((a ") * ((b ") * (a * b)))) * b is Element of the carrier of G
(((b ") * ((a ") * ((b ") * (a * b)))) * b) * (((b ") * (b ")) * (b * b)) is Element of the carrier of G
(b ") * (a ") is Element of the carrier of G
((b ") * (a ")) * ((b ") * (a * b)) is Element of the carrier of G
(((b ") * (a ")) * ((b ") * (a * b))) * b is Element of the carrier of G
((((b ") * (a ")) * ((b ") * (a * b))) * b) * (((b ") * (b ")) * (b * b)) is Element of the carrier of G
((b ") * (a ")) * (b ") is Element of the carrier of G
(((b ") * (a ")) * (b ")) * (a * b) is Element of the carrier of G
((((b ") * (a ")) * (b ")) * (a * b)) * b is Element of the carrier of G
(((((b ") * (a ")) * (b ")) * (a * b)) * b) * (((b ") * (b ")) * (b * b)) is Element of the carrier of G
(((b ") * (a ")) * (b ")) * a is Element of the carrier of G
((((b ") * (a ")) * (b ")) * a) * b is Element of the carrier of G
(((((b ") * (a ")) * (b ")) * a) * b) * b is Element of the carrier of G
((((((b ") * (a ")) * (b ")) * a) * b) * b) * (((b ") * (b ")) * (b * b)) is Element of the carrier of G
b * b is Element of the carrier of G
((((b ") * (a ")) * (b ")) * a) * (b * b) is Element of the carrier of G
(((((b ") * (a ")) * (b ")) * a) * (b * b)) * (((b ") * (b ")) * (b * b)) is Element of the carrier of G
(((((b ") * (a ")) * (b ")) * a) * (b * b)) * ((b ") * (b ")) is Element of the carrier of G
((((((b ") * (a ")) * (b ")) * a) * (b * b)) * ((b ") * (b "))) * (b * b) is Element of the carrier of G
(b * b) " is Element of the carrier of G
(((((b ") * (a ")) * (b ")) * a) * (b * b)) * ((b * b) ") is Element of the carrier of G
((((((b ") * (a ")) * (b ")) * a) * (b * b)) * ((b * b) ")) * (b * b) is Element of the carrier of G
(b * b) * ((b * b) ") is Element of the carrier of G
((((b ") * (a ")) * (b ")) * a) * ((b * b) * ((b * b) ")) is Element of the carrier of G
(((((b ") * (a ")) * (b ")) * a) * ((b * b) * ((b * b) "))) * (b * b) is Element of the carrier of G
((((b ") * (a ")) * (b ")) * a) * (1_ G) is Element of the carrier of G
(((((b ") * (a ")) * (b ")) * a) * (1_ G)) * (b * b) is Element of the carrier of G
((((b ") * (a ")) * (b ")) * a) * (b * b) is Element of the carrier of G
(((a * b) ") * (b ")) * a is Element of the carrier of G
((((a * b) ") * (b ")) * a) * (b * b) is Element of the carrier of G
a * (b * b) is Element of the carrier of G
(((a * b) ") * (b ")) * (a * (b * b)) is Element of the carrier of G
(a * b) * b is Element of the carrier of G
(((a * b) ") * (b ")) * ((a * b) * b) is Element of the carrier of G
G is non empty unital Group-like associative L11()
the carrier of G is non empty set
a is Element of the carrier of G
b is Element of the carrier of G
(G,a,b) is Element of the carrier of G
a " is Element of the carrier of G
b " is Element of the carrier of G
(a ") * (b ") is Element of the carrier of G
((a ") * (b ")) * a is Element of the carrier of G
(((a ") * (b ")) * a) * b is Element of the carrier of G
b is Element of the carrier of G
b * b is Element of the carrier of G
(G,a,(b * b)) is Element of the carrier of G
(b * b) " is Element of the carrier of G
(a ") * ((b * b) ") is Element of the carrier of G
((a ") * ((b * b) ")) * a is Element of the carrier of G
(((a ") * ((b * b) ")) * a) * (b * b) is Element of the carrier of G
(G,a,b) is Element of the carrier of G
b " is Element of the carrier of G
(a ") * (b ") is Element of the carrier of G
((a ") * (b ")) * a is Element of the carrier of G
(((a ") * (b ")) * a) * b is Element of the carrier of G
(G,a,b) * (G,a,b) is Element of the carrier of G
(G,a,b,b) is Element of the carrier of G
(G,(G,a,b),b) is Element of the carrier of G
(G,a,b) " is Element of the carrier of G
((G,a,b) ") * (b ") is Element of the carrier of G
(((G,a,b) ") * (b ")) * (G,a,b) is Element of the carrier of G
((((G,a,b) ") * (b ")) * (G,a,b)) * b is Element of the carrier of G
((G,a,b) * (G,a,b)) * (G,a,b,b) is Element of the carrier of G
(G,a,b) * (G,(G,a,b),b) is Element of the carrier of G
(G,a,b) * ((G,a,b) * (G,(G,a,b),b)) is Element of the carrier of G
a * b is Element of the carrier of G
((a ") * (b ")) * (a * b) is Element of the carrier of G
(((a ") * (b ")) * (a * b)) * (((((G,a,b) ") * (b ")) * (G,a,b)) * b) is Element of the carrier of G
(G,a,b) * ((((a ") * (b ")) * (a * b)) * (((((G,a,b) ") * (b ")) * (G,a,b)) * b)) is Element of the carrier of G
(G,b,a) is Element of the carrier of G
(b ") * (a ") is Element of the carrier of G
((b ") * (a ")) * b is Element of the carrier of G
(((b ") * (a ")) * b) * a is Element of the carrier of G
(G,b,a) * (b ") is Element of the carrier of G
((G,b,a) * (b ")) * (G,a,b) is Element of the carrier of G
(((G,b,a) * (b ")) * (G,a,b)) * b is Element of the carrier of G
(((a ") * (b ")) * (a * b)) * ((((G,b,a) * (b ")) * (G,a,b)) * b) is Element of the carrier of G
(G,a,b) * ((((a ") * (b ")) * (a * b)) * ((((G,b,a) * (b ")) * (G,a,b)) * b)) is Element of the carrier of G
b * a is Element of the carrier of G
((b ") * (a ")) * (b * a) is Element of the carrier of G
(((b ") * (a ")) * (b * a)) * (b ") is Element of the carrier of G
((((b ") * (a ")) * (b * a)) * (b ")) * (G,a,b) is Element of the carrier of G
(((((b ") * (a ")) * (b * a)) * (b ")) * (G,a,b)) * b is Element of the carrier of G
(((a ") * (b ")) * (a * b)) * ((((((b ") * (a ")) * (b * a)) * (b ")) * (G,a,b)) * b) is Element of the carrier of G
(G,a,b) * ((((a ") * (b ")) * (a * b)) * ((((((b ") * (a ")) * (b * a)) * (b ")) * (G,a,b)) * b)) is Element of the carrier of G
(a * b) * ((((((b ") * (a ")) * (b * a)) * (b ")) * (G,a,b)) * b) is Element of the carrier of G
((a ") * (b ")) * ((a * b) * ((((((b ") * (a ")) * (b * a)) * (b ")) * (G,a,b)) * b)) is Element of the carrier of G
(G,a,b) * (((a ") * (b ")) * ((a * b) * ((((((b ") * (a ")) * (b * a)) * (b ")) * (G,a,b)) * b))) is Element of the carrier of G
(G,a,b) * b is Element of the carrier of G
((((b ") * (a ")) * (b * a)) * (b ")) * ((G,a,b) * b) is Element of the carrier of G
(a * b) * (((((b ") * (a ")) * (b * a)) * (b ")) * ((G,a,b) * b)) is Element of the carrier of G
((a ") * (b ")) * ((a * b) * (((((b ") * (a ")) * (b * a)) * (b ")) * ((G,a,b) * b))) is Element of the carrier of G
(G,a,b) * (((a ") * (b ")) * ((a * b) * (((((b ") * (a ")) * (b * a)) * (b ")) * ((G,a,b) * b)))) is Element of the carrier of G
(b ") * ((G,a,b) * b) is Element of the carrier of G
(((b ") * (a ")) * (b * a)) * ((b ") * ((G,a,b) * b)) is Element of the carrier of G
(a * b) * ((((b ") * (a ")) * (b * a)) * ((b ") * ((G,a,b) * b))) is Element of the carrier of G
((a ") * (b ")) * ((a * b) * ((((b ") * (a ")) * (b * a)) * ((b ") * ((G,a,b) * b)))) is Element of the carrier of G
(G,a,b) * (((a ") * (b ")) * ((a * b) * ((((b ") * (a ")) * (b * a)) * ((b ") * ((G,a,b) * b))))) is Element of the carrier of G
(a * b) * (((b ") * (a ")) * (b * a)) is Element of the carrier of G
((a * b) * (((b ") * (a ")) * (b * a))) * ((b ") * ((G,a,b) * b)) is Element of the carrier of G
((a ") * (b ")) * (((a * b) * (((b ") * (a ")) * (b * a))) * ((b ") * ((G,a,b) * b))) is Element of the carrier of G
(G,a,b) * (((a ") * (b ")) * (((a * b) * (((b ") * (a ")) * (b * a))) * ((b ") * ((G,a,b) * b)))) is Element of the carrier of G
(a * b) * ((b ") * (a ")) is Element of the carrier of G
((a * b) * ((b ") * (a "))) * (b * a) is Element of the carrier of G
(((a * b) * ((b ") * (a "))) * (b * a)) * ((b ") * ((G,a,b) * b)) is Element of the carrier of G
((a ") * (b ")) * ((((a * b) * ((b ") * (a "))) * (b * a)) * ((b ") * ((G,a,b) * b))) is Element of the carrier of G
(G,a,b) * (((a ") * (b ")) * ((((a * b) * ((b ") * (a "))) * (b * a)) * ((b ") * ((G,a,b) * b)))) is Element of the carrier of G
(a * b) " is Element of the carrier of G
(a * b) * ((a * b) ") is Element of the carrier of G
((a * b) * ((a * b) ")) * (b * a) is Element of the carrier of G
(((a * b) * ((a * b) ")) * (b * a)) * ((b ") * ((G,a,b) * b)) is Element of the carrier of G
((a ") * (b ")) * ((((a * b) * ((a * b) ")) * (b * a)) * ((b ") * ((G,a,b) * b))) is Element of the carrier of G
(G,a,b) * (((a ") * (b ")) * ((((a * b) * ((a * b) ")) * (b * a)) * ((b ") * ((G,a,b) * b)))) is Element of the carrier of G
1_ G is non being_of_order_0 Element of the carrier of G
(1_ G) * (b * a) is Element of the carrier of G
((1_ G) * (b * a)) * ((b ") * ((G,a,b) * b)) is Element of the carrier of G
((a ") * (b ")) * (((1_ G) * (b * a)) * ((b ") * ((G,a,b) * b))) is Element of the carrier of G
(G,a,b) * (((a ") * (b ")) * (((1_ G) * (b * a)) * ((b ") * ((G,a,b) * b)))) is Element of the carrier of G
(b * a) * ((b ") * ((G,a,b) * b)) is Element of the carrier of G
((a ") * (b ")) * ((b * a) * ((b ") * ((G,a,b) * b))) is Element of the carrier of G
(G,a,b) * (((a ") * (b ")) * ((b * a) * ((b ") * ((G,a,b) * b)))) is Element of the carrier of G
((a ") * (b ")) * (b * a) is Element of the carrier of G
(((a ") * (b ")) * (b * a)) * ((b ") * ((G,a,b) * b)) is Element of the carrier of G
(G,a,b) * ((((a ") * (b ")) * (b * a)) * ((b ") * ((G,a,b) * b))) is Element of the carrier of G
(b * a) " is Element of the carrier of G
((b * a) ") * (b * a) is Element of the carrier of G
(((b * a) ") * (b * a)) * ((b ") * ((G,a,b) * b)) is Element of the carrier of G
(G,a,b) * ((((b * a) ") * (b * a)) * ((b ") * ((G,a,b) * b))) is Element of the carrier of G
(1_ G) * ((b ") * ((G,a,b) * b)) is Element of the carrier of G
(G,a,b) * ((1_ G) * ((b ") * ((G,a,b) * b))) is Element of the carrier of G
(G,a,b) * ((b ") * ((G,a,b) * b)) is Element of the carrier of G
a * b is Element of the carrier of G
((a ") * (b ")) * (a * b) is Element of the carrier of G
(((a ") * (b ")) * (a * b)) * ((b ") * ((G,a,b) * b)) is Element of the carrier of G
(b ") * a is Element of the carrier of G
((b ") * a) * b is Element of the carrier of G
(a ") * (((b ") * a) * b) is Element of the carrier of G
((a ") * (((b ") * a) * b)) * b is Element of the carrier of G
(b ") * (((a ") * (((b ") * a) * b)) * b) is Element of the carrier of G
(((a ") * (b ")) * (a * b)) * ((b ") * (((a ") * (((b ") * a) * b)) * b)) is Element of the carrier of G
(b ") * ((a ") * (((b ") * a) * b)) is Element of the carrier of G
((b ") * ((a ") * (((b ") * a) * b))) * b is Element of the carrier of G
(((a ") * (b ")) * (a * b)) * (((b ") * ((a ") * (((b ") * a) * b))) * b) is Element of the carrier of G
(b ") * (a ") is Element of the carrier of G
((b ") * (a ")) * (((b ") * a) * b) is Element of the carrier of G
(((b ") * (a ")) * (((b ") * a) * b)) * b is Element of the carrier of G
(((a ") * (b ")) * (a * b)) * ((((b ") * (a ")) * (((b ") * a) * b)) * b) is Element of the carrier of G
(((b ") * a) * b) * b is Element of the carrier of G
((b ") * (a ")) * ((((b ") * a) * b) * b) is Element of the carrier of G
(((a ") * (b ")) * (a * b)) * (((b ") * (a ")) * ((((b ") * a) * b) * b)) is Element of the carrier of G
(((a ") * (b ")) * (a * b)) * ((b ") * (a ")) is Element of the carrier of G
((((a ") * (b ")) * (a * b)) * ((b ") * (a "))) * ((((b ") * a) * b) * b) is Element of the carrier of G
(a * b) * ((b ") * (a ")) is Element of the carrier of G
((a ") * (b ")) * ((a * b) * ((b ") * (a "))) is Element of the carrier of G
(((a ") * (b ")) * ((a * b) * ((b ") * (a ")))) * ((((b ") * a) * b) * b) is Element of the carrier of G
(a * b) " is Element of the carrier of G
(a * b) * ((a * b) ") is Element of the carrier of G
((a ") * (b ")) * ((a * b) * ((a * b) ")) is Element of the carrier of G
(((a ") * (b ")) * ((a * b) * ((a * b) "))) * ((((b ") * a) * b) * b) is Element of the carrier of G
((a ") * (b ")) * (1_ G) is Element of the carrier of G
(((a ") * (b ")) * (1_ G)) * ((((b ") * a) * b) * b) is Element of the carrier of G
((a ") * (b ")) * ((((b ") * a) * b) * b) is Element of the carrier of G
((a ") * (b ")) * (((b ") * a) * b) is Element of the carrier of G
(((a ") * (b ")) * (((b ") * a) * b)) * b is Element of the carrier of G
(b ") * (a * b) is Element of the carrier of G
((a ") * (b ")) * ((b ") * (a * b)) is Element of the carrier of G
(((a ") * (b ")) * ((b ") * (a * b))) * b is Element of the carrier of G
((a ") * (b ")) * (b ") is Element of the carrier of G
(((a ") * (b ")) * (b ")) * (a * b) is Element of the carrier of G
((((a ") * (b ")) * (b ")) * (a * b)) * b is Element of the carrier of G
(b ") * (b ") is Element of the carrier of G
(a ") * ((b ") * (b ")) is Element of the carrier of G
((a ") * ((b ") * (b "))) * (a * b) is Element of the carrier of G
(((a ") * ((b ") * (b "))) * (a * b)) * b is Element of the carrier of G
(a * b) * b is Element of the carrier of G
((a ") * ((b ") * (b "))) * ((a * b) * b) is Element of the carrier of G
a * (b * b) is Element of the carrier of G
((a ") * ((b ") * (b "))) * (a * (b * b)) is Element of the carrier of G
((a ") * ((b * b) ")) * (a * (b * b)) is Element of the carrier of G
G is non empty unital Group-like associative L11()
the carrier of G 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
a " is Element of the carrier of G
b is Element of the carrier of G
b " is Element of the carrier of G
b is Element of the carrier of G
(G,a,(b "),b) is Element of the carrier of G
(G,a,(b ")) is Element of the carrier of G
(b ") " is Element of the carrier of G
(a ") * ((b ") ") is Element of the carrier of G
((a ") * ((b ") ")) * a is Element of the carrier of G
(((a ") * ((b ") ")) * a) * (b ") is Element of the carrier of G
(G,(G,a,(b ")),b) is Element of the carrier of G
(G,a,(b ")) " is Element of the carrier of G
b " is Element of the carrier of G
((G,a,(b ")) ") * (b ") is Element of the carrier of G
(((G,a,(b ")) ") * (b ")) * (G,a,(b ")) is Element of the carrier of G
((((G,a,(b ")) ") * (b ")) * (G,a,(b "))) * b is Element of the carrier of G
(G,a,(b "),b) |^ b is Element of the carrier of G
(b ") * (G,a,(b "),b) is Element of the carrier of G
((b ") * (G,a,(b "),b)) * b is Element of the carrier of G
(G,b,(b "),a) is Element of the carrier of G
(G,b,(b ")) is Element of the carrier of G
(b ") " is Element of the carrier of G
(b ") * ((b ") ") is Element of the carrier of G
((b ") * ((b ") ")) * b is Element of the carrier of G
(((b ") * ((b ") ")) * b) * (b ") is Element of the carrier of G
(G,(G,b,(b ")),a) is Element of the carrier of G
(G,b,(b ")) " is Element of the carrier of G
((G,b,(b ")) ") * (a ") is Element of the carrier of G
(((G,b,(b ")) ") * (a ")) * (G,b,(b ")) is Element of the carrier of G
((((G,b,(b ")) ") * (a ")) * (G,b,(b "))) * a is Element of the carrier of G
(G,b,(b "),a) |^ b is Element of the carrier of G
(b ") * (G,b,(b "),a) is Element of the carrier of G
((b ") * (G,b,(b "),a)) * b is Element of the carrier of G
((G,a,(b "),b) |^ b) * ((G,b,(b "),a) |^ b) is Element of the carrier of G
(G,b,(a "),b) is Element of the carrier of G
(G,b,(a ")) is Element of the carrier of G
(a ") " is Element of the carrier of G
(b ") * ((a ") ") is Element of the carrier of G
((b ") * ((a ") ")) * b is Element of the carrier of G
(((b ") * ((a ") ")) * b) * (a ") is Element of the carrier of G
(G,(G,b,(a ")),b) is Element of the carrier of G
(G,b,(a ")) " is Element of the carrier of G
((G,b,(a ")) ") * (b ") is Element of the carrier of G
(((G,b,(a ")) ") * (b ")) * (G,b,(a ")) is Element of the carrier of G
((((G,b,(a ")) ") * (b ")) * (G,b,(a "))) * b is Element of the carrier of G
(G,b,(a "),b) |^ a is Element of the carrier of G
(a ") * (G,b,(a "),b) is Element of the carrier of G
((a ") * (G,b,(a "),b)) * a is Element of the carrier of G
(((G,a,(b "),b) |^ b) * ((G,b,(b "),a) |^ b)) * ((G,b,(a "),b) |^ a) is Element of the carrier of G
(a ") * (G,b,(b ")) is Element of the carrier of G
((a ") * (G,b,(b "))) * a is Element of the carrier of G
(b ") * (G,a,(b ")) is Element of the carrier of G
((b ") * (G,a,(b "))) * b is Element of the carrier of G
(b ") * (G,b,(a ")) is Element of the carrier of G
((b ") * (G,b,(a "))) * b is Element of the carrier of G
(G,(b "),b) is Element of the carrier of G
((b ") ") * (b ") is Element of the carrier of G
(((b ") ") * (b ")) * (b ") is Element of the carrier of G
((((b ") ") * (b ")) * (b ")) * b is Element of the carrier of G
(b ") * (b ") is Element of the carrier of G
((b ") * (b ")) * b is Element of the carrier of G
((b ") ") * (((b ") * (b ")) * b) is Element of the carrier of G
(G,(a "),b) is Element of the carrier of G
((a ") ") * (b ") is Element of the carrier of G
(((a ") ") * (b ")) * (a ") is Element of the carrier of G
((((a ") ") * (b ")) * (a ")) * b is Element of the carrier of G
(b ") * (a ") is Element of the carrier of G
((b ") * (a ")) * b is Element of the carrier of G
((a ") ") * (((b ") * (a ")) * b) is Element of the carrier of G
(G,(b "),a) is Element of the carrier of G
((b ") ") * (a ") is Element of the carrier of G
(((b ") ") * (a ")) * (b ") is Element of the carrier of G
((((b ") ") * (a ")) * (b ")) * a is Element of the carrier of G
(a ") * (b ") is Element of the carrier of G
((a ") * (b ")) * a is Element of the carrier of G
((b ") ") * (((a ") * (b ")) * a) is Element of the carrier of G
((G,a,(b ")) ") * (((b ") * (G,a,(b "))) * b) is Element of the carrier of G
(G,(b "),a) * (((b ") * (G,a,(b "))) * b) is Element of the carrier of G
(((a ") * (b ")) * a) * (((b ") * (G,a,(b "))) * b) is Element of the carrier of G
((b ") ") * ((((a ") * (b ")) * a) * (((b ") * (G,a,(b "))) * b)) is Element of the carrier of G
(b ") * (((b ") ") * ((((a ") * (b ")) * a) * (((b ") * (G,a,(b "))) * b))) is Element of the carrier of G
((b ") * (((b ") ") * ((((a ") * (b ")) * a) * (((b ") * (G,a,(b "))) * b)))) * b is Element of the carrier of G
((((a ") * (b ")) * a) * (((b ") * (G,a,(b "))) * b)) * b is Element of the carrier of G
((G,b,(a ")) ") * (((b ") * (G,b,(a "))) * b) is Element of the carrier of G
(G,(a "),b) * (((b ") * (G,b,(a "))) * b) is Element of the carrier of G
(((b ") * (a ")) * b) * (((b ") * (G,b,(a "))) * b) is Element of the carrier of G
((a ") ") * ((((b ") * (a ")) * b) * (((b ") * (G,b,(a "))) * b)) is Element of the carrier of G
(a ") * (((a ") ") * ((((b ") * (a ")) * b) * (((b ") * (G,b,(a "))) * b))) is Element of the carrier of G
((a ") * (((a ") ") * ((((b ") * (a ")) * b) * (((b ") * (G,b,(a "))) * b)))) * a is Element of the carrier of G
((((b ") * (a ")) * b) * (((b ") * (G,b,(a "))) * b)) * a is Element of the carrier of G
((G,b,(b ")) ") * (((a ") * (G,b,(b "))) * a) is Element of the carrier of G
(G,(b "),b) * (((a ") * (G,b,(b "))) * a) is Element of the carrier of G
(((b ") * (b ")) * b) * (((a ") * (G,b,(b "))) * a) is Element of the carrier of G
((b ") ") * ((((b ") * (b ")) * b) * (((a ") * (G,b,(b "))) * a)) is Element of the carrier of G
(b ") * (((b ") ") * ((((b ") * (b ")) * b) * (((a ") * (G,b,(b "))) * a))) is Element of the carrier of G
((b ") * (((b ") ") * ((((b ") * (b ")) * b) * (((a ") * (G,b,(b "))) * a)))) * b is Element of the carrier of G
((((b ") * (b ")) * b) * (((a ") * (G,b,(b "))) * a)) * b is Element of the carrier of G
(((a ") * (G,b,(b "))) * a) * b is Element of the carrier of G
(((b ") * (b ")) * b) * ((((a ") * (G,b,(b "))) * a) * b) is Element of the carrier of G
(b ") * b is Element of the carrier of G
(b ") * ((b ") * b) is Element of the carrier of G
((b ") * ((b ") * b)) * ((((a ") * (G,b,(b "))) * a) * b) is Element of the carrier of G
((b ") * b) * ((((a ") * (G,b,(b "))) * a) * b) is Element of the carrier of G
(b ") * (((b ") * b) * ((((a ") * (G,b,(b "))) * a) * b)) is Element of the carrier of G
b * ((b ") * (((b ") * b) * ((((a ") * (G,b,(b "))) * a) * b))) is Element of the carrier of G
((((a ") * (b ")) * a) * (((b ") * (G,a,(b "))) * b)) * (b * ((b ") * (((b ") * b) * ((((a ") * (G,b,(b "))) * a) * b)))) is Element of the carrier of G
((((a ") * (b ")) * a) * (((b ") * (G,a,(b "))) * b)) * (((b ") * b) * ((((a ") * (G,b,(b "))) * a) * b)) is Element of the carrier of G
(G,a,(b ")) * b is Element of the carrier of G
(b ") * ((G,a,(b ")) * b) is Element of the carrier of G
(((a ") * (b ")) * a) * ((b ") * ((G,a,(b ")) * b)) is Element of the carrier of G
((((a ") * (b ")) * a) * ((b ") * ((G,a,(b ")) * b))) * (((b ") * b) * ((((a ") * (G,b,(b "))) * a) * b)) is Element of the carrier of G
(((a ") * (b ")) * a) * (b ") is Element of the carrier of G
((((a ") * (b ")) * a) * (b ")) * ((G,a,(b ")) * b) is Element of the carrier of G
(((((a ") * (b ")) * a) * (b ")) * ((G,a,(b ")) * b)) * (((b ") * b) * ((((a ") * (G,b,(b "))) * a) * b)) is Element of the carrier of G
((G,a,(b ")) * b) * (((b ") * b) * ((((a ") * (G,b,(b "))) * a) * b)) is Element of the carrier of G
((((a ") * (b ")) * a) * (b ")) * (((G,a,(b ")) * b) * (((b ") * b) * ((((a ") * (G,b,(b "))) * a) * b))) is Element of the carrier of G
((G,a,(b ")) * b) * ((b ") * b) is Element of the carrier of G
(((G,a,(b ")) * b) * ((b ") * b)) * ((((a ") * (G,b,(b "))) * a) * b) is Element of the carrier of G
((((a ") * (b ")) * a) * (b ")) * ((((G,a,(b ")) * b) * ((b ") * b)) * ((((a ") * (G,b,(b "))) * a) * b)) is Element of the carrier of G
((G,a,(b ")) * b) * (b ") is Element of the carrier of G
(((G,a,(b ")) * b) * (b ")) * b is Element of the carrier of G
((((G,a,(b ")) * b) * (b ")) * b) * ((((a ") * (G,b,(b "))) * a) * b) is Element of the carrier of G
((((a ") * (b ")) * a) * (b ")) * (((((G,a,(b ")) * b) * (b ")) * b) * ((((a ") * (G,b,(b "))) * a) * b)) is Element of the carrier of G
((((a ") * ((b ") ")) * a) * (b ")) * b is Element of the carrier of G
(((((a ") * ((b ") ")) * a) * (b ")) * b) * ((((a ") * (G,b,(b "))) * a) * b) is Element of the carrier of G
((((a ") * (b ")) * a) * (b ")) * ((((((a ") * ((b ") ")) * a) * (b ")) * b) * ((((a ") * (G,b,(b "))) * a) * b)) is Element of the carrier of G
(((a ") * ((b ") ")) * a) * ((((a ") * (G,b,(b "))) * a) * b) is Element of the carrier of G
((((a ") * (b ")) * a) * (b ")) * ((((a ") * ((b ") ")) * a) * ((((a ") * (G,b,(b "))) * a) * b)) is Element of the carrier of G
a * b is Element of the carrier of G
((a ") * (G,b,(b "))) * (a * b) is Element of the carrier of G
(((a ") * ((b ") ")) * a) * (((a ") * (G,b,(b "))) * (a * b)) is Element of the carrier of G
((((a ") * (b ")) * a) * (b ")) * ((((a ") * ((b ") ")) * a) * (((a ") * (G,b,(b "))) * (a * b))) is Element of the carrier of G
(G,b,(b ")) * (a * b) is Element of the carrier of G
(a ") * ((G,b,(b ")) * (a * b)) is Element of the carrier of G
(((a ") * ((b ") ")) * a) * ((a ") * ((G,b,(b ")) * (a * b))) is Element of the carrier of G
((((a ") * (b ")) * a) * (b ")) * ((((a ") * ((b ") ")) * a) * ((a ") * ((G,b,(b ")) * (a * b)))) is Element of the carrier of G
(((a ") * ((b ") ")) * a) * (a ") is Element of the carrier of G
((((a ") * ((b ") ")) * a) * (a ")) * ((G,b,(b ")) * (a * b)) is Element of the carrier of G
((((a ") * (b ")) * a) * (b ")) * (((((a ") * ((b ") ")) * a) * (a ")) * ((G,b,(b ")) * (a * b))) is Element of the carrier of G
((a ") * ((b ") ")) * ((G,b,(b ")) * (a * b)) is Element of the carrier of G
((((a ") * (b ")) * a) * (b ")) * (((a ") * ((b ") ")) * ((G,b,(b ")) * (a * b))) is Element of the carrier of G
((a ") * ((b ") ")) * (G,b,(b ")) is Element of the carrier of G
(((a ") * ((b ") ")) * (G,b,(b "))) * (a * b) is Element of the carrier of G
((((a ") * (b ")) * a) * (b ")) * ((((a ") * ((b ") ")) * (G,b,(b "))) * (a * b)) is Element of the carrier of G
((b ") ") * b is Element of the carrier of G
(((b ") ") * b) * (b ") is Element of the carrier of G
(b ") * ((((b ") ") * b) * (b ")) is Element of the carrier of G
((a ") * ((b ") ")) * ((b ") * ((((b ") ") * b) * (b "))) is Element of the carrier of G
(((a ") * ((b ") ")) * ((b ") * ((((b ") ") * b) * (b ")))) * (a * b) is Element of the carrier of G
((((a ") * (b ")) * a) * (b ")) * ((((a ") * ((b ") ")) * ((b ") * ((((b ") ") * b) * (b ")))) * (a * b)) is Element of the carrier of G
((b ") * ((((b ") ") * b) * (b "))) * (a * b) is Element of the carrier of G
((a ") * ((b ") ")) * (((b ") * ((((b ") ") * b) * (b "))) * (a * b)) is Element of the carrier of G
((((a ") * (b ")) * a) * (b ")) * (((a ") * ((b ") ")) * (((b ") * ((((b ") ") * b) * (b "))) * (a * b))) is Element of the carrier of G
((((b ") ") * b) * (b ")) * (a * b) is Element of the carrier of G
(b ") * (((((b ") ") * b) * (b ")) * (a * b)) is Element of the carrier of G
((a ") * ((b ") ")) * ((b ") * (((((b ") ") * b) * (b ")) * (a * b))) is Element of the carrier of G
((((a ") * (b ")) * a) * (b ")) * (((a ") * ((b ") ")) * ((b ") * (((((b ") ") * b) * (b ")) * (a * b)))) is Element of the carrier of G
((a ") * ((b ") ")) * (b ") is Element of the carrier of G
(((a ") * ((b ") ")) * (b ")) * (((((b ") ") * b) * (b ")) * (a * b)) is Element of the carrier of G
((((a ") * (b ")) * a) * (b ")) * ((((a ") * ((b ") ")) * (b ")) * (((((b ") ") * b) * (b ")) * (a * b))) is Element of the carrier of G
(a ") * (((((b ") ") * b) * (b ")) * (a * b)) is Element of the carrier of G
((((a ") * (b ")) * a) * (b ")) * ((a ") * (((((b ") ") * b) * (b ")) * (a * b))) is Element of the carrier of G
(a ") * ((((b ") ") * b) * (b ")) is Element of the carrier of G
((a ") * ((((b ") ") * b) * (b "))) * (a * b) is Element of the carrier of G
((((a ") * (b ")) * a) * (b ")) * (((a ") * ((((b ") ") * b) * (b "))) * (a * b)) is Element of the carrier of G
(((((a ") * (b ")) * a) * (b ")) * (((a ") * ((((b ") ") * b) * (b "))) * (a * b))) * (((((b ") * (a ")) * b) * (((b ") * (G,b,(a "))) * b)) * a) is Element of the carrier of G
(b ") * (((a ") * ((((b ") ") * b) * (b "))) * (a * b)) is Element of the carrier of G
(((a ") * (b ")) * a) * ((b ") * (((a ") * ((((b ") ") * b) * (b "))) * (a * b))) is Element of the carrier of G
((((a ") * (b ")) * a) * ((b ") * (((a ") * ((((b ") ") * b) * (b "))) * (a * b)))) * (((((b ") * (a ")) * b) * (((b ") * (G,b,(a "))) * b)) * a) is Element of the carrier of G
(b ") * ((a ") * (((((b ") ") * b) * (b ")) * (a * b))) is Element of the carrier of G
(((a ") * (b ")) * a) * ((b ") * ((a ") * (((((b ") ") * b) * (b ")) * (a * b)))) is Element of the carrier of G
((((a ") * (b ")) * a) * ((b ") * ((a ") * (((((b ") ") * b) * (b ")) * (a * b))))) * (((((b ") * (a ")) * b) * (((b ") * (G,b,(a "))) * b)) * a) is Element of the carrier of G
(((((a ") * (b ")) * a) * (b ")) * ((a ") * (((((b ") ") * b) * (b ")) * (a * b)))) * (((((b ") * (a ")) * b) * (((b ") * (G,b,(a "))) * b)) * a) is Element of the carrier of G
b * (b ") is Element of the carrier of G
((b ") ") * (b * (b ")) is Element of the carrier of G
(((b ") ") * (b * (b "))) * (a * b) is Element of the carrier of G
(a ") * ((((b ") ") * (b * (b "))) * (a * b)) is Element of the carrier of G
((((a ") * (b ")) * a) * (b ")) * ((a ") * ((((b ") ") * (b * (b "))) * (a * b))) is Element of the carrier of G
(((((a ") * (b ")) * a) * (b ")) * ((a ") * ((((b ") ") * (b * (b "))) * (a * b)))) * (((((b ") * (a ")) * b) * (((b ") * (G,b,(a "))) * b)) * a) is Element of the carrier of G
(b * (b ")) * (a * b) is Element of the carrier of G
((b ") ") * ((b * (b ")) * (a * b)) is Element of the carrier of G
(a ") * (((b ") ") * ((b * (b ")) * (a * b))) is Element of the carrier of G
((((a ") * (b ")) * a) * (b ")) * ((a ") * (((b ") ") * ((b * (b ")) * (a * b)))) is Element of the carrier of G
(((((a ") * (b ")) * a) * (b ")) * ((a ") * (((b ") ") * ((b * (b ")) * (a * b))))) * (((((b ") * (a ")) * b) * (((b ") * (G,b,(a "))) * b)) * a) is Element of the carrier of G
((((a ") * (b ")) * a) * (b ")) * (a ") is Element of the carrier of G
(((((a ") * (b ")) * a) * (b ")) * (a ")) * (((b ") ") * ((b * (b ")) * (a * b))) is Element of the carrier of G
((((((a ") * (b ")) * a) * (b ")) * (a ")) * (((b ") ") * ((b * (b ")) * (a * b)))) * (((((b ") * (a ")) * b) * (((b ") * (G,b,(a "))) * b)) * a) is Element of the carrier of G
(((((a ") * (b ")) * a) * (b ")) * (a ")) * ((b ") ") is Element of the carrier of G
((((((a ") * (b ")) * a) * (b ")) * (a ")) * ((b ") ")) * ((b * (b ")) * (a * b)) is Element of the carrier of G
(((((((a ") * (b ")) * a) * (b ")) * (a ")) * ((b ") ")) * ((b * (b ")) * (a * b))) * (((((b ") * (a ")) * b) * (((b ") * (G,b,(a "))) * b)) * a) is Element of the carrier of G
(b ") * (a * b) is Element of the carrier of G
b * ((b ") * (a * b)) is Element of the carrier of G
((((((a ") * (b ")) * a) * (b ")) * (a ")) * ((b ") ")) * (b * ((b ") * (a * b))) is Element of the carrier of G
(((((((a ") * (b ")) * a) * (b ")) * (a ")) * ((b ") ")) * (b * ((b ") * (a * b)))) * (((((b ") * (a ")) * b) * (((b ") * (G,b,(a "))) * b)) * a) is Element of the carrier of G
((((((a ") * (b ")) * a) * (b ")) * (a ")) * ((b ") ")) * b is Element of the carrier of G
(((((((a ") * (b ")) * a) * (b ")) * (a ")) * ((b ") ")) * b) * ((b ") * (a * b)) is Element of the carrier of G
((((((((a ") * (b ")) * a) * (b ")) * (a ")) * ((b ") ")) * b) * ((b ") * (a * b))) * (((((b ") * (a ")) * b) * (((b ") * (G,b,(a "))) * b)) * a) is Element of the carrier of G
(((((((a ") * (b ")) * a) * (b ")) * (a ")) * ((b ") ")) * b) * (b ") is Element of the carrier of G
((((((((a ") * (b ")) * a) * (b ")) * (a ")) * ((b ") ")) * b) * (b ")) * (a * b) is Element of the carrier of G
(((((((((a ") * (b ")) * a) * (b ")) * (a ")) * ((b ") ")) * b) * (b ")) * (a * b)) * (((((b ") * (a ")) * b) * (((b ") * (G,b,(a "))) * b)) * a) is Element of the carrier of G
(a * b) * (((((b ") * (a ")) * b) * (((b ") * (G,b,(a "))) * b)) * a) is Element of the carrier of G
((((((((a ") * (b ")) * a) * (b ")) * (a ")) * ((b ") ")) * b) * (b ")) * ((a * b) * (((((b ") * (a ")) * b) * (((b ") * (G,b,(a "))) * b)) * a)) is Element of the carrier of G
(((b ") * (G,b,(a "))) * b) * a is Element of the carrier of G
(((b ") * (a ")) * b) * ((((b ") * (G,b,(a "))) * b) * a) is Element of the carrier of G
(a * b) * ((((b ") * (a ")) * b) * ((((b ") * (G,b,(a "))) * b) * a)) is Element of the carrier of G
((((((((a ") * (b ")) * a) * (b ")) * (a ")) * ((b ") ")) * b) * (b ")) * ((a * b) * ((((b ") * (a ")) * b) * ((((b ") * (G,b,(a "))) * b) * a))) is Element of the carrier of G
b * ((((b ") * (G,b,(a "))) * b) * a) is Element of the carrier of G
((b ") * (a ")) * (b * ((((b ") * (G,b,(a "))) * b) * a)) is Element of the carrier of G
(a * b) * (((b ") * (a ")) * (b * ((((b ") * (G,b,(a "))) * b) * a))) is Element of the carrier of G
((((((((a ") * (b ")) * a) * (b ")) * (a ")) * ((b ") ")) * b) * (b ")) * ((a * b) * (((b ") * (a ")) * (b * ((((b ") * (G,b,(a "))) * b) * a)))) is Element of the carrier of G
(a * b) * ((b ") * (a ")) is Element of the carrier of G
((a * b) * ((b ") * (a "))) * (b * ((((b ") * (G,b,(a "))) * b) * a)) is Element of the carrier of G
((((((((a ") * (b ")) * a) * (b ")) * (a ")) * ((b ") ")) * b) * (b ")) * (((a * b) * ((b ") * (a "))) * (b * ((((b ") * (G,b,(a "))) * b) * a))) is Element of the carrier of G
(a * b) " is Element of the carrier of G
(a * b) * ((a * b) ") is Element of the carrier of G
((a * b) * ((a * b) ")) * (b * ((((b ") * (G,b,(a "))) * b) * a)) is Element of the carrier of G
((((((((a ") * (b ")) * a) * (b ")) * (a ")) * ((b ") ")) * b) * (b ")) * (((a * b) * ((a * b) ")) * (b * ((((b ") * (G,b,(a "))) * b) * a))) is Element of the carrier of G
(1_ G) * (b * ((((b ") * (G,b,(a "))) * b) * a)) is Element of the carrier of G
((((((((a ") * (b ")) * a) * (b ")) * (a ")) * ((b ") ")) * b) * (b ")) * ((1_ G) * (b * ((((b ") * (G,b,(a "))) * b) * a))) is Element of the carrier of G
((((((((a ") * (b ")) * a) * (b ")) * (a ")) * ((b ") ")) * b) * (b ")) * (b * ((((b ") * (G,b,(a "))) * b) * a)) is Element of the carrier of G
((((((((a ") * (b ")) * a) * (b ")) * (a ")) * ((b ") ")) * b) * (b ")) * b is Element of the carrier of G
(((((((((a ") * (b ")) * a) * (b ")) * (a ")) * ((b ") ")) * b) * (b ")) * b) * ((((b ") * (G,b,(a "))) * b) * a) is Element of the carrier of G
(((((((a ") * (b ")) * a) * (b ")) * (a ")) * ((b ") ")) * b) * ((((b ") * (G,b,(a "))) * b) * a) is Element of the carrier of G
b * a is Element of the carrier of G
((b ") * (G,b,(a "))) * (b * a) is Element of the carrier of G
(((((((a ") * (b ")) * a) * (b ")) * (a ")) * ((b ") ")) * b) * (((b ") * (G,b,(a "))) * (b * a)) is Element of the carrier of G
(G,b,(a ")) * (b * a) is Element of the carrier of G
(b ") * ((G,b,(a ")) * (b * a)) is Element of the carrier of G
(((((((a ") * (b ")) * a) * (b ")) * (a ")) * ((b ") ")) * b) * ((b ") * ((G,b,(a ")) * (b * a))) is Element of the carrier of G
(((((((a ") * (b ")) * a) * (b ")) * (a ")) * ((b ") ")) * b) * (b ") is Element of the carrier of G
((((((((a ") * (b ")) * a) * (b ")) * (a ")) * ((b ") ")) * b) * (b ")) * ((G,b,(a ")) * (b * a)) is Element of the carrier of G
((((((a ") * (b ")) * a) * (b ")) * (a ")) * ((b ") ")) * ((G,b,(a ")) * (b * a)) is Element of the carrier of G
((a ") ") * b is Element of the carrier of G
(((a ") ") * b) * (a ") is Element of the carrier of G
(b ") * ((((a ") ") * b) * (a ")) is Element of the carrier of G
((b ") * ((((a ") ") * b) * (a "))) * (b * a) is Element of the carrier of G
((((((a ") * (b ")) * a) * (b ")) * (a ")) * ((b ") ")) * (((b ") * ((((a ") ") * b) * (a "))) * (b * a)) is Element of the carrier of G
((((a ") ") * b) * (a ")) * (b * a) is Element of the carrier of G
(b ") * (((((a ") ") * b) * (a ")) * (b * a)) is Element of the carrier of G
((((((a ") * (b ")) * a) * (b ")) * (a ")) * ((b ") ")) * ((b ") * (((((a ") ") * b) * (a ")) * (b * a))) is Element of the carrier of G
((((((a ") * (b ")) * a) * (b ")) * (a ")) * ((b ") ")) * (b ") is Element of the carrier of G
(((((((a ") * (b ")) * a) * (b ")) * (a ")) * ((b ") ")) * (b ")) * (((((a ") ") * b) * (a ")) * (b * a)) is Element of the carrier of G
(((((a ") * (b ")) * a) * (b ")) * (a ")) * (((((a ") ") * b) * (a ")) * (b * a)) is Element of the carrier of G
b * (a ") is Element of the carrier of G
((a ") ") * (b * (a ")) is Element of the carrier of G
(((a ") ") * (b * (a "))) * (b * a) is Element of the carrier of G
(((((a ") * (b ")) * a) * (b ")) * (a ")) * ((((a ") ") * (b * (a "))) * (b * a)) is Element of the carrier of G
(b * (a ")) * (b * a) is Element of the carrier of G
((a ") ") * ((b * (a ")) * (b * a)) is Element of the carrier of G
(((((a ") * (b ")) * a) * (b ")) * (a ")) * (((a ") ") * ((b * (a ")) * (b * a))) is Element of the carrier of G
(((((a ") * (b ")) * a) * (b ")) * (a ")) * ((a ") ") is Element of the carrier of G
((((((a ") * (b ")) * a) * (b ")) * (a ")) * ((a ") ")) * ((b * (a ")) * (b * a)) is Element of the carrier of G
((((a ") * (b ")) * a) * (b ")) * ((b * (a ")) * (b * a)) is Element of the carrier of G
((((a ") * (b ")) * a) * (b ")) * (b * (a ")) is Element of the carrier of G
(((((a ") * (b ")) * a) * (b ")) * (b * (a "))) * (b * a) is Element of the carrier of G
a * (b ") is Element of the carrier of G
((a ") * (b ")) * (a * (b ")) is Element of the carrier of G
(((a ") * (b ")) * (a * (b "))) * (b * (a ")) is Element of the carrier of G
((((a ") * (b ")) * (a * (b "))) * (b * (a "))) * (b * a) is Element of the carrier of G
((b ") ") * (a ") is Element of the carrier of G
(((a ") * (b ")) * (a * (b "))) * (((b ") ") * (a ")) is Element of the carrier of G
((((a ") * (b ")) * (a * (b "))) * (((b ") ") * (a "))) * (b * a) is Element of the carrier of G
(a * (b ")) " is Element of the carrier of G
(((a ") * (b ")) * (a * (b "))) * ((a * (b ")) ") is Element of the carrier of G
((((a ") * (b ")) * (a * (b "))) * ((a * (b ")) ")) * (b * a) is Element of the carrier of G
(a * (b ")) * ((a * (b ")) ") is Element of the carrier of G
((a ") * (b ")) * ((a * (b ")) * ((a * (b ")) ")) is Element of the carrier of G
(((a ") * (b ")) * ((a * (b ")) * ((a * (b ")) "))) * (b * a) is Element of the carrier of G
((a ") * (b ")) * (1_ G) is Element of the carrier of G
(((a ") * (b ")) * (1_ G)) * (b * a) is Element of the carrier of G
((a ") * (b ")) * (b * a) is Element of the carrier of G
(b * a) " is Element of the carrier of G
((b * a) ") * (b * a) is Element of the carrier of G
G is non empty unital Group-like associative L11()
the carrier of G is non empty set
K19( the carrier of G) is non empty set
a is Element of K19( the carrier of G)
b is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in a & b₂ in b ) } is set
{ H₁(b₁,b₂) where b₁, b₂ is Element of the carrier of G : S₁[b₁,b₂] } is set
a is non empty unital Group-like associative L11()
the carrier of a is non empty set
K19( the carrier of a) is non empty set
d is non empty unital Group-like associative L11()
the carrier of d is non empty set
K19( the carrier of d) is non empty set
G is set
b is Element of K19( the carrier of a)
b is Element of K19( the carrier of a)
(a,b,b) is Element of K19( the carrier of a)
{ (a,b₁,b₂) where b₁, b₂ is Element of the carrier of a : ( b₁ in b & b₂ in b ) } is set
c is set
e is Element of the carrier of d
c is Element of the carrier of d
(d,e,c) is Element of the carrier of d
e " is Element of the carrier of d
c " is Element of the carrier of d
(e ") * (c ") is Element of the carrier of d
((e ") * (c ")) * e is Element of the carrier of d
(((e ") * (c ")) * e) * c is Element of the carrier of d
e is Element of K19( the carrier of d)
d is Element of K19( the carrier of d)
(d,e,d) is Element of K19( the carrier of d)
{ (d,b₁,b₂) where b₁, b₂ is Element of the carrier of d : ( b₁ in e & b₂ in d ) } is set
G is non empty unital Group-like associative L11()
the carrier of G is non empty set
K19( the carrier of G) is non empty set
{} the carrier of G is functional empty proper V18() V19() V20() V22() V23() V24() V25() V26() finite cardinal {} -element FinSequence-membered V50() integer Element of K19( the carrier of G)
a is Element of K19( the carrier of G)
(G,({} the carrier of G),a) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in {} the carrier of G & b₂ in a ) } is set
(G,a,({} the carrier of G)) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in a & b₂ in {} the carrier of G ) } is set
b is set
b is Element of the carrier of G
c is Element of the carrier of G
(G,b,c) is Element of the carrier of G
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
((b ") * (c ")) * b is Element of the carrier of G
(((b ") * (c ")) * b) * c is Element of the carrier of G
b is set
b is Element of the carrier of G
c is Element of the carrier of G
(G,b,c) is Element of the carrier of G
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
((b ") * (c ")) * b is Element of the carrier of G
(((b ") * (c ")) * b) * c is Element of the carrier of G
G is non empty unital Group-like associative L11()
the carrier of G is non empty set
a is Element of the carrier of G
{a} is non empty V12() 1 -element Element of K19( the carrier of G)
K19( the carrier of G) is non empty set
b is Element of the carrier of G
{b} is non empty V12() 1 -element Element of K19( the carrier of G)
(G,{a},{b}) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in {a} & b₂ in {b} ) } is set
(G,a,b) is Element of the carrier of G
a " is Element of the carrier of G
b " is Element of the carrier of G
(a ") * (b ") is Element of the carrier of G
((a ") * (b ")) * a is Element of the carrier of G
(((a ") * (b ")) * a) * b is Element of the carrier of G
{(G,a,b)} is non empty V12() 1 -element Element of K19( the carrier of G)
b is set
c is Element of the carrier of G
d is Element of the carrier of G
(G,c,d) is Element of the carrier of G
c " is Element of the carrier of G
d " is Element of the carrier of G
(c ") * (d ") is Element of the carrier of G
((c ") * (d ")) * c is Element of the carrier of G
(((c ") * (d ")) * c) * d is Element of the carrier of G
b is set
G is non empty unital Group-like associative L11()
the carrier of G is non empty set
K19( the carrier of G) is non empty set
a is Element of K19( the carrier of G)
b is Element of K19( the carrier of G)
b is Element of K19( the carrier of G)
(G,a,b) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in a & b₂ in b ) } is set
c is Element of K19( the carrier of G)
(G,b,c) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in b & b₂ in c ) } is set
d is set
e is Element of the carrier of G
d is Element of the carrier of G
(G,e,d) is Element of the carrier of G
e " is Element of the carrier of G
d " is Element of the carrier of G
(e ") * (d ") is Element of the carrier of G
((e ") * (d ")) * e is Element of the carrier of G
(((e ") * (d ")) * e) * d is Element of the carrier of G
G is non empty unital Group-like associative L11()
the carrier of G is non empty set
K19( 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 V12() 1 -element Element of K19( the carrier of G)
a is Element of K19( the carrier of G)
b is Element of K19( the carrier of G)
(G,a,b) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in a & b₂ in b ) } is set
b is set
c is Element of the carrier of G
d is Element of the carrier of G
(G,c,d) is Element of the carrier of G
c " is Element of the carrier of G
d " is Element of the carrier of G
(c ") * (d ") is Element of the carrier of G
((c ") * (d ")) * c is Element of the carrier of G
(((c ") * (d ")) * c) * d is Element of the carrier of G
(d ") * c is Element of the carrier of G
(c ") * ((d ") * c) is Element of the carrier of G
((c ") * ((d ") * c)) * d is Element of the carrier of G
c * (d ") is Element of the carrier of G
(c ") * (c * (d ")) is Element of the carrier of G
((c ") * (c * (d "))) * d is Element of the carrier of G
(d ") * d is Element of the carrier of G
the Element of b is Element of b
the Element of a is Element of a
d is set
d is Element of the carrier of G
e is Element of the carrier of G
(G,d,e) is Element of the carrier of G
d " is Element of the carrier of G
e " is Element of the carrier of G
(d ") * (e ") is Element of the carrier of G
((d ") * (e ")) * d is Element of the carrier of G
(((d ") * (e ")) * d) * e is Element of the carrier of G
(e ") * d is Element of the carrier of G
(d ") * ((e ") * d) is Element of the carrier of G
((d ") * ((e ") * d)) * e is Element of the carrier of G
d * (e ") is Element of the carrier of G
(d ") * (d * (e ")) is Element of the carrier of G
((d ") * (d * (e "))) * e is Element of the carrier of G
(e ") * e is Element of the carrier of G
a is Element of the carrier of G
b is Element of the carrier of G
a * b is Element of the carrier of G
b * a is Element of the carrier of G
{a} is non empty V12() 1 -element Element of K19( the carrier of G)
{b} is non empty V12() 1 -element Element of K19( the carrier of G)
(G,a,b) is Element of the carrier of G
a " is Element of the carrier of G
b " is Element of the carrier of G
(a ") * (b ") is Element of the carrier of G
((a ") * (b ")) * a is Element of the carrier of G
(((a ") * (b ")) * a) * b is Element of the carrier of G
(G,{a},{b}) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in {a} & b₂ in {b} ) } is set
((a ") * (b ")) * (a * b) is Element of the carrier of G
(b * a) " is Element of the carrier of G
((b * a) ") * (a * b) is Element of the carrier of G
((b * a) ") " is Element of the carrier of G
G is non empty unital Group-like associative L11()
a is non empty unital Group-like associative Subgroup of G
carr a is Element of K19( the carrier of G)
the carrier of G is non empty set
K19( the carrier of G) is non empty set
the carrier of a is non empty set
b is non empty unital Group-like associative Subgroup of G
carr b is Element of K19( the carrier of G)
the carrier of b is non empty set
(G,(carr a),(carr b)) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr a & b₂ in carr b ) } is set
G is set
a is non empty unital Group-like associative L11()
the carrier of a is non empty set
b is non empty unital Group-like associative Subgroup of a
b is non empty unital Group-like associative Subgroup of a
(a,b,b) is Element of K19( the carrier of a)
K19( the carrier of a) is non empty set
carr b is Element of K19( the carrier of a)
the carrier of b is non empty set
carr b is Element of K19( the carrier of a)
the carrier of b is non empty set
(a,(carr b),(carr b)) is Element of K19( the carrier of a)
{ (a,b₁,b₂) where b₁, b₂ is Element of the carrier of a : ( b₁ in carr b & b₂ in carr b ) } is set
c is Element of the carrier of a
d is Element of the carrier of a
(a,c,d) is Element of the carrier of a
c " is Element of the carrier of a
d " is Element of the carrier of a
(c ") * (d ") is Element of the carrier of a
((c ") * (d ")) * c is Element of the carrier of a
(((c ") * (d ")) * c) * d is Element of the carrier of a
c is Element of the carrier of a
d is Element of the carrier of a
(a,c,d) is Element of the carrier of a
c " is Element of the carrier of a
d " is Element of the carrier of a
(c ") * (d ") is Element of the carrier of a
((c ") * (d ")) * c is Element of the carrier of a
(((c ") * (d ")) * c) * d is Element of the carrier of a
G is non empty unital Group-like associative L11()
1_ G is non being_of_order_0 Element of the carrier of G
the carrier of G is non empty set
a is non empty unital Group-like associative Subgroup of G
b is non empty unital Group-like associative Subgroup of G
(G,a,b) is Element of K19( the carrier of G)
K19( the carrier of G) is non empty set
carr a is Element of K19( the carrier of G)
the carrier of a is non empty set
carr b is Element of K19( the carrier of G)
the carrier of b is non empty set
(G,(carr a),(carr b)) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr a & b₂ in carr b ) } is set
(G,(1_ G),(1_ G)) is Element of the carrier of G
(1_ G) " is Element of the carrier of G
((1_ G) ") * ((1_ G) ") is Element of the carrier of G
(((1_ G) ") * ((1_ G) ")) * (1_ G) is Element of the carrier of G
((((1_ G) ") * ((1_ G) ")) * (1_ G)) * (1_ G) is Element of the carrier of G
G is non empty unital Group-like associative L11()
(1). G is non empty finite strict unital Group-like associative Subgroup of G
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 V12() 1 -element Element of K19( the carrier of G)
K19( the carrier of G) is non empty set
a is non empty unital Group-like associative Subgroup of G
(G,((1). G),a) is Element of K19( the carrier of G)
carr ((1). G) is Element of K19( the carrier of G)
the carrier of ((1). G) is non empty finite set
carr a is Element of K19( the carrier of G)
the carrier of a is non empty set
(G,(carr ((1). G)),(carr a)) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr ((1). G) & b₂ in carr a ) } is set
(G,a,((1). G)) is Element of K19( the carrier of G)
(G,(carr a),(carr ((1). G))) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr a & b₂ in carr ((1). G) ) } is set
b is set
b is Element of the carrier of G
c is Element of the carrier of G
(G,b,c) is Element of the carrier of G
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
((b ") * (c ")) * b is Element of the carrier of G
(((b ") * (c ")) * b) * c is Element of the carrier of G
b is set
b is Element of the carrier of G
c is Element of the carrier of G
(G,b,c) is Element of the carrier of G
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
((b ") * (c ")) * b is Element of the carrier of G
(((b ") * (c ")) * b) * c is Element of the carrier of G
G is non empty unital Group-like associative L11()
a is non empty unital Group-like associative Subgroup of G
b is non empty strict unital Group-like associative normal Subgroup of G
(G,a,b) is Element of K19( the carrier of G)
the carrier of G is non empty set
K19( the carrier of G) is non empty set
carr a is Element of K19( the carrier of G)
the carrier of a is non empty set
carr b is Element of K19( the carrier of G)
the carrier of b is non empty set
(G,(carr a),(carr b)) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr a & b₂ in carr b ) } is set
(G,b,a) is Element of K19( the carrier of G)
(G,(carr b),(carr a)) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr b & b₂ in carr a ) } is set
b is set
c is Element of the carrier of G
d is Element of the carrier of G
(G,c,d) is Element of the carrier of G
c " is Element of the carrier of G
d " is Element of the carrier of G
(c ") * (d ") is Element of the carrier of G
((c ") * (d ")) * c is Element of the carrier of G
(((c ") * (d ")) * c) * d is Element of the carrier of G
b |^ c is non empty strict unital Group-like associative Subgroup of G
(d ") |^ c is Element of the carrier of G
b is set
c is Element of the carrier of G
d is Element of the carrier of G
(G,c,d) is Element of the carrier of G
c " is Element of the carrier of G
d " is Element of the carrier of G
(c ") * (d ") is Element of the carrier of G
((c ") * (d ")) * c is Element of the carrier of G
(((c ") * (d ")) * c) * d is Element of the carrier of G
b |^ d is non empty strict unital Group-like associative Subgroup of G
c |^ d is Element of the carrier of G
(d ") * c is Element of the carrier of G
((d ") * c) * d is Element of the carrier of G
(c ") * (c |^ d) is Element of the carrier of G
G is non empty unital Group-like associative L11()
a is non empty unital Group-like associative Subgroup of G
b is non empty unital Group-like associative Subgroup of G
b is non empty unital Group-like associative Subgroup of G
(G,a,b) is Element of K19( the carrier of G)
the carrier of G is non empty set
K19( the carrier of G) is non empty set
carr a is Element of K19( the carrier of G)
the carrier of a is non empty set
carr b is Element of K19( the carrier of G)
the carrier of b is non empty set
(G,(carr a),(carr b)) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr a & b₂ in carr b ) } is set
c is non empty unital Group-like associative Subgroup of G
(G,b,c) is Element of K19( the carrier of G)
carr b is Element of K19( the carrier of G)
the carrier of b is non empty set
carr c is Element of K19( the carrier of G)
the carrier of c is non empty set
(G,(carr b),(carr c)) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr b & b₂ in carr c ) } is set
G is non empty unital Group-like associative L11()
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 V12() 1 -element Element of K19( the carrier of G)
K19( the carrier of G) is non empty set
a is non empty unital Group-like associative Subgroup of G
b is non empty unital Group-like associative Subgroup of G
(G,a,b) is Element of K19( the carrier of G)
carr a is Element of K19( the carrier of G)
the carrier of a is non empty set
carr b is Element of K19( the carrier of G)
the carrier of b is non empty set
(G,(carr a),(carr b)) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr a & b₂ in carr b ) } is set
a is Element of the carrier of G
b is Element of the carrier of G
a * b is Element of the carrier of G
b * a is Element of the carrier of G
{b} is non empty V12() 1 -element Element of K19( the carrier of G)
gr {b} is non empty strict unital Group-like associative Subgroup of G
{a} is non empty V12() 1 -element Element of K19( the carrier of G)
gr {a} is non empty strict unital Group-like associative Subgroup of G
(G,a,b) is Element of the carrier of G
a " is Element of the carrier of G
b " is Element of the carrier of G
(a ") * (b ") is Element of the carrier of G
((a ") * (b ")) * a is Element of the carrier of G
(((a ") * (b ")) * a) * b is Element of the carrier of G
(G,(gr {a}),(gr {b})) is Element of K19( the carrier of G)
carr (gr {a}) is Element of K19( the carrier of G)
the carrier of (gr {a}) is non empty set
carr (gr {b}) is Element of K19( the carrier of G)
the carrier of (gr {b}) is non empty set
(G,(carr (gr {a})),(carr (gr {b}))) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr (gr {a}) & b₂ in carr (gr {b}) ) } is set
G is non empty unital Group-like associative L11()
(Omega). G is non empty strict unital Group-like associative Subgroup of G
the carrier of G is non empty set
the U8 of G is V1() V4(K20( the carrier of G, the carrier of G)) V5( the carrier of G) Function-like V32(K20( the carrier of G, the carrier of G), the carrier of G) Element of K19(K20(K20( the carrier of G, the carrier of G), the carrier of G))
K20( the carrier of G, the carrier of G) is non empty set
K20(K20( the carrier of G, the carrier of G), the carrier of G) is non empty set
K19(K20(K20( the carrier of G, the carrier of G), the carrier of G)) is non empty set
G11( the carrier of G, the U8 of G) is strict L11()
(G,((Omega). G),((Omega). G)) is Element of K19( the carrier of G)
K19( the carrier of G) is non empty set
carr ((Omega). G) is Element of K19( the carrier of G)
the carrier of ((Omega). G) is non empty set
(G,(carr ((Omega). G)),(carr ((Omega). G))) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr ((Omega). G) & b₂ in carr ((Omega). G) ) } is set
G is set
a is non empty unital Group-like associative L11()
(a) is Element of K19( the carrier of a)
the carrier of a is non empty set
K19( the carrier of a) is non empty set
(Omega). a is non empty strict unital Group-like associative Subgroup of a
the U8 of a is V1() V4(K20( the carrier of a, the carrier of a)) V5( the carrier of a) Function-like V32(K20( the carrier of a, the carrier of a), the carrier of a) Element of K19(K20(K20( the carrier of a, the carrier of a), the carrier of a))
K20( the carrier of a, the carrier of a) is non empty set
K20(K20( the carrier of a, the carrier of a), the carrier of a) is non empty set
K19(K20(K20( the carrier of a, the carrier of a), the carrier of a)) is non empty set
G11( the carrier of a, the U8 of a) is strict L11()
(a,((Omega). a),((Omega). a)) is Element of K19( the carrier of a)
carr ((Omega). a) is Element of K19( the carrier of a)
the carrier of ((Omega). a) is non empty set
(a,(carr ((Omega). a)),(carr ((Omega). a))) is Element of K19( the carrier of a)
{ (a,b₁,b₂) where b₁, b₂ is Element of the carrier of a : ( b₁ in carr ((Omega). a) & b₂ in carr ((Omega). a) ) } is set
b is Element of the carrier of a
b is Element of the carrier of a
(a,b,b) is Element of the carrier of a
b " is Element of the carrier of a
b " is Element of the carrier of a
(b ") * (b ") is Element of the carrier of a
((b ") * (b ")) * b is Element of the carrier of a
(((b ") * (b ")) * b) * b is Element of the carrier of a
b is Element of the carrier of a
b is Element of the carrier of a
(a,b,b) is Element of the carrier of a
b " is Element of the carrier of a
b " is Element of the carrier of a
(b ") * (b ") is Element of the carrier of a
((b ") * (b ")) * b is Element of the carrier of a
(((b ") * (b ")) * b) * b is Element of the carrier of a
G is non empty unital Group-like associative L11()
(G) is Element of K19( the carrier of G)
the carrier of G is non empty set
K19( the carrier of G) is non empty set
(Omega). G is non empty strict unital Group-like associative Subgroup of G
the U8 of G is V1() V4(K20( the carrier of G, the carrier of G)) V5( the carrier of G) Function-like V32(K20( the carrier of G, the carrier of G), the carrier of G) Element of K19(K20(K20( the carrier of G, the carrier of G), the carrier of G))
K20( the carrier of G, the carrier of G) is non empty set
K20(K20( the carrier of G, the carrier of G), the carrier of G) is non empty set
K19(K20(K20( the carrier of G, the carrier of G), the carrier of G)) is non empty set
G11( the carrier of G, the U8 of G) is strict L11()
(G,((Omega). G),((Omega). G)) is Element of K19( the carrier of G)
carr ((Omega). G) is Element of K19( the carrier of G)
the carrier of ((Omega). G) is non empty set
(G,(carr ((Omega). G)),(carr ((Omega). G))) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr ((Omega). G) & b₂ in carr ((Omega). G) ) } is set
1_ G is non being_of_order_0 Element of the carrier of G
{(1_ G)} is non empty V12() 1 -element Element of K19( the carrier of G)
a is Element of the carrier of G
b is Element of the carrier of G
a * b is Element of the carrier of G
b * a is Element of the carrier of G
(G,a,b) is Element of the carrier of G
a " is Element of the carrier of G
b " is Element of the carrier of G
(a ") * (b ") is Element of the carrier of G
((a ") * (b ")) * a is Element of the carrier of G
(((a ") * (b ")) * a) * b is Element of the carrier of G
G is non empty unital Group-like associative L11()
the carrier of G is non empty set
K19( the carrier of G) is non empty set
a is Element of K19( the carrier of G)
b is Element of K19( the carrier of G)
(G,a,b) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in a & b₂ in b ) } is set
gr (G,a,b) is non empty strict unital Group-like associative Subgroup of G
G is non empty unital Group-like associative L11()
the carrier of G is non empty set
K19( the carrier of G) is non empty set
a is Element of the carrier of G
b is Element of the carrier of G
(G,a,b) is Element of the carrier of G
a " is Element of the carrier of G
b " is Element of the carrier of G
(a ") * (b ") is Element of the carrier of G
((a ") * (b ")) * a is Element of the carrier of G
(((a ") * (b ")) * a) * b is Element of the carrier of G
b is Element of K19( the carrier of G)
c is Element of K19( the carrier of G)
(G,b,c) is non empty strict unital Group-like associative Subgroup of G
(G,b,c) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in b & b₂ in c ) } is set
gr (G,b,c) is non empty strict unital Group-like associative Subgroup of G
G is set
a is non empty unital Group-like associative L11()
the carrier of a is non empty set
K19( the carrier of a) is non empty set
b is Element of K19( the carrier of a)
b is Element of K19( the carrier of a)
(a,b,b) is non empty strict unital Group-like associative Subgroup of a
(a,b,b) is Element of K19( the carrier of a)
{ (a,b₁,b₂) where b₁, b₂ is Element of the carrier of a : ( b₁ in b & b₂ in b ) } is set
gr (a,b,b) is non empty strict unital Group-like associative Subgroup of a
c is Element of the carrier of a
c is V1() V4( NAT ) V5( the carrier of a) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a
len c is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
d is V1() V4( NAT ) V5( INT ) Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
len d is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
rng c is set
c |^ d is V1() V4( NAT ) V5( the carrier of a) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a
Product (c |^ d) is Element of the carrier of a
the U8 of a is V1() V4(K20( the carrier of a, the carrier of a)) V5( the carrier of a) Function-like V32(K20( the carrier of a, the carrier of a), the carrier of a) Element of K19(K20(K20( the carrier of a, the carrier of a), the carrier of a))
K20( the carrier of a, the carrier of a) is non empty set
K20(K20( the carrier of a, the carrier of a), the carrier of a) is non empty set
K19(K20(K20( the carrier of a, the carrier of a), the carrier of a)) is non empty set
K173( the carrier of a,(c |^ d), the U8 of a) is Element of the carrier of a
G is non empty unital Group-like associative L11()
the carrier of G is non empty set
K19( the carrier of G) is non empty set
a is Element of K19( the carrier of G)
b is Element of K19( the carrier of G)
b is Element of K19( the carrier of G)
c is Element of K19( the carrier of G)
(G,a,b) is non empty strict unital Group-like associative Subgroup of G
(G,a,b) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in a & b₂ in b ) } is set
gr (G,a,b) is non empty strict unital Group-like associative Subgroup of G
(G,b,c) is non empty strict unital Group-like associative Subgroup of G
(G,b,c) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in b & b₂ in c ) } is set
gr (G,b,c) is non empty strict unital Group-like associative Subgroup of G
G is non empty unital Group-like associative L11()
a is non empty unital Group-like associative Subgroup of G
carr a is Element of K19( the carrier of G)
the carrier of G is non empty set
K19( the carrier of G) is non empty set
the carrier of a is non empty set
b is non empty unital Group-like associative Subgroup of G
carr b is Element of K19( the carrier of G)
the carrier of b is non empty set
(G,(carr a),(carr b)) is non empty strict unital Group-like associative Subgroup of G
(G,(carr a),(carr b)) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr a & b₂ in carr b ) } is set
gr (G,(carr a),(carr b)) is non empty strict unital Group-like associative Subgroup of G
G is non empty unital Group-like associative L11()
a is non empty unital Group-like associative Subgroup of G
b is non empty unital Group-like associative Subgroup of G
(G,a,b) is non empty strict unital Group-like associative Subgroup of G
carr a is Element of K19( the carrier of G)
the carrier of G is non empty set
K19( the carrier of G) is non empty set
the carrier of a is non empty set
carr b is Element of K19( the carrier of G)
the carrier of b is non empty set
(G,(carr a),(carr b)) is non empty strict unital Group-like associative Subgroup of G
(G,(carr a),(carr b)) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr a & b₂ in carr b ) } is set
gr (G,(carr a),(carr b)) is non empty strict unital Group-like associative Subgroup of G
(G,a,b) is Element of K19( the carrier of G)
gr (G,a,b) is non empty strict unital Group-like associative Subgroup of G
a is non empty unital Group-like associative L11()
d is non empty unital Group-like associative L11()
the carrier of d is non empty set
b is non empty unital Group-like associative Subgroup of a
b is non empty unital Group-like associative Subgroup of a
(a,b,b) is non empty strict unital Group-like associative Subgroup of a
carr b is Element of K19( the carrier of a)
the carrier of a is non empty set
K19( the carrier of a) is non empty set
the carrier of b is non empty set
carr b is Element of K19( the carrier of a)
the carrier of b is non empty set
(a,(carr b),(carr b)) is non empty strict unital Group-like associative Subgroup of a
(a,(carr b),(carr b)) is Element of K19( the carrier of a)
{ (a,b₁,b₂) where b₁, b₂ is Element of the carrier of a : ( b₁ in carr b & b₂ in carr b ) } is set
gr (a,(carr b),(carr b)) is non empty strict unital Group-like associative Subgroup of a
G is set
(a,b,b) is Element of K19( the carrier of a)
e is V1() V4( NAT ) V5( the carrier of d) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of d
len e is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
c is V1() V4( NAT ) V5( INT ) Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
len c is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
rng e is set
e is non empty unital Group-like associative Subgroup of d
d is non empty unital Group-like associative Subgroup of d
(d,e,d) is Element of K19( the carrier of d)
K19( the carrier of d) is non empty set
carr e is Element of K19( the carrier of d)
the carrier of e is non empty set
carr d is Element of K19( the carrier of d)
the carrier of d is non empty set
(d,(carr e),(carr d)) is Element of K19( the carrier of d)
{ (d,b₁,b₂) where b₁, b₂ is Element of the carrier of d : ( b₁ in carr e & b₂ in carr d ) } is set
c is set
e |^ c is V1() V4( NAT ) V5( the carrier of d) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of d
Product (e |^ c) is Element of the carrier of d
the U8 of d is V1() V4(K20( the carrier of d, the carrier of d)) V5( the carrier of d) Function-like V32(K20( the carrier of d, the carrier of d), the carrier of d) Element of K19(K20(K20( the carrier of d, the carrier of d), the carrier of d))
K20( the carrier of d, the carrier of d) is non empty set
K20(K20( the carrier of d, the carrier of d), the carrier of d) is non empty set
K19(K20(K20( the carrier of d, the carrier of d), the carrier of d)) is non empty set
K173( the carrier of d,(e |^ c), the U8 of d) is Element of the carrier of d
(d,e,d) is non empty strict unital Group-like associative Subgroup of d
(d,(carr e),(carr d)) is non empty strict unital Group-like associative Subgroup of d
gr (d,(carr e),(carr d)) is non empty strict unital Group-like associative Subgroup of d
G is non empty unital Group-like associative L11()
the carrier of G is non empty set
a is Element of the carrier of G
b is Element of the carrier of G
(G,a,b) is Element of the carrier of G
a " is Element of the carrier of G
b " is Element of the carrier of G
(a ") * (b ") is Element of the carrier of G
((a ") * (b ")) * a is Element of the carrier of G
(((a ") * (b ")) * a) * b is Element of the carrier of G
b is non empty unital Group-like associative Subgroup of G
c is non empty unital Group-like associative Subgroup of G
(G,b,c) is non empty strict unital Group-like associative Subgroup of G
carr b is Element of K19( the carrier of G)
K19( the carrier of G) is non empty set
the carrier of b is non empty set
carr c is Element of K19( the carrier of G)
the carrier of c is non empty set
(G,(carr b),(carr c)) is non empty strict unital Group-like associative Subgroup of G
(G,(carr b),(carr c)) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr b & b₂ in carr c ) } is set
gr (G,(carr b),(carr c)) is non empty strict unital Group-like associative Subgroup of G
G is non empty unital Group-like associative L11()
a is non empty unital Group-like associative Subgroup of G
b is non empty unital Group-like associative Subgroup of G
b is non empty unital Group-like associative Subgroup of G
(G,a,b) is non empty strict unital Group-like associative Subgroup of G
carr a is Element of K19( the carrier of G)
the carrier of G is non empty set
K19( the carrier of G) is non empty set
the carrier of a is non empty set
carr b is Element of K19( the carrier of G)
the carrier of b is non empty set
(G,(carr a),(carr b)) is non empty strict unital Group-like associative Subgroup of G
(G,(carr a),(carr b)) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr a & b₂ in carr b ) } is set
gr (G,(carr a),(carr b)) is non empty strict unital Group-like associative Subgroup of G
c is non empty unital Group-like associative Subgroup of G
(G,b,c) is non empty strict unital Group-like associative Subgroup of G
carr b is Element of K19( the carrier of G)
the carrier of b is non empty set
carr c is Element of K19( the carrier of G)
the carrier of c is non empty set
(G,(carr b),(carr c)) is non empty strict unital Group-like associative Subgroup of G
(G,(carr b),(carr c)) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr b & b₂ in carr c ) } is set
gr (G,(carr b),(carr c)) is non empty strict unital Group-like associative Subgroup of G
(G,a,b) is Element of K19( the carrier of G)
(G,b,c) is Element of K19( the carrier of G)
G is non empty unital Group-like associative L11()
a is non empty unital Group-like associative Subgroup of G
b is non empty strict unital Group-like associative normal Subgroup of G
(G,b,a) is non empty strict unital Group-like associative Subgroup of G
carr b is Element of K19( the carrier of G)
the carrier of G is non empty set
K19( the carrier of G) is non empty set
the carrier of b is non empty set
carr a is Element of K19( the carrier of G)
the carrier of a is non empty set
(G,(carr b),(carr a)) is non empty strict unital Group-like associative Subgroup of G
(G,(carr b),(carr a)) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr b & b₂ in carr a ) } is set
gr (G,(carr b),(carr a)) is non empty strict unital Group-like associative Subgroup of G
(G,a,b) is non empty strict unital Group-like associative Subgroup of G
(G,(carr a),(carr b)) is non empty strict unital Group-like associative Subgroup of G
(G,(carr a),(carr b)) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr a & b₂ in carr b ) } is set
gr (G,(carr a),(carr b)) is non empty strict unital Group-like associative Subgroup of G
b is Element of the carrier of G
(G,b,a) is Element of K19( the carrier of G)
c is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len c is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
d is V1() V4( NAT ) V5( INT ) Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
len d is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
rng c is set
c |^ d is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
Product (c |^ d) is Element of the carrier of G
the U8 of G is V1() V4(K20( the carrier of G, the carrier of G)) V5( the carrier of G) Function-like V32(K20( the carrier of G, the carrier of G), the carrier of G) Element of K19(K20(K20( the carrier of G, the carrier of G), the carrier of G))
K20( the carrier of G, the carrier of G) is non empty set
K20(K20( the carrier of G, the carrier of G), the carrier of G) is non empty set
K19(K20(K20( the carrier of G, the carrier of G), the carrier of G)) is non empty set
K173( the carrier of G,(c |^ d), the U8 of G) is Element of the carrier of G
gr (carr b) is non empty strict unital Group-like associative Subgroup of G
b is Element of the carrier of G
(G,a,b) is Element of K19( the carrier of G)
c is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len c is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
d is V1() V4( NAT ) V5( INT ) Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
len d is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
rng c is set
c |^ d is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
Product (c |^ d) is Element of the carrier of G
K173( the carrier of G,(c |^ d), the U8 of G) is Element of the carrier of G
G is non empty unital Group-like associative L11()
a is non empty strict unital Group-like associative normal Subgroup of G
b is non empty strict unital Group-like associative normal Subgroup of G
(G,a,b) is non empty strict unital Group-like associative Subgroup of G
carr a is Element of K19( the carrier of G)
the carrier of G is non empty set
K19( the carrier of G) is non empty set
the carrier of a is non empty set
carr b is Element of K19( the carrier of G)
the carrier of b is non empty set
(G,(carr a),(carr b)) is non empty strict unital Group-like associative Subgroup of G
(G,(carr a),(carr b)) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr a & b₂ in carr b ) } is set
gr (G,(carr a),(carr b)) is non empty strict unital Group-like associative Subgroup of G
b is Element of the carrier of G
(G,a,b) |^ b is non empty strict unital Group-like associative Subgroup of G
c is Element of the carrier of G
d is Element of the carrier of G
d |^ b is Element of the carrier of G
b " is Element of the carrier of G
(b ") * d is Element of the carrier of G
((b ") * d) * b is Element of the carrier of G
e is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len e is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
d is V1() V4( NAT ) V5( INT ) Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
len d is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
rng e is set
e |^ d is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
Product (e |^ d) is Element of the carrier of G
the U8 of G is V1() V4(K20( the carrier of G, the carrier of G)) V5( the carrier of G) Function-like V32(K20( the carrier of G, the carrier of G), the carrier of G) Element of K19(K20(K20( the carrier of G, the carrier of G), the carrier of G))
K20( the carrier of G, the carrier of G) is non empty set
K20(K20( the carrier of G, the carrier of G), the carrier of G) is non empty set
K19(K20(K20( the carrier of G, the carrier of G), the carrier of G)) is non empty set
K173( the carrier of G,(e |^ d), the U8 of G) is Element of the carrier of G
(G,e,b) is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len (G,e,b) is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
rng (G,e,b) is set
e is set
dom (G,e,b) is Element of K19(NAT)
c is set
(G,e,b) . c is set
X is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
dom e is Element of K19(NAT)
e . X is set
e /. X is Element of the carrier of G
a is Element of the carrier of G
b is Element of the carrier of G
(G,a,b) is Element of the carrier of G
a " is Element of the carrier of G
b " is Element of the carrier of G
(a ") * (b ") is Element of the carrier of G
((a ") * (b ")) * a is Element of the carrier of G
(((a ") * (b ")) * a) * b is Element of the carrier of G
a |^ b is non empty strict unital Group-like associative Subgroup of G
a |^ b is Element of the carrier of G
(b ") * a is Element of the carrier of G
((b ") * a) * b is Element of the carrier of G
b |^ b is non empty strict unital Group-like associative Subgroup of G
b |^ b is Element of the carrier of G
(b ") * b is Element of the carrier of G
((b ") * b) * b is Element of the carrier of G
(e /. X) |^ b is Element of the carrier of G
(b ") * (e /. X) is Element of the carrier of G
((b ") * (e /. X)) * b is Element of the carrier of G
(G,(a |^ b),(b |^ b)) is Element of the carrier of G
(a |^ b) " is Element of the carrier of G
(b |^ b) " is Element of the carrier of G
((a |^ b) ") * ((b |^ b) ") is Element of the carrier of G
(((a |^ b) ") * ((b |^ b) ")) * (a |^ b) is Element of the carrier of G
((((a |^ b) ") * ((b |^ b) ")) * (a |^ b)) * (b |^ b) is Element of the carrier of G
(G,(e |^ d),b) is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
Product (G,(e |^ d),b) is Element of the carrier of G
K173( the carrier of G,(G,(e |^ d),b), the U8 of G) is Element of the carrier of G
(G,e,b) |^ d is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
Product ((G,e,b) |^ d) is Element of the carrier of G
K173( the carrier of G,((G,e,b) |^ d), the U8 of G) is Element of the carrier of G
G is non empty unital Group-like associative L11()
a is non empty unital Group-like associative normal Subgroup of G
b is non empty unital Group-like associative normal Subgroup of G
(G,a,b) is non empty strict unital Group-like associative Subgroup of G
carr a is Element of K19( the carrier of G)
the carrier of G is non empty set
K19( the carrier of G) is non empty set
the carrier of a is non empty set
carr b is Element of K19( the carrier of G)
the carrier of b is non empty set
(G,(carr a),(carr b)) is non empty strict unital Group-like associative Subgroup of G
(G,(carr a),(carr b)) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr a & b₂ in carr b ) } is set
gr (G,(carr a),(carr b)) is non empty strict unital Group-like associative Subgroup of G
(G,b,a) is non empty strict unital Group-like associative Subgroup of G
(G,(carr b),(carr a)) is non empty strict unital Group-like associative Subgroup of G
(G,(carr b),(carr a)) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr b & b₂ in carr a ) } is set
gr (G,(carr b),(carr a)) is non empty strict unital Group-like associative Subgroup of G
b is Element of the carrier of G
(G,a,b) is Element of K19( the carrier of G)
c is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len c is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
d is V1() V4( NAT ) V5( INT ) Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
len d is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
rng c is set
c |^ d is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
Product (c |^ d) is Element of the carrier of G
the U8 of G is V1() V4(K20( the carrier of G, the carrier of G)) V5( the carrier of G) Function-like V32(K20( the carrier of G, the carrier of G), the carrier of G) Element of K19(K20(K20( the carrier of G, the carrier of G), the carrier of G))
K20( the carrier of G, the carrier of G) is non empty set
K20(K20( the carrier of G, the carrier of G), the carrier of G) is non empty set
K19(K20(K20( the carrier of G, the carrier of G), the carrier of G)) is non empty set
K173( the carrier of G,(c |^ d), the U8 of G) is Element of the carrier of G
e is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len e is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
dom e is Element of K19(NAT)
dom c is Element of K19(NAT)
Seg (len c) is finite len c -element Element of K19(NAT)
rng e is set
(G,b,a) is Element of K19( the carrier of G)
d is set
e is set
e . e is set
c is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
c /. c is Element of the carrier of G
c . c is set
X is Element of the carrier of G
a is Element of the carrier of G
(G,X,a) is Element of the carrier of G
X " is Element of the carrier of G
a " is Element of the carrier of G
(X ") * (a ") is Element of the carrier of G
((X ") * (a ")) * X is Element of the carrier of G
(((X ") * (a ")) * X) * a is Element of the carrier of G
(c /. c) " is Element of the carrier of G
(G,a,X) is Element of the carrier of G
(a ") * (X ") is Element of the carrier of G
((a ") * (X ")) * a is Element of the carrier of G
(((a ") * (X ")) * a) * X is Element of the carrier of G
len (c |^ d) is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
dom (c |^ d) is Element of K19(NAT)
d is V1() V4( NAT ) V5( INT ) Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
len d is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
dom d is Element of K19(NAT)
e |^ d is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
c is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer set
(e |^ d) . c is set
d /. c is V25() V26() V50() integer Element of INT
@ (d /. c) is V25() V26() V50() integer Element of INT
e /. c is Element of the carrier of G
(e /. c) |^ (@ (d /. c)) is Element of the carrier of G
e . c is set
d . c is set
d /. c is V25() V26() V50() integer Element of INT
@ (d /. c) is V25() V26() V50() integer Element of INT
- (@ (d /. c)) is V25() V26() V50() integer set
@ (- (@ (d /. c))) is V25() V26() V50() integer Element of INT
c /. c is Element of the carrier of G
(c /. c) " is Element of the carrier of G
((c /. c) ") |^ (@ (d /. c)) is Element of the carrier of G
(((c /. c) ") |^ (@ (d /. c))) " is Element of the carrier of G
(c /. c) |^ (@ (d /. c)) is Element of the carrier of G
((c /. c) |^ (@ (d /. c))) " is Element of the carrier of G
(((c /. c) |^ (@ (d /. c))) ") " is Element of the carrier of G
(c |^ d) . c is set
len (e |^ d) is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
G is non empty unital Group-like associative L11()
a is non empty unital Group-like associative normal Subgroup of G
b is non empty unital Group-like associative normal Subgroup of G
(G,a,b) is non empty strict unital Group-like associative Subgroup of G
carr a is Element of K19( the carrier of G)
the carrier of G is non empty set
K19( the carrier of G) is non empty set
the carrier of a is non empty set
carr b is Element of K19( the carrier of G)
the carrier of b is non empty set
(G,(carr a),(carr b)) is non empty strict unital Group-like associative Subgroup of G
(G,(carr a),(carr b)) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr a & b₂ in carr b ) } is set
gr (G,(carr a),(carr b)) is non empty strict unital Group-like associative Subgroup of G
(G,b,a) is non empty strict unital Group-like associative Subgroup of G
(G,(carr b),(carr a)) is non empty strict unital Group-like associative Subgroup of G
(G,(carr b),(carr a)) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr b & b₂ in carr a ) } is set
gr (G,(carr b),(carr a)) is non empty strict unital Group-like associative Subgroup of G
G is non empty unital Group-like associative L11()
a is non empty strict unital Group-like associative normal Subgroup of G
b is non empty strict unital Group-like associative normal Subgroup of G
a "\/" b is non empty strict unital Group-like associative Subgroup of G
the carrier of G is non empty set
carr a is Element of K19( the carrier of G)
K19( the carrier of G) is non empty set
the carrier of a is non empty set
carr b is Element of K19( the carrier of G)
the carrier of b is non empty set
(carr a) \/ (carr b) is Element of K19( the carrier of G)
gr ((carr a) \/ (carr b)) is non empty strict unital Group-like associative Subgroup of G
b is non empty strict unital Group-like associative normal Subgroup of G
(G,(a "\/" b),b) is non empty strict unital Group-like associative Subgroup of G
carr (a "\/" b) is Element of K19( the carrier of G)
the carrier of (a "\/" b) is non empty set
carr b is Element of K19( the carrier of G)
the carrier of b is non empty set
(G,(carr (a "\/" b)),(carr b)) is non empty strict unital Group-like associative Subgroup of G
(G,(carr (a "\/" b)),(carr b)) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr (a "\/" b) & b₂ in carr b ) } is set
gr (G,(carr (a "\/" b)),(carr b)) is non empty strict unital Group-like associative Subgroup of G
(G,a,b) is non empty strict unital Group-like associative Subgroup of G
(G,(carr a),(carr b)) is non empty strict unital Group-like associative Subgroup of G
(G,(carr a),(carr b)) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr a & b₂ in carr b ) } is set
gr (G,(carr a),(carr b)) is non empty strict unital Group-like associative Subgroup of G
(G,b,b) is non empty strict unital Group-like associative Subgroup of G
(G,(carr b),(carr b)) is non empty strict unital Group-like associative Subgroup of G
(G,(carr b),(carr b)) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr b & b₂ in carr b ) } is set
gr (G,(carr b),(carr b)) is non empty strict unital Group-like associative Subgroup of G
(G,a,b) "\/" (G,b,b) is non empty strict unital Group-like associative Subgroup of G
carr (G,a,b) is Element of K19( the carrier of G)
the carrier of (G,a,b) is non empty set
carr (G,b,b) is Element of K19( the carrier of G)
the carrier of (G,b,b) is non empty set
(carr (G,a,b)) \/ (carr (G,b,b)) is Element of K19( the carrier of G)
gr ((carr (G,a,b)) \/ (carr (G,b,b))) is non empty strict unital Group-like associative Subgroup of G
(G,b,b) is Element of K19( the carrier of G)
(G,(a "\/" b),b) is Element of K19( the carrier of G)
c is Element of the carrier of G
d is Element of the carrier of G
e is Element of the carrier of G
d * e is Element of the carrier of G
(G,a,b) is Element of K19( the carrier of G)
d is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len d is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
e is V1() V4( NAT ) V5( INT ) Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
len e is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
rng d is set
d |^ e is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
Product (d |^ e) is Element of the carrier of G
the U8 of G is V1() V4(K20( the carrier of G, the carrier of G)) V5( the carrier of G) Function-like V32(K20( the carrier of G, the carrier of G), the carrier of G) Element of K19(K20(K20( the carrier of G, the carrier of G), the carrier of G))
K20( the carrier of G, the carrier of G) is non empty set
K20(K20( the carrier of G, the carrier of G), the carrier of G) is non empty set
K19(K20(K20( the carrier of G, the carrier of G), the carrier of G)) is non empty set
K173( the carrier of G,(d |^ e), the U8 of G) is Element of the carrier of G
c is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len c is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
X is V1() V4( NAT ) V5( INT ) Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
len X is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
rng c is set
c |^ X is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
Product (c |^ X) is Element of the carrier of G
K173( the carrier of G,(c |^ X), the U8 of G) is Element of the carrier of G
d ^ c is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len (d ^ c) is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
(len e) + (len X) is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
e ^ X is V1() V4( NAT ) V5( INT ) Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
len (e ^ X) is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
rng (d ^ c) is set
(rng d) \/ (rng c) is set
(G,a,b) \/ (G,b,b) is Element of K19( the carrier of G)
(d ^ c) |^ (e ^ X) is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
Product ((d ^ c) |^ (e ^ X)) is Element of the carrier of G
K173( the carrier of G,((d ^ c) |^ (e ^ X)), the U8 of G) is Element of the carrier of G
(d |^ e) ^ (c |^ X) is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
Product ((d |^ e) ^ (c |^ X)) is Element of the carrier of G
K173( the carrier of G,((d |^ e) ^ (c |^ X)), the U8 of G) is Element of the carrier of G
(G,a,b) * (G,b,b) is Element of K19( the carrier of G)
(carr (G,a,b)) * (carr (G,b,b)) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr (G,a,b) & b₂ in carr (G,b,b) ) } is set
c is set
d is Element of the carrier of G
e is Element of the carrier of G
(G,d,e) is Element of the carrier of G
d " is Element of the carrier of G
e " is Element of the carrier of G
(d ") * (e ") is Element of the carrier of G
((d ") * (e ")) * d is Element of the carrier of G
(((d ") * (e ")) * d) * e is Element of the carrier of G
d is Element of the carrier of G
e is Element of the carrier of G
d * e is Element of the carrier of G
(G,d,e) is Element of the carrier of G
d " is Element of the carrier of G
(d ") * (e ") is Element of the carrier of G
((d ") * (e ")) * d is Element of the carrier of G
(((d ") * (e ")) * d) * e is Element of the carrier of G
(G,a,b) |^ e is non empty strict unital Group-like associative Subgroup of G
(G,d,e) |^ e is Element of the carrier of G
e " is Element of the carrier of G
(e ") * (G,d,e) is Element of the carrier of G
((e ") * (G,d,e)) * e is Element of the carrier of G
(G,e,e) is Element of the carrier of G
(e ") * (e ") is Element of the carrier of G
((e ") * (e ")) * e is Element of the carrier of G
(((e ") * (e ")) * e) * e is Element of the carrier of G
((G,d,e) |^ e) * (G,e,e) is Element of the carrier of G
gr (G,(a "\/" b),b) is non empty strict unital Group-like associative Subgroup of G
gr ((G,a,b) * (G,b,b)) is non empty strict unital Group-like associative Subgroup of G
G is non empty unital Group-like associative L11()
a is non empty strict unital Group-like associative normal Subgroup of G
b is non empty strict unital Group-like associative normal Subgroup of G
b is non empty strict unital Group-like associative normal Subgroup of G
b "\/" b is non empty strict unital Group-like associative Subgroup of G
the carrier of G is non empty set
carr b is Element of K19( the carrier of G)
K19( the carrier of G) is non empty set
the carrier of b is non empty set
carr b is Element of K19( the carrier of G)
the carrier of b is non empty set
(carr b) \/ (carr b) is Element of K19( the carrier of G)
gr ((carr b) \/ (carr b)) is non empty strict unital Group-like associative Subgroup of G
(G,a,(b "\/" b)) is non empty strict unital Group-like associative Subgroup of G
carr a is Element of K19( the carrier of G)
the carrier of a is non empty set
carr (b "\/" b) is Element of K19( the carrier of G)
the carrier of (b "\/" b) is non empty set
(G,(carr a),(carr (b "\/" b))) is non empty strict unital Group-like associative Subgroup of G
(G,(carr a),(carr (b "\/" b))) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr a & b₂ in carr (b "\/" b) ) } is set
gr (G,(carr a),(carr (b "\/" b))) is non empty strict unital Group-like associative Subgroup of G
(G,a,b) is non empty strict unital Group-like associative Subgroup of G
(G,(carr a),(carr b)) is non empty strict unital Group-like associative Subgroup of G
(G,(carr a),(carr b)) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr a & b₂ in carr b ) } is set
gr (G,(carr a),(carr b)) is non empty strict unital Group-like associative Subgroup of G
(G,a,b) is non empty strict unital Group-like associative Subgroup of G
(G,(carr a),(carr b)) is non empty strict unital Group-like associative Subgroup of G
(G,(carr a),(carr b)) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr a & b₂ in carr b ) } is set
gr (G,(carr a),(carr b)) is non empty strict unital Group-like associative Subgroup of G
(G,a,b) "\/" (G,a,b) is non empty strict unital Group-like associative Subgroup of G
carr (G,a,b) is Element of K19( the carrier of G)
the carrier of (G,a,b) is non empty set
carr (G,a,b) is Element of K19( the carrier of G)
the carrier of (G,a,b) is non empty set
(carr (G,a,b)) \/ (carr (G,a,b)) is Element of K19( the carrier of G)
gr ((carr (G,a,b)) \/ (carr (G,a,b))) is non empty strict unital Group-like associative Subgroup of G
(G,(b "\/" b),a) is non empty strict unital Group-like associative Subgroup of G
(G,(carr (b "\/" b)),(carr a)) is non empty strict unital Group-like associative Subgroup of G
(G,(carr (b "\/" b)),(carr a)) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr (b "\/" b) & b₂ in carr a ) } is set
gr (G,(carr (b "\/" b)),(carr a)) is non empty strict unital Group-like associative Subgroup of G
(G,b,a) is non empty strict unital Group-like associative Subgroup of G
(G,(carr b),(carr a)) is non empty strict unital Group-like associative Subgroup of G
(G,(carr b),(carr a)) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr b & b₂ in carr a ) } is set
gr (G,(carr b),(carr a)) is non empty strict unital Group-like associative Subgroup of G
(G,b,a) is non empty strict unital Group-like associative Subgroup of G
(G,(carr b),(carr a)) is non empty strict unital Group-like associative Subgroup of G
(G,(carr b),(carr a)) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr b & b₂ in carr a ) } is set
gr (G,(carr b),(carr a)) is non empty strict unital Group-like associative Subgroup of G
(G,b,a) "\/" (G,b,a) is non empty strict unital Group-like associative Subgroup of G
carr (G,b,a) is Element of K19( the carrier of G)
the carrier of (G,b,a) is non empty set
carr (G,b,a) is Element of K19( the carrier of G)
the carrier of (G,b,a) is non empty set
(carr (G,b,a)) \/ (carr (G,b,a)) is Element of K19( the carrier of G)
gr ((carr (G,b,a)) \/ (carr (G,b,a))) is non empty strict unital Group-like associative Subgroup of G
(G,a,b) "\/" (G,b,a) is non empty strict unital Group-like associative Subgroup of G
(carr (G,a,b)) \/ (carr (G,b,a)) is Element of K19( the carrier of G)
gr ((carr (G,a,b)) \/ (carr (G,b,a))) is non empty strict unital Group-like associative Subgroup of G
G is non empty unital Group-like associative L11()
(Omega). G is non empty strict unital Group-like associative Subgroup of G
the carrier of G is non empty set
the U8 of G is V1() V4(K20( the carrier of G, the carrier of G)) V5( the carrier of G) Function-like V32(K20( the carrier of G, the carrier of G), the carrier of G) Element of K19(K20(K20( the carrier of G, the carrier of G), the carrier of G))
K20( the carrier of G, the carrier of G) is non empty set
K20(K20( the carrier of G, the carrier of G), the carrier of G) is non empty set
K19(K20(K20( the carrier of G, the carrier of G), the carrier of G)) is non empty set
G11( the carrier of G, the U8 of G) is strict L11()
(G,((Omega). G),((Omega). G)) is non empty strict unital Group-like associative Subgroup of G
carr ((Omega). G) is Element of K19( the carrier of G)
K19( the carrier of G) is non empty set
the carrier of ((Omega). G) is non empty set
(G,(carr ((Omega). G)),(carr ((Omega). G))) is non empty strict unital Group-like associative Subgroup of G
(G,(carr ((Omega). G)),(carr ((Omega). G))) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr ((Omega). G) & b₂ in carr ((Omega). G) ) } is set
gr (G,(carr ((Omega). G)),(carr ((Omega). G))) is non empty strict unital Group-like associative Subgroup of G
G is non empty unital Group-like associative L11()
(G) is non empty strict unital Group-like associative normal Subgroup of G
(Omega). G is non empty strict unital Group-like associative Subgroup of G
the carrier of G is non empty set
the U8 of G is V1() V4(K20( the carrier of G, the carrier of G)) V5( the carrier of G) Function-like V32(K20( the carrier of G, the carrier of G), the carrier of G) Element of K19(K20(K20( the carrier of G, the carrier of G), the carrier of G))
K20( the carrier of G, the carrier of G) is non empty set
K20(K20( the carrier of G, the carrier of G), the carrier of G) is non empty set
K19(K20(K20( the carrier of G, the carrier of G), the carrier of G)) is non empty set
G11( the carrier of G, the U8 of G) is strict L11()
(G,((Omega). G),((Omega). G)) is non empty strict unital Group-like associative Subgroup of G
carr ((Omega). G) is Element of K19( the carrier of G)
K19( the carrier of G) is non empty set
the carrier of ((Omega). G) is non empty set
(G,(carr ((Omega). G)),(carr ((Omega). G))) is non empty strict unital Group-like associative Subgroup of G
(G,(carr ((Omega). G)),(carr ((Omega). G))) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr ((Omega). G) & b₂ in carr ((Omega). G) ) } is set
gr (G,(carr ((Omega). G)),(carr ((Omega). G))) is non empty strict unital Group-like associative Subgroup of G
(G) is Element of K19( the carrier of G)
(G,((Omega). G),((Omega). G)) is Element of K19( the carrier of G)
gr (G) is non empty strict unital Group-like associative Subgroup of G
G is set
a is non empty unital Group-like associative L11()
(a) is non empty strict unital Group-like associative normal Subgroup of a
(Omega). a is non empty strict unital Group-like associative Subgroup of a
the carrier of a is non empty set
the U8 of a is V1() V4(K20( the carrier of a, the carrier of a)) V5( the carrier of a) Function-like V32(K20( the carrier of a, the carrier of a), the carrier of a) Element of K19(K20(K20( the carrier of a, the carrier of a), the carrier of a))
K20( the carrier of a, the carrier of a) is non empty set
K20(K20( the carrier of a, the carrier of a), the carrier of a) is non empty set
K19(K20(K20( the carrier of a, the carrier of a), the carrier of a)) is non empty set
G11( the carrier of a, the U8 of a) is strict L11()
(a,((Omega). a),((Omega). a)) is non empty strict unital Group-like associative Subgroup of a
carr ((Omega). a) is Element of K19( the carrier of a)
K19( the carrier of a) is non empty set
the carrier of ((Omega). a) is non empty set
(a,(carr ((Omega). a)),(carr ((Omega). a))) is non empty strict unital Group-like associative Subgroup of a
(a,(carr ((Omega). a)),(carr ((Omega). a))) is Element of K19( the carrier of a)
{ (a,b₁,b₂) where b₁, b₂ is Element of the carrier of a : ( b₁ in carr ((Omega). a) & b₂ in carr ((Omega). a) ) } is set
gr (a,(carr ((Omega). a)),(carr ((Omega). a))) is non empty strict unital Group-like associative Subgroup of a
(a) is Element of K19( the carrier of a)
(a,((Omega). a),((Omega). a)) is Element of K19( the carrier of a)
b is Element of the carrier of a
b is V1() V4( NAT ) V5( the carrier of a) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a
len b is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
c is V1() V4( NAT ) V5( INT ) Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
len c is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
rng b is set
b |^ c is V1() V4( NAT ) V5( the carrier of a) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a
Product (b |^ c) is Element of the carrier of a
K173( the carrier of a,(b |^ c), the U8 of a) is Element of the carrier of a
b is V1() V4( NAT ) V5( the carrier of a) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a
len b is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
b is V1() V4( NAT ) V5( INT ) Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
len b is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
rng b is set
b |^ b is V1() V4( NAT ) V5( the carrier of a) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a
Product (b |^ b) is Element of the carrier of a
K173( the carrier of a,(b |^ b), the U8 of a) is Element of the carrier of a
G is non empty strict unital Group-like associative L11()
the carrier of G is non empty set
(G) is non empty strict unital Group-like associative normal Subgroup of G
(Omega). G is non empty strict unital Group-like associative Subgroup of G
the U8 of G is V1() V4(K20( the carrier of G, the carrier of G)) V5( the carrier of G) Function-like V32(K20( the carrier of G, the carrier of G), the carrier of G) Element of K19(K20(K20( the carrier of G, the carrier of G), the carrier of G))
K20( the carrier of G, the carrier of G) is non empty set
K20(K20( the carrier of G, the carrier of G), the carrier of G) is non empty set
K19(K20(K20( the carrier of G, the carrier of G), the carrier of G)) is non empty set
G11( the carrier of G, the U8 of G) is strict L11()
(G,((Omega). G),((Omega). G)) is non empty strict unital Group-like associative Subgroup of G
carr ((Omega). G) is Element of K19( the carrier of G)
K19( the carrier of G) is non empty set
the carrier of ((Omega). G) is non empty set
(G,(carr ((Omega). G)),(carr ((Omega). G))) is non empty strict unital Group-like associative Subgroup of G
(G,(carr ((Omega). G)),(carr ((Omega). G))) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr ((Omega). G) & b₂ in carr ((Omega). G) ) } is set
gr (G,(carr ((Omega). G)),(carr ((Omega). G))) is non empty strict unital Group-like associative Subgroup of G
a is Element of the carrier of G
b is Element of the carrier of G
(G,a,b) is Element of the carrier of G
a " is Element of the carrier of G
b " is Element of the carrier of G
(a ") * (b ") is Element of the carrier of G
((a ") * (b ")) * a is Element of the carrier of G
(((a ") * (b ")) * a) * b is Element of the carrier of G
G is non empty strict unital Group-like associative L11()
(G) is non empty strict unital Group-like associative normal Subgroup of G
(Omega). G is non empty strict unital Group-like associative Subgroup of G
the carrier of G is non empty set
the U8 of G is V1() V4(K20( the carrier of G, the carrier of G)) V5( the carrier of G) Function-like V32(K20( the carrier of G, the carrier of G), the carrier of G) Element of K19(K20(K20( the carrier of G, the carrier of G), the carrier of G))
K20( the carrier of G, the carrier of G) is non empty set
K20(K20( the carrier of G, the carrier of G), the carrier of G) is non empty set
K19(K20(K20( the carrier of G, the carrier of G), the carrier of G)) is non empty set
G11( the carrier of G, the U8 of G) is strict L11()
(G,((Omega). G),((Omega). G)) is non empty strict unital Group-like associative Subgroup of G
carr ((Omega). G) is Element of K19( the carrier of G)
K19( the carrier of G) is non empty set
the carrier of ((Omega). G) is non empty set
(G,(carr ((Omega). G)),(carr ((Omega). G))) is non empty strict unital Group-like associative Subgroup of G
(G,(carr ((Omega). G)),(carr ((Omega). G))) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr ((Omega). G) & b₂ in carr ((Omega). G) ) } is set
gr (G,(carr ((Omega). G)),(carr ((Omega). G))) is non empty strict unital Group-like associative Subgroup of G
(1). G is non empty finite strict unital Group-like associative Subgroup of G
a is Element of the carrier of G
1_ G is non being_of_order_0 Element of the carrier of G
{(1_ G)} is non empty V12() 1 -element Element of K19( the carrier of G)
gr {(1_ G)} is non empty strict unital Group-like associative Subgroup of G
{(1_ G)} \ {(1_ G)} is Element of K19( the carrier of G)
gr ({(1_ G)} \ {(1_ G)}) is non empty strict unital Group-like associative Subgroup of G
{} the carrier of G is functional empty proper V18() V19() V20() V22() V23() V24() V25() V26() finite cardinal {} -element FinSequence-membered V50() integer Element of K19( the carrier of G)
gr ({} the carrier of G) is non empty strict unital Group-like associative Subgroup of G
a is Element of the carrier of G
b is Element of the carrier of G
a * b is Element of the carrier of G
b * a is Element of the carrier of G
(G,a,b) is Element of the carrier of G
a " is Element of the carrier of G
b " is Element of the carrier of G
(a ") * (b ") is Element of the carrier of G
((a ") * (b ")) * a is Element of the carrier of G
(((a ") * (b ")) * a) * b 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 L11()
(G) is non empty strict unital Group-like associative normal Subgroup of G
(Omega). G is non empty strict unital Group-like associative Subgroup of G
the carrier of G is non empty set
the U8 of G is V1() V4(K20( the carrier of G, the carrier of G)) V5( the carrier of G) Function-like V32(K20( the carrier of G, the carrier of G), the carrier of G) Element of K19(K20(K20( the carrier of G, the carrier of G), the carrier of G))
K20( the carrier of G, the carrier of G) is non empty set
K20(K20( the carrier of G, the carrier of G), the carrier of G) is non empty set
K19(K20(K20( the carrier of G, the carrier of G), the carrier of G)) is non empty set
G11( the carrier of G, the U8 of G) is strict L11()
(G,((Omega). G),((Omega). G)) is non empty strict unital Group-like associative Subgroup of G
carr ((Omega). G) is Element of K19( the carrier of G)
K19( the carrier of G) is non empty set
the carrier of ((Omega). G) is non empty set
(G,(carr ((Omega). G)),(carr ((Omega). G))) is non empty strict unital Group-like associative Subgroup of G
(G,(carr ((Omega). G)),(carr ((Omega). G))) is Element of K19( the carrier of G)
{ (G,b₁,b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr ((Omega). G) & b₂ in carr ((Omega). G) ) } is set
gr (G,(carr ((Omega). G)),(carr ((Omega). G))) is non empty strict unital Group-like associative Subgroup of G
a is non empty strict unital Group-like associative Subgroup of G
Left_Cosets a is Element of K19(K19( the carrier of G))
K19(K19( the carrier of G)) is non empty set
index a is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
b is Element of the carrier of G
(G) is Element of K19( the carrier of G)
(G,((Omega). G),((Omega). G)) is Element of K19( the carrier of G)
b is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
len b is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
c is V1() V4( NAT ) V5( INT ) Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
len c is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
rng b is set
b |^ c is V1() V4( NAT ) V5( the carrier of G) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of G
Product (b |^ c) is Element of the carrier of G
K173( the carrier of G,(b |^ c), the U8 of G) is Element of the carrier of G
carr a is Element of K19( the carrier of G)
the carrier of a is non empty set
d is finite set
card d is V18() V19() V20() V24() V25() V26() finite cardinal V50() integer Element of NAT
d is set
e is set
{d,e} is non empty set
d is Element of the carrier of G
d * a is Element of K19( the carrier of G)
d * (carr a) is Element of K19( the carrier of G)
{d} is non empty V12() 1 -element Element of K19( the carrier of G)
{d} * (carr a) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in {d} & b₂ in carr a ) } is set
e is Element of the carrier of G
e * a is Element of K19( the carrier of G)
e * (carr a) is Element of K19( the carrier of G)
{e} is non empty V12() 1 -element Element of K19( the carrier of G)
{e} * (carr a) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in {e} & b₂ in carr a ) } is set
{(carr a),(e * a)} is non empty Element of K19(K19( the carrier of G))
{(d * a),(carr a)} is non empty Element of K19(K19( the carrier of G))
c is Element of the carrier of G
c * a is Element of K19( the carrier of G)
c * (carr a) is Element of K19( the carrier of G)
{c} is non empty V12() 1 -element Element of K19( the carrier of G)
{c} * (carr a) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in {c} & b₂ in carr a ) } is set
{(carr a),(c * a)} is non empty Element of K19(K19( the carrier of G))
X is set
a is Element of the carrier of G
b is Element of the carrier of G
(G,a,b) is Element of the carrier of G
a " is Element of the carrier of G
b " is Element of the carrier of G
(a ") * (b ") is Element of the carrier of G
((a ") * (b ")) * a is Element of the carrier of G
(((a ") * (b ")) * a) * b is Element of the carrier of G
union (Left_Cosets a) is set
(carr a) \/ (c * a) is Element of K19( the carrier of G)
a |^ b is Element of the carrier of G
(b ") * a is Element of the carrier of G
((b ") * a) * b is Element of the carrier of G
(a ") * (a |^ b) is Element of the carrier of G
(b ") |^ a is Element of the carrier of G
((b ") |^ a) * b is Element of the carrier of G
d is Element of the carrier of G
c * d is Element of the carrier of G
e is Element of the carrier of G
c * e is Element of the carrier of G
e " is Element of the carrier of G
(e ") |^ c is Element of the carrier of G
c " is Element of the carrier of G
(c ") * (e ") is Element of the carrier of G
((c ") * (e ")) * c is Element of the carrier of G
d " is Element of the carrier of G
(d ") * ((e ") |^ c) is Element of the carrier of G
d |^ c is Element of the carrier of G
(c ") * d is Element of the carrier of G
((c ") * d) * c is Element of the carrier of G
(d |^ c) * e is Element of the carrier of G
a * b is Element of the carrier of G
((a ") * (b ")) * (a * b) is Element of the carrier of G
(d ") * (c ") is Element of the carrier of G
((d ") * (c ")) * (b ") is Element of the carrier of G
(c * d) * (c * e) is Element of the carrier of G
(((d ") * (c ")) * (b ")) * ((c * d) * (c * e)) is Element of the carrier of G
(e ") * (c ") is Element of the carrier of G
((d ") * (c ")) * ((e ") * (c ")) is Element of the carrier of G
(((d ") * (c ")) * ((e ") * (c "))) * ((c * d) * (c * e)) is Element of the carrier of G
((d ") * (c ")) * (e ") is Element of the carrier of G
(((d ") * (c ")) * (e ")) * (c ") is Element of the carrier of G
((((d ") * (c ")) * (e ")) * (c ")) * ((c * d) * (c * e)) is Element of the carrier of G
d * (c * e) is Element of the carrier of G
c * (d * (c * e)) is Element of the carrier of G
((((d ") * (c ")) * (e ")) * (c ")) * (c * (d * (c * e))) is Element of the carrier of G
((((d ") * (c ")) * (e ")) * (c ")) * c is Element of the carrier of G
(((((d ") * (c ")) * (e ")) * (c ")) * c) * (d * (c * e)) is Element of the carrier of G
(c ") * c is Element of the carrier of G
(((d ") * (c ")) * (e ")) * ((c ") * c) is Element of the carrier of G
((((d ") * (c ")) * (e ")) * ((c ") * c)) * (d * (c * e)) is Element of the carrier of G
1_ G is non being_of_order_0 Element of the carrier of G
(((d ") * (c ")) * (e ")) * (1_ G) is Element of the carrier of G
((((d ") * (c ")) * (e ")) * (1_ G)) * (d * (c * e)) is Element of the carrier of G
c * (c ") is Element of the carrier of G
(((d ") * (c ")) * (e ")) * (c * (c ")) is Element of the carrier of G
((((d ") * (c ")) * (e ")) * (c * (c "))) * (d * (c * e)) is Element of the carrier of G
(((d ") * (c ")) * (e ")) * c is Element of the carrier of G
((((d ") * (c ")) * (e ")) * c) * (c ") is Element of the carrier of G
(((((d ") * (c ")) * (e ")) * c) * (c ")) * (d * (c * e)) is Element of the carrier of G
(d ") * ((c ") * (e ")) is Element of the carrier of G
((d ") * ((c ") * (e "))) * c is Element of the carrier of G
(((d ") * ((c ") * (e "))) * c) * (c ") is Element of the carrier of G
((((d ") * ((c ") * (e "))) * c) * (c ")) * (d * (c * e)) is Element of the carrier of G
((d ") * ((e ") |^ c)) * (c ") is Element of the carrier of G
(((d ") * ((e ") |^ c)) * (c ")) * (d * (c * e)) is Element of the carrier of G
d * c is Element of the carrier of G
(d * c) * e is Element of the carrier of G
(((d ") * ((e ") |^ c)) * (c ")) * ((d * c) * e) is Element of the carrier of G
(c ") * ((d * c) * e) is Element of the carrier of G
((d ") * ((e ") |^ c)) * ((c ") * ((d * c) * e)) is Element of the carrier of G
(c ") * (d * (c * e)) is Element of the carrier of G
((d ") * ((e ") |^ c)) * ((c ") * (d * (c * e))) is Element of the carrier of G
((c ") * d) * (c * e) is Element of the carrier of G
((d ") * ((e ") |^ c)) * (((c ") * d) * (c * e)) is Element of the carrier of G
((d ") * ((e ") |^ c)) * ((d |^ c) * e) is Element of the carrier of G
gr (carr a) is non empty strict unital Group-like associative Subgroup of G
G is non empty unital Group-like associative L11()
the carrier of G is non empty set
{ b₁ where b₁ is Element of the carrier of G : for b₂ being Element of the carrier of G holds b₁ * b₂ = b₂ * b₁ } is set
K19( the carrier of G) is non empty set
{ b₁ where b₁ is Element of the carrier of G : S₁[b₁] } is set
b is Element of the carrier of G
a is Element of K19( the carrier of G)
b is Element of the carrier of G
c is Element of the carrier of G
d is Element of the carrier of G
b * b is Element of the carrier of G
e is Element of the carrier of G
(b * b) * e is Element of the carrier of G
b * e is Element of the carrier of G
b * (b * e) is Element of the carrier of G
e * d is Element of the carrier of G
b * (e * d) is Element of the carrier of G
b * e is Element of the carrier of G
(b * e) * b is Element of the carrier of G
e * c is Element of the carrier of G
(e * c) * b is Element of the carrier of G
e * (b * b) is Element of the carrier of G
b is Element of the carrier of G
b is Element of the carrier of G
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
((b ") * c) " is Element of the carrier of G
(((b ") * c) ") " is Element of the carrier of G
c " is Element of the carrier of G
(b ") " is Element of the carrier of G
(c ") * ((b ") ") is Element of the carrier of G
((c ") * ((b ") ")) " is Element of the carrier of G
(c ") * b is Element of the carrier of G
((c ") * b) " is Element of the carrier of G
b * (c ") is Element of the carrier of G
(b * (c ")) " is Element of the carrier of G
((b ") ") * (c ") is Element of the carrier of G
(((b ") ") * (c ")) " is Element of the carrier of G
c * (b ") is Element of the carrier of G
(c * (b ")) " is Element of the carrier of G
((c * (b ")) ") " is Element of the carrier of G
1_ G is non being_of_order_0 Element of the carrier of G
b is Element of the carrier of G
(1_ G) * b is Element of the carrier of G
b * (1_ G) 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
b is non empty strict unital Group-like associative Subgroup of G
the carrier of b is non empty set
G is non empty unital Group-like associative L11()
the carrier of G is non empty set
(G) is non empty strict unital Group-like associative Subgroup of G
a 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 : for b₂ being Element of the carrier of G holds b₁ * b₂ = b₂ * b₁ } is set
b is Element of the carrier of G
a * b is Element of the carrier of G
b * a is Element of the carrier of G
b is Element of the carrier of G
{ b₁ where b₁ is Element of the carrier of G : for b₂ being Element of the carrier of G holds b₁ * b₂ = b₂ * b₁ } is set
the carrier of (G) is non empty set
G is non empty unital Group-like associative L11()
(G) is non empty strict unital Group-like associative Subgroup of G
the carrier of G is non empty set
a is Element of the carrier of G
a * (G) is Element of K19( the carrier of G)
K19( the carrier of G) is non empty set
carr (G) is Element of K19( the carrier of G)
the carrier of (G) is non empty set
a * (carr (G)) is Element of K19( the carrier of G)
{a} is non empty V12() 1 -element Element of K19( the carrier of G)
{a} * (carr (G)) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in {a} & b₂ in carr (G) ) } is set
(G) * a is Element of K19( the carrier of G)
(carr (G)) * a is Element of K19( the carrier of G)
(carr (G)) * {a} is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr (G) & b₂ in {a} ) } is set
b is set
b is Element of the carrier of G
a * b is Element of the carrier of G
b * a is Element of the carrier of G
G is non empty unital Group-like associative L11()
(G) is non empty strict unital Group-like associative Subgroup of G
a is non empty unital Group-like associative Subgroup of G
the carrier of G is non empty set
b is Element of the carrier of G
a * b is Element of K19( the carrier of G)
K19( the carrier of G) is non empty set
carr a is Element of K19( the carrier of G)
the carrier of a is non empty set
(carr a) * b is Element of K19( the carrier of G)
{b} is non empty V12() 1 -element Element of K19( the carrier of G)
(carr a) * {b} is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr a & b₂ in {b} ) } is set
b * a is Element of K19( the carrier of G)
b * (carr a) is Element of K19( the carrier of G)
{b} * (carr a) is Element of K19( the carrier of G)
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in {b} & b₂ in carr a ) } is set
b is set
c is Element of the carrier of G
c * b is Element of the carrier of G
b * c is Element of the carrier of G
G is non empty unital Group-like associative L11()
(G) is non empty strict unital Group-like associative Subgroup of G
the carrier of (G) is non empty set
a is Element of the carrier of (G)
b is Element of the carrier of (G)
a * b is Element of the carrier of (G)
b * a is Element of the carrier of (G)
the carrier of G is non empty 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
c * b is Element of the carrier of G
G is non empty unital Group-like associative L11()
the carrier of G is non empty set
(G) is non empty strict unital Group-like associative Subgroup of G
a is Element of the carrier of G
con_class a is Element of K19( the carrier of G)
K19( the carrier of G) is non empty set
(Omega). G is non empty strict unital Group-like associative Subgroup of G
the U8 of G is V1() V4(K20( the carrier of G, the carrier of G)) V5( the carrier of G) Function-like V32(K20( the carrier of G, the carrier of G), the carrier of G) Element of K19(K20(K20( the carrier of G, the carrier of G), the carrier of G))
K20( the carrier of G, the carrier of G) is non empty set
K20(K20( the carrier of G, the carrier of G), the carrier of G) is non empty set
K19(K20(K20( the carrier of G, the carrier of G), the carrier of G)) is non empty set
G11( the carrier of G, the U8 of G) is strict L11()
carr ((Omega). G) is Element of K19( the carrier of G)
the carrier of ((Omega). G) is non empty set
a |^ (carr ((Omega). G)) is Element of K19( the carrier of G)
{a} is non empty V12() 1 -element Element of K19( the carrier of G)
{a} |^ (carr ((Omega). G)) is Element of K19( the carrier of G)
{ (b₁ |^ b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in {a} & b₂ in carr ((Omega). G) ) } is set
b 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
c " is Element of the carrier of G
(c ") * b is Element of the carrier of G
((c ") * b) * c is Element of the carrier of G
b * c is Element of the carrier of G
(c ") * (b * c) is Element of the carrier of G
c * a is Element of the carrier of G
a * c is Element of the carrier of G
b is Element of the carrier of G
a |^ b is Element of the carrier of G
b " is Element of the carrier of G
(b ") * a is Element of the carrier of G
((b ") * a) * b is Element of the carrier of G
a * b is Element of the carrier of G
(b ") * (a * b) is Element of the carrier of G
b * a is Element of the carrier of G
G is non empty strict unital Group-like associative L11()
(G) is non empty strict unital Group-like associative Subgroup of G
the carrier of G is non empty set
a is Element of the carrier of G
b is Element of the carrier of G
a * b is Element of the carrier of G
b * a is Element of the carrier of G
the carrier of G is non empty set
a is Element of the carrier of G
b is Element of the carrier of G
a * b is Element of the carrier of G
b * a is Element of the carrier of G