:: GROUP_6 semantic presentation

REAL is set
NAT is non empty V41() V42() V43() Element of bool REAL

NAT is non empty V41() V42() V43() 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

{} 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

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

B is non empty unital Group-like associative Subgroup of G
N is non empty unital Group-like associative Subgroup of B

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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)

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

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

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
[:(),():] is set
[:[:(),():],():] is set
bool [:[:(),():],():] 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

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

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 [:(),():] -defined Left_Cosets B -valued Function-like V22([:(),():]) quasi_total Element of bool [:[:(),():],():]
[:(),():] is set
[:[:(),():],():] is set
bool [:[:(),():],():] is set
multMagma(# (),(G,B) #) is strict 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 [:(),():] -defined Left_Cosets B -valued Function-like V22([:(),():]) quasi_total Element of bool [:[:(),():],():]
[:(),():] is set
[:[:(),():],():] is set
bool [:[:(),():],():] is set
multMagma(# (),(G,B) #) is strict 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 [:(),():] -defined Left_Cosets B -valued Function-like V22([:(),():]) quasi_total Element of bool [:[:(),():],():]
[:(),():] is set
[:[:(),():],():] is set
bool [:[:(),():],():] is set
multMagma(# (),(G,B) #) is strict multMagma
the carrier of (G,B) is non empty set

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 [:(),():] -defined Left_Cosets B -valued Function-like V22([:(),():]) quasi_total Element of bool [:[:(),():],():]
[:(),():] is set
[:[:(),():],():] is set
bool [:[:(),():],():] is set
multMagma(# (),(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

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 [:(),():] -defined Left_Cosets B -valued Function-like V22([:(),():]) quasi_total Element of bool [:[:(),():],():]
[:(),():] is set
[:[:(),():],():] is set
bool [:[:(),():],():] is set
multMagma(# (),(G,B) #) is strict multMagma
the carrier of (G,B) is non empty set
N is Element of the carrier of (G,B)

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 [:(),():] -defined Left_Cosets B -valued Function-like V22([:(),():]) quasi_total Element of bool [:[:(),():],():]
[:(),():] is set
[:[:(),():],():] is set
bool [:[:(),():],():] is set
multMagma(# (),(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

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 [:(),():] -defined Left_Cosets B -valued Function-like V22([:(),():]) quasi_total Element of bool [:[:(),():],():]
[:(),():] is set
[:[:(),():],():] is set
bool [:[:(),():],():] is set
multMagma(# (),(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

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 [:(),():] -defined Left_Cosets B -valued Function-like V22([:(),():]) quasi_total Element of bool [:[:(),():],():]
[:(),():] is set
[:[:(),():],():] is set
bool [:[:(),():],():] is set
multMagma(# (),(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