:: GROUP_2 semantic presentation

REAL is V46() V47() V48() V52() set

NAT is non trivial V20() V46() V47() V48() V49() V50() V51() V52() non finite cardinal limit_cardinal Element of bool REAL

bool REAL is non empty cup-closed diff-closed preBoolean set

{} is empty V20() V24() V46() V47() V48() V49() V50() V51() V52() finite V57() cardinal {} -element set

the empty V20() V24() V46() V47() V48() V49() V50() V51() V52() finite V57() cardinal {} -element set is empty V20() V24() V46() V47() V48() V49() V50() V51() V52() finite V57() cardinal {} -element set

COMPLEX is V46() V52() set

NAT is non trivial V20() V46() V47() V48() V49() V50() V51() V52() non finite cardinal limit_cardinal set

bool NAT is non empty non trivial cup-closed diff-closed preBoolean non finite set

1 is non empty V20() V24() ext-real positive V42() V43() V44() V46() V47() V48() V49() V50() V51() finite cardinal Element of NAT

card {} is empty V20() V24() V46() V47() V48() V49() V50() V51() V52() finite V57() cardinal {} -element set

2 is non empty V20() V24() ext-real positive V42() V43() V44() V46() V47() V48() V49() V50() V51() finite cardinal Element of NAT

union {} is finite set

0 is empty V20() V24() ext-real V42() V43() V44() V46() V47() V48() V49() V50() V51() V52() finite V57() cardinal {} -element Element of NAT

H is non empty 1-sorted

the carrier of H is non empty set

bool the carrier of H is non empty cup-closed diff-closed preBoolean set

G is set

x is Element of bool the carrier of H

G is non empty 1-sorted

the carrier of G is non empty set

bool the carrier of G is non empty cup-closed diff-closed preBoolean set

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 cup-closed diff-closed preBoolean set

H is Element of bool the carrier of G

