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

(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 * b is Element of K19( the carrier of a)

(carr b) * (carr b) is Element of K19( the carrier of a)

{ (b

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 * b is Element of K19( the carrier of a)

(carr b) * (carr b) is Element of K19( the carrier of a)

{ (b

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 * b is Element of K19( the carrier of a)

(carr b) * (carr b) is Element of K19( the carrier of a)

{ (b

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 * a is Element of K19( the carrier of G)

(carr b) * (carr a) is Element of K19( the carrier of G)

{ (b

(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

(((