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
{ (b1 ") where b1 is Element of the carrier of G : b1 in H } is set
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
{ (b1 ") where b1 is Element of the carrier of G : b1 in y } is set
{ (b1 ") where b1 is Element of the carrier of G : b1 in x } is set
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
{ (b1 ") where b1 is Element of the carrier of H : b1 in x } is set
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
{ (b1 ") where b1 is Element of the carrier of y : b1 in B } 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 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
{ (b1 ") where b1 is Element of the carrier of G : b1 in {H} } is 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 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
{ (b1 ") where b1 is Element of the carrier of G : b1 in {H,x} } is set
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
{ (b1 ") where b1 is Element of the carrier of G : b1 in {} the carrier of G } is set
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
{ (b1 ") where b1 is Element of the carrier of G : b1 in [#] the carrier of G } is set
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
{ (b1 ") where b1 is Element of the carrier of G : b1 in H } is set
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
{ (b1 ") where b1 is Element of the carrier of G : b1 in H } 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 non empty Element of bool the carrier of G
(G,H) is Element of bool the carrier of G
{ (b1 ") where b1 is Element of the carrier of G : b1 in 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
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in H & b2 in x ) } 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
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
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in y & b2 in y ) } is set
(G,y,y) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in y & b2 in y ) } 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
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
{ (b1 * b2) where b1, b2 is Element of the carrier of H : ( b1 in x & b2 in y ) } is set
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
{ (b1 * b2) where b1, b2 is Element of the carrier of B : ( b1 in B & b2 in a ) } 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
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in H & b2 in x ) } is set
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
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in H & b2 in x ) } is set
y is Element of bool the carrier of G
(G,(G,H,x),y) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in (G,H,x) & b2 in y ) } is set
(G,x,y) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in x & b2 in y ) } is set
(G,H,(G,x,y)) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in H & b2 in (G,x,y) ) } 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
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
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in H & b2 in x ) } is set
(G,(G,H,x)) is Element of bool the carrier of G
{ (b1 ") where b1 is Element of the carrier of G : b1 in (G,H,x) } is set
(G,x) is Element of bool the carrier of G
{ (b1 ") where b1 is Element of the carrier of G : b1 in x } is set
(G,H) is Element of bool the carrier of G
{ (b1 ") where b1 is Element of the carrier of G : b1 in H } is set
(G,(G,x),(G,H)) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in (G,x) & b2 in (G,H) ) } 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
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
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in H & b2 in x ) } is set
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
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in H & b2 in x \/ y ) } is set
(G,H,y) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in H & b2 in y ) } is set
(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
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in H \/ x & b2 in y ) } is set
(G,H,y) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in H & b2 in y ) } is set
(G,x,y) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in x & b2 in y ) } is set
(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
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in H & b2 in x ) } is set
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
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in H & b2 in x /\ y ) } is set
(G,H,y) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in H & b2 in y ) } is set
(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
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in H /\ x & b2 in y ) } is set
(G,H,y) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in H & b2 in y ) } is set
(G,x,y) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in x & b2 in y ) } is set
(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
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {} the carrier of G & b2 in H ) } is set
(G,H,({} the carrier of G)) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in H & b2 in {} the carrier of G ) } is set
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
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in [#] the carrier of G & b2 in H ) } is set
(G,H,([#] the carrier of G)) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in H & b2 in [#] the carrier of G ) } is set
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
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {H} & b2 in {x} ) } is set
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
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {H} & b2 in {x,y} ) } is set
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
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {H,x} & b2 in {y} ) } is set
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
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {H,x} & b2 in {y,y} ) } is set
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
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in H & b2 in H ) } 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
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
{ (b1 ") where b1 is Element of the carrier of G : b1 in H } is set
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
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in H & b2 in x ) } is set
(G,x,H) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in x & b2 in H ) } 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
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
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in H & b2 in x ) } is set
(G,x,H) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in x & b2 in H ) } 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
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
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in H & b2 in x ) } is set
(G,(G,H,x)) is Element of bool the carrier of G
{ (b1 ") where b1 is Element of the carrier of G : b1 in (G,H,x) } is set
(G,H) is Element of bool the carrier of G
{ (b1 ") where b1 is Element of the carrier of G : b1 in H } is set
(G,x) is Element of bool the carrier of G
{ (b1 ") where b1 is Element of the carrier of G : b1 in x } is set
(G,(G,H),(G,x)) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in (G,H) & b2 in (G,x) ) } 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
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
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in {H} & b2 in x ) } is set
(G,x,{H}) is Element of bool the carrier of G
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1