{ (b

y is set

y is Element of the carrier of G

y " is Element of the carrier of G

x is Element of bool the carrier of G

y is Element of bool the carrier of G

{ (b

{ (b

y is set

B is Element of the carrier of G

B " is Element of the carrier of G

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

y is set

B is Element of the carrier of G

B " is Element of the carrier of G

B is Element of the carrier of G

B " is Element of the carrier of G

H is non empty unital Group-like associative multMagma

the carrier of H is non empty set

bool the carrier of H is non empty cup-closed diff-closed preBoolean set

y is non empty unital Group-like associative multMagma

the carrier of y is non empty set

bool the carrier of y is non empty cup-closed diff-closed preBoolean set

G is set

x is Element of bool the carrier of H

(H,x) is Element of bool the carrier of H

{ (b

y is set

B is Element of the carrier of y

B " is Element of the carrier of y

B is Element of bool the carrier of y

(y,B) is Element of bool the carrier of y

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

{H} is non empty trivial finite 1 -element Element of bool the carrier of G

bool the carrier of G is non empty cup-closed diff-closed preBoolean set

(G,{H}) is Element of bool the carrier of G

{ (b

H " is Element of the carrier of G

{(H ")} is non empty trivial finite 1 -element Element of bool the carrier of G

x is set

y is Element of the carrier of G

y " is Element of the carrier of G

x 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

H " is Element of the carrier of G

x is Element of the carrier of G

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

bool the carrier of G is non empty cup-closed diff-closed preBoolean set

(G,{H,x}) is Element of bool the carrier of G

{ (b

x " is Element of the carrier of G

{(H "),(x ")} is non empty finite Element of bool the carrier of G

y is set

y is Element of the carrier of G

y " is Element of the carrier of G

y is set

G is non empty unital Group-like associative multMagma

the carrier of G is non empty set

{} the carrier of G is empty proper V20() V24() V46() V47() V48() V49() V50() V51() V52() finite V57() cardinal {} -element Element of bool the carrier of G

bool the carrier of G is non empty cup-closed diff-closed preBoolean set

(G,({} the carrier of G)) is Element of bool the carrier of G

{ (b

H is set

x is Element of the carrier of G

x " is Element of the carrier of G

G is non empty unital Group-like associative multMagma

the carrier of G is non empty set

[#] the carrier of G is non empty non proper Element of bool the carrier of G

bool the carrier of G is non empty cup-closed diff-closed preBoolean set

(G,([#] the carrier of G)) is Element of bool the carrier of G

{ (b

H is set

x is Element of the carrier of G

x " is Element of the carrier of G

(x ") " is Element of 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 cup-closed diff-closed preBoolean set

H is Element of bool the carrier of G

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

{ (b

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

the Element of H is Element of H

y is Element of the carrier of G

y " is Element of the carrier of G

y is Element of the carrier of G

y " is Element of 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 cup-closed diff-closed preBoolean set

H is empty proper V20() V24() V46() V47() V48() V49() V50() V51() V52() finite V57() cardinal {} -element Element of bool the carrier of G

(G,H) 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 non empty cup-closed diff-closed preBoolean set

H is non empty Element of bool the carrier of G

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

{ (b

G is non empty multMagma

the carrier of G is non empty set

bool the carrier of G is non empty cup-closed diff-closed preBoolean set

H is Element of bool the carrier of G

x is Element of bool the carrier of G

{ (b

y is set

B is Element of the carrier of G

B is Element of the carrier of G

B * 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) 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 cup-closed diff-closed preBoolean set

the multF of G . (B,B) is Element of the carrier of G

[B,B] is set

{B,B} is non empty finite set

{B} is non empty trivial finite 1 -element set

{{B,B},{B}} is non empty finite V57() set

the multF of G . [B,B] is set

G is non empty commutative multMagma

the carrier of G is non empty set

bool the carrier of G is non empty cup-closed diff-closed preBoolean set

y is Element of bool the carrier of G

y is Element of bool the carrier of G

(G,y,y) is Element of bool the carrier of G

{ (b

(G,y,y) is Element of bool the carrier of G

{ (b

B is set

B is Element of the carrier of G

a is Element of the carrier of G

B * 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) 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 cup-closed diff-closed preBoolean set

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

[B,a] is set

{B,a} is non empty finite set

{B} is non empty trivial finite 1 -element set

{{B,a},{B}} is non empty finite V57() set

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

B is set

B is Element of the carrier of G

a is Element of the carrier of G

B * 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) 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 cup-closed diff-closed preBoolean set

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

[B,a] is set

{B,a} is non empty finite set

{B} is non empty trivial finite 1 -element set

{{B,a},{B}} is non empty finite V57() set

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

H is non empty multMagma

the carrier of H is non empty set

bool the carrier of H is non empty cup-closed diff-closed preBoolean set

B is non empty multMagma

the carrier of B is non empty set

bool the carrier of B is non empty cup-closed diff-closed preBoolean set

G is set

x is Element of bool the carrier of H

y is Element of bool the carrier of H

(H,x,y) is Element of bool the carrier of H

{ (b

y is set

Y is Element of the carrier of B

y is Element of the carrier of B

Y * y 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 V28([: the carrier of B, the carrier of B:], the carrier of B) Element of bool [:[: the carrier of B, the carrier of B:], the carrier of B:]

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

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

bool [:[: the carrier of B, the carrier of B:], the carrier of B:] is non empty cup-closed diff-closed preBoolean set

the multF of B . (Y,y) is Element of the carrier of B

[Y,y] is set

{Y,y} is non empty finite set

{Y} is non empty trivial finite 1 -element set

{{Y,y},{Y}} is non empty finite V57() set

the multF of B . [Y,y] is set

B is Element of bool the carrier of B

a is Element of bool the carrier of B

(B,B,a) is Element of bool the carrier of B

{ (b

G is non empty multMagma

the carrier of G is non empty set

bool the carrier of G is non empty cup-closed diff-closed preBoolean set

H is Element of bool the carrier of G

x is Element of bool the carrier of G

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

{ (b

the Element of H is Element of H

the Element of x is Element of x

y is Element of the carrier of G

y is Element of the carrier of G

y * y 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) 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 cup-closed diff-closed preBoolean set

the multF of G . (y,y) is Element of the carrier of G

[y,y] is set

{y,y} is non empty finite set

{y} is non empty trivial finite 1 -element set

{{y,y},{y}} is non empty finite V57() set

the multF of G . [y,y] is set

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

y is Element of the carrier of G

B is Element of the carrier of G

y * 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) 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 cup-closed diff-closed preBoolean set

the multF of G . (y,B) is Element of the carrier of G

[y,B] is set

{y,B} is non empty finite set

{y} is non empty trivial finite 1 -element set

{{y,B},{y}} is non empty finite V57() set

the multF of G . [y,B] is set

G is non empty multMagma

the carrier of G is non empty set

bool the carrier of G is non empty cup-closed diff-closed preBoolean set

H is Element of bool the carrier of G

x is Element of bool the carrier of G

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

{ (b

y is Element of bool the carrier of G

(G,(G,H,x),y) is Element of bool the carrier of G

{ (b

(G,x,y) is Element of bool the carrier of G

{ (b

(G,H,(G,x,y)) is Element of bool the carrier of G

{ (b

y is set

B is Element of the carrier of G

B is Element of the carrier of G

B * 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) 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 cup-closed diff-closed preBoolean set

the multF of G . (B,B) is Element of the carrier of G

[B,B] is set

{B,B} is non empty finite set

{B} is non empty trivial finite 1 -element set

{{B,B},{B}} is non empty finite V57() set

the multF of G . [B,B] is set

a is Element of the carrier of G

Y is Element of the carrier of G

a * Y is Element of the carrier of G

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

[a,Y] is set

{a,Y} is non empty finite set

{a} is non empty trivial finite 1 -element set

{{a,Y},{a}} is non empty finite V57() set

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

Y * B is Element of the carrier of G

the multF of G . (Y,B) is Element of the carrier of G

[Y,B] is set

{Y,B} is non empty finite set

{Y} is non empty trivial finite 1 -element set

{{Y,B},{Y}} is non empty finite V57() set

the multF of G . [Y,B] is set

a * (Y * B) is Element of the carrier of G

the multF of G . (a,(Y * B)) is Element of the carrier of G

[a,(Y * B)] is set

{a,(Y * B)} is non empty finite set

{{a,(Y * B)},{a}} is non empty finite V57() set

the multF of G . [a,(Y * B)] is set

y is set

B is Element of the carrier of G

B is Element of the carrier of G

B * 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) 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 cup-closed diff-closed preBoolean set

the multF of G . (B,B) is Element of the carrier of G

[B,B] is set

{B,B} is non empty finite set

{B} is non empty trivial finite 1 -element set

{{B,B},{B}} is non empty finite V57() set

the multF of G . [B,B] is set

a is Element of the carrier of G

Y is Element of the carrier of G

a * Y is Element of the carrier of G

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

[a,Y] is set

{a,Y} is non empty finite set

{a} is non empty trivial finite 1 -element set

{{a,Y},{a}} is non empty finite V57() set

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

B * a is Element of the carrier of G

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

[B,a] is set

{B,a} is non empty finite set

{{B,a},{B}} is non empty finite V57() set

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

(B * a) * Y is Element of the carrier of G

the multF of G . ((B * a),Y) is Element of the carrier of G

[(B * a),Y] is set

{(B * a),Y} is non empty finite set

{(B * a)} is non empty trivial finite 1 -element set

{{(B * a),Y},{(B * a)}} is non empty finite V57() set

the multF of G . [(B * a),Y] 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 cup-closed diff-closed preBoolean set

H is Element of bool the carrier of G

x is Element of bool the carrier of G

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

{ (b

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

{ (b

(G,x) is Element of bool the carrier of G

{ (b

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

{ (b

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

{ (b

y is set

y is Element of the carrier of G

y " is Element of the carrier of G

B is Element of the carrier of G

B is Element of the carrier of G

B * 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 having_a_unity 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 cup-closed diff-closed preBoolean set

the multF of G . (B,B) is Element of the carrier of G

[B,B] is set

{B,B} is non empty finite set

{B} is non empty trivial finite 1 -element set

{{B,B},{B}} is non empty finite V57() set

the multF of G . [B,B] is set

B " is Element of the carrier of G

B " is Element of the carrier of G

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

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

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

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

{(B ")} is non empty trivial finite 1 -element set

{{(B "),(B ")},{(B ")}} is non empty finite V57() set

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

y is set

y is Element of the carrier of G

B is Element of the carrier of G

y * 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 having_a_unity 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 cup-closed diff-closed preBoolean set

the multF of G . (y,B) is Element of the carrier of G

[y,B] is set

{y,B} is non empty finite set

{y} is non empty trivial finite 1 -element set

{{y,B},{y}} is non empty finite V57() set

the multF of G . [y,B] is set

B is Element of the carrier of G

B " is Element of the carrier of G

a is Element of the carrier of G

a " is Element of the carrier of G

B * a is Element of the carrier of G

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

[B,a] is set

{B,a} is non empty finite set

{B} is non empty trivial finite 1 -element set

{{B,a},{B}} is non empty finite V57() set

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

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

G is non empty multMagma

the carrier of G is non empty set

bool the carrier of G is non empty cup-closed diff-closed preBoolean set

H is Element of bool the carrier of G

x is Element of bool the carrier of G

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

{ (b

y is Element of bool the carrier of G

x \/ y is Element of bool the carrier of G

(G,H,(x \/ y)) is Element of bool the carrier of G

{ (b

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

{ (b

(G,H,x) \/ (G,H,y) is Element of bool the carrier of G

y is set

B is Element of the carrier of G

B is Element of the carrier of G

B * 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) 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 cup-closed diff-closed preBoolean set

the multF of G . (B,B) is Element of the carrier of G

[B,B] is set

{B,B} is non empty finite set

{B} is non empty trivial finite 1 -element set

{{B,B},{B}} is non empty finite V57() set

the multF of G . [B,B] is set

y is set

B is Element of the carrier of G

B is Element of the carrier of G

B * 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) 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 cup-closed diff-closed preBoolean set

the multF of G . (B,B) is Element of the carrier of G

[B,B] is set

{B,B} is non empty finite set

{B} is non empty trivial finite 1 -element set

{{B,B},{B}} is non empty finite V57() set

the multF of G . [B,B] is set

B is Element of the carrier of G

B is Element of the carrier of G

B * 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) 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 cup-closed diff-closed preBoolean set

the multF of G . (B,B) is Element of the carrier of G

[B,B] is set

{B,B} is non empty finite set

{B} is non empty trivial finite 1 -element set

{{B,B},{B}} is non empty finite V57() set

the multF of G . [B,B] is set

G is non empty multMagma

the carrier of G is non empty set

bool the carrier of G is non empty cup-closed diff-closed preBoolean set

H is Element of bool the carrier of G

x is Element of bool the carrier of G

H \/ x is Element of bool the carrier of G

y is Element of bool the carrier of G

(G,(H \/ x),y) is Element of bool the carrier of G

{ (b

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

{ (b

(G,x,y) is Element of bool the carrier of G

{ (b

(G,H,y) \/ (G,x,y) is Element of bool the carrier of G

y is set

B is Element of the carrier of G

B is Element of the carrier of G

B * 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) 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 cup-closed diff-closed preBoolean set

the multF of G . (B,B) is Element of the carrier of G

[B,B] is set

{B,B} is non empty finite set

{B} is non empty trivial finite 1 -element set

{{B,B},{B}} is non empty finite V57() set

the multF of G . [B,B] is set

y is set

B is Element of the carrier of G

B is Element of the carrier of G

B * 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) 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 cup-closed diff-closed preBoolean set

the multF of G . (B,B) is Element of the carrier of G

[B,B] is set

{B,B} is non empty finite set

{B} is non empty trivial finite 1 -element set

{{B,B},{B}} is non empty finite V57() set

the multF of G . [B,B] is set

B is Element of the carrier of G

B is Element of the carrier of G

B * 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) 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 cup-closed diff-closed preBoolean set

the multF of G . (B,B) is Element of the carrier of G

[B,B] is set

{B,B} is non empty finite set

{B} is non empty trivial finite 1 -element set

{{B,B},{B}} is non empty finite V57() set

the multF of G . [B,B] is set

G is non empty multMagma

the carrier of G is non empty set

bool the carrier of G is non empty cup-closed diff-closed preBoolean set

H is Element of bool the carrier of G

x is Element of bool the carrier of G

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

{ (b

y is Element of bool the carrier of G

x /\ y is Element of bool the carrier of G

(G,H,(x /\ y)) is Element of bool the carrier of G

{ (b

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

{ (b

(G,H,x) /\ (G,H,y) is Element of bool the carrier of G

y is set

B is Element of the carrier of G

B is Element of the carrier of G

B * 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) 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 cup-closed diff-closed preBoolean set

the multF of G . (B,B) is Element of the carrier of G

[B,B] is set

{B,B} is non empty finite set

{B} is non empty trivial finite 1 -element set

{{B,B},{B}} is non empty finite V57() set

the multF of G . [B,B] is set

G is non empty multMagma

the carrier of G is non empty set

bool the carrier of G is non empty cup-closed diff-closed preBoolean set

H is Element of bool the carrier of G

x is Element of bool the carrier of G

H /\ x is Element of bool the carrier of G

y is Element of bool the carrier of G

(G,(H /\ x),y) is Element of bool the carrier of G

{ (b

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

{ (b

(G,x,y) is Element of bool the carrier of G

{ (b

(G,H,y) /\ (G,x,y) is Element of bool the carrier of G

y is set

B is Element of the carrier of G

B is Element of the carrier of G

B * 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) 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 cup-closed diff-closed preBoolean set

the multF of G . (B,B) is Element of the carrier of G

[B,B] is set

{B,B} is non empty finite set

{B} is non empty trivial finite 1 -element set

{{B,B},{B}} is non empty finite V57() set

the multF of G . [B,B] is set

G is non empty multMagma

the carrier of G is non empty set

bool the carrier of G is non empty cup-closed diff-closed preBoolean set

{} the carrier of G is empty proper V20() V24() V46() V47() V48() V49() V50() V51() V52() finite V57() cardinal {} -element Element of bool the carrier of G

H is Element of bool the carrier of G

(G,({} the carrier of G),H) is Element of bool the carrier of G

{ (b

(G,H,({} the carrier of G)) is Element of bool the carrier of G

{ (b

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

y is Element of the carrier of G

y is Element of the carrier of G

y * y 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) 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 cup-closed diff-closed preBoolean set

the multF of G . (y,y) is Element of the carrier of G

[y,y] is set

{y,y} is non empty finite set

{y} is non empty trivial finite 1 -element set

{{y,y},{y}} is non empty finite V57() set

the multF of G . [y,y] is set

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

y is Element of the carrier of G

y is Element of the carrier of G

y * y 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) 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 cup-closed diff-closed preBoolean set

the multF of G . (y,y) is Element of the carrier of G

[y,y] is set

{y,y} is non empty finite set

{y} is non empty trivial finite 1 -element set

{{y,y},{y}} is non empty finite V57() set

the multF of G . [y,y] 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 cup-closed diff-closed preBoolean set

[#] the carrier of G is non empty non proper Element of bool the carrier of G

H is Element of bool the carrier of G

(G,([#] the carrier of G),H) is Element of bool the carrier of G

{ (b

(G,H,([#] the carrier of G)) is Element of bool the carrier of G

{ (b

the Element of H is Element of H

B is set

a is Element of the carrier of G

B 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 having_a_unity 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 cup-closed diff-closed preBoolean 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 trivial finite 1 -element set

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

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

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

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

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

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

{(a * (B "))} is non empty trivial finite 1 -element set

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

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

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

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

[(B "),B] is set

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

{(B ")} is non empty trivial finite 1 -element set

{{(B "),B},{(B ")}} is non empty finite V57() set

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

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

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

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

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

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

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

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

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

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

[a,(1_ G)] is set

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

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

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

y is set

y is Element of the carrier of G

y " is Element of the carrier of G

B is Element of the carrier of G

(y ") * 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 having_a_unity 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 cup-closed diff-closed preBoolean set

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

[(y "),B] is set

{(y "),B} is non empty finite set

{(y ")} is non empty trivial finite 1 -element set

{{(y "),B},{(y ")}} is non empty finite V57() set

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

y * ((y ") * B) is Element of the carrier of G

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

[y,((y ") * B)] is set

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

{y} is non empty trivial finite 1 -element set

{{y,((y ") * B)},{y}} is non empty finite V57() set

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

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

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

[y,(y ")] is set

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

{{y,(y ")},{y}} is non empty finite V57() set

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

(y * (y ")) * B is Element of the carrier of G

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

[(y * (y ")),B] is set

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

{(y * (y "))} is non empty trivial finite 1 -element set

{{(y * (y ")),B},{(y * (y "))}} is non empty finite V57() set

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

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

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

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

[(1_ G),B] is set

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

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

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

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

G is non empty multMagma

the carrier of G is non empty set

H is Element of the carrier of G

{H} is non empty trivial finite 1 -element Element of bool the carrier of G

bool the carrier of G is non empty cup-closed diff-closed preBoolean set

x is Element of the carrier of G

{x} is non empty trivial finite 1 -element Element of bool the carrier of G

(G,{H},{x}) is Element of bool the carrier of G

{ (b

H * x 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) 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 cup-closed diff-closed preBoolean set

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

[H,x] is set

{H,x} is non empty finite set

{H} is non empty trivial finite 1 -element set

{{H,x},{H}} is non empty finite V57() set

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

{(H * x)} is non empty trivial finite 1 -element Element of bool the carrier of G

y is set

y is Element of the carrier of G

B is Element of the carrier of G

y * B is Element of the carrier of G

the multF of G . (y,B) is Element of the carrier of G

[y,B] is set

{y,B} is non empty finite set

{y} is non empty trivial finite 1 -element set

{{y,B},{y}} is non empty finite V57() set

the multF of G . [y,B] is set

y is set

G is non empty multMagma

the carrier of G is non empty set

H is Element of the carrier of G

{H} is non empty trivial finite 1 -element Element of bool the carrier of G

bool the carrier of G is non empty cup-closed diff-closed preBoolean set

x is Element of the carrier of G

H * x 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) 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 cup-closed diff-closed preBoolean set

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

[H,x] is set

{H,x} is non empty finite set

{H} is non empty trivial finite 1 -element set

{{H,x},{H}} is non empty finite V57() set

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

y is Element of the carrier of G

{x,y} is non empty finite Element of bool the carrier of G

(G,{H},{x,y}) is Element of bool the carrier of G

{ (b

H * y is Element of the carrier of G

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

[H,y] is set

{H,y} is non empty finite set

{{H,y},{H}} is non empty finite V57() set

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

{(H * x),(H * y)} is non empty finite Element of bool the carrier of G

y is set

B is Element of the carrier of G

B is Element of the carrier of G

B * B is Element of the carrier of G

the multF of G . (B,B) is Element of the carrier of G

[B,B] is set

{B,B} is non empty finite set

{B} is non empty trivial finite 1 -element set

{{B,B},{B}} is non empty finite V57() set

the multF of G . [B,B] is set

y is set

G is non empty multMagma

the carrier of G is non empty set

H is Element of the carrier of G

x is Element of the carrier of G

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

bool the carrier of G is non empty cup-closed diff-closed preBoolean set

y is Element of the carrier of G

{y} is non empty trivial finite 1 -element Element of bool the carrier of G

(G,{H,x},{y}) is Element of bool the carrier of G

{ (b

H * y 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) 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 cup-closed diff-closed preBoolean set

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

[H,y] is set

{H,y} is non empty finite set

{H} is non empty trivial finite 1 -element set

{{H,y},{H}} is non empty finite V57() set

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

x * y is Element of the carrier of G

the multF of G . (x,y) is Element of the carrier of G

[x,y] is set

{x,y} is non empty finite set

{x} is non empty trivial finite 1 -element set

{{x,y},{x}} is non empty finite V57() set

the multF of G . [x,y] is set

{(H * y),(x * y)} is non empty finite Element of bool the carrier of G

y is set

B is Element of the carrier of G

B is Element of the carrier of G

B * B is Element of the carrier of G

the multF of G . (B,B) is Element of the carrier of G

[B,B] is set

{B,B} is non empty finite set

{B} is non empty trivial finite 1 -element set

{{B,B},{B}} is non empty finite V57() set

the multF of G . [B,B] is set

y is set

G is non empty multMagma

the carrier of G is non empty set

H is Element of the carrier of G

x is Element of the carrier of G

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

bool the carrier of G is non empty cup-closed diff-closed preBoolean set

y is Element of the carrier of G

H * y 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) 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 cup-closed diff-closed preBoolean set

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

[H,y] is set

{H,y} is non empty finite set

{H} is non empty trivial finite 1 -element set

{{H,y},{H}} is non empty finite V57() set

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

x * y is Element of the carrier of G

the multF of G . (x,y) is Element of the carrier of G

[x,y] is set

{x,y} is non empty finite set

{x} is non empty trivial finite 1 -element set

{{x,y},{x}} is non empty finite V57() set

the multF of G . [x,y] is set

y is Element of the carrier of G

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

(G,{H,x},{y,y}) is Element of bool the carrier of G

{ (b

H * y is Element of the carrier of G

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

[H,y] is set

{H,y} is non empty finite set

{{H,y},{H}} is non empty finite V57() set

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

x * y is Element of the carrier of G

the multF of G . (x,y) is Element of the carrier of G

[x,y] is set

{x,y} is non empty finite set

{{x,y},{x}} is non empty finite V57() set

the multF of G . [x,y] is set

{(H * y),(H * y),(x * y),(x * y)} is non empty finite Element of bool the carrier of G

a is set

Y is Element of the carrier of G

y is Element of the carrier of G

Y * y is Element of the carrier of G

the multF of G . (Y,y) is Element of the carrier of G

[Y,y] is set

{Y,y} is non empty finite set

{Y} is non empty trivial finite 1 -element set

{{Y,y},{Y}} is non empty finite V57() set

the multF of G . [Y,y] is set

a 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 cup-closed diff-closed preBoolean set

H is Element of bool the carrier of G

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

{ (b

x is set

y is Element of the carrier of G

y is Element of the carrier of G

y * y 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 having_a_unity 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 cup-closed diff-closed preBoolean set

the multF of G . (y,y) is Element of the carrier of G

[y,y] is set

{y,y} is non empty finite set

{y} is non empty trivial finite 1 -element set

{{y,y},{y}} is non empty finite V57() set

the multF of G . [y,y] is set

x is set

y is Element of the carrier of G

y " is Element of the carrier of G

(y ") * y 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 having_a_unity 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 cup-closed diff-closed preBoolean set

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

[(y "),y] is set

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

{(y ")} is non empty trivial finite 1 -element set

{{(y "),y},{(y ")}} is non empty finite V57() set

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

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

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

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

[(1_ G),y] is set

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

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

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

the multF of G . [(1_ G),y] 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 cup-closed diff-closed preBoolean set

H is Element of bool the carrier of G

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

{ (b

x is set

y is Element of the carrier of G

y " is Element of the carrier of G

x is set

y is Element of the carrier of G

y " is Element of the carrier of G

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

G is non empty multMagma

the carrier of G is non empty set

bool the carrier of G is non empty cup-closed diff-closed preBoolean set

H is Element of bool the carrier of G

x is Element of bool the carrier of G

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

{ (b

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

{ (b

y is set

y is Element of the carrier of G

B is Element of the carrier of G

y * 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) 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 cup-closed diff-closed preBoolean set

the multF of G . (y,B) is Element of the carrier of G

[y,B] is set

{y,B} is non empty finite set

{y} is non empty trivial finite 1 -element set

{{y,B},{y}} is non empty finite V57() set

the multF of G . [y,B] is set

B * y is Element of the carrier of G

the multF of G . (B,y) is Element of the carrier of G

[B,y] is set

{B,y} is non empty finite set

{B} is non empty trivial finite 1 -element set

{{B,y},{B}} is non empty finite V57() set

the multF of G . [B,y] is set

y is set

y is Element of the carrier of G

B is Element of the carrier of G

y * 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) 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 cup-closed diff-closed preBoolean set

the multF of G . (y,B) is Element of the carrier of G

[y,B] is set

{y,B} is non empty finite set

{y} is non empty trivial finite 1 -element set

{{y,B},{y}} is non empty finite V57() set

the multF of G . [y,B] is set

B * y is Element of the carrier of G

the multF of G . (B,y) is Element of the carrier of G

[B,y] is set

{B,y} is non empty finite set

{B} is non empty trivial finite 1 -element set

{{B,y},{B}} is non empty finite V57() set

the multF of G . [B,y] 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

x is Element of the carrier of G

H * x 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 having_a_unity 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 cup-closed diff-closed preBoolean set

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

[H,x] is set

{H,x} is non empty finite set

{H} is non empty trivial finite 1 -element set

{{H,x},{H}} is non empty finite V57() set

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

x * H is Element of the carrier of G

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

[x,H] is set

{x,H} is non empty finite set

{x} is non empty trivial finite 1 -element set

{{x,H},{x}} is non empty finite V57() set

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

G is non empty multMagma

the carrier of G is non empty set

bool the carrier of G is non empty cup-closed diff-closed preBoolean set

H is Element of bool the carrier of G

x is Element of bool the carrier of G

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

{ (b

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

{ (b

y is set

y is Element of the carrier of G

B is Element of the carrier of G

y * 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) 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 cup-closed diff-closed preBoolean set

the multF of G . (y,B) is Element of the carrier of G

[y,B] is set

{y,B} is non empty finite set

{y} is non empty trivial finite 1 -element set

{{y,B},{y}} is non empty finite V57() set

the multF of G . [y,B] is set

B * y is Element of the carrier of G

the multF of G . (B,y) is Element of the carrier of G

[B,y] is set

{B,y} is non empty finite set

{B} is non empty trivial finite 1 -element set

{{B,y},{B}} is non empty finite V57() set

the multF of G . [B,y] is set

y is set

y is Element of the carrier of G

B is Element of the carrier of G

y * 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) 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 cup-closed diff-closed preBoolean set

the multF of G . (y,B) is Element of the carrier of G

[y,B] is set

{y,B} is non empty finite set

{y} is non empty trivial finite 1 -element set

{{y,B},{y}} is non empty finite V57() set

the multF of G . [y,B] is set

B * y is Element of the carrier of G

the multF of G . (B,y) is Element of the carrier of G

[B,y] is set

{B,y} is non empty finite set

{B} is non empty trivial finite 1 -element set

{{B,y},{B}} is non empty finite V57() set

the multF of G . [B,y] is set

G is non empty unital Group-like associative commutative multMagma

the carrier of G is non empty set

bool the carrier of G is non empty cup-closed diff-closed preBoolean set

H is Element of bool the carrier of G

x is Element of bool the carrier of G

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

{ (b

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

{ (b

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

{ (b

(G,x) is Element of bool the carrier of G

{ (b

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

{ (b

y is set

y is Element of the carrier of G

y " is Element of the carrier of G

B is Element of the carrier of G

B is Element of the carrier of G

B * 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 having_a_unity 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 cup-closed diff-closed preBoolean set

the multF of G . (B,B) is Element of the carrier of G

[B,B] is set

{B,B} is non empty finite set

{B} is non empty trivial finite 1 -element set

{{B,B},{B}} is non empty finite V57() set

the multF of G . [B,B] is set

B " is Element of the carrier of G

B " is Element of the carrier of G

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

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

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

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

{(B ")} is non empty trivial finite 1 -element set

{{(B "),(B ")},{(B ")}} is non empty finite V57() set

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

y is set

y is Element of the carrier of G

B is Element of the carrier of G

y * 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 having_a_unity 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 cup-closed diff-closed preBoolean set

the multF of G . (y,B) is Element of the carrier of G

[y,B] is set

{y,B} is non empty finite set

{y} is non empty trivial finite 1 -element set

{{y,B},{y}} is non empty finite V57() set

the multF of G . [y,B] is set

B is Element of the carrier of G

B " is Element of the carrier of G

a is Element of the carrier of G

a " is Element of the carrier of G

a * B is Element of the carrier of G

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 trivial finite 1 -element set

{{a,B},{a}} is non empty finite V57() set

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

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

G is non empty multMagma

the carrier of G is non empty set

bool the carrier of G is non empty cup-closed diff-closed preBoolean set

H is Element of the carrier of G

{H} is non empty trivial finite 1 -element Element of bool the carrier of G

x is Element of bool the carrier of G

(G,{H},x) is Element of bool the carrier of G

{ (b

(G,x,{H}) is Element of bool the carrier of G

{ (b