:: GROUP_6 semantic presentation

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

{ (b

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

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

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

{ (b

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

{ (b

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

{ (b

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

{ (b

(N * B) * B is Element of bool the carrier of G

(N * B) * (carr B) is Element of bool the carrier of G

{ (b

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

{ (b

(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

{ (b

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

{ (b

B * (B * N) is Element of bool the carrier of G

(carr B) * (B * N) is Element of bool the carrier of G

{ (b

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

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

{ H

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

{ (b

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

{ (b

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

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

{ (b

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

{ (b

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

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

{ (b

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

{ (b

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

{ (b

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

{ (b

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

{ (b

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

{ (b

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

{ (b

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

{ (b

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

{ (b

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

{ (b

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

{ (b

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

{ (b

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

{ (b

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

{ (b

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

{ (b

f * (I * f) is Element of bool the carrier of G

(carr f) * (I * f) is Element of bool the carrier of G

{ (b

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

{ (b

(I * f) * f is Element of bool the carrier of G

(I * f) * (carr f) is Element of bool the carrier of G

{ (b

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

{ (b

f * f is Element of bool the carrier of G

(carr f) * (carr f) is Element of bool the carrier of G

{ (b

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

{ (b

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

{ (b

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

{ (b

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

{ (b

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

{ (b

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

{ (b

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

{ (b

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

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

{ (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)

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

{ (b

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

{ (b

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

{ (b

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

{ (b

(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

{ (b

(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

{ (b

(I * B) * ((G,B,f) * (G,B,g)) is Element of bool the carrier of G

{ (b

(G,B,N) * (G,B,f) is Element of bool the carrier of G

{ (b

((G,B,N) * (G,B,f)) * (J * B) is Element of bool the carrier of G

{ (b

(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

{ (b

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

{ (b

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

{ (b

(g * B) * B is Element of bool the carrier of G

(g * B) * (carr B) is Element of bool the carrier of G

{ (b

B * B is Element of bool the carrier of G

(carr B) * (carr B) is Element of bool the carrier of G

{ (b

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

{ (b

B * (B * g) is Element of bool the carrier of G

(carr B) * (B * g) is Element of bool the carrier of G

{ (b

(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

{ (b

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

{ (b

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

{ (b

(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

{ (b

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

{ (b

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

{ (b

(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

{ (b

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

{ (b

(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

{ (b

(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

{ (b

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

{ (b

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

{ (b

(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

{ (b

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

{ (b

(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

{ (b

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

{ (b

(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