:: GROUP_3 semantic presentation

K109() is set

K113() is non empty V12() V13() V14() Element of bool K109()

bool K109() is non empty set

K110() is set

K46() is non empty V12() V13() V14() set

bool K46() is non empty set

K111() is set

K112() is set

[:K110(),K110():] is set

bool [:K110(),K110():] is non empty set

[:[:K110(),K110():],K110():] is set

bool [:[:K110(),K110():],K110():] is non empty set

[:K109(),K109():] is set

bool [:K109(),K109():] is non empty set

[:[:K109(),K109():],K109():] is set

bool [:[:K109(),K109():],K109():] is non empty set

[:K111(),K111():] is set

bool [:K111(),K111():] is non empty set

[:[:K111(),K111():],K111():] is set

bool [:[:K111(),K111():],K111():] is non empty set

[:K112(),K112():] is set

bool [:K112(),K112():] is non empty set

[:[:K112(),K112():],K112():] is set

bool [:[:K112(),K112():],K112():] is non empty set

[:K113(),K113():] is non empty set

[:[:K113(),K113():],K113():] is non empty set

bool [:[:K113(),K113():],K113():] is non empty set

{} is empty V12() V13() V14() V16() V17() V18() Function-like functional ext-real V37() V38() integer finite V45() set

the empty V12() V13() V14() V16() V17() V18() Function-like functional ext-real V37() V38() integer finite V45() set is empty V12() V13() V14() V16() V17() V18() Function-like functional ext-real V37() V38() integer finite V45() set

1 is non empty V12() V13() V14() V18() ext-real V37() V38() integer Element of K113()

K114() is empty V12() V13() V14() V16() V17() V18() Function-like functional ext-real V37() V38() integer finite V45() Element of K113()

2 is non empty V12() V13() V14() V18() ext-real V37() V38() integer Element of K113()

G is non empty unital Group-like associative multMagma

the carrier of G is non empty set

H is Element of the carrier of G

a is Element of the carrier of G

H * a is Element of the carrier of G

the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V28([: the carrier of G, the carrier of G:], the carrier of G) 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 non empty set

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

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

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

[H,a] is set

{H,a} is non empty finite set

{H} is non empty finite set

{{H,a},{H}} is non empty finite V45() set

the multF of G . [H,a] is set

a " is Element of the carrier of G

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

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

