:: 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₁₄ is Element of the carrier of G
c₁₄ * b is Element of the carrier of G
K94( the carrier of G, the multF of G,c₁₄,b) is Element of the carrier of G
c₁₅ is Element of the carrier of G
(c₁₄ * b) * c₁₅ is Element of the carrier of G
K94( the carrier of G, the multF of G,(c₁₄ * b),c₁₅) is Element of the carrier of G
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₁₄ is Element of the carrier of G
c₁₄ * H is Element of the carrier of G
K94( the carrier of G, the multF of G,c₁₄,H) is Element of the carrier of G
c₁₅ is Element of the carrier of G
(c₁₄ * H) * c₁₅ is Element of the carrier of G
K94( the carrier of G, the multF of G,(c₁₄ * H),c₁₅) is Element of the carrier of G
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₁₄ is Element of the carrier of G
c₁₅ is Element of the carrier of H
c₁₄ * b is Element of bool the carrier of G
c₁₅ * m is Element of bool the carrier of H
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-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
multMagma(# the carrier of G, the multF of G #) is strict unital Group-like V109() multMagma
b is Element of the carrier of G
{b} is non empty finite Element of bool the carrier of G
bool the carrier of G is non empty set
gr {b} is non empty strict unital Group-like V109() V111() Subgroup of G
m is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT
b |^ m is Element of the carrier of G
m is V6() V7() V8() V12() V31() V32() integer ext-real non negative set
b |^ m is Element of the carrier of G
m is V6() V7() V8() V12() V31() V32() integer ext-real non negative set
b |^ m is Element of the carrier of G
m is V6() V7() V8() V12() V31() V32() integer ext-real non negative set
b |^ m is Element of the carrier of G
the carrier of H is non empty set
c is Element of the carrier of H
a is Element of the carrier of H
t is V31() V32() integer ext-real set
b |^ t is Element of the carrier of G
t is V31() V32() integer ext-real set
b |^ t is Element of the carrier of G
t is V31() V32() integer ext-real set
b |^ t is Element of the carrier of G
t div m is V31() V32() integer ext-real set
m * (t div m) is V31() V32() integer ext-real set
t mod m is V31() V32() integer ext-real set
(m * (t div m)) + (t mod m) is V31() V32() integer ext-real set
s is V31() V32() integer ext-real set
r is V31() V32() integer ext-real set
m * r is V31() V32() integer ext-real set
(m * r) + s is V31() V32() integer ext-real set
s is V31() V32() integer ext-real set
r is V31() V32() integer ext-real set
m * r is V31() V32() integer ext-real set
(m * r) + s is V31() V32() integer ext-real set
b |^ (m * r) is Element of the carrier of G
s is V6() V7() V8() V12() V31() V32() integer ext-real non negative Element of NAT
b |^ s is Element of the carrier of G
(b |^ (m * r)) * (b |^ s) is Element of the carrier of G
K94( the carrier of G, the multF of G,(b |^ (m * r)),(b |^ s)) is Element of the carrier of G
(b |^ m) |^ r is Element of the carrier of G
((b |^ m) |^ r) * (b |^ s) is Element of the carrier of G
K94( the carrier of G, the multF of G,((b |^ m) |^ r),(b |^ s)) is Element of the carrier of G
((b |^ m) |^ r) " is Element of the carrier of G
(((b |^ m) |^ r) ") * (b |^ t) is Element of the carrier of G
K94( the carrier of G, the multF of G,(((b |^ m) |^ r) "),(b |^ t)) is Element of the carrier of G
(((b |^ m) |^ r) ") * ((b |^ m) |^ r) is Element of the carrier of G
K94( the carrier of G, the multF of G,(((b |^ m) |^ r) "),((b |^ m) |^ r)) is Element of the carrier of G
((((b |^ m) |^ r) ") * ((b |^ m) |^ r)) * (b |^ s) is Element of the carrier of G
K94( the carrier of G, the multF of G,((((b |^ m) |^ r) ") * ((b |^ m) |^ r)),(b |^ s)) is Element of the carrier of G
1_ G is non being_of_order_0 Element of the carrier of G
(1_ G) * (b |^ s) is Element of the carrier of G
K94( the carrier of G, the multF of G,(1_ G),(b |^ s)) is Element of the carrier of G
1_ G is non being_of_order_0 Element of the carrier of G
c |^ r is Element of the carrier of H
{c} is non empty finite Element of bool the carrier of H
bool the carrier of H is non empty set
gr {c} is non empty strict unital Group-like V109() V111() Subgroup of H
(1). G is non empty finite strict unital Group-like V109() V111() cyclic Subgroup of G