:: GROUP_8 semantic presentation

REAL is set

NAT is V6() V7() V8() non empty Element of bool REAL

bool REAL is non empty set

COMPLEX is set

RAT is set

INT is set

[:COMPLEX,COMPLEX:] is set

bool [:COMPLEX,COMPLEX:] is non empty set

[:[:COMPLEX,COMPLEX:],COMPLEX:] is set

bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set

[:REAL,REAL:] is set

bool [:REAL,REAL:] is non empty set

[:[:REAL,REAL:],REAL:] is set

bool [:[:REAL,REAL:],REAL:] is non empty set

[:RAT,RAT:] is set

bool [:RAT,RAT:] is non empty set

[:[:RAT,RAT:],RAT:] is set

bool [:[:RAT,RAT:],RAT:] is non empty set

[:INT,INT:] is set

bool [:INT,INT:] is non empty set

[:[:INT,INT:],INT:] is set

bool [:[:INT,INT:],INT:] is non empty set

[:NAT,NAT:] is non empty set

[:[:NAT,NAT:],NAT:] is non empty set

bool [:[:NAT,NAT:],NAT:] is non empty set

NAT is V6() V7() V8() non empty set

bool NAT is non empty set

bool NAT is non empty set

2 is V6() V7() V8() V12() non empty V31() V32() integer ext-real positive non negative Element of NAT

[:2,2:] is non empty set

[:[:2,2:],2:] is non empty set

bool [:[:2,2:],2:] is non empty set

K484() is non empty strict unital Group-like V109() V111() cyclic multMagma

the carrier of K484() is non empty V180() set

{} is V6() V7() V8() V10() V11() V12() functional empty V31() V32() integer finite V40() FinSequence-membered ext-real non positive non negative set

1 is V6() V7() V8() V12() non empty V31() V32() integer ext-real positive non negative Element of NAT

3 is V6() V7() V8() V12() non empty V31() V32() integer ext-real positive non negative Element of NAT

0 is V6() V7() V8() V10() V11() V12() functional empty V31() V32() integer finite V40() FinSequence-membered ext-real non positive non negative Element of NAT

K174(1) is V31() V32() integer ext-real non positive Element of INT

K110(1) is V31() V32() integer ext-real non positive Element of REAL

G is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

H is non empty finite strict unital Group-like V109() multMagma

card H is V6() V7() V8() V12() non empty V31() V32() integer cardinal ext-real positive non negative Element of NAT

the carrier of H is non empty finite set

card the carrier of H is cardinal set

G is non empty unital Group-like V109() multMagma

the carrier of G is non empty set

H is non empty unital Group-like V109() Subgroup of G

the carrier of H is non empty set

b is Element of the carrier of H

m is Element of the carrier of H

b * m is Element of the carrier of H

the multF of H is Relation-like [: the carrier of H, the carrier of H:] -defined the carrier of H -valued Function-like V25([: the carrier of H, the carrier of H:], the carrier of H) V29( the carrier of H) Element of bool [:[: the carrier of H, the carrier of H:], the carrier of H:]

[: the carrier of H, the carrier of H:] is non empty set

[:[: the carrier of H, the carrier of H:], the carrier of H:] is non empty set

bool [:[: the carrier of H, the carrier of H:], the carrier of H:] is non empty set

K94( the carrier of H, the multF of H,b,m) is Element of the carrier of H

c is Element of the carrier of G

c is Element of the carrier of G

c * c is Element of the carrier of G