[(H * a),(a ")] is set

{(H * a),(a ")} is non empty finite set

{(H * a)} is non empty finite set

{{(H * a),(a ")},{(H * a)}} is non empty finite V45() set

the multF of G . [(H * a),(a ")] is set

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

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

[H,(a ")] is set

{H,(a ")} is non empty finite set

{{H,(a ")},{H}} is non empty finite V45() set

the multF of G . [H,(a ")] is set

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

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

[(H * (a ")),a] is set

{(H * (a ")),a} is non empty finite set

{(H * (a "))} is non empty finite set

{{(H * (a ")),a},{(H * (a "))}} is non empty finite V45() set

the multF of G . [(H * (a ")),a] is set

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

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

[(a "),a] is set

{(a "),a} is non empty finite set

{(a ")} is non empty finite set

{{(a "),a},{(a ")}} is non empty finite V45() set

the multF of G . [(a "),a] is set

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

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

[((a ") * a),H] is set

{((a ") * a),H} is non empty finite set

{((a ") * a)} is non empty finite set

{{((a ") * a),H},{((a ") * a)}} is non empty finite V45() set

the multF of G . [((a ") * a),H] is set

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

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

[a,(a ")] is set

{a,(a ")} is non empty finite set

{a} is non empty finite set

{{a,(a ")},{a}} is non empty finite V45() set

the multF of G . [a,(a ")] is set

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

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

[(a * (a ")),H] is set

{(a * (a ")),H} is non empty finite set

{(a * (a "))} is non empty finite set

{{(a * (a ")),H},{(a * (a "))}} is non empty finite V45() set

the multF of G . [(a * (a ")),H] is set

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

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

[H,(a * (a "))] is set

{H,(a * (a "))} is non empty finite set

{{H,(a * (a "))},{H}} is non empty finite V45() set

the multF of G . [H,(a * (a "))] is set

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

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

[H,((a ") * a)] is set

{H,((a ") * a)} is non empty finite set

{{H,((a ") * a)},{H}} is non empty finite V45() set

the multF of G . [H,((a ") * a)] is set

a * H is Element of the carrier of G

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

[a,H] is set

{a,H} is non empty finite set

{{a,H},{a}} is non empty finite V45() set

the multF of G . [a,H] is set

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

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

[(a "),(a * H)] is set

{(a "),(a * H)} is non empty finite set

{{(a "),(a * H)},{(a ")}} is non empty finite V45() set

the multF of G . [(a "),(a * H)] is set

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

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

[(a "),H] is set

{(a "),H} is non empty finite set

{{(a "),H},{(a ")}} is non empty finite V45() set

the multF of G . [(a "),H] is set

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

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

[a,((a ") * H)] is set

{a,((a ") * H)} is non empty finite set

{{a,((a ") * H)},{a}} is non empty finite V45() set

the multF of G . [a,((a ") * H)] is set

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

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

the multF of G . (H,(1_ G)) is Element of the carrier of G

[H,(1_ G)] is set

{H,(1_ G)} is non empty finite set

{{H,(1_ G)},{H}} is non empty finite V45() set

the multF of G . [H,(1_ G)] is set

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

the multF of G . ((1_ G),H) is Element of the carrier of G

[(1_ G),H] is set

{(1_ G),H} is non empty finite set

{(1_ G)} is non empty finite set

{{(1_ G),H},{(1_ G)}} is non empty finite V45() set

the multF of G . [(1_ G),H] is set

G is non empty unital Group-like associative commutative multMagma

the carrier of G is non empty set

H is Element of the carrier of G

a is Element of the carrier of G

H * a is Element of the carrier of G

the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V28([: the carrier of G, the carrier of G:], the carrier of G) 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 non empty set

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

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

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

[H,a] is set

{H,a} is non empty finite set

{H} is non empty finite set

{{H,a},{H}} is non empty finite V45() set

the multF of G . [H,a] is set

a * H is Element of the carrier of G

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

[a,H] is set

{a,H} is non empty finite set

{a} is non empty finite set

{{a,H},{a}} is non empty finite V45() set

the multF of G . [a,H] is set

G is non empty unital Group-like associative multMagma

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 V28([: the carrier of G, the carrier of G:], the carrier of G) 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 non empty set

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

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

H is Element of the carrier of G

a is Element of the carrier of G

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

[H,a] is set

{H,a} is non empty finite set

{H} is non empty finite set

{{H,a},{H}} is non empty finite V45() set

the multF of G . [H,a] is set

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

[a,H] is set

{a,H} is non empty finite set

{a} is non empty finite set

{{a,H},{a}} is non empty finite V45() set

the multF of G . [a,H] is set

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

H * a is Element of the carrier of G

a * H is Element of the carrier of G

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

H is Element of the carrier of G

a is Element of the carrier of G

H * a is Element of the carrier of G

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

[H,a] is set

{H,a} is non empty finite set

{H} is non empty finite set

{{H,a},{H}} is non empty finite V45() set

the multF of G . [H,a] is set

a * H is Element of the carrier of G

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

[a,H] is set

{a,H} is non empty finite set

{a} is non empty finite set

{{a,H},{a}} is non empty finite V45() set

the multF of G . [a,H] is set

G is non empty unital Group-like associative multMagma

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

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

H is Element of the carrier of ((1). G)

a is Element of the carrier of ((1). G)

H * a is Element of the carrier of ((1). G)

the multF of ((1). G) is Relation-like [: the carrier of ((1). G), the carrier of ((1). G):] -defined the carrier of ((1). G) -valued Function-like V28([: the carrier of ((1). G), the carrier of ((1). G):], the carrier of ((1). G)) associative finite Element of bool [:[: the carrier of ((1). G), the carrier of ((1). G):], the carrier of ((1). G):]

[: the carrier of ((1). G), the carrier of ((1). G):] is non empty finite set

[:[: the carrier of ((1). G), the carrier of ((1). G):], the carrier of ((1). G):] is non empty finite set

bool [:[: the carrier of ((1). G), the carrier of ((1). G):], the carrier of ((1). G):] is non empty finite V45() set

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

[H,a] is set

{H,a} is non empty finite set

{H} is non empty finite set

{{H,a},{H}} is non empty finite V45() set

the multF of ((1). G) . [H,a] is set

a * H is Element of the carrier of ((1). G)

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

[a,H] is set

{a,H} is non empty finite set

{a} is non empty finite set

{{a,H},{a}} is non empty finite V45() set

the multF of ((1). G) . [a,H] is set

the carrier of G is non empty set

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

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

bool the carrier of G is non empty set

G is non empty unital Group-like associative multMagma

the carrier of G is non empty set

bool the carrier of G is non empty set

H is Element of bool the carrier of G

a is Element of bool the carrier of G

c

H * c

{ (b

y is Element of bool the carrier of G

a * y is Element of bool the carrier of G

{ (b

H1 is set

a is Element of the carrier of G

b is Element of the carrier of G

a * b is Element of the carrier of G

the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V28([: the carrier of G, the carrier of G:], the carrier of G) 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 non empty set

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

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

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

[a,b] is set

{a,b} is non empty finite set

{a} is non empty finite set

{{a,b},{a}} is non empty finite V45() set

the multF of G . [a,b] 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 non empty set

a is Element of bool the carrier of G

c

H is Element of the carrier of G

H * a is Element of bool the carrier of G

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

{H} * a is Element of bool the carrier of G

{ (b

H * c

{H} * c

{ (b

a * H is Element of bool the carrier of G

a * {H} is Element of bool the carrier of G

{ (b

c

c

{ (b

G is non empty unital Group-like associative multMagma

the carrier of G is non empty set

H is Element of the carrier of G

a is non empty unital Group-like associative Subgroup of G

H * a is Element of bool the carrier of G

bool the carrier of G is non empty set

carr a is Element of bool the carrier of G

the carrier of a is non empty set

H * (carr a) is Element of bool the carrier of G

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

{H} * (carr a) is Element of bool the carrier of G

{ (b

a * H is Element of bool the carrier of G

(carr a) * H is Element of bool the carrier of G

(carr a) * {H} is Element of bool the carrier of G

{ (b

c

H * c

carr c

the carrier of c

H * (carr c

{H} * (carr c

{ (b

c

(carr c

(carr c

{ (b

G is non empty unital Group-like associative multMagma

the carrier of G is non empty set

a is non empty unital Group-like associative Subgroup of G

H is Element of the carrier of G

H * a is Element of bool the carrier of G

bool the carrier of G is non empty set

carr a is Element of bool the carrier of G

the carrier of a is non empty set

H * (carr a) is Element of bool the carrier of G

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

{H} * (carr a) is Element of bool the carrier of G

{ (b

{H} * a is Element of bool the carrier of G

G is non empty unital Group-like associative multMagma

the carrier of G is non empty set

a is non empty unital Group-like associative Subgroup of G

H is Element of the carrier of G

a * H is Element of bool the carrier of G

bool the carrier of G is non empty set

carr a is Element of bool the carrier of G

the carrier of a is non empty set

(carr a) * H is Element of bool the carrier of G

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

(carr a) * {H} is Element of bool the carrier of G

{ (b

a * {H} is Element of bool the carrier of G

G is non empty unital Group-like associative multMagma

the carrier of G is non empty set

bool the carrier of G is non empty set

H is Element of the carrier of G

a is Element of bool the carrier of G

a * H is Element of bool the carrier of G

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

a * {H} is Element of bool the carrier of G

{ (b

c

(a * H) * c

carr c

the carrier of c

(a * H) * (carr c

{ (b

H * c

H * (carr c

{H} * (carr c

{ (b

a * (H * c

{ (b

{H} * c

a * ({H} * c

{ (b

G is non empty unital Group-like associative multMagma

the carrier of G is non empty set

bool the carrier of G is non empty set

H is Element of the carrier of G

a is Element of bool the carrier of G

c

H * c

carr c

the carrier of c

H * (carr c

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

{H} * (carr c

{ (b

(H * c

{ (b

c

(carr c

{ (b

H * (c

{H} * (c

{ (b

{H} * c

({H} * c

{ (b

G is non empty unital Group-like associative multMagma

the carrier of G is non empty set

bool the carrier of G is non empty set

H is Element of the carrier of G

a is Element of bool the carrier of G

c

a * c

carr c

the carrier of c

a * (carr c

{ (b

(a * c

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

(a * c

{ (b

c

(carr c

(carr c

{ (b

a * (c

{ (b

c

a * (c

{ (b

G is non empty unital Group-like associative multMagma

the carrier of G is non empty set

bool the carrier of G is non empty set

H is Element of the carrier of G

a is Element of bool the carrier of G

H * a is Element of bool the carrier of G

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

{H} * a is Element of bool the carrier of G

{ (b

c

c

carr c

the carrier of c

(carr c

(carr c

{ (b

(c

{ (b

c

(carr c

{ (b

c

(c

{ (b

G is non empty unital Group-like associative multMagma

the carrier of G is non empty set

c

a is non empty unital Group-like associative Subgroup of G

H is Element of the carrier of G

a * H is Element of bool the carrier of G

bool the carrier of G is non empty set

carr a is Element of bool the carrier of G

the carrier of a is non empty set

(carr a) * H is Element of bool the carrier of G

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

(carr a) * {H} is Element of bool the carrier of G

{ (b

(a * H) * c

carr c

the carrier of c

(a * H) * (carr c

{ (b

H * c

H * (carr c

{H} * (carr c

{ (b

a * (H * c

(carr a) * (H * c

{ (b

G is non empty unital Group-like associative multMagma

the carrier of G is non empty set

bool the carrier of G is non empty set

H is set

c

H1 is non empty strict unital Group-like associative Subgroup of G

a is set

the carrier of H1 is non empty set

y is set

a is non empty strict unital Group-like associative Subgroup of G

the carrier of a is non empty set

a is Relation-like Function-like set

c

y is non empty strict unital Group-like associative Subgroup of G

the carrier of y is non empty set

H1 is set

[c

{c

{c

{{c

y is set

[c

{c

{c

{{c

dom a is set

rng a is set

c

y is set

a . y is set

[y,c

{y,c

{y} is non empty finite set

{{y,c

H1 is non empty strict unital Group-like associative Subgroup of G

the carrier of H1 is non empty set

y is non empty strict unital Group-like associative Subgroup of G

the carrier of y is non empty set

H1 is set

[H1,c

{H1,c

{H1} is non empty finite set

{{H1,c

a . H1 is set

H is set

a is set

G is non empty unital Group-like associative multMagma

(G) is set

the non empty strict unital Group-like associative Subgroup of G is non empty strict unital Group-like associative Subgroup of G

G is non empty strict unital Group-like associative multMagma

(G) is non empty set

G is non empty unital Group-like associative multMagma

(G) is non empty set

H is set

a is non empty strict unital Group-like associative Subgroup of G

the carrier of a is non empty set

c

H is Relation-like Function-like set

dom H is set

rng H is set

the carrier of G is non empty set

bool the carrier of G is non empty set

a is set

c

H . c

y is non empty strict unital Group-like associative Subgroup of G

the carrier of y is non empty set

a is set

H . a is set

c

H . c

y is non empty strict unital Group-like associative Subgroup of G

the carrier of y is non empty set

H1 is non empty strict unital Group-like associative Subgroup of G

the carrier of H1 is non empty set

card (G) is cardinal set

card (bool the carrier of G) is cardinal set

G is non empty unital Group-like associative multMagma

the carrier of G is non empty set

a is Element of the carrier of G

a " is Element of the carrier of G

H is Element of the carrier of G

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

the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V28([: the carrier of G, the carrier of G:], the carrier of G) 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 non empty set

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

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

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

[(a "),H] is set

{(a "),H} is non empty finite set

{(a ")} is non empty finite set

{{(a "),H},{(a ")}} is non empty finite V45() set

the multF of G . [(a "),H] is set

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

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

[((a ") * H),a] is set

{((a ") * H),a} is non empty finite set

{((a ") * H)} is non empty finite set

{{((a ") * H),a},{((a ") * H)}} is non empty finite V45() set

the multF of G . [((a ") * H),a] is set

G is non empty unital Group-like associative multMagma

the carrier of G is non empty set

H is Element of the carrier of G

a is Element of the carrier of G

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

a " is Element of the carrier of G

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

the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V28([: the carrier of G, the carrier of G:], the carrier of G) 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 non empty set

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

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

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

[(a "),H] is set

{(a "),H} is non empty finite set

{(a ")} is non empty finite set

{{(a "),H},{(a ")}} is non empty finite V45() set

the multF of G . [(a "),H] is set

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

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

[((a ") * H),a] is set

{((a ") * H),a} is non empty finite set

{((a ") * H)} is non empty finite set

{{((a ") * H),a},{((a ") * H)}} is non empty finite V45() set

the multF of G . [((a ") * H),a] is set

c

(G,c

(a ") * c

the multF of G . ((a "),c

[(a "),c

{(a "),c

{{(a "),c

the multF of G . [(a "),c

((a ") * c

the multF of G . (((a ") * c

[((a ") * c

{((a ") * c

{((a ") * c

{{((a ") * c

the multF of G . [((a ") * c

G is non empty unital Group-like associative multMagma

the carrier of G is non empty set

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

H is Element of the carrier of G

(G,(1_ G),H) is Element of the carrier of G

H " is Element of the carrier of G

(H ") * (1_ 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 V28([: the carrier of G, the carrier of G:], the carrier of G) 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 non empty set

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

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

the multF of G . ((H "),(1_ G)) is Element of the carrier of G

[(H "),(1_ G)] is set

{(H "),(1_ G)} is non empty finite set

{(H ")} is non empty finite set

{{(H "),(1_ G)},{(H ")}} is non empty finite V45() set

the multF of G . [(H "),(1_ G)] is set

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

the multF of G . (((H ") * (1_ G)),H) is Element of the carrier of G

[((H ") * (1_ G)),H] is set

{((H ") * (1_ G)),H} is non empty finite set

{((H ") * (1_ G))} is non empty finite set

{{((H ") * (1_ G)),H},{((H ") * (1_ G))}} is non empty finite V45() set

the multF of G . [((H ") * (1_ G)),H] is set

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

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

[(H "),H] is set

{(H "),H} is non empty finite set

{{(H "),H},{(H ")}} is non empty finite V45() set

the multF of G . [(H "),H] is set

G is non empty unital Group-like associative multMagma

the carrier of G is non empty set

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

H is Element of the carrier of G

a is Element of the carrier of G

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

a " is Element of the carrier of G

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

the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V28([: the carrier of G, the carrier of G:], the carrier of G) 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 non empty set

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

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

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

[(a "),H] is set

{(a "),H} is non empty finite set

{(a ")} is non empty finite set

{{(a "),H},{(a ")}} is non empty finite V45() set

the multF of G . [(a "),H] is set

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

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

[((a ") * H),a] is set

{((a ") * H),a} is non empty finite set

{((a ") * H)} is non empty finite set

{{((a ") * H),a},{((a ") * H)}} is non empty finite V45() set

the multF of G . [((a ") * H),a] is set

G is non empty unital Group-like associative multMagma

the carrier of G is non empty set

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

H is Element of the carrier of G

(G,H,(1_ G)) is Element of the carrier of G

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

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

the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V28([: the carrier of G, the carrier of G:], the carrier of G) 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 non empty set

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

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

the multF of G . (((1_ G) "),H) is Element of the carrier of G

[((1_ G) "),H] is set

{((1_ G) "),H} is non empty finite set

{((1_ G) ")} is non empty finite set

{{((1_ G) "),H},{((1_ G) ")}} is non empty finite V45() set

the multF of G . [((1_ G) "),H] is set

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

the multF of G . ((((1_ G) ") * H),(1_ G)) is Element of the carrier of G

[(((1_ G) ") * H),(1_ G)] is set

{(((1_ G) ") * H),(1_ G)} is non empty finite set

{(((1_ G) ") * H)} is non empty finite set

{{(((1_ G) ") * H),(1_ G)},{(((1_ G) ") * H)}} is non empty finite V45() set

the multF of G . [(((1_ G) ") * H),(1_ G)] is set

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

the multF of G . ((1_ G),H) is Element of the carrier of G

[(1_ G),H] is set

{(1_ G),H} is non empty finite set

{(1_ G)} is non empty finite set

{{(1_ G),H},{(1_ G)}} is non empty finite V45() set

the multF of G . [(1_ G),H] is set

G is non empty unital Group-like associative multMagma

the carrier of G is non empty set

H is Element of the carrier of G

(G,H,H) is Element of the carrier of G

H " is Element of the carrier of G

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

the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V28([: the carrier of G, the carrier of G:], the carrier of G) 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 non empty set

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

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

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

[(H "),H] is set

{(H "),H} is non empty finite set

{(H ")} is non empty finite set

{{(H "),H},{(H ")}} is non empty finite V45() set

the multF of G . [(H "),H] is set

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

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

[((H ") * H),H] is set

{((H ") * H),H} is non empty finite set

{((H ") * H)} is non empty finite set

{{((H ") * H),H},{((H ") * H)}} is non empty finite V45() set

the multF of G . [((H ") * H),H] is set

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

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

the multF of G . ((1_ G),H) is Element of the carrier of G

[(1_ G),H] is set

{(1_ G),H} is non empty finite set

{(1_ G)} is non empty finite set

{{(1_ G),H},{(1_ G)}} is non empty finite V45() set

the multF of G . [(1_ G),H] is set

G is non empty unital Group-like associative multMagma

the carrier of G is non empty set

a is non empty unital Group-like associative multMagma

the carrier of a is non empty set

H is Element of the carrier of G

H " is Element of the carrier of G

(G,H,(H ")) is Element of the carrier of G

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

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

the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V28([: the carrier of G, the carrier of G:], the carrier of G) 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 non empty set

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

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

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

[((H ") "),H] is set

{((H ") "),H} is non empty finite set

{((H ") ")} is non empty finite set

{{((H ") "),H},{((H ") ")}} is non empty finite V45() set

the multF of G . [((H ") "),H] is set

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

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

[(((H ") ") * H),(H ")] is set

{(((H ") ") * H),(H ")} is non empty finite set

{(((H ") ") * H)} is non empty finite set

{{(((H ") ") * H),(H ")},{(((H ") ") * H)}} is non empty finite V45() set

the multF of G . [(((H ") ") * H),(H ")] is set

c

c

(a,(c

(c

the multF of a is Relation-like [: the carrier of a, the carrier of a:] -defined the carrier of a -valued Function-like V28([: the carrier of a, the carrier of a:], the carrier of a) associative Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]

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

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

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

the multF of a . ((c

[(c

{(c

{(c

{{(c

the multF of a . [(c

((c

the multF of a . (((c

[((c

{((c

{((c

{{((c

the multF of a . [((c

G is non empty unital Group-like associative multMagma

the carrier of G is non empty set

H is Element of the carrier of G

a is Element of the carrier of G

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

a " is Element of the carrier of G

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

the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V28([: the carrier of G, the carrier of G:], the carrier of G) 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 non empty set

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

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

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

[(a "),H] is set

{(a "),H} is non empty finite set

{(a ")} is non empty finite set

{{(a "),H},{(a ")}} is non empty finite V45() set

the multF of G . [(a "),H] is set

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

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

[((a ") * H),a] is set

{((a ") * H),a} is non empty finite set

{((a ") * H)} is non empty finite set

{{((a ") * H),a},{((a ") * H)}} is non empty finite V45() set

the multF of G . [((a ") * H),a] is set

H * a is Element of the carrier of G

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

[H,a] is set

{H,a} is non empty finite set

{H} is non empty finite set

{{H,a},{H}} is non empty finite V45() set

the multF of G . [H,a] is set

a * H is Element of the carrier of G

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

[a,H] is set

{a,H} is non empty finite set

{a} is non empty finite set

{{a,H},{a}} is non empty finite V45() set

the multF of G . [a,H] is set

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

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

[(a "),(H * a)] is set

{(a "),(H * a)} is non empty finite set

{{(a "),(H * a)},{(a ")}} is non empty finite V45() set

the multF of G . [(a "),(H * a)] is set

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

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

[(a "),(H * a)] is set

{(a "),(H * a)} is non empty finite set

{{(a "),(H * a)},{(a ")}} is non empty finite V45() set

the multF of G . [(a "),(H * a)] is set

G is non empty unital Group-like associative multMagma

the carrier of G is non empty set

H is Element of the carrier of G

a is Element of the carrier of G

H * a is Element of the carrier of G

the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like V28([: the carrier of G, the carrier of G:], the carrier of G) 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 non empty set

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

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

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

[H,a] is set

{H,a} is non empty finite set

{H} is non empty finite set

{{H,a},{H}} is non empty finite V45() set

the multF of G . [H,a] is set

c

(G,(H * a),c

c

(c

the multF of G . ((c

[(c

{(c

{(c

{{(c

the multF of G . [(c

((c

the multF of G . (((c

[((c

{((c

{((c

{{((c

the multF of G . [((c

(G,H,c

(c

the multF of G . ((c

[(c

{(c

{{(c

the multF of G . [(c

((c

the multF of G . (((c

[((c

{((c

{((c

{{((c

the multF of G . [((c

(G,a,c

(c

the multF of G . ((c

[(c

{(c

{{(c

the multF of G . [(c

((c

the multF of G . (((c

[((c

{((c

{((c

{{((c

the multF of G . [((c

(G,H,c

the multF of G . ((G,H,c

[(G,H,c

{(G,H,c

{(G,H,c

{{(G,H,c

the multF of G . [(G,H,c

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

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

the multF of G . (H,(1_ G)) is Element of the carrier of G

[H,(1_ G)] is set

{H,(1_ G)} is non empty finite set

{{H,(1_ G)},{H}} is non empty finite V45() set

the multF of G . [H,(1_ G)] is set

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

the multF of G . ((H * (1_ G)),a) is Element of the carrier of G

[(H * (1_ G)),a] is set

{(H * (1_ G)),a} is non empty finite set

{(H * (1_ G))} is non empty finite set

{{(H * (1_ G)),a},{(H * (1_ G))}} is non empty finite V45() set

the multF of G . [(H * (1_ G)),a] is set

(c

the multF of G . ((c

[(c

{(c

{{(c

the multF of G . [(c

((c

the multF of G . (((c

[((c

{((c

{((c

{{((c

the multF of G . [((c

c

the multF of G . (c

[c

{c

{c

{{c

the multF of G . [c

H * (c

the multF of G . (H,(c

[H,(c

{H,(c

{{H,(c

the multF of G . [H,(c

(H * (c

the multF of G . ((H * (c

[(H * (c

{(H * (c

{(H * (c

{{(H * (c

the multF of G . [(H * (c

(c

the multF of G . ((c

[(c

{(c

{{(c

the multF of G . [(c

((c

the multF of G . (((c

[((c

{((c

{((c

{{((c

the multF of G . [((c

H * c

the multF of G . (H,c

[H,c

{H,c

{{H,c

the multF of G . [H,c

(H * c

the multF of G . ((H * c

[(H * c

{(H * c

{(H * c

{{(H * c

the multF of G . [(H * c

((H * c

the multF of G . (((H * c

[((H * c

{((H * c

{((H * c

{{((H * c

the multF of G . [((H * c

(c

the multF of G . ((c

[(c

{(c

{{(c

the multF of G . [(c

((c

the multF of G . (((c

[((c

{((c

{((c

{{((c

the multF of G . [((c

(H * c

the multF of G . ((H * c

[(H * c

{(H * c

{{(H * c

the multF of G . [(H * c

(c

the multF of G . ((c

[(c

{(c

{{(c

the multF of G . [(c

((c

the multF of G . (((c

[((c

{((c

{((c

{{((c

the multF of G . [((c

(c

the multF of G . ((c

[(c

{(c

{{(c

the multF of G .