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