REAL is set
NAT is non empty V41() V42() V43() Element of bool REAL
bool REAL is set
COMPLEX is set
NAT is non empty V41() V42() V43() set
bool NAT is set
bool NAT is set
2 is non empty ext-real V41() V42() V43() V47() V48() V49() integer Element of NAT
[:2,2:] is set
[:[:2,2:],2:] is set
bool [:[:2,2:],2:] is set
INT is set
RAT is set
[:COMPLEX,COMPLEX:] is set
bool [:COMPLEX,COMPLEX:] is set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is set
[:REAL,REAL:] is set
bool [:REAL,REAL:] is set
[:[:REAL,REAL:],REAL:] is set
bool [:[:REAL,REAL:],REAL:] is set
[:RAT,RAT:] is set
bool [:RAT,RAT:] is set
[:[:RAT,RAT:],RAT:] is set
bool [:[:RAT,RAT:],RAT:] is set
[:INT,INT:] is set
bool [:INT,INT:] is set
[:[:INT,INT:],INT:] is set
bool [:[:INT,INT:],INT:] is set
[:NAT,NAT:] is set
[:[:NAT,NAT:],NAT:] is set
bool [:[:NAT,NAT:],NAT:] is set
{} is set
the Function-like functional empty ext-real V41() V42() V43() V45() V46() V47() V48() V49() integer finite V56() set is Function-like functional empty ext-real V41() V42() V43() V45() V46() V47() V48() V49() integer finite V56() set
1 is non empty ext-real V41() V42() V43() V47() V48() V49() integer Element of NAT
0 is ext-real V41() V42() V43() V47() V48() V49() integer Element of NAT
G is non empty set
B is non empty set
[:G,B:] is set
bool [:G,B:] is set
N is Relation-like G -defined B -valued Function-like non empty V22(G) quasi_total Element of bool [:G,B:]
f is Element of G
N . f is Element of B
g is Element of G
N . g is Element of B
f is set
g is set
N . f is set
N . g is set
G is non empty unital Group-like associative multMagma
B is non empty unital Group-like associative Subgroup of G
N is non empty unital Group-like associative Subgroup of B
G is non empty unital Group-like associative multMagma
(1). G is non empty finite strict unital Group-like associative Subgroup of G
(Omega). G is non empty strict unital Group-like associative Subgroup of G
the carrier of G is non empty set
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V22([: the carrier of G, the carrier of G:]) quasi_total associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
multMagma(# the carrier of G, the multF of G #) is strict multMagma
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
B is non empty unital Group-like associative Subgroup of G
the carrier of B is non empty set
N is Element of the carrier of G
f is non empty unital Group-like associative (G,B)
N * f is Element of bool the carrier of G
bool the carrier of G is set
carr f is Element of bool the carrier of G
the carrier of f is non empty set
N * (carr f) is Element of bool the carrier of G
K245( the carrier of G,N) is finite Element of bool the carrier of G
K245( the carrier of G,N) * (carr f) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in K245( the carrier of G,N) & b2 in carr f ) } is set
f * N is Element of bool the carrier of G
(carr f) * N is Element of bool the carrier of G
(carr f) * K245( the carrier of G,N) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in carr f & b2 in K245( the carrier of G,N) ) } is set
g is Element of the carrier of B
g * f is Element of bool the carrier of B
bool the carrier of B is set
carr f is Element of bool the carrier of B
g * (carr f) is Element of bool the carrier of B
K245( the carrier of B,g) is finite Element of bool the carrier of B
K245( the carrier of B,g) * (carr f) is Element of bool the carrier of B
{ (b1 * b2) where b1, b2 is Element of the carrier of B : ( b1 in K245( the carrier of B,g) & b2 in carr f ) } is set
f * g is Element of bool the carrier of B
(carr f) * g is Element of bool the carrier of B
(carr f) * K245( the carrier of B,g) is Element of bool the carrier of B
{ (b1 * b2) where b1, b2 is Element of the carrier of B : ( b1 in carr f & b2 in K245( the carrier of B,g) ) } is set
J is set
g is Element of the carrier of B
g * g is Element of the carrier of B
the multF of B is Relation-like [: the carrier of B, the carrier of B:] -defined the carrier of B -valued Function-like V22([: the carrier of B, the carrier of B:]) quasi_total associative Element of bool [:[: the carrier of B, the carrier of B:], the carrier of B:]
[: the carrier of B, the carrier of B:] is set
[:[: the carrier of B, the carrier of B:], the carrier of B:] is set
bool [:[: the carrier of B, the carrier of B:], the carrier of B:] is set
the multF of B . (g,g) is Element of the carrier of B
[g,g] is set
{g,g} is finite set
{g} is finite set
{{g,g},{g}} is finite V56() set
the multF of B . [g,g] is set
g is Element of the carrier of G
N * g 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 V22([: the carrier of G, the carrier of G:]) quasi_total associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (N,g) is Element of the carrier of G
[N,g] is set
{N,g} is finite set
{N} is finite set
{{N,g},{N}} is finite V56() set
the multF of G . [N,g] is set
J is set
g is Element of the carrier of G
N * g 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 V22([: the carrier of G, the carrier of G:]) quasi_total associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (N,g) is Element of the carrier of G
[N,g] is set
{N,g} is finite set
{N} is finite set
{{N,g},{N}} is finite V56() set
the multF of G . [N,g] is set
g is Element of the carrier of f
x is Element of the carrier of B
g * x is Element of the carrier of B
the multF of B is Relation-like [: the carrier of B, the carrier of B:] -defined the carrier of B -valued Function-like V22([: the carrier of B, the carrier of B:]) quasi_total associative Element of bool [:[: the carrier of B, the carrier of B:], the carrier of B:]
[: the carrier of B, the carrier of B:] is set
[:[: the carrier of B, the carrier of B:], the carrier of B:] is set
bool [:[: the carrier of B, the carrier of B:], the carrier of B:] is set
the multF of B . (g,x) is Element of the carrier of B
[g,x] is set
{g,x} is finite set
{g} is finite set
{{g,x},{g}} is finite V56() set
the multF of B . [g,x] is set
J is set
g is Element of the carrier of B
g * g is Element of the carrier of B
the multF of B is Relation-like [: the carrier of B, the carrier of B:] -defined the carrier of B -valued Function-like V22([: the carrier of B, the carrier of B:]) quasi_total associative Element of bool [:[: the carrier of B, the carrier of B:], the carrier of B:]
[: the carrier of B, the carrier of B:] is set
[:[: the carrier of B, the carrier of B:], the carrier of B:] is set
bool [:[: the carrier of B, the carrier of B:], the carrier of B:] is set
the multF of B . (g,g) is Element of the carrier of B
[g,g] is set
{g,g} is finite set
{g} is finite set
{{g,g},{g}} is finite V56() set
the multF of B . [g,g] is set
g is Element of the carrier of G
g * N 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 V22([: the carrier of G, the carrier of G:]) quasi_total associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (g,N) is Element of the carrier of G
[g,N] is set
{g,N} is finite set
{g} is finite set
{{g,N},{g}} is finite V56() set
the multF of G . [g,N] is set
J is set
g is Element of the carrier of G
g * N 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 V22([: the carrier of G, the carrier of G:]) quasi_total associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (g,N) is Element of the carrier of G
[g,N] is set
{g,N} is finite set
{g} is finite set
{{g,N},{g}} is finite V56() set
the multF of G . [g,N] is set
g is Element of the carrier of f
x is Element of the carrier of B
x * g is Element of the carrier of B
the multF of B is Relation-like [: the carrier of B, the carrier of B:] -defined the carrier of B -valued Function-like V22([: the carrier of B, the carrier of B:]) quasi_total associative Element of bool [:[: the carrier of B, the carrier of B:], the carrier of B:]
[: the carrier of B, the carrier of B:] is set
[:[: the carrier of B, the carrier of B:], the carrier of B:] is set
bool [:[: the carrier of B, the carrier of B:], the carrier of B:] is set
the multF of B . (x,g) is Element of the carrier of B
[x,g] is set
{x,g} is finite set
{x} is finite set
{{x,g},{x}} is finite V56() set
the multF of B . [x,g] is set
G is non empty unital Group-like associative multMagma
B is non empty unital Group-like associative Subgroup of G
N is non empty unital Group-like associative (G,B)
f is non empty unital Group-like associative (G,B)
N /\ f is non empty strict unital Group-like associative Subgroup of G
N /\ f is non empty strict unital Group-like associative Subgroup of B
the carrier of (N /\ f) is non empty set
the carrier of B is non empty set
carr N is Element of bool the carrier of B
bool the carrier of B is set
the carrier of N is non empty set
carr f is Element of bool the carrier of B
the carrier of f is non empty set
(carr N) /\ (carr f) is Element of bool the carrier of B
g is non empty unital Group-like associative Subgroup of G
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
B is Element of the carrier of G
B " is Element of the carrier of G
N is Element of the carrier of G
B * N 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 V22([: the carrier of G, the carrier of G:]) quasi_total associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (B,N) is Element of the carrier of G
[B,N] is set
{B,N} is finite set
{B} is finite set
{{B,N},{B}} is finite V56() set
the multF of G . [B,N] is set
(B * N) * (B ") is Element of the carrier of G
the multF of G . ((B * N),(B ")) is Element of the carrier of G
[(B * N),(B ")] is set
{(B * N),(B ")} is finite set
{(B * N)} is finite set
{{(B * N),(B ")},{(B * N)}} is finite V56() set
the multF of G . [(B * N),(B ")] is set
N |^ (B ") is Element of the carrier of G
N * (B ") is Element of the carrier of G
the multF of G . (N,(B ")) is Element of the carrier of G
[N,(B ")] is set
{N,(B ")} is finite set
{N} is finite set
{{N,(B ")},{N}} is finite V56() set
the multF of G . [N,(B ")] is set
B * (N * (B ")) is Element of the carrier of G
the multF of G . (B,(N * (B "))) is Element of the carrier of G
[B,(N * (B "))] is set
{B,(N * (B "))} is finite set
{{B,(N * (B "))},{B}} is finite V56() set
the multF of G . [B,(N * (B "))] is set
(B ") " is Element of the carrier of G
((B ") ") * N is Element of the carrier of G
the multF of G . (((B ") "),N) is Element of the carrier of G
[((B ") "),N] is set
{((B ") "),N} is finite set
{((B ") ")} is finite set
{{((B ") "),N},{((B ") ")}} is finite V56() set
the multF of G . [((B ") "),N] is set
(((B ") ") * N) * (B ") is Element of the carrier of G
the multF of G . ((((B ") ") * N),(B ")) is Element of the carrier of G
[(((B ") ") * N),(B ")] is set
{(((B ") ") * N),(B ")} is finite set
{(((B ") ") * N)} is finite set
{{(((B ") ") * N),(B ")},{(((B ") ") * N)}} is finite V56() set
the multF of G . [(((B ") ") * N),(B ")] is set
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
B is non empty unital Group-like associative Subgroup of G
B * B is Element of bool the carrier of G
bool the carrier of G is set
carr B is Element of bool the carrier of G
the carrier of B is non empty set
(carr B) * (carr B) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in carr B & b2 in carr B ) } is set
N is Element of the carrier of G
N * B is Element of bool the carrier of G
N * (carr B) is Element of bool the carrier of G
K245( the carrier of G,N) is finite Element of bool the carrier of G
K245( the carrier of G,N) * (carr B) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in K245( the carrier of G,N) & b2 in carr B ) } is set
(N * B) * B is Element of bool the carrier of G
(N * B) * (carr B) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in N * B & b2 in carr B ) } is set
N * (B * B) is Element of bool the carrier of G
K245( the carrier of G,N) * (B * B) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in K245( the carrier of G,N) & b2 in B * B ) } is set
(B * B) * N is Element of bool the carrier of G
(B * B) * K245( the carrier of G,N) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in B * B & b2 in K245( the carrier of G,N) ) } is set
B * N is Element of bool the carrier of G
(carr B) * N is Element of bool the carrier of G
(carr B) * K245( the carrier of G,N) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in carr B & b2 in K245( the carrier of G,N) ) } is set
B * (B * N) is Element of bool the carrier of G
(carr B) * (B * N) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in carr B & b2 in B * N ) } is set
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
bool the carrier of G is set
{ [.b1,b2.] where b1, b2 is Element of the carrier of G : verum } is set
G ` is non empty strict unital Group-like associative normal Subgroup of G
B is Element of bool the carrier of G
gr B is non empty strict unital Group-like associative Subgroup of G
commutators G is Element of bool the carrier of G
N is set
f is Element of the carrier of G
g is Element of the carrier of G
[.f,g.] is Element of the carrier of G
N is set
f is Element of the carrier of G
g is Element of the carrier of G
[.f,g.] is Element of the carrier of G
G is non empty strict unital Group-like associative multMagma
G ` is non empty strict unital Group-like associative normal Subgroup of G
the carrier of G is non empty set
B is non empty strict unital Group-like associative Subgroup of G
N is Element of the carrier of G
f is Element of the carrier of G
[.N,f.] is Element of the carrier of G
bool the carrier of G is set
{ H1(b1,b2) where b1, b2 is Element of the carrier of G : S1[b1,b2] } is set
N is Element of bool the carrier of G
the carrier of B is non empty set
f is set
g is Element of the carrier of G
I is Element of the carrier of G
[.g,I.] is Element of the carrier of G
gr N is non empty strict unital Group-like associative Subgroup of G
G is non empty unital Group-like associative multMagma
B is non empty unital Group-like associative Subgroup of G
N is non empty unital Group-like associative normal Subgroup of G
the carrier of B is non empty set
f is non empty unital Group-like associative (G,B)
g is Element of the carrier of B
g * f is Element of bool the carrier of B
bool the carrier of B is set
carr f is Element of bool the carrier of B
the carrier of f is non empty set
g * (carr f) is Element of bool the carrier of B
K245( the carrier of B,g) is finite Element of bool the carrier of B
K245( the carrier of B,g) * (carr f) is Element of bool the carrier of B
{ (b1 * b2) where b1, b2 is Element of the carrier of B : ( b1 in K245( the carrier of B,g) & b2 in carr f ) } is set
f * g is Element of bool the carrier of B
(carr f) * g is Element of bool the carrier of B
(carr f) * K245( the carrier of B,g) is Element of bool the carrier of B
{ (b1 * b2) where b1, b2 is Element of the carrier of B : ( b1 in carr f & b2 in K245( the carrier of B,g) ) } is set
I is set
J is Element of the carrier of B
g * J is Element of the carrier of B
the multF of B is Relation-like [: the carrier of B, the carrier of B:] -defined the carrier of B -valued Function-like V22([: the carrier of B, the carrier of B:]) quasi_total associative Element of bool [:[: the carrier of B, the carrier of B:], the carrier of B:]
[: the carrier of B, the carrier of B:] is set
[:[: the carrier of B, the carrier of B:], the carrier of B:] is set
bool [:[: the carrier of B, the carrier of B:], the carrier of B:] is set
the multF of B . (g,J) is Element of the carrier of B
[g,J] is set
{g,J} is finite set
{g} is finite set
{{g,J},{g}} is finite V56() set
the multF of B . [g,J] is set
the carrier of G is non empty set
g is Element of the carrier of G
g is Element of the carrier of G
g * g 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 V22([: the carrier of G, the carrier of G:]) quasi_total associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (g,g) is Element of the carrier of G
[g,g] is set
{g,g} is finite set
{g} is finite set
{{g,g},{g}} is finite V56() set
the multF of G . [g,g] is set
g * N is Element of bool the carrier of G
bool the carrier of G is set
carr N is Element of bool the carrier of G
the carrier of N is non empty set
g * (carr N) is Element of bool the carrier of G
K245( the carrier of G,g) is finite Element of bool the carrier of G
K245( the carrier of G,g) * (carr N) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in K245( the carrier of G,g) & b2 in carr N ) } is set
N * g is Element of bool the carrier of G
(carr N) * g is Element of bool the carrier of G
(carr N) * K245( the carrier of G,g) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in carr N & b2 in K245( the carrier of G,g) ) } is set
x is Element of the carrier of G
x * g is Element of the carrier of G
the multF of G . (x,g) is Element of the carrier of G
[x,g] is set
{x,g} is finite set
{x} is finite set
{{x,g},{x}} is finite V56() set
the multF of G . [x,g] is set
b is Element of the carrier of B
b * g is Element of the carrier of B
the multF of B . (b,g) is Element of the carrier of B
[b,g] is set
{b,g} is finite set
{b} is finite set
{{b,g},{b}} is finite V56() set
the multF of B . [b,g] is set
G is non empty unital Group-like associative multMagma
N is non empty unital Group-like associative normal Subgroup of G
the carrier of N is non empty set
the multF of N is Relation-like [: the carrier of N, the carrier of N:] -defined the carrier of N -valued Function-like V22([: the carrier of N, the carrier of N:]) quasi_total associative Element of bool [:[: the carrier of N, the carrier of N:], the carrier of N:]
[: the carrier of N, the carrier of N:] is set
[:[: the carrier of N, the carrier of N:], the carrier of N:] is set
bool [:[: the carrier of N, the carrier of N:], the carrier of N:] is set
multMagma(# the carrier of N, the multF of N #) is strict multMagma
B is non empty unital Group-like associative Subgroup of G
the carrier of G is non empty set
f is non empty unital Group-like associative Subgroup of G
g is Element of the carrier of G
g * f is Element of bool the carrier of G
bool the carrier of G is set
carr f is Element of bool the carrier of G
the carrier of f is non empty set
g * (carr f) is Element of bool the carrier of G
K245( the carrier of G,g) is finite Element of bool the carrier of G
K245( the carrier of G,g) * (carr f) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in K245( the carrier of G,g) & b2 in carr f ) } is set
g * N is Element of bool the carrier of G
carr N is Element of bool the carrier of G
g * (carr N) is Element of bool the carrier of G
K245( the carrier of G,g) * (carr N) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in K245( the carrier of G,g) & b2 in carr N ) } is set
N * g is Element of bool the carrier of G
(carr N) * g is Element of bool the carrier of G
(carr N) * K245( the carrier of G,g) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in carr N & b2 in K245( the carrier of G,g) ) } is set
f * g is Element of bool the carrier of G
(carr f) * g is Element of bool the carrier of G
(carr f) * K245( the carrier of G,g) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in carr f & b2 in K245( the carrier of G,g) ) } is set
G is non empty unital Group-like associative multMagma
B is non empty unital Group-like associative Subgroup of G
N is non empty unital Group-like associative normal Subgroup of G
B /\ N is non empty strict unital Group-like associative Subgroup of G
N /\ B is non empty strict unital Group-like associative Subgroup of G
the carrier of B is non empty set
f is non empty unital Group-like associative (G,B)
g is Element of the carrier of B
g * f is Element of bool the carrier of B
bool the carrier of B is set
carr f is Element of bool the carrier of B
the carrier of f is non empty set
g * (carr f) is Element of bool the carrier of B
K245( the carrier of B,g) is finite Element of bool the carrier of B
K245( the carrier of B,g) * (carr f) is Element of bool the carrier of B
{ (b1 * b2) where b1, b2 is Element of the carrier of B : ( b1 in K245( the carrier of B,g) & b2 in carr f ) } is set
f * g is Element of bool the carrier of B
(carr f) * g is Element of bool the carrier of B
(carr f) * K245( the carrier of B,g) is Element of bool the carrier of B
{ (b1 * b2) where b1, b2 is Element of the carrier of B : ( b1 in carr f & b2 in K245( the carrier of B,g) ) } is set
I is set
J is Element of the carrier of B
g * J is Element of the carrier of B
the multF of B is Relation-like [: the carrier of B, the carrier of B:] -defined the carrier of B -valued Function-like V22([: the carrier of B, the carrier of B:]) quasi_total associative Element of bool [:[: the carrier of B, the carrier of B:], the carrier of B:]
[: the carrier of B, the carrier of B:] is set
[:[: the carrier of B, the carrier of B:], the carrier of B:] is set
bool [:[: the carrier of B, the carrier of B:], the carrier of B:] is set
the multF of B . (g,J) is Element of the carrier of B
[g,J] is set
{g,J} is finite set
{g} is finite set
{{g,J},{g}} is finite V56() set
the multF of B . [g,J] is set
the carrier of G is non empty set
g is Element of the carrier of G
g is Element of the carrier of G
g * g 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 V22([: the carrier of G, the carrier of G:]) quasi_total associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (g,g) is Element of the carrier of G
[g,g] is set
{g,g} is finite set
{g} is finite set
{{g,g},{g}} is finite V56() set
the multF of G . [g,g] is set
g * N is Element of bool the carrier of G
bool the carrier of G is set
carr N is Element of bool the carrier of G
the carrier of N is non empty set
g * (carr N) is Element of bool the carrier of G
K245( the carrier of G,g) is finite Element of bool the carrier of G
K245( the carrier of G,g) * (carr N) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in K245( the carrier of G,g) & b2 in carr N ) } is set
g " is Element of the carrier of G
g " is Element of the carrier of B
N * g is Element of bool the carrier of G
(carr N) * g is Element of bool the carrier of G
(carr N) * K245( the carrier of G,g) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in carr N & b2 in K245( the carrier of G,g) ) } is set
b is Element of the carrier of G
b * g is Element of the carrier of G
the multF of G . (b,g) is Element of the carrier of G
[b,g] is set
{b,g} is finite set
{b} is finite set
{{b,g},{b}} is finite V56() set
the multF of G . [b,g] is set
a1 is Element of the carrier of G
a1 * (g ") is Element of the carrier of G
the multF of G . (a1,(g ")) is Element of the carrier of G
[a1,(g ")] is set
{a1,(g ")} is finite set
{a1} is finite set
{{a1,(g ")},{a1}} is finite V56() set
the multF of G . [a1,(g ")] is set
x is Element of the carrier of B
x * (g ") is Element of the carrier of B
the multF of B . (x,(g ")) is Element of the carrier of B
[x,(g ")] is set
{x,(g ")} is finite set
{x} is finite set
{{x,(g ")},{x}} is finite V56() set
the multF of B . [x,(g ")] is set
a2 is Element of the carrier of B
a2 * g is Element of the carrier of B
the multF of B . (a2,g) is Element of the carrier of B
[a2,g] is set
{a2,g} is finite set
{a2} is finite set
{{a2,g},{a2}} is finite V56() set
the multF of B . [a2,g] is set
G is non empty unital Group-like associative multMagma
B is non empty unital Group-like associative Subgroup of G
N is non empty unital Group-like associative normal Subgroup of G
B /\ N is non empty strict unital Group-like associative Subgroup of G
G is non empty unital Group-like associative multMagma
B is non empty unital Group-like associative normal Subgroup of G
N is non empty unital Group-like associative Subgroup of G
B /\ N is non empty strict unital Group-like associative Subgroup of G
G is non empty 1-sorted
the carrier of G is non empty set
the Element of the carrier of G is Element of the carrier of G
N is set
f is set
{ the Element of the carrier of G} is finite set
B is set
{B} is finite set
N is Element of the carrier of G
f is Element of the carrier of G
G is non empty unital Group-like associative multMagma
(1). G is non empty finite strict unital Group-like associative normal Subgroup of G
the carrier of ((1). G) is non empty finite 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)} is finite set
G is non empty unital Group-like associative multMagma
(1). G is non empty finite strict unital Group-like associative normal Subgroup of G
the non empty unital Group-like associative multMagma is non empty unital Group-like associative multMagma
(1). the non empty unital Group-like associative multMagma is non empty trivial finite 1 -element strict unital Group-like associative normal Subgroup of the non empty unital Group-like associative multMagma
G is non empty trivial finite 1 -element unital Group-like associative multMagma
card G is non empty ext-real V41() V42() V43() V47() V48() V49() integer cardinal Element of NAT
the carrier of G is non empty trivial finite set
card the carrier of G is cardinal set
B is set
{B} is finite set
G is non empty finite unital Group-like associative multMagma
card G is non empty ext-real V41() V42() V43() V47() V48() V49() integer cardinal Element of NAT
the carrier of G is non empty finite set
card the carrier of G is cardinal set
G is non empty trivial finite 1 -element strict unital Group-like associative multMagma
(1). G is non empty trivial finite 1 -element strict unital Group-like associative normal Subgroup of G
card G is non empty ext-real V41() V42() V43() V47() V48() V49() integer cardinal Element of NAT
the carrier of G is non empty trivial finite set
card the carrier of G is cardinal set
card ((1). G) is non empty ext-real V41() V42() V43() V47() V48() V49() integer cardinal Element of NAT
the carrier of ((1). G) is non empty trivial finite set
card the carrier of ((1). G) is cardinal set
G is non empty unital Group-like associative multMagma
G is non empty unital Group-like associative multMagma
B is non empty unital Group-like associative normal Subgroup of G
Left_Cosets B is Element of bool (bool the carrier of G)
the carrier of G is non empty set
bool the carrier of G is set
bool (bool the carrier of G) is set
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
B is set
N is non empty unital Group-like associative normal Subgroup of G
Left_Cosets N is non empty Element of bool (bool the carrier of G)
bool the carrier of G is set
bool (bool the carrier of G) is set
f is Element of the carrier of G
f * N is Element of bool the carrier of G
carr N is Element of bool the carrier of G
the carrier of N is non empty set
f * (carr N) is Element of bool the carrier of G
K245( the carrier of G,f) is finite Element of bool the carrier of G
K245( the carrier of G,f) * (carr N) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in K245( the carrier of G,f) & b2 in carr N ) } is set
N * f is Element of bool the carrier of G
(carr N) * f is Element of bool the carrier of G
(carr N) * K245( the carrier of G,f) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in carr N & b2 in K245( the carrier of G,f) ) } is set
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
B is Element of the carrier of G
N is non empty unital Group-like associative normal Subgroup of G
B * N is Element of bool the carrier of G
bool the carrier of G is set
carr N is Element of bool the carrier of G
the carrier of N is non empty set
B * (carr N) is Element of bool the carrier of G
K245( the carrier of G,B) is finite Element of bool the carrier of G
K245( the carrier of G,B) * (carr N) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in K245( the carrier of G,B) & b2 in carr N ) } is set
Left_Cosets N is non empty Element of bool (bool the carrier of G)
bool (bool the carrier of G) is set
N * B is Element of bool the carrier of G
(carr N) * B is Element of bool the carrier of G
(carr N) * K245( the carrier of G,B) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in carr N & b2 in K245( the carrier of G,B) ) } is set
Right_Cosets N is Element of bool (bool the carrier of G)
G is non empty unital Group-like associative multMagma
B is set
N is non empty unital Group-like associative normal Subgroup of G
Left_Cosets N 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 set
bool (bool the carrier of G) is set
G is non empty unital Group-like associative multMagma
the carrier of G is non empty set
bool the carrier of G is set
B is Element of bool the carrier of G
N is Element of bool the carrier of G
B * N is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in B & b2 in N ) } is set
f is non empty unital Group-like associative normal Subgroup of G
Left_Cosets f is non empty Element of bool (bool the carrier of G)
bool (bool the carrier of G) is set
g is Element of the carrier of G
g * f is Element of bool the carrier of G
carr f is Element of bool the carrier of G
the carrier of f is non empty set
g * (carr f) is Element of bool the carrier of G
K245( the carrier of G,g) is finite Element of bool the carrier of G
K245( the carrier of G,g) * (carr f) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in K245( the carrier of G,g) & b2 in carr f ) } is set
f * g is Element of bool the carrier of G
(carr f) * g is Element of bool the carrier of G
(carr f) * K245( the carrier of G,g) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in carr f & b2 in K245( the carrier of G,g) ) } is set
I is Element of the carrier of G
I * f is Element of bool the carrier of G
I * (carr f) is Element of bool the carrier of G
K245( the carrier of G,I) is finite Element of bool the carrier of G
K245( the carrier of G,I) * (carr f) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in K245( the carrier of G,I) & b2 in carr f ) } is set
f * I is Element of bool the carrier of G
(carr f) * I is Element of bool the carrier of G
(carr f) * K245( the carrier of G,I) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in carr f & b2 in K245( the carrier of G,I) ) } is set
f * (I * f) is Element of bool the carrier of G
(carr f) * (I * f) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in carr f & b2 in I * f ) } is set
g * (f * (I * f)) is Element of bool the carrier of G
K245( the carrier of G,g) * (f * (I * f)) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in K245( the carrier of G,g) & b2 in f * (I * f) ) } is set
(I * f) * f is Element of bool the carrier of G
(I * f) * (carr f) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in I * f & b2 in carr f ) } is set
g * ((I * f) * f) is Element of bool the carrier of G
K245( the carrier of G,g) * ((I * f) * f) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in K245( the carrier of G,g) & b2 in (I * f) * f ) } is set
f * f is Element of bool the carrier of G
(carr f) * (carr f) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in carr f & b2 in carr f ) } is set
I * (f * f) is Element of bool the carrier of G
K245( the carrier of G,I) * (f * f) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in K245( the carrier of G,I) & b2 in f * f ) } is set
g * (I * (f * f)) is Element of bool the carrier of G
K245( the carrier of G,g) * (I * (f * f)) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in K245( the carrier of G,g) & b2 in I * (f * f) ) } is set
g * (I * f) is Element of bool the carrier of G
K245( the carrier of G,g) * (I * f) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in K245( the carrier of G,g) & b2 in I * f ) } is set
g * I 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 V22([: the carrier of G, the carrier of G:]) quasi_total associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (g,I) is Element of the carrier of G
[g,I] is set
{g,I} is finite set
{g} is finite set
{{g,I},{g}} is finite V56() set
the multF of G . [g,I] is set
(g * I) * f is Element of bool the carrier of G
(g * I) * (carr f) is Element of bool the carrier of G
K245( the carrier of G,(g * I)) is finite Element of bool the carrier of G
K245( the carrier of G,(g * I)) * (carr f) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in K245( the carrier of G,(g * I)) & b2 in carr f ) } is set
G is non empty unital Group-like associative multMagma
B is non empty unital Group-like associative normal Subgroup of G
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 set
bool (bool the carrier of G) is set
[:(Left_Cosets B),(Left_Cosets B):] is set
[:[:(Left_Cosets B),(Left_Cosets B):],(Left_Cosets B):] is set
bool [:[:(Left_Cosets B),(Left_Cosets B):],(Left_Cosets B):] is set
N is Element of Left_Cosets B
f is Element of Left_Cosets B
g is Element of bool the carrier of G
I is Element of bool the carrier of G
g * I is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in g & b2 in I ) } is set
J is Element of Left_Cosets B
g is Element of bool the carrier of G
g is Element of bool the carrier of G
g * g is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in g & b2 in g ) } is set
N is Relation-like [:(Left_Cosets B),(Left_Cosets B):] -defined Left_Cosets B -valued Function-like V22([:(Left_Cosets B),(Left_Cosets B):]) quasi_total Element of bool [:[:(Left_Cosets B),(Left_Cosets B):],(Left_Cosets B):]
f is Relation-like [:(Left_Cosets B),(Left_Cosets B):] -defined Left_Cosets B -valued Function-like V22([:(Left_Cosets B),(Left_Cosets B):]) quasi_total Element of bool [:[:(Left_Cosets B),(Left_Cosets B):],(Left_Cosets B):]
g is set
I is set
J is Element of Left_Cosets B
g is Element of Left_Cosets B
N . (J,g) is Element of Left_Cosets B
[J,g] is set
{J,g} is finite set
{J} is finite set
{{J,g},{J}} is finite V56() set
N . [J,g] is set
g is Element of bool the carrier of G
x is Element of bool the carrier of G
g * x is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in g & b2 in x ) } is set
N . (g,I) is set
[g,I] is set
{g,I} is finite set
{g} is finite set
{{g,I},{g}} is finite V56() set
N . [g,I] is set
f . (g,I) is set
f . [g,I] is set
G is non empty unital Group-like associative multMagma
B is non empty unital Group-like associative normal Subgroup of G
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 set
bool (bool the carrier of G) is set
(G,B) is Relation-like [:(Left_Cosets B),(Left_Cosets B):] -defined Left_Cosets B -valued Function-like V22([:(Left_Cosets B),(Left_Cosets B):]) quasi_total Element of bool [:[:(Left_Cosets B),(Left_Cosets B):],(Left_Cosets B):]
[:(Left_Cosets B),(Left_Cosets B):] is set
[:[:(Left_Cosets B),(Left_Cosets B):],(Left_Cosets B):] is set
bool [:[:(Left_Cosets B),(Left_Cosets B):],(Left_Cosets B):] is set
multMagma(# (Left_Cosets B),(G,B) #) is strict multMagma
G is non empty unital Group-like associative multMagma
B is non empty unital Group-like associative normal Subgroup of G
(G,B) is multMagma
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 set
bool (bool the carrier of G) is set
(G,B) is Relation-like [:(Left_Cosets B),(Left_Cosets B):] -defined Left_Cosets B -valued Function-like V22([:(Left_Cosets B),(Left_Cosets B):]) quasi_total Element of bool [:[:(Left_Cosets B),(Left_Cosets B):],(Left_Cosets B):]
[:(Left_Cosets B),(Left_Cosets B):] is set
[:[:(Left_Cosets B),(Left_Cosets B):],(Left_Cosets B):] is set
bool [:[:(Left_Cosets B),(Left_Cosets B):],(Left_Cosets B):] is set
multMagma(# (Left_Cosets B),(G,B) #) is strict multMagma
G is non empty unital Group-like associative multMagma
B is non empty unital Group-like associative normal Subgroup of G
(G,B) is non empty strict multMagma
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 set
bool (bool the carrier of G) is set
(G,B) is Relation-like [:(Left_Cosets B),(Left_Cosets B):] -defined Left_Cosets B -valued Function-like V22([:(Left_Cosets B),(Left_Cosets B):]) quasi_total Element of bool [:[:(Left_Cosets B),(Left_Cosets B):],(Left_Cosets B):]
[:(Left_Cosets B),(Left_Cosets B):] is set
[:[:(Left_Cosets B),(Left_Cosets B):],(Left_Cosets B):] is set
bool [:[:(Left_Cosets B),(Left_Cosets B):],(Left_Cosets B):] is set
multMagma(# (Left_Cosets B),(G,B) #) is strict multMagma
the carrier of (G,B) is non empty set
G is non empty unital Group-like associative multMagma
B is non empty unital Group-like associative normal Subgroup of G
(G,B) is non empty strict multMagma
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 set
bool (bool the carrier of G) is set
(G,B) is Relation-like [:(Left_Cosets B),(Left_Cosets B):] -defined Left_Cosets B -valued Function-like V22([:(Left_Cosets B),(Left_Cosets B):]) quasi_total Element of bool [:[:(Left_Cosets B),(Left_Cosets B):],(Left_Cosets B):]
[:(Left_Cosets B),(Left_Cosets B):] is set
[:[:(Left_Cosets B),(Left_Cosets B):],(Left_Cosets B):] is set
bool [:[:(Left_Cosets B),(Left_Cosets B):],(Left_Cosets B):] is set
multMagma(# (Left_Cosets B),(G,B) #) is strict multMagma
the carrier of (G,B) is non empty set
[: the carrier of (G,B), the carrier of (G,B):] is set
the multF of (G,B) is Relation-like [: the carrier of (G,B), the carrier of (G,B):] -defined the carrier of (G,B) -valued Function-like V22([: the carrier of (G,B), the carrier of (G,B):]) quasi_total Element of bool [:[: the carrier of (G,B), the carrier of (G,B):], the carrier of (G,B):]
[:[: the carrier of (G,B), the carrier of (G,B):], the carrier of (G,B):] is set
bool [:[: the carrier of (G,B), the carrier of (G,B):], the carrier of (G,B):] is set
G is non empty unital Group-like associative multMagma
B is non empty unital Group-like associative normal Subgroup of G
(G,B) is non empty strict multMagma
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 set
bool (bool the carrier of G) is set
(G,B) is Relation-like [:(Left_Cosets B),(Left_Cosets B):] -defined Left_Cosets B -valued Function-like V22([:(Left_Cosets B),(Left_Cosets B):]) quasi_total Element of bool [:[:(Left_Cosets B),(Left_Cosets B):],(Left_Cosets B):]
[:(Left_Cosets B),(Left_Cosets B):] is set
[:[:(Left_Cosets B),(Left_Cosets B):],(Left_Cosets B):] is set
bool [:[:(Left_Cosets B),(Left_Cosets B):],(Left_Cosets B):] is set
multMagma(# (Left_Cosets B),(G,B) #) is strict multMagma
the carrier of (G,B) is non empty set
N is Element of the carrier of (G,B)
G is non empty unital Group-like associative multMagma
B is non empty unital Group-like associative normal Subgroup of G
(G,B) is non empty strict multMagma
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 set
bool (bool the carrier of G) is set
(G,B) is Relation-like [:(Left_Cosets B),(Left_Cosets B):] -defined Left_Cosets B -valued Function-like V22([:(Left_Cosets B),(Left_Cosets B):]) quasi_total Element of bool [:[:(Left_Cosets B),(Left_Cosets B):],(Left_Cosets B):]
[:(Left_Cosets B),(Left_Cosets B):] is set
[:[:(Left_Cosets B),(Left_Cosets B):],(Left_Cosets B):] is set
bool [:[:(Left_Cosets B),(Left_Cosets B):],(Left_Cosets B):] is set
multMagma(# (Left_Cosets B),(G,B) #) is strict multMagma
the carrier of (G,B) is non empty set
N is Element of the carrier of (G,B)
(G,B,N) is Element of bool the carrier of G
f is Element of the carrier of (G,B)
(G,B,f) is Element of bool the carrier of G
(G,B,N) * (G,B,f) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in (G,B,N) & b2 in (G,B,f) ) } is set
N * f is Element of the carrier of (G,B)
the multF of (G,B) is Relation-like [: the carrier of (G,B), the carrier of (G,B):] -defined the carrier of (G,B) -valued Function-like V22([: the carrier of (G,B), the carrier of (G,B):]) quasi_total Element of bool [:[: the carrier of (G,B), the carrier of (G,B):], the carrier of (G,B):]
[: the carrier of (G,B), the carrier of (G,B):] is set
[:[: the carrier of (G,B), the carrier of (G,B):], the carrier of (G,B):] is set
bool [:[: the carrier of (G,B), the carrier of (G,B):], the carrier of (G,B):] is set
the multF of (G,B) . (N,f) is Element of the carrier of (G,B)
[N,f] is set
{N,f} is finite set
{N} is finite set
{{N,f},{N}} is finite V56() set
the multF of (G,B) . [N,f] is set
G is non empty unital Group-like associative multMagma
B is non empty unital Group-like associative normal Subgroup of G
(G,B) is non empty strict multMagma
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 set
bool (bool the carrier of G) is set
(G,B) is Relation-like [:(Left_Cosets B),(Left_Cosets B):] -defined Left_Cosets B -valued Function-like V22([:(Left_Cosets B),(Left_Cosets B):]) quasi_total Element of bool [:[:(Left_Cosets B),(Left_Cosets B):],(Left_Cosets B):]
[:(Left_Cosets B),(Left_Cosets B):] is set
[:[:(Left_Cosets B),(Left_Cosets B):],(Left_Cosets B):] is set
bool [:[:(Left_Cosets B),(Left_Cosets B):],(Left_Cosets B):] is set
multMagma(# (Left_Cosets B),(G,B) #) is strict multMagma
the carrier of (G,B) is non empty set
N is Element of the carrier of (G,B)
f is Element of the carrier of (G,B)
N * f is Element of the carrier of (G,B)
the multF of (G,B) is Relation-like [: the carrier of (G,B), the carrier of (G,B):] -defined the carrier of (G,B) -valued Function-like V22([: the carrier of (G,B), the carrier of (G,B):]) quasi_total Element of bool [:[: the carrier of (G,B), the carrier of (G,B):], the carrier of (G,B):]
[: the carrier of (G,B), the carrier of (G,B):] is set
[:[: the carrier of (G,B), the carrier of (G,B):], the carrier of (G,B):] is set
bool [:[: the carrier of (G,B), the carrier of (G,B):], the carrier of (G,B):] is set
the multF of (G,B) . (N,f) is Element of the carrier of (G,B)
[N,f] is set
{N,f} is finite set
{N} is finite set
{{N,f},{N}} is finite V56() set
the multF of (G,B) . [N,f] is set
(G,B,(N * f)) is Element of bool the carrier of G
(G,B,N) is Element of bool the carrier of G
(G,B,f) is Element of bool the carrier of G
(G,B,N) * (G,B,f) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in (G,B,N) & b2 in (G,B,f) ) } is set
G is non empty unital Group-like associative multMagma
B is non empty unital Group-like associative normal Subgroup of G
(G,B) is non empty strict multMagma
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 set
bool (bool the carrier of G) is set
(G,B) is Relation-like [:(Left_Cosets B),(Left_Cosets B):] -defined Left_Cosets B -valued Function-like V22([:(Left_Cosets B),(Left_Cosets B):]) quasi_total Element of bool [:[:(Left_Cosets B),(Left_Cosets B):],(Left_Cosets B):]
[:(Left_Cosets B),(Left_Cosets B):] is set
[:[:(Left_Cosets B),(Left_Cosets B):],(Left_Cosets B):] is set
bool [:[:(Left_Cosets B),(Left_Cosets B):],(Left_Cosets B):] is set
multMagma(# (Left_Cosets B),(G,B) #) is strict multMagma
the carrier of (G,B) is non empty set
N is Element of the carrier of (G,B)
f is Element of the carrier of (G,B)
g is Element of the carrier of (G,B)
f * g is Element of the carrier of (G,B)
the multF of (G,B) is Relation-like [: the carrier of (G,B), the carrier of (G,B):] -defined the carrier of (G,B) -valued Function-like V22([: the carrier of (G,B), the carrier of (G,B):]) quasi_total Element of bool [:[: the carrier of (G,B), the carrier of (G,B):], the carrier of (G,B):]
[: the carrier of (G,B), the carrier of (G,B):] is set
[:[: the carrier of (G,B), the carrier of (G,B):], the carrier of (G,B):] is set
bool [:[: the carrier of (G,B), the carrier of (G,B):], the carrier of (G,B):] is set
the multF of (G,B) . (f,g) is Element of the carrier of (G,B)
[f,g] is set
{f,g} is finite set
{f} is finite set
{{f,g},{f}} is finite V56() set
the multF of (G,B) . [f,g] is set
N * (f * g) is Element of the carrier of (G,B)
the multF of (G,B) . (N,(f * g)) is Element of the carrier of (G,B)
[N,(f * g)] is set
{N,(f * g)} is finite set
{N} is finite set
{{N,(f * g)},{N}} is finite V56() set
the multF of (G,B) . [N,(f * g)] is set
N * f is Element of the carrier of (G,B)
the multF of (G,B) . (N,f) is Element of the carrier of (G,B)
[N,f] is set
{N,f} is finite set
{{N,f},{N}} is finite V56() set
the multF of (G,B) . [N,f] is set
(N * f) * g is Element of the carrier of (G,B)
the multF of (G,B) . ((N * f),g) is Element of the carrier of (G,B)
[(N * f),g] is set
{(N * f),g} is finite set
{(N * f)} is finite set
{{(N * f),g},{(N * f)}} is finite V56() set
the multF of (G,B) . [(N * f),g] is set
I is Element of the carrier of G
I * B is Element of bool the carrier of G
carr B is Element of bool the carrier of G
the carrier of B is non empty set
I * (carr B) is Element of bool the carrier of G
K245( the carrier of G,I) is finite Element of bool the carrier of G
K245( the carrier of G,I) * (carr B) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in K245( the carrier of G,I) & b2 in carr B ) } is set
B * I is Element of bool the carrier of G
(carr B) * I is Element of bool the carrier of G
(carr B) * K245( the carrier of G,I) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in carr B & b2 in K245( the carrier of G,I) ) } is set
J is Element of the carrier of G
J * B is Element of bool the carrier of G
J * (carr B) is Element of bool the carrier of G
K245( the carrier of G,J) is finite Element of bool the carrier of G
K245( the carrier of G,J) * (carr B) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in K245( the carrier of G,J) & b2 in carr B ) } is set
B * J is Element of bool the carrier of G
(carr B) * J is Element of bool the carrier of G
(carr B) * K245( the carrier of G,J) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in carr B & b2 in K245( the carrier of G,J) ) } is set
(G,B,N) is Element of bool the carrier of G
(G,B,(f * g)) is Element of bool the carrier of G
(G,B,N) * (G,B,(f * g)) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in (G,B,N) & b2 in (G,B,(f * g)) ) } is set
(G,B,f) is Element of bool the carrier of G
(G,B,g) is Element of bool the carrier of G
(G,B,f) * (G,B,g) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in (G,B,f) & b2 in (G,B,g) ) } is set
(I * B) * ((G,B,f) * (G,B,g)) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in I * B & b2 in (G,B,f) * (G,B,g) ) } is set
(G,B,N) * (G,B,f) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in (G,B,N) & b2 in (G,B,f) ) } is set
((G,B,N) * (G,B,f)) * (J * B) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in (G,B,N) * (G,B,f) & b2 in J * B ) } is set
(G,B,(N * f)) is Element of bool the carrier of G
(G,B,(N * f)) * (G,B,g) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in (G,B,(N * f)) & b2 in (G,B,g) ) } is set
carr B is Element of bool the carrier of G
the carrier of B is non empty set
N is Element of the carrier of (G,B)
f is Element of the carrier of (G,B)
f * N is Element of the carrier of (G,B)
the multF of (G,B) is Relation-like [: the carrier of (G,B), the carrier of (G,B):] -defined the carrier of (G,B) -valued Function-like V22([: the carrier of (G,B), the carrier of (G,B):]) quasi_total Element of bool [:[: the carrier of (G,B), the carrier of (G,B):], the carrier of (G,B):]
[: the carrier of (G,B), the carrier of (G,B):] is set
[:[: the carrier of (G,B), the carrier of (G,B):], the carrier of (G,B):] is set
bool [:[: the carrier of (G,B), the carrier of (G,B):], the carrier of (G,B):] is set
the multF of (G,B) . (f,N) is Element of the carrier of (G,B)
[f,N] is set
{f,N} is finite set
{f} is finite set
{{f,N},{f}} is finite V56() set
the multF of (G,B) . [f,N] is set
N * f is Element of the carrier of (G,B)
the multF of (G,B) . (N,f) is Element of the carrier of (G,B)
[N,f] is set
{N,f} is finite set
{N} is finite set
{{N,f},{N}} is finite V56() set
the multF of (G,B) . [N,f] is set
g is Element of the carrier of G
g * B is Element of bool the carrier of G
g * (carr B) is Element of bool the carrier of G
K245( the carrier of G,g) is finite Element of bool the carrier of G
K245( the carrier of G,g) * (carr B) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in K245( the carrier of G,g) & b2 in carr B ) } is set
B * g is Element of bool the carrier of G
(carr B) * g is Element of bool the carrier of G
(carr B) * K245( the carrier of G,g) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in carr B & b2 in K245( the carrier of G,g) ) } is set
(g * B) * B is Element of bool the carrier of G
(g * B) * (carr B) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in g * B & b2 in carr B ) } is set
B * B is Element of bool the carrier of G
(carr B) * (carr B) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in carr B & b2 in carr B ) } is set
g * (B * B) is Element of bool the carrier of G
K245( the carrier of G,g) * (B * B) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in K245( the carrier of G,g) & b2 in B * B ) } is set
B * (B * g) is Element of bool the carrier of G
(carr B) * (B * g) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in carr B & b2 in B * g ) } is set
(B * B) * g is Element of bool the carrier of G
(B * B) * K245( the carrier of G,g) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in B * B & b2 in K245( the carrier of G,g) ) } is set
g " is Element of the carrier of G
(g ") * B is Element of bool the carrier of G
(g ") * (carr B) is Element of bool the carrier of G
K245( the carrier of G,(g ")) is finite Element of bool the carrier of G
K245( the carrier of G,(g ")) * (carr B) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in K245( the carrier of G,(g ")) & b2 in carr B ) } is set
I is Element of the carrier of (G,B)
f * I is Element of the carrier of (G,B)
the multF of (G,B) . (f,I) is Element of the carrier of (G,B)
[f,I] is set
{f,I} is finite set
{{f,I},{f}} is finite V56() set
the multF of (G,B) . [f,I] is set
I * f is Element of the carrier of (G,B)
the multF of (G,B) . (I,f) is Element of the carrier of (G,B)
[I,f] is set
{I,f} is finite set
{I} is finite set
{{I,f},{I}} is finite V56() set
the multF of (G,B) . [I,f] is set
(B * g) * ((g ") * B) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in B * g & b2 in (g ") * B ) } is set
(B * g) * (g ") is Element of bool the carrier of G
(B * g) * K245( the carrier of G,(g ")) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in B * g & b2 in K245( the carrier of G,(g ")) ) } is set
((B * g) * (g ")) * B is Element of bool the carrier of G
((B * g) * (g ")) * (carr B) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in (B * g) * (g ") & b2 in carr B ) } is set
g * (g ") 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 V22([: the carrier of G, the carrier of G:]) quasi_total associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (g,(g ")) is Element of the carrier of G
[g,(g ")] is set
{g,(g ")} is finite set
{g} is finite set
{{g,(g ")},{g}} is finite V56() set
the multF of G . [g,(g ")] is set
B * (g * (g ")) is Element of bool the carrier of G
(carr B) * (g * (g ")) is Element of bool the carrier of G
K245( the carrier of G,(g * (g "))) is finite Element of bool the carrier of G
(carr B) * K245( the carrier of G,(g * (g "))) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in carr B & b2 in K245( the carrier of G,(g * (g "))) ) } is set
(B * (g * (g "))) * B is Element of bool the carrier of G
(B * (g * (g "))) * (carr B) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in B * (g * (g ")) & b2 in carr B ) } is set
1_ G is non being_of_order_0 Element of the carrier of G
B * (1_ G) is Element of bool the carrier of G
(carr B) * (1_ G) is Element of bool the carrier of G
K245( the carrier of G,(1_ G)) is finite Element of bool the carrier of G
(carr B) * K245( the carrier of G,(1_ G)) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in carr B & b2 in K245( the carrier of G,(1_ G)) ) } is set
(B * (1_ G)) * B is Element of bool the carrier of G
(B * (1_ G)) * (carr B) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in B * (1_ G) & b2 in carr B ) } is set
(G,B,I) is Element of bool the carrier of G
(G,B,f) is Element of bool the carrier of G
(G,B,I) * (G,B,f) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in (G,B,I) & b2 in (G,B,f) ) } is set
((g ") * B) * g is Element of bool the carrier of G
((g ") * B) * K245( the carrier of G,g) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in (g ") * B & b2 in K245( the carrier of G,g) ) } is set
(((g ") * B) * g) * B is Element of bool the carrier of G
(((g ") * B) * g) * (carr B) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in ((g ") * B) * g & b2 in carr B ) } is set
(g ") * (B * g) is Element of bool the carrier of G
K245( the carrier of G,(g ")) * (B * g) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in K245( the carrier of G,(g ")) & b2 in B * g ) } is set
((g ") * (B * g)) * B is Element of bool the carrier of G
((g ") * (B * g)) * (carr B) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in (g ") * (B * g) & b2 in carr B ) } is set
(g ") * (g * B) is Element of bool the carrier of G
K245( the carrier of G,(g ")) * (g * B) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in K245( the carrier of G,(g ")) & b2 in g * B ) } is set
((g ") * (g * B)) * B is Element of bool the carrier of G
((g ") * (g * B)) * (carr B) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in (g ") * (g * B) & b2 in carr B ) } is set
(g ") * g is Element of the carrier of G
the multF of G . ((g "),g) is Element of the carrier of G
[(g "),g] is set
{(g "),g} is finite set
{(g ")} is finite set
{{(g "),g},{(g ")}} is finite V56() set
the