the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V25([: the carrier of G, the carrier of G:], the carrier of G) V29( the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

K94( the carrier of G, the multF of G,c,c) is Element of the carrier of G

dom the multF of G is Relation-like set

the multF of G || the carrier of H is set

the multF of G | [: the carrier of H, the carrier of H:] is Relation-like set

G is non empty unital Group-like V109() multMagma

H is non empty unital Group-like V109() Subgroup of G

the carrier of H is non empty set

the carrier of G is non empty set

b is Element of the carrier of H

m is Element of the carrier of G

c is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

b |^ c is Element of the carrier of H

m |^ c is Element of the carrier of G

G is non empty unital Group-like V109() multMagma

H is non empty unital Group-like V109() Subgroup of G

the carrier of H is non empty set

the carrier of G is non empty set

b is Element of the carrier of H

m is Element of the carrier of G

c is V31() V32() integer ext-real set

b |^ c is Element of the carrier of H

m |^ c is Element of the carrier of G

G is non empty unital Group-like V109() multMagma

the carrier of G is non empty set

H is non empty unital Group-like V109() Subgroup of G

the carrier of H is non empty set

b is Element of the carrier of H

ord b is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

m is Element of the carrier of G

ord m is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

b |^ (ord b) is Element of the carrier of H

1_ H is non being_of_order_0 Element of the carrier of H

m |^ (ord m) is Element of the carrier of G

1_ G is non being_of_order_0 Element of the carrier of G

m |^ (ord b) is Element of the carrier of G

b |^ (ord m) is Element of the carrier of H

G is non empty unital Group-like V109() multMagma

the carrier of G is non empty set

H is non empty unital Group-like V109() Subgroup of G

the carrier of H is non empty set

b is Element of the carrier of G

H * b is Element of bool the carrier of G

bool the carrier of G is non empty set

m is set

c is Element of the carrier of G

c * b is Element of the carrier of G

the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V25([: the carrier of G, the carrier of G:], the carrier of G) V29( the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

K94( the carrier of G, the multF of G,c,b) is Element of the carrier of G

G is non empty unital Group-like V109() multMagma

the carrier of G is non empty set

1_ G is non being_of_order_0 Element of the carrier of G

(1). G is non empty finite strict unital Group-like V109() V111() cyclic Subgroup of G

H is Element of the carrier of G

{H} is non empty finite Element of bool the carrier of G

bool the carrier of G is non empty set

gr {H} is non empty strict unital Group-like V109() Subgroup of G

the carrier of ((1). G) is non empty finite set

{(1_ G)} is non empty finite Element of bool the carrier of G

the carrier of (gr {H}) is non empty set

b is set

G is non empty unital Group-like V109() multMagma

H is V31() V32() integer ext-real set

1_ G is non being_of_order_0 Element of the carrier of G

the carrier of G is non empty set

(1_ G) |^ H is Element of the carrier of G

G is non empty strict unital Group-like V109() multMagma

the carrier of G is non empty set

1_ G is non being_of_order_0 Element of the carrier of G

H is Element of the carrier of G

ord H is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

b is V31() V32() integer ext-real set

b * (ord H) is V31() V32() integer ext-real set

H |^ (b * (ord H)) is Element of the carrier of G

H |^ (ord H) is Element of the carrier of G

(1_ G) |^ b is Element of the carrier of G

G is non empty strict unital Group-like V109() multMagma

the carrier of G is non empty set

H is Element of the carrier of G

ord H is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

b is V31() V32() integer ext-real set

H |^ b is Element of the carrier of G

b mod (ord H) is V31() V32() integer ext-real set

H |^ (b mod (ord H)) is Element of the carrier of G

b div (ord H) is V31() V32() integer ext-real set

(b div (ord H)) * (ord H) is V31() V32() integer ext-real set

b - ((b div (ord H)) * (ord H)) is V31() V32() integer ext-real set

1 * (b div (ord H)) is V31() V32() integer ext-real set

(1 * (b div (ord H))) * (ord H) is V31() V32() integer ext-real set

- ((1 * (b div (ord H))) * (ord H)) is V31() V32() integer ext-real set

b + (- ((1 * (b div (ord H))) * (ord H))) is V31() V32() integer ext-real set

H |^ (b + (- ((1 * (b div (ord H))) * (ord H)))) is Element of the carrier of G

- (b div (ord H)) is V31() V32() integer ext-real set

(- (b div (ord H))) * (ord H) is V31() V32() integer ext-real set

H |^ ((- (b div (ord H))) * (ord H)) is Element of the carrier of G

(H |^ b) * (H |^ ((- (b div (ord H))) * (ord H))) is Element of the carrier of G

the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V25([: the carrier of G, the carrier of G:], the carrier of G) V29( the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

K94( the carrier of G, the multF of G,(H |^ b),(H |^ ((- (b div (ord H))) * (ord H)))) is Element of the carrier of G

1_ G is non being_of_order_0 Element of the carrier of G

(H |^ b) * (1_ G) is Element of the carrier of G

K94( the carrier of G, the multF of G,(H |^ b),(1_ G)) is Element of the carrier of G

G is non empty strict unital Group-like V109() multMagma

the carrier of G is non empty set

H is Element of the carrier of G

{H} is non empty finite Element of bool the carrier of G

bool the carrier of G is non empty set

gr {H} is non empty strict unital Group-like V109() Subgroup of G

ord H is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

b is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len b is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

dom b is finite Element of bool NAT

Seg (ord H) is finite ord H -element Element of bool NAT

the carrier of (gr {H}) is non empty set

rng b is finite set

m is set

c is Element of the carrier of G

c is V31() V32() integer ext-real set

H |^ c is Element of the carrier of G

c mod (ord H) is V31() V32() integer ext-real set

t is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

H |^ t is Element of the carrier of G

0 + 1 is V6() V7() V8() V12() non empty V31() V32() integer ext-real positive non negative Element of NAT

1_ G is non being_of_order_0 Element of the carrier of G

H |^ (ord H) is Element of the carrier of G

b . (ord H) is set

0 + 1 is V6() V7() V8() V12() non empty V31() V32() integer ext-real positive non negative Element of NAT

b . t is set

G is non empty strict unital Group-like V109() multMagma

the carrier of G is non empty set

H is Element of the carrier of G

H " is Element of the carrier of G

1_ G is non being_of_order_0 Element of the carrier of G

b is V6() V7() V8() V12() V31() V32() integer ext-real non negative set

(H ") |^ b is Element of the carrier of G

H |^ b is Element of the carrier of G

(H |^ b) " is Element of the carrier of G

(1_ G) " is Element of the carrier of G

G is non empty strict unital Group-like V109() multMagma

the carrier of G is non empty set

1_ G is non being_of_order_0 Element of the carrier of G

H is Element of the carrier of G

b is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

- b is V31() V32() integer ext-real non positive set

H |^ (- b) is Element of the carrier of G

H |^ b is Element of the carrier of G

(H |^ b) " is Element of the carrier of G

H " is Element of the carrier of G

(H ") |^ b is Element of the carrier of G

b is V31() V32() integer ext-real set

H |^ b is Element of the carrier of G

m is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

- m is V31() V32() integer ext-real non positive set

b is V31() V32() integer ext-real set

H |^ b is Element of the carrier of G

b is V6() V7() V8() V12() V31() V32() integer ext-real non negative set

H |^ b is Element of the carrier of G

G is non empty strict unital Group-like V109() multMagma

the carrier of G is non empty set

1_ G is non being_of_order_0 Element of the carrier of G

(1). G is non empty finite strict unital Group-like V109() V111() cyclic Subgroup of G

card G is cardinal set

card the carrier of G is cardinal set

H is Element of the carrier of G

H is Element of the carrier of G

{H} is non empty finite Element of bool the carrier of G

bool the carrier of G is non empty set

gr {H} is non empty strict unital Group-like V109() Subgroup of G

H |^ 2 is Element of the carrier of G

{(H |^ 2)} is non empty finite Element of bool the carrier of G

gr {(H |^ 2)} is non empty strict unital Group-like V109() Subgroup of G

b is V31() V32() integer ext-real set

(H |^ 2) |^ b is Element of the carrier of G

2 * b is V31() V32() integer ext-real set

H |^ (2 * b) is Element of the carrier of G

H " is Element of the carrier of G

(H ") * (H |^ (2 * b)) is Element of the carrier of G

the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V25([: the carrier of G, the carrier of G:], the carrier of G) V29( the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

K94( the carrier of G, the multF of G,(H "),(H |^ (2 * b))) is Element of the carrier of G

- 1 is V31() V32() integer ext-real non positive set

H |^ (- 1) is Element of the carrier of G

(H |^ (- 1)) * (H |^ (2 * b)) is Element of the carrier of G

K94( the carrier of G, the multF of G,(H |^ (- 1)),(H |^ (2 * b))) is Element of the carrier of G

(- 1) + (2 * b) is V31() V32() integer ext-real set

H |^ ((- 1) + (2 * b)) is Element of the carrier of G

ord H is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

b is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

m is V6() V7() V8() V12() V31() V32() integer ext-real non negative set

m is V6() V7() V8() V12() V31() V32() integer ext-real non negative set

c is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

c is V6() V7() V8() V12() V31() V32() integer ext-real non negative set

c * c is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

t is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

a is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

r is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

t * r is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

b div 0 is V31() V32() integer ext-real set

0 * (b div 0) is V31() V32() integer ext-real set

0 + 1 is V6() V7() V8() V12() non empty V31() V32() integer ext-real positive non negative Element of NAT

m is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

c is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

m * c is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

m is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

c is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

m * c is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

H |^ c is Element of the carrier of G

ord (H |^ c) is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

{(H |^ c)} is non empty finite Element of bool the carrier of G

gr {(H |^ c)} is non empty strict unital Group-like V109() Subgroup of G

card (gr {(H |^ c)}) is cardinal set

the carrier of (gr {(H |^ c)}) is non empty set

card the carrier of (gr {(H |^ c)}) is cardinal set

H is non empty strict unital Group-like V109() Subgroup of G

b is non empty finite unital Group-like V109() multMagma

card b is V6() V7() V8() V12() non empty V31() V32() integer cardinal ext-real positive non negative Element of NAT

the carrier of b is non empty finite set

card the carrier of b is cardinal set

m is non empty finite unital Group-like V109() Subgroup of b

card m is V6() V7() V8() V12() non empty V31() V32() integer cardinal ext-real positive non negative Element of NAT

the carrier of m is non empty finite set

card the carrier of m is cardinal set

index m is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

(card m) * (index m) is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

c is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

G is non empty unital Group-like V109() multMagma

the carrier of G is non empty set

bool the carrier of G is non empty set

m is Element of the carrier of G

b is Element of the carrier of G

H is Element of the carrier of G

c is Element of bool the carrier of G

H * c is Element of bool the carrier of G

(H * c) * b is Element of bool the carrier of G

c is Element of the carrier of G

c * b is Element of the carrier of G

the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V25([: the carrier of G, the carrier of G:], the carrier of G) V29( the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

K94( the carrier of G, the multF of G,c,b) is Element of the carrier of G

a is Element of the carrier of G

H * a is Element of the carrier of G

K94( the carrier of G, the multF of G,H,a) is Element of the carrier of G

(H * a) * b is Element of the carrier of G

K94( the carrier of G, the multF of G,(H * a),b) is Element of the carrier of G

c is Element of the carrier of G

H * c is Element of the carrier of G

the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V25([: the carrier of G, the carrier of G:], the carrier of G) V29( the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

K94( the carrier of G, the multF of G,H,c) is Element of the carrier of G

(H * c) * b is Element of the carrier of G

K94( the carrier of G, the multF of G,(H * c),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

K94( the carrier of G, the multF of G,a,b) is Element of the carrier of G

G is non empty unital Group-like V109() multMagma

the carrier of G is non empty set

bool the carrier of G is non empty set

H is non empty Element of bool the carrier of G

card H is cardinal set

b is Element of the carrier of G

b " is Element of the carrier of G

(b ") * H is Element of bool the carrier of G

((b ") * H) * b is Element of bool the carrier of G

card (((b ") * H) * b) is cardinal set

the Element of H is Element of H

(b ") * the Element of H is Element of the carrier of G

the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V25([: the carrier of G, the carrier of G:], the carrier of G) V29( the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

K94( the carrier of G, the multF of G,(b "), the Element of H) is Element of the carrier of G

((b ") * the Element of H) * b is Element of the carrier of G

K94( the carrier of G, the multF of G,((b ") * the Element of H),b) is Element of the carrier of G

[:H, the carrier of G:] is non empty set

bool [:H, the carrier of G:] is non empty set

c is Relation-like H -defined the carrier of G -valued Function-like V25(H, the carrier of G) Element of bool [:H, the carrier of G:]

dom c is set

rng c is set

c is non empty Element of bool the carrier of G

a is set

t is set

c . t is set

r is Element of H

(b ") * r is Element of the carrier of G

the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V25([: the carrier of G, the carrier of G:], the carrier of G) V29( the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

K94( the carrier of G, the multF of G,(b "),r) is Element of the carrier of G

((b ") * r) * b is Element of the carrier of G

K94( the carrier of G, the multF of G,((b ") * r),b) is Element of the carrier of G

a is set

t is Element of the carrier of G

(b ") * t is Element of the carrier of G

the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V25([: the carrier of G, the carrier of G:], the carrier of G) V29( the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

K94( the carrier of G, the multF of G,(b "),t) is Element of the carrier of G

((b ") * t) * b is Element of the carrier of G

K94( the carrier of G, the multF of G,((b ") * t),b) is Element of the carrier of G

c . t is set

r is Element of the carrier of G

c . r is set

[:H,c:] is non empty set

bool [:H,c:] is non empty set

[:c, the carrier of G:] is non empty set

bool [:c, the carrier of G:] is non empty set

t is Relation-like c -defined the carrier of G -valued Function-like V25(c, the carrier of G) Element of bool [:c, the carrier of G:]

dom t is set

rng t is set

r is set

s is set

t . s is set

s is Element of c

b * s is Element of the carrier of G

the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V25([: the carrier of G, the carrier of G:], the carrier of G) V29( the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

K94( the carrier of G, the multF of G,b,s) is Element of the carrier of G

(b * s) * (b ") is Element of the carrier of G

K94( the carrier of G, the multF of G,(b * s),(b ")) is Element of the carrier of G

u is Element of the carrier of G

(b ") * u is Element of the carrier of G

K94( the carrier of G, the multF of G,(b "),u) is Element of the carrier of G

((b ") * u) * b is Element of the carrier of G

K94( the carrier of G, the multF of G,((b ") * u),b) is Element of the carrier of G

b * ((b ") * u) is Element of the carrier of G

K94( the carrier of G, the multF of G,b,((b ") * u)) is Element of the carrier of G

(b * ((b ") * u)) * b is Element of the carrier of G

K94( the carrier of G, the multF of G,(b * ((b ") * u)),b) is Element of the carrier of G

((b * ((b ") * u)) * b) * (b ") is Element of the carrier of G

K94( the carrier of G, the multF of G,((b * ((b ") * u)) * b),(b ")) is Element of the carrier of G

b * (b ") is Element of the carrier of G

K94( the carrier of G, the multF of G,b,(b ")) is Element of the carrier of G

(b * (b ")) * u is Element of the carrier of G

K94( the carrier of G, the multF of G,(b * (b ")),u) is Element of the carrier of G

((b * (b ")) * u) * b is Element of the carrier of G

K94( the carrier of G, the multF of G,((b * (b ")) * u),b) is Element of the carrier of G

(((b * (b ")) * u) * b) * (b ") is Element of the carrier of G

K94( the carrier of G, the multF of G,(((b * (b ")) * u) * b),(b ")) is Element of the carrier of G

((b * (b ")) * u) * (b * (b ")) is Element of the carrier of G

K94( the carrier of G, the multF of G,((b * (b ")) * u),(b * (b "))) is Element of the carrier of G

1_ G is non being_of_order_0 Element of the carrier of G

(1_ G) * u is Element of the carrier of G

K94( the carrier of G, the multF of G,(1_ G),u) is Element of the carrier of G

((1_ G) * u) * (b * (b ")) is Element of the carrier of G

K94( the carrier of G, the multF of G,((1_ G) * u),(b * (b "))) is Element of the carrier of G

((1_ G) * u) * (1_ G) is Element of the carrier of G

K94( the carrier of G, the multF of G,((1_ G) * u),(1_ G)) is Element of the carrier of G

[:c,H:] is non empty set

bool [:c,H:] is non empty set

a is Relation-like H -defined c -valued Function-like V25(H,c) Element of bool [:H,c:]

s is Element of H

a . s is Element of c

s is Element of H

a . s is Element of c

(b ") * s is Element of the carrier of G

the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V25([: the carrier of G, the carrier of G:], the carrier of G) V29( the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

K94( the carrier of G, the multF of G,(b "),s) is Element of the carrier of G

((b ") * s) * b is Element of the carrier of G

K94( the carrier of G, the multF of G,((b ") * s),b) is Element of the carrier of G

(b ") * s is Element of the carrier of G

K94( the carrier of G, the multF of G,(b "),s) is Element of the carrier of G

((b ") * s) * b is Element of the carrier of G

K94( the carrier of G, the multF of G,((b ") * s),b) is Element of the carrier of G

r is Relation-like c -defined H -valued Function-like V25(c,H) Element of bool [:c,H:]

r . (a . s) is Element of H

r . (((b ") * s) * b) is set

b * (((b ") * s) * b) is Element of the carrier of G

K94( the carrier of G, the multF of G,b,(((b ") * s) * b)) is Element of the carrier of G

(b * (((b ") * s) * b)) * (b ") is Element of the carrier of G

K94( the carrier of G, the multF of G,(b * (((b ") * s) * b)),(b ")) is Element of the carrier of G

b * ((b ") * s) is Element of the carrier of G

K94( the carrier of G, the multF of G,b,((b ") * s)) is Element of the carrier of G

(b * ((b ") * s)) * b is Element of the carrier of G

K94( the carrier of G, the multF of G,(b * ((b ") * s)),b) is Element of the carrier of G

((b * ((b ") * s)) * b) * (b ") is Element of the carrier of G

K94( the carrier of G, the multF of G,((b * ((b ") * s)) * b),(b ")) is Element of the carrier of G

b * (b ") is Element of the carrier of G

K94( the carrier of G, the multF of G,b,(b ")) is Element of the carrier of G

(b * (b ")) * s is Element of the carrier of G

K94( the carrier of G, the multF of G,(b * (b ")),s) is Element of the carrier of G

((b * (b ")) * s) * b is Element of the carrier of G

K94( the carrier of G, the multF of G,((b * (b ")) * s),b) is Element of the carrier of G

(((b * (b ")) * s) * b) * (b ") is Element of the carrier of G

K94( the carrier of G, the multF of G,(((b * (b ")) * s) * b),(b ")) is Element of the carrier of G

((b * (b ")) * s) * (b * (b ")) is Element of the carrier of G

K94( the carrier of G, the multF of G,((b * (b ")) * s),(b * (b "))) is Element of the carrier of G

1_ G is non being_of_order_0 Element of the carrier of G

(1_ G) * s is Element of the carrier of G

K94( the carrier of G, the multF of G,(1_ G),s) is Element of the carrier of G

((1_ G) * s) * (b * (b ")) is Element of the carrier of G

K94( the carrier of G, the multF of G,((1_ G) * s),(b * (b "))) is Element of the carrier of G

s * (b * (b ")) is Element of the carrier of G

K94( the carrier of G, the multF of G,s,(b * (b "))) is Element of the carrier of G

s * (1_ G) is Element of the carrier of G

K94( the carrier of G, the multF of G,s,(1_ G)) is Element of the carrier of G

r . (a . s) is Element of H

r . (((b ") * s) * b) is set

b * (((b ") * s) * b) is Element of the carrier of G

K94( the carrier of G, the multF of G,b,(((b ") * s) * b)) is Element of the carrier of G

(b * (((b ") * s) * b)) * (b ") is Element of the carrier of G

K94( the carrier of G, the multF of G,(b * (((b ") * s) * b)),(b ")) is Element of the carrier of G

b * ((b ") * s) is Element of the carrier of G

K94( the carrier of G, the multF of G,b,((b ") * s)) is Element of the carrier of G

(b * ((b ") * s)) * b is Element of the carrier of G

K94( the carrier of G, the multF of G,(b * ((b ") * s)),b) is Element of the carrier of G

((b * ((b ") * s)) * b) * (b ") is Element of the carrier of G

K94( the carrier of G, the multF of G,((b * ((b ") * s)) * b),(b ")) is Element of the carrier of G

(b * (b ")) * s is Element of the carrier of G

K94( the carrier of G, the multF of G,(b * (b ")),s) is Element of the carrier of G

((b * (b ")) * s) * b is Element of the carrier of G

K94( the carrier of G, the multF of G,((b * (b ")) * s),b) is Element of the carrier of G

(((b * (b ")) * s) * b) * (b ") is Element of the carrier of G

K94( the carrier of G, the multF of G,(((b * (b ")) * s) * b),(b ")) is Element of the carrier of G

((b * (b ")) * s) * (b * (b ")) is Element of the carrier of G

K94( the carrier of G, the multF of G,((b * (b ")) * s),(b * (b "))) is Element of the carrier of G

(1_ G) * s is Element of the carrier of G

K94( the carrier of G, the multF of G,(1_ G),s) is Element of the carrier of G

((1_ G) * s) * (b * (b ")) is Element of the carrier of G

K94( the carrier of G, the multF of G,((1_ G) * s),(b * (b "))) is Element of the carrier of G

s * (b * (b ")) is Element of the carrier of G

K94( the carrier of G, the multF of G,s,(b * (b "))) is Element of the carrier of G

s * (1_ G) is Element of the carrier of G

K94( the carrier of G, the multF of G,s,(1_ G)) is Element of the carrier of G

dom a is set

rng a is set

G is non empty strict unital Group-like V109() multMagma

the carrier of G is non empty set

bool the carrier of G is non empty set

bool (bool the carrier of G) is non empty set

b is non empty strict unital Group-like V109() Subgroup of G

H is non empty strict unital Group-like V109() Subgroup of G

m is Element of bool (bool the carrier of G)

m is Element of bool (bool the carrier of G)

c is Element of bool (bool the carrier of G)

G is non empty strict unital Group-like V109() multMagma

the carrier of G is non empty set

H is Element of the carrier of G

b is Element of the carrier of G

m is non empty strict unital Group-like V109() Subgroup of G

m * b is Element of bool the carrier of G

bool the carrier of G is non empty set

c is non empty strict unital Group-like V109() Subgroup of G

(m * b) * c is Element of bool the carrier of G

c is Element of the carrier of G

a is Element of the carrier of G

c * a is Element of the carrier of G

the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V25([: the carrier of G, the carrier of G:], the carrier of G) V29( the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

K94( the carrier of G, the multF of G,c,a) is Element of the carrier of G

t is Element of the carrier of G

t * b is Element of the carrier of G

K94( the carrier of G, the multF of G,t,b) is Element of the carrier of G

c is Element of the carrier of G

c * b is Element of the carrier of G

the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V25([: the carrier of G, the carrier of G:], the carrier of G) V29( the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

K94( the carrier of G, the multF of G,c,b) is Element of the carrier of G

a is Element of the carrier of G

(c * b) * a is Element of the carrier of G

K94( the carrier of G, the multF of G,(c * b),a) is Element of the carrier of G

t is Element of the carrier of G

r is Element of the carrier of G

t * r is Element of the carrier of G

K94( the carrier of G, the multF of G,t,r) is Element of the carrier of G

G is non empty strict unital Group-like V109() multMagma

the carrier of G is non empty set

H is Element of the carrier of G

b is Element of the carrier of G

m is non empty strict unital Group-like V109() Subgroup of G

m * H is Element of bool the carrier of G

bool the carrier of G is non empty set

m * b is Element of bool the carrier of G

c is non empty strict unital Group-like V109() Subgroup of G

(m * H) * c is Element of bool the carrier of G

(m * b) * c is Element of bool the carrier of G

c is Element of the carrier of G

c is Element of the carrier of G

c is Element of the carrier of G

a is Element of the carrier of G

a * H is Element of the carrier of G

the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V25([: the carrier of G, the carrier of G:], the carrier of G) V29( the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

K94( the carrier of G, the multF of G,a,H) is Element of the carrier of G

t is Element of the carrier of G

(a * H) * t is Element of the carrier of G

K94( the carrier of G, the multF of G,(a * H),t) is Element of the carrier of G

r is Element of the carrier of G

r * b is Element of the carrier of G

K94( the carrier of G, the multF of G,r,b) is Element of the carrier of G

s is Element of the carrier of G

(r * b) * s is Element of the carrier of G

K94( the carrier of G, the multF of G,(r * b),s) is Element of the carrier of G

s is set

u is Element of the carrier of G

u * H is Element of the carrier of G

K94( the carrier of G, the multF of G,u,H) is Element of the carrier of G

v is Element of the carrier of G

(u * H) * v is Element of the carrier of G

K94( the carrier of G, the multF of G,(u * H),v) is Element of the carrier of G

1_ G is non being_of_order_0 Element of the carrier of G

u * (1_ G) is Element of the carrier of G

K94( the carrier of G, the multF of G,u,(1_ G)) is Element of the carrier of G

(u * (1_ G)) * H is Element of the carrier of G

K94( the carrier of G, the multF of G,(u * (1_ G)),H) is Element of the carrier of G

((u * (1_ G)) * H) * (1_ G) is Element of the carrier of G

K94( the carrier of G, the multF of G,((u * (1_ G)) * H),(1_ G)) is Element of the carrier of G

(((u * (1_ G)) * H) * (1_ G)) * v is Element of the carrier of G

K94( the carrier of G, the multF of G,(((u * (1_ G)) * H) * (1_ G)),v) is Element of the carrier of G

a " is Element of the carrier of G

(a ") * a is Element of the carrier of G

K94( the carrier of G, the multF of G,(a "),a) is Element of the carrier of G

u * ((a ") * a) is Element of the carrier of G

K94( the carrier of G, the multF of G,u,((a ") * a)) is Element of the carrier of G

(u * ((a ") * a)) * H is Element of the carrier of G

K94( the carrier of G, the multF of G,(u * ((a ") * a)),H) is Element of the carrier of G

t " is Element of the carrier of G

t * (t ") is Element of the carrier of G

K94( the carrier of G, the multF of G,t,(t ")) is Element of the carrier of G

((u * ((a ") * a)) * H) * (t * (t ")) is Element of the carrier of G

K94( the carrier of G, the multF of G,((u * ((a ") * a)) * H),(t * (t "))) is Element of the carrier of G

(((u * ((a ") * a)) * H) * (t * (t "))) * v is Element of the carrier of G

K94( the carrier of G, the multF of G,(((u * ((a ") * a)) * H) * (t * (t "))),v) is Element of the carrier of G

((u * ((a ") * a)) * H) * t is Element of the carrier of G

K94( the carrier of G, the multF of G,((u * ((a ") * a)) * H),t) is Element of the carrier of G

(((u * ((a ") * a)) * H) * t) * (t ") is Element of the carrier of G

K94( the carrier of G, the multF of G,(((u * ((a ") * a)) * H) * t),(t ")) is Element of the carrier of G

((((u * ((a ") * a)) * H) * t) * (t ")) * v is Element of the carrier of G

K94( the carrier of G, the multF of G,((((u * ((a ") * a)) * H) * t) * (t ")),v) is Element of the carrier of G

u * (a ") is Element of the carrier of G

K94( the carrier of G, the multF of G,u,(a ")) is Element of the carrier of G

(u * (a ")) * a is Element of the carrier of G

K94( the carrier of G, the multF of G,(u * (a ")),a) is Element of the carrier of G

((u * (a ")) * a) * H is Element of the carrier of G

K94( the carrier of G, the multF of G,((u * (a ")) * a),H) is Element of the carrier of G

(((u * (a ")) * a) * H) * t is Element of the carrier of G

K94( the carrier of G, the multF of G,(((u * (a ")) * a) * H),t) is Element of the carrier of G

((((u * (a ")) * a) * H) * t) * (t ") is Element of the carrier of G

K94( the carrier of G, the multF of G,((((u * (a ")) * a) * H) * t),(t ")) is Element of the carrier of G

(((((u * (a ")) * a) * H) * t) * (t ")) * v is Element of the carrier of G

K94( the carrier of G, the multF of G,(((((u * (a ")) * a) * H) * t) * (t ")),v) is Element of the carrier of G

(u * (a ")) * (a * H) is Element of the carrier of G

K94( the carrier of G, the multF of G,(u * (a ")),(a * H)) is Element of the carrier of G

((u * (a ")) * (a * H)) * t is Element of the carrier of G

K94( the carrier of G, the multF of G,((u * (a ")) * (a * H)),t) is Element of the carrier of G

(((u * (a ")) * (a * H)) * t) * (t ") is Element of the carrier of G

K94( the carrier of G, the multF of G,(((u * (a ")) * (a * H)) * t),(t ")) is Element of the carrier of G

((((u * (a ")) * (a * H)) * t) * (t ")) * v is Element of the carrier of G

K94( the carrier of G, the multF of G,((((u * (a ")) * (a * H)) * t) * (t ")),v) is Element of the carrier of G

(u * (a ")) * ((r * b) * s) is Element of the carrier of G

K94( the carrier of G, the multF of G,(u * (a ")),((r * b) * s)) is Element of the carrier of G

((u * (a ")) * ((r * b) * s)) * (t ") is Element of the carrier of G

K94( the carrier of G, the multF of G,((u * (a ")) * ((r * b) * s)),(t ")) is Element of the carrier of G

(((u * (a ")) * ((r * b) * s)) * (t ")) * v is Element of the carrier of G

K94( the carrier of G, the multF of G,(((u * (a ")) * ((r * b) * s)) * (t ")),v) is Element of the carrier of G

(u * (a ")) * (r * b) is Element of the carrier of G

K94( the carrier of G, the multF of G,(u * (a ")),(r * b)) is Element of the carrier of G

((u * (a ")) * (r * b)) * s is Element of the carrier of G

K94( the carrier of G, the multF of G,((u * (a ")) * (r * b)),s) is Element of the carrier of G

(((u * (a ")) * (r * b)) * s) * (t ") is Element of the carrier of G

K94( the carrier of G, the multF of G,(((u * (a ")) * (r * b)) * s),(t ")) is Element of the carrier of G

((((u * (a ")) * (r * b)) * s) * (t ")) * v is Element of the carrier of G

K94( the carrier of G, the multF of G,((((u * (a ")) * (r * b)) * s) * (t ")),v) is Element of the carrier of G

(u * (a ")) * r is Element of the carrier of G

K94( the carrier of G, the multF of G,(u * (a ")),r) is Element of the carrier of G

((u * (a ")) * r) * b is Element of the carrier of G

K94( the carrier of G, the multF of G,((u * (a ")) * r),b) is Element of the carrier of G

(((u * (a ")) * r) * b) * s is Element of the carrier of G

K94( the carrier of G, the multF of G,(((u * (a ")) * r) * b),s) is Element of the carrier of G

((((u * (a ")) * r) * b) * s) * (t ") is Element of the carrier of G

K94( the carrier of G, the multF of G,((((u * (a ")) * r) * b) * s),(t ")) is Element of the carrier of G

(((((u * (a ")) * r) * b) * s) * (t ")) * v is Element of the carrier of G

K94( the carrier of G, the multF of G,(((((u * (a ")) * r) * b) * s) * (t ")),v) is Element of the carrier of G

s * (t ") is Element of the carrier of G

K94( the carrier of G, the multF of G,s,(t ")) is Element of the carrier of G

(((u * (a ")) * r) * b) * (s * (t ")) is Element of the carrier of G

K94( the carrier of G, the multF of G,(((u * (a ")) * r) * b),(s * (t "))) is Element of the carrier of G

((((u * (a ")) * r) * b) * (s * (t "))) * v is Element of the carrier of G

K94( the carrier of G, the multF of G,((((u * (a ")) * r) * b) * (s * (t "))),v) is Element of the carrier of G

(s * (t ")) * v is Element of the carrier of G

K94( the carrier of G, the multF of G,(s * (t ")),v) is Element of the carrier of G

(((u * (a ")) * r) * b) * ((s * (t ")) * v) is Element of the carrier of G

K94( the carrier of G, the multF of G,(((u * (a ")) * r) * b),((s * (t ")) * v)) is Element of the carrier of G

c

c

K94( the carrier of G, the multF of G,c

c

(c

K94( the carrier of G, the multF of G,(c

s is set

u is Element of the carrier of G

u * b is Element of the carrier of G

K94( the carrier of G, the multF of G,u,b) is Element of the carrier of G

v is Element of the carrier of G

(u * b) * v is Element of the carrier of G

K94( the carrier of G, the multF of G,(u * b),v) is Element of the carrier of G

1_ G is non being_of_order_0 Element of the carrier of G

u * (1_ G) is Element of the carrier of G

K94( the carrier of G, the multF of G,u,(1_ G)) is Element of the carrier of G

(u * (1_ G)) * b is Element of the carrier of G

K94( the carrier of G, the multF of G,(u * (1_ G)),b) is Element of the carrier of G

((u * (1_ G)) * b) * (1_ G) is Element of the carrier of G

K94( the carrier of G, the multF of G,((u * (1_ G)) * b),(1_ G)) is Element of the carrier of G

(((u * (1_ G)) * b) * (1_ G)) * v is Element of the carrier of G

K94( the carrier of G, the multF of G,(((u * (1_ G)) * b) * (1_ G)),v) is Element of the carrier of G

r " is Element of the carrier of G

(r ") * r is Element of the carrier of G

K94( the carrier of G, the multF of G,(r "),r) is Element of the carrier of G

u * ((r ") * r) is Element of the carrier of G

K94( the carrier of G, the multF of G,u,((r ") * r)) is Element of the carrier of G

(u * ((r ") * r)) * b is Element of the carrier of G

K94( the carrier of G, the multF of G,(u * ((r ") * r)),b) is Element of the carrier of G

s " is Element of the carrier of G

s * (s ") is Element of the carrier of G

K94( the carrier of G, the multF of G,s,(s ")) is Element of the carrier of G

((u * ((r ") * r)) * b) * (s * (s ")) is Element of the carrier of G

K94( the carrier of G, the multF of G,((u * ((r ") * r)) * b),(s * (s "))) is Element of the carrier of G

(((u * ((r ") * r)) * b) * (s * (s "))) * v is Element of the carrier of G

K94( the carrier of G, the multF of G,(((u * ((r ") * r)) * b) * (s * (s "))),v) is Element of the carrier of G

((u * ((r ") * r)) * b) * s is Element of the carrier of G

K94( the carrier of G, the multF of G,((u * ((r ") * r)) * b),s) is Element of the carrier of G

(((u * ((r ") * r)) * b) * s) * (s ") is Element of the carrier of G

K94( the carrier of G, the multF of G,(((u * ((r ") * r)) * b) * s),(s ")) is Element of the carrier of G

((((u * ((r ") * r)) * b) * s) * (s ")) * v is Element of the carrier of G

K94( the carrier of G, the multF of G,((((u * ((r ") * r)) * b) * s) * (s ")),v) is Element of the carrier of G

u * (r ") is Element of the carrier of G

K94( the carrier of G, the multF of G,u,(r ")) is Element of the carrier of G

(u * (r ")) * r is Element of the carrier of G

K94( the carrier of G, the multF of G,(u * (r ")),r) is Element of the carrier of G

((u * (r ")) * r) * b is Element of the carrier of G

K94( the carrier of G, the multF of G,((u * (r ")) * r),b) is Element of the carrier of G

(((u * (r ")) * r) * b) * s is Element of the carrier of G

K94( the carrier of G, the multF of G,(((u * (r ")) * r) * b),s) is Element of the carrier of G

((((u * (r ")) * r) * b) * s) * (s ") is Element of the carrier of G

K94( the carrier of G, the multF of G,((((u * (r ")) * r) * b) * s),(s ")) is Element of the carrier of G

(((((u * (r ")) * r) * b) * s) * (s ")) * v is Element of the carrier of G

K94( the carrier of G, the multF of G,(((((u * (r ")) * r) * b) * s) * (s ")),v) is Element of the carrier of G

(u * (r ")) * (r * b) is Element of the carrier of G

K94( the carrier of G, the multF of G,(u * (r ")),(r * b)) is Element of the carrier of G

((u * (r ")) * (r * b)) * s is Element of the carrier of G

K94( the carrier of G, the multF of G,((u * (r ")) * (r * b)),s) is Element of the carrier of G

(((u * (r ")) * (r * b)) * s) * (s ") is Element of the carrier of G

K94( the carrier of G, the multF of G,(((u * (r ")) * (r * b)) * s),(s ")) is Element of the carrier of G

((((u * (r ")) * (r * b)) * s) * (s ")) * v is Element of the carrier of G

K94( the carrier of G, the multF of G,((((u * (r ")) * (r * b)) * s) * (s ")),v) is Element of the carrier of G

(u * (r ")) * ((a * H) * t) is Element of the carrier of G

K94( the carrier of G, the multF of G,(u * (r ")),((a * H) * t)) is Element of the carrier of G

((u * (r ")) * ((a * H) * t)) * (s ") is Element of the carrier of G

K94( the carrier of G, the multF of G,((u * (r ")) * ((a * H) * t)),(s ")) is Element of the carrier of G

(((u * (r ")) * ((a * H) * t)) * (s ")) * v is Element of the carrier of G

K94( the carrier of G, the multF of G,(((u * (r ")) * ((a * H) * t)) * (s ")),v) is Element of the carrier of G

(u * (r ")) * (a * H) is Element of the carrier of G

K94( the carrier of G, the multF of G,(u * (r ")),(a * H)) is Element of the carrier of G

((u * (r ")) * (a * H)) * t is Element of the carrier of G

K94( the carrier of G, the multF of G,((u * (r ")) * (a * H)),t) is Element of the carrier of G

(((u * (r ")) * (a * H)) * t) * (s ") is Element of the carrier of G

K94( the carrier of G, the multF of G,(((u * (r ")) * (a * H)) * t),(s ")) is Element of the carrier of G

((((u * (r ")) * (a * H)) * t) * (s ")) * v is Element of the carrier of G

K94( the carrier of G, the multF of G,((((u * (r ")) * (a * H)) * t) * (s ")),v) is Element of the carrier of G

(u * (r ")) * a is Element of the carrier of G

K94( the carrier of G, the multF of G,(u * (r ")),a) is Element of the carrier of G

((u * (r ")) * a) * H is Element of the carrier of G

K94( the carrier of G, the multF of G,((u * (r ")) * a),H) is Element of the carrier of G

(((u * (r ")) * a) * H) * t is Element of the carrier of G

K94( the carrier of G, the multF of G,(((u * (r ")) * a) * H),t) is Element of the carrier of G

((((u * (r ")) * a) * H) * t) * (s ") is Element of the carrier of G

K94( the carrier of G, the multF of G,((((u * (r ")) * a) * H) * t),(s ")) is Element of the carrier of G

(((((u * (r ")) * a) * H) * t) * (s ")) * v is Element of the carrier of G

K94( the carrier of G, the multF of G,(((((u * (r ")) * a) * H) * t) * (s ")),v) is Element of the carrier of G

t * (s ") is Element of the carrier of G

K94( the carrier of G, the multF of G,t,(s ")) is Element of the carrier of G

(((u * (r ")) * a) * H) * (t * (s ")) is Element of the carrier of G

K94( the carrier of G, the multF of G,(((u * (r ")) * a) * H),(t * (s "))) is Element of the carrier of G

((((u * (r ")) * a) * H) * (t * (s "))) * v is Element of the carrier of G

K94( the carrier of G, the multF of G,((((u * (r ")) * a) * H) * (t * (s "))),v) is Element of the carrier of G

(t * (s ")) * v is Element of the carrier of G

K94( the carrier of G, the multF of G,(t * (s ")),v) is Element of the carrier of G

(((u * (r ")) * a) * H) * ((t * (s ")) * v) is Element of the carrier of G

K94( the carrier of G, the multF of G,(((u * (r ")) * a) * H),((t * (s ")) * v)) is Element of the carrier of G

c

c

K94( the carrier of G, the multF of G,c

c

(c

K94( the carrier of G, the multF of G,(c

s is Element of the carrier of G

c is Element of the carrier of G

G is non empty unital Group-like V109() multMagma

H is non empty unital Group-like V109() Subgroup of G

Left_Cosets H is Element of bool (bool the carrier of G)

the carrier of G is non empty set

bool the carrier of G is non empty set

bool (bool the carrier of G) is non empty set

G is non empty unital Group-like V109() multMagma

G is non empty unital Group-like V109() multMagma

H is non empty unital Group-like V109() Subgroup of G

b is non empty unital Group-like V109() Subgroup of G

H /\ b is non empty strict unital Group-like V109() Subgroup of G

index b is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

m is non empty unital Group-like V109() Subgroup of H

index m is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

Left_Cosets b is non empty Element of bool (bool the carrier of G)

the carrier of G is non empty set

bool the carrier of G is non empty set

bool (bool the carrier of G) is non empty set

Left_Cosets m is non empty Element of bool (bool the carrier of H)

the carrier of H is non empty set

bool the carrier of H is non empty set

bool (bool the carrier of H) is non empty set

r is Element of the carrier of H

a is Element of the carrier of G

s is Element of the carrier of H

t is Element of the carrier of G

s " is Element of the carrier of H

t " is Element of the carrier of G

(s ") * r is Element of the carrier of H

the multF of H is Relation-like [: the carrier of H, the carrier of H:] -defined the carrier of H -valued Function-like V25([: the carrier of H, the carrier of H:], the carrier of H) V29( the carrier of H) Element of bool [:[: the carrier of H, the carrier of H:], the carrier of H:]

[: the carrier of H, the carrier of H:] is non empty set

[:[: the carrier of H, the carrier of H:], the carrier of H:] is non empty set

bool [:[: the carrier of H, the carrier of H:], the carrier of H:] is non empty set

K94( the carrier of H, the multF of H,(s "),r) is Element of the carrier of H

a * b is Element of bool the carrier of G

t * b is Element of bool the carrier of G

(t ") * a is Element of the carrier of G

the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V25([: the carrier of G, the carrier of G:], the carrier of G) V29( the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

K94( the carrier of G, the multF of G,(t "),a) is Element of the carrier of G

r * m is Element of bool the carrier of H

s * m is Element of bool the carrier of H

c is non empty finite set

c is non empty finite set

a is Element of c

t is Element of the carrier of H

t * m is Element of bool the carrier of H

r is Element of the carrier of G

r * b is Element of bool the carrier of G

s is Element of c

[:c,c:] is non empty finite set

bool [:c,c:] is non empty finite V40() set

a is Relation-like c -defined c -valued Function-like V25(c,c) finite Element of bool [:c,c:]

dom a is finite set

rng a is finite set

card c is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

card c is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

t is set

r is set

a . t is set

a . r is set

s is Element of c

a . s is Element of c

s is Element of c

a . s is Element of c

u is Element of the carrier of G

v is Element of the carrier of H

u * b is Element of bool the carrier of G

v * m is Element of bool the carrier of H

c

c

c

c

G is non empty finite unital Group-like V109() multMagma

H is non empty finite unital Group-like V109() Subgroup of G

index H is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

card G is V6() V7() V8() V12() non empty V31() V32() integer cardinal ext-real positive non negative Element of NAT

the carrier of G is non empty finite set

card the carrier of G is cardinal set

card H is V6() V7() V8() V12() non empty V31() V32() integer cardinal ext-real positive non negative Element of NAT

the carrier of H is non empty finite set

card the carrier of H is cardinal set

(card H) * (index H) is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

G is non empty unital Group-like V109() multMagma

H is non empty unital Group-like V109() Subgroup of G

b is non empty unital Group-like V109() Subgroup of H

m is non empty unital Group-like V109() Subgroup of H

b /\ m is non empty strict unital Group-like V109() Subgroup of H

index b is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

index m is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

c is non empty unital Group-like V109() Subgroup of b

index c is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

c is non empty unital Group-like V109() Subgroup of m

index c is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

a is non empty unital Group-like V109() Subgroup of H

index a is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

(index c) * (index m) is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

(index c) * (index b) is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

(index b) * (index c) is V6() V7() V8() V12() V31() V32() integer ext-real non negative set

t is V31() V32() integer ext-real set

(index m) * t is V31() V32() integer ext-real set

r is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

(index m) * r is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

t is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

(index m) * t is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

(index m) * (index c) is V6() V7() V8() V12() V31() V32() integer ext-real non negative set

t is V31() V32() integer ext-real set

(index b) * t is V31() V32() integer ext-real set

r is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

(index b) * r is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

t is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

(index b) * t is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

G is non empty unital Group-like V109() multMagma

the carrier of G is non empty set

H is non empty unital Group-like V109() Subgroup of G

b is Element of the carrier of G

m is V31() V32() integer ext-real set

b |^ m is Element of the carrier of G

c is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

- c is V31() V32() integer ext-real non positive set

b |^ 0 is Element of the carrier of G

1_ G is non being_of_order_0 Element of the carrier of G

c is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

b |^ c is Element of the carrier of G

c + 1 is V6() V7() V8() V12() non empty V31() V32() integer ext-real positive non negative Element of NAT

b |^ (c + 1) is Element of the carrier of G

(b |^ c) * b is Element of the carrier of G

the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V25([: the carrier of G, the carrier of G:], the carrier of G) V29( the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

K94( the carrier of G, the multF of G,(b |^ c),b) is Element of the carrier of G

b |^ 0 is Element of the carrier of G

1_ G is non being_of_order_0 Element of the carrier of G

- 0 is V6() V7() V8() V10() V11() V12() functional empty V31() V32() integer finite V40() FinSequence-membered ext-real non positive non negative set

b |^ (- 0) is Element of the carrier of G

c is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

- c is V31() V32() integer ext-real non positive set

b |^ (- c) is Element of the carrier of G

c + 1 is V6() V7() V8() V12() non empty V31() V32() integer ext-real positive non negative Element of NAT

- (c + 1) is V31() V32() integer ext-real non positive set

b |^ (- (c + 1)) is Element of the carrier of G

b " is Element of the carrier of G

(b |^ (- c)) * (b ") is Element of the carrier of G

the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V25([: the carrier of G, the carrier of G:], the carrier of G) V29( the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]

[: the carrier of G, the carrier of G:] is non empty set

[:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is non empty set

K94( the carrier of G, the multF of G,(b |^ (- c)),(b ")) is Element of the carrier of G

- 1 is V31() V32() integer ext-real non positive set

b |^ (- 1) is Element of the carrier of G

(b |^ (- c)) * (b |^ (- 1)) is Element of the carrier of G

K94( the carrier of G, the multF of G,(b |^ (- c)),(b |^ (- 1))) is Element of the carrier of G

(- c) + (- 1) is V31() V32() integer ext-real non positive set

b |^ ((- c) + (- 1)) is Element of the carrier of G

G is non empty strict unital Group-like V109() multMagma

(1). G is non empty finite strict unital Group-like V109() V111() cyclic Subgroup of G

the carrier of G is non empty set

1_ G is non being_of_order_0 Element of the carrier of G

H is Element of the carrier of G

b is Element of the carrier of G

G is non empty strict unital Group-like V109() multMagma

the carrier of G is non empty set

(1). G is non empty finite strict unital Group-like V109() V111() cyclic Subgroup of G

H is Element of the carrier of G

{H} is non empty finite Element of bool the carrier of G

bool the carrier of G is non empty set

gr {H} is non empty strict unital Group-like V109() Subgroup of G

b is non empty strict unital Group-like V109() Subgroup of G

(1). b is non empty finite strict unital Group-like V109() V111() cyclic Subgroup of b

the carrier of b is non empty set

1_ b is non being_of_order_0 Element of the carrier of b

m is Element of the carrier of b

c is Element of the carrier of G

c is V31() V32() integer ext-real set

H |^ c is Element of the carrier of G

1_ G is non being_of_order_0 Element of the carrier of G

c is V31() V32() integer ext-real set

H |^ c is Element of the carrier of G

c is V31() V32() integer ext-real set

H |^ c is Element of the carrier of G

a is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT

- a is V31() V32() integer ext-real non positive set

H |^ a is Element of the carrier of G

(H |^ a) " is Element of the carrier of G

((H |^ a) ") " is Element of the carrier of G

G is non empty strict unital Group-like V109() V111() cyclic multMagma

H is non empty strict unital Group-like V109() V111() Subgroup of G

(1). G is non empty finite strict unital Group-like V109() V111() cyclic Subgroup of G

(1). G is non empty finite strict unital Group-like V109() V111() cyclic Subgroup of G

the carrier of G is non empty set

the multF of G is Relation