:: AUTGROUP semantic presentation

K126() is Element of bool K122()
K122() is set
bool K122() is set
K121() is set
bool K121() is set
bool K126() is set
{} is Function-like functional empty set
1 is non empty set
G is non empty strict unital Group-like associative multMagma
the carrier of G is non empty set
f is non empty unital Group-like associative Subgroup of G
the carrier of f is non empty set
f1 is Element of the carrier of G
f * f1 is Element of bool the carrier of G
bool the carrier of G is set
carr f is Element of bool the carrier of G
(carr f) * f1 is Element of bool the carrier of G
K102( the carrier of G,f1) is non empty Element of bool the carrier of G
(carr f) * K102( the carrier of G,f1) is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr f & b₂ in K102( the carrier of G,f1) ) } is set
f1 * f is Element of bool the carrier of G
f1 * (carr f) is Element of bool the carrier of G
K102( the carrier of G,f1) * (carr f) is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K102( the carrier of G,f1) & b₂ in carr f ) } is set
x is set
y1 is Element of the carrier of G
y1 * f1 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 V14([: the carrier of G, the carrier of G:]) quasi_total associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (y1,f1) is Element of the carrier of G
[y1,f1] is set
{y1,f1} is non empty set
{y1} is non empty set
{{y1,f1},{y1}} is non empty set
the multF of G . [y1,f1] is set
y1 |^ f1 is Element of the carrier of G
f1 " is Element of the carrier of G
(f1 ") * y1 is Element of the carrier of G
the multF of G . ((f1 "),y1) is Element of the carrier of G
[(f1 "),y1] is set
{(f1 "),y1} is non empty set
{(f1 ")} is non empty set
{{(f1 "),y1},{(f1 ")}} is non empty set
the multF of G . [(f1 "),y1] is set
((f1 ") * y1) * f1 is Element of the carrier of G
the multF of G . (((f1 ") * y1),f1) is Element of the carrier of G
[((f1 ") * y1),f1] is set
{((f1 ") * y1),f1} is non empty set
{((f1 ") * y1)} is non empty set
{{((f1 ") * y1),f1},{((f1 ") * y1)}} is non empty set
the multF of G . [((f1 ") * y1),f1] is set
f1 * (((f1 ") * y1) * f1) is Element of the carrier of G
the multF of G . (f1,(((f1 ") * y1) * f1)) is Element of the carrier of G
[f1,(((f1 ") * y1) * f1)] is set
{f1,(((f1 ") * y1) * f1)} is non empty set
{f1} is non empty set
{{f1,(((f1 ") * y1) * f1)},{f1}} is non empty set
the multF of G . [f1,(((f1 ") * y1) * f1)] is set
(f1 ") * (y1 * f1) is Element of the carrier of G
the multF of G . ((f1 "),(y1 * f1)) is Element of the carrier of G
[(f1 "),(y1 * f1)] is set
{(f1 "),(y1 * f1)} is non empty set
{{(f1 "),(y1 * f1)},{(f1 ")}} is non empty set
the multF of G . [(f1 "),(y1 * f1)] is set
f1 * ((f1 ") * (y1 * f1)) is Element of the carrier of G
the multF of G . (f1,((f1 ") * (y1 * f1))) is Element of the carrier of G
[f1,((f1 ") * (y1 * f1))] is set
{f1,((f1 ") * (y1 * f1))} is non empty set
{{f1,((f1 ") * (y1 * f1))},{f1}} is non empty set
the multF of G . [f1,((f1 ") * (y1 * f1))] is set
f1 * (f1 ") is Element of the carrier of G
the multF of G . (f1,(f1 ")) is Element of the carrier of G
[f1,(f1 ")] is set
{f1,(f1 ")} is non empty set
{{f1,(f1 ")},{f1}} is non empty set
the multF of G . [f1,(f1 ")] is set
(f1 * (f1 ")) * (y1 * f1) is Element of the carrier of G
the multF of G . ((f1 * (f1 ")),(y1 * f1)) is Element of the carrier of G
[(f1 * (f1 ")),(y1 * f1)] is set
{(f1 * (f1 ")),(y1 * f1)} is non empty set
{(f1 * (f1 "))} is non empty set
{{(f1 * (f1 ")),(y1 * f1)},{(f1 * (f1 "))}} is non empty set
the multF of G . [(f1 * (f1 ")),(y1 * f1)] is set
(f1 * (f1 ")) * y1 is Element of the carrier of G
the multF of G . ((f1 * (f1 ")),y1) is Element of the carrier of G
[(f1 * (f1 ")),y1] is set
{(f1 * (f1 ")),y1} is non empty set
{{(f1 * (f1 ")),y1},{(f1 * (f1 "))}} is non empty set
the multF of G . [(f1 * (f1 ")),y1] is set
((f1 * (f1 ")) * y1) * f1 is Element of the carrier of G
the multF of G . (((f1 * (f1 ")) * y1),f1) is Element of the carrier of G
[((f1 * (f1 ")) * y1),f1] is set
{((f1 * (f1 ")) * y1),f1} is non empty set
{((f1 * (f1 ")) * y1)} is non empty set
{{((f1 * (f1 ")) * y1),f1},{((f1 * (f1 ")) * y1)}} is non empty set
the multF of G . [((f1 * (f1 ")) * y1),f1] is set
1_ G is non being_of_order_0 Element of the carrier of G
(1_ G) * y1 is Element of the carrier of G
the multF of G . ((1_ G),y1) is Element of the carrier of G
[(1_ G),y1] is set
{(1_ G),y1} is non empty set
{(1_ G)} is non empty set
{{(1_ G),y1},{(1_ G)}} is non empty set
the multF of G . [(1_ G),y1] is set
((1_ G) * y1) * f1 is Element of the carrier of G
the multF of G . (((1_ G) * y1),f1) is Element of the carrier of G
[((1_ G) * y1),f1] is set
{((1_ G) * y1),f1} is non empty set
{((1_ G) * y1)} is non empty set
{{((1_ G) * y1),f1},{((1_ G) * y1)}} is non empty set
the multF of G . [((1_ G) * y1),f1] is set
G is non empty strict unital Group-like associative multMagma
the carrier of G is non empty set
f is non empty unital Group-like associative Subgroup of G
the carrier of f is non empty set
carr f is Element of bool the carrier of G
bool the carrier of G is set
a is Element of the carrier of G
x is Element of the carrier of G
x |^ a is Element of the carrier of G
a " is Element of the carrier of G
(a ") * 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 V14([: the carrier of G, the carrier of G:]) quasi_total associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . ((a "),x) is Element of the carrier of G
[(a "),x] is set
{(a "),x} is non empty set
{(a ")} is non empty set
{{(a "),x},{(a ")}} is non empty set
the multF of G . [(a "),x] is set
((a ") * x) * a is Element of the carrier of G
the multF of G . (((a ") * x),a) is Element of the carrier of G
[((a ") * x),a] is set
{((a ") * x),a} is non empty set
{((a ") * x)} is non empty set
{{((a ") * x),a},{((a ") * x)}} is non empty set
the multF of G . [((a ") * x),a] is set
f * a is Element of bool the carrier of G
(carr f) * a is Element of bool the carrier of G
K102( the carrier of G,a) is non empty Element of bool the carrier of G
(carr f) * K102( the carrier of G,a) is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr f & b₂ in K102( the carrier of G,a) ) } is set
a * f is Element of bool the carrier of G
a * (carr f) is Element of bool the carrier of G
K102( the carrier of G,a) * (carr f) is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K102( the carrier of G,a) & b₂ in carr f ) } is set
(a ") * f is Element of bool the carrier of G
(a ") * (carr f) is Element of bool the carrier of G
K102( the carrier of G,(a ")) is non empty Element of bool the carrier of G
K102( the carrier of G,(a ")) * (carr f) is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K102( the carrier of G,(a ")) & b₂ in carr f ) } is set
((a ") * f) * a is Element of bool the carrier of G
((a ") * f) * K102( the carrier of G,a) is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in (a ") * f & b₂ in K102( the carrier of G,a) ) } is set
(a ") * (a * f) is Element of bool the carrier of G
K102( the carrier of G,(a ")) * (a * f) is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K102( the carrier of G,(a ")) & b₂ in a * f ) } is set
(a ") * a is Element of the carrier of G
the multF of G . ((a "),a) is Element of the carrier of G
[(a "),a] is set
{(a "),a} is non empty set
{{(a "),a},{(a ")}} is non empty set
the multF of G . [(a "),a] is set
((a ") * a) * f is Element of bool the carrier of G
((a ") * a) * (carr f) is Element of bool the carrier of G
K102( the carrier of G,((a ") * a)) is non empty Element of bool the carrier of G
K102( the carrier of G,((a ") * a)) * (carr f) is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K102( the carrier of G,((a ") * a)) & b₂ in carr f ) } is set
1_ G is non being_of_order_0 Element of the carrier of G
(1_ G) * f is Element of bool the carrier of G
(1_ G) * (carr f) is Element of bool the carrier of G
K102( the carrier of G,(1_ G)) is non empty Element of bool the carrier of G
K102( the carrier of G,(1_ G)) * (carr f) is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in K102( the carrier of G,(1_ G)) & b₂ in carr f ) } is set
f |^ a is non empty strict unital Group-like associative Subgroup of G
the carrier of (f |^ a) is non empty set
(carr f) |^ a is Element of bool the carrier of G
(carr f) |^ K102( the carrier of G,a) is Element of bool the carrier of G
{ (b₁ |^ b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in carr f & b₂ in K102( the carrier of G,a) ) } is set
((a ") * (carr f)) * a is Element of bool the carrier of G
((a ") * (carr f)) * K102( the carrier of G,a) is Element of bool the carrier of G
{ (b₁ * b₂) where b₁, b₂ is Element of the carrier of G : ( b₁ in (a ") * (carr f) & b₂ in K102( the carrier of G,a) ) } is set
G is non empty strict unital Group-like associative multMagma
f1 is non empty strict unital Group-like associative multMagma
the carrier of f1 is non empty set
the carrier of G is non empty set
f is non empty unital Group-like associative Subgroup of G
the carrier of f is non empty set
a is non empty unital Group-like associative Subgroup of f1
y1 is Element of the carrier of f1
the carrier of a is non empty set
x is Element of the carrier of f1
y1 |^ x is Element of the carrier of f1
x " is Element of the carrier of f1
(x ") * y1 is Element of the carrier of f1
the multF of f1 is Relation-like [: the carrier of f1, the carrier of f1:] -defined the carrier of f1 -valued Function-like V14([: the carrier of f1, the carrier of f1:]) quasi_total associative Element of bool [:[: the carrier of f1, the carrier of f1:], the carrier of f1:]
[: the carrier of f1, the carrier of f1:] is set
[:[: the carrier of f1, the carrier of f1:], the carrier of f1:] is set
bool [:[: the carrier of f1, the carrier of f1:], the carrier of f1:] is set
the multF of f1 . ((x "),y1) is Element of the carrier of f1
[(x "),y1] is set
{(x "),y1} is non empty set
{(x ")} is non empty set
{{(x "),y1},{(x ")}} is non empty set
the multF of f1 . [(x "),y1] is set
((x ") * y1) * x is Element of the carrier of f1
the multF of f1 . (((x ") * y1),x) is Element of the carrier of f1
[((x ") * y1),x] is set
{((x ") * y1),x} is non empty set
{((x ") * y1)} is non empty set
{{((x ") * y1),x},{((x ") * y1)}} is non empty set
the multF of f1 . [((x ") * y1),x] is set
G is non empty strict unital Group-like associative multMagma
the carrier of G is non empty set
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is set
Funcs ( the carrier of G, the carrier of G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
{ b₁ where b₁ is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of Funcs ( the carrier of G, the carrier of G) : ex b₂ being Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total unity-preserving V102(G,G) Element of bool [: the carrier of G, the carrier of G:] st
( b₁ = b₂ & b₂ is one-to-one & b₂ is onto ) } is set
id the carrier of G is Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
a is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total unity-preserving V102(G,G) Element of bool [: the carrier of G, the carrier of G:]
rng a is Element of bool the carrier of G
bool the carrier of G is set
f1 is set
a is set
x is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of Funcs ( the carrier of G, the carrier of G)
y1 is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total unity-preserving V102(G,G) Element of bool [: the carrier of G, the carrier of G:]
a is functional non empty set
x is Relation-like Function-like Element of a
y1 is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of Funcs ( the carrier of G, the carrier of G)
b is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total unity-preserving V102(G,G) Element of bool [: the carrier of G, the carrier of G:]
x is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
y1 is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of x
b is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of Funcs ( the carrier of G, the carrier of G)
q1 is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total unity-preserving V102(G,G) Element of bool [: the carrier of G, the carrier of G:]
y1 is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total unity-preserving V102(G,G) Element of bool [: the carrier of G, the carrier of G:]
b is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of Funcs ( the carrier of G, the carrier of G)
q1 is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total unity-preserving V102(G,G) Element of bool [: the carrier of G, the carrier of G:]
f is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
f1 is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
a is set
x is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total unity-preserving V102(G,G) Element of bool [: the carrier of G, the carrier of G:]
a is set
x is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total unity-preserving V102(G,G) Element of bool [: the carrier of G, the carrier of G:]
G is non empty strict unital Group-like associative multMagma
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
the carrier of G is non empty set
Funcs ( the carrier of G, the carrier of G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
f is set
f1 is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
G is non empty strict unital Group-like associative multMagma
the carrier of G is non empty set
id the carrier of G is Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is set
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
f is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total unity-preserving V102(G,G) Element of bool [: the carrier of G, the carrier of G:]
rng f is Element of bool the carrier of G
bool the carrier of G is set
G is non empty strict unital Group-like associative multMagma
the carrier of G is non empty set
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is set
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
f is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total unity-preserving V102(G,G) Element of bool [: the carrier of G, the carrier of G:]
G is non empty strict unital Group-like associative multMagma
the carrier of G is non empty set
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
f is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
dom f is Element of bool the carrier of G
bool the carrier of G is set
rng f is Element of bool the carrier of G
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is set
f1 is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total unity-preserving V102(G,G) Element of bool [: the carrier of G, the carrier of G:]
dom f1 is Element of bool the carrier of G
G is non empty strict unital Group-like associative multMagma
the carrier of G is non empty set
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is set
f is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
f " is Relation-like Function-like set
f1 is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total unity-preserving V102(G,G) Element of bool [: the carrier of G, the carrier of G:]
G is non empty strict unital Group-like associative multMagma
the carrier of G is non empty set
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
f is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
f " is Relation-like Function-like set
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is set
f1 is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total unity-preserving V102(G,G) Element of bool [: the carrier of G, the carrier of G:]
f1 " is Relation-like Function-like set
a is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total unity-preserving V102(G,G) Element of bool [: the carrier of G, the carrier of G:]
G is non empty strict unital Group-like associative multMagma
the carrier of G is non empty set
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
f1 is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
f is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
f * f1 is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is set
a is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total unity-preserving V102(G,G) Element of bool [: the carrier of G, the carrier of G:]
x is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total unity-preserving V102(G,G) Element of bool [: the carrier of G, the carrier of G:]
a * x is Relation-like the carrier of G -defined the carrier of G -defined the carrier of G -valued the carrier of G -valued Function-like non empty V14( the carrier of G) V14( the carrier of G) quasi_total quasi_total unity-preserving V102(G,G) Element of bool [: the carrier of G, the carrier of G:]
G is non empty strict unital Group-like associative multMagma
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
the carrier of G is non empty set
[:(G),(G):] is set
[:[:(G),(G):],(G):] is set
bool [:[:(G),(G):],(G):] is set
f is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
f1 is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
f * f1 is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is set
x is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total unity-preserving V102(G,G) Element of bool [: the carrier of G, the carrier of G:]
a is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total unity-preserving V102(G,G) Element of bool [: the carrier of G, the carrier of G:]
a * x is Relation-like the carrier of G -defined the carrier of G -defined the carrier of G -valued the carrier of G -valued Function-like non empty V14( the carrier of G) V14( the carrier of G) quasi_total quasi_total unity-preserving V102(G,G) Element of bool [: the carrier of G, the carrier of G:]
y1 is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
f is Relation-like [:(G),(G):] -defined (G) -valued Function-like V14([:(G),(G):]) quasi_total Element of bool [:[:(G),(G):],(G):]
f1 is Relation-like [:(G),(G):] -defined (G) -valued Function-like V14([:(G),(G):]) quasi_total Element of bool [:[:(G),(G):],(G):]
a is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
x is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
f . (a,x) is Relation-like Function-like Element of (G)
[a,x] is set
{a,x} is functional non empty set
{a} is functional non empty set
{{a,x},{a}} is non empty set
f . [a,x] is Relation-like Function-like set
f1 . (a,x) is Relation-like Function-like Element of (G)
f1 . [a,x] is Relation-like Function-like set
a * x is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is set
G is non empty strict unital Group-like associative multMagma
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
the carrier of G is non empty set
(G) is Relation-like [:(G),(G):] -defined (G) -valued Function-like V14([:(G),(G):]) quasi_total Element of bool [:[:(G),(G):],(G):]
[:(G),(G):] is set
[:[:(G),(G):],(G):] is set
bool [:[:(G),(G):],(G):] is set
multMagma(# (G),(G) #) is strict multMagma
the carrier of multMagma(# (G),(G) #) is set
id the carrier of G is Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is set
f1 is Element of the carrier of multMagma(# (G),(G) #)
a is Element of the carrier of multMagma(# (G),(G) #)
a * f1 is Element of the carrier of multMagma(# (G),(G) #)
the multF of multMagma(# (G),(G) #) is Relation-like [: the carrier of multMagma(# (G),(G) #), the carrier of multMagma(# (G),(G) #):] -defined the carrier of multMagma(# (G),(G) #) -valued Function-like quasi_total Element of bool [:[: the carrier of multMagma(# (G),(G) #), the carrier of multMagma(# (G),(G) #):], the carrier of multMagma(# (G),(G) #):]
[: the carrier of multMagma(# (G),(G) #), the carrier of multMagma(# (G),(G) #):] is set
[:[: the carrier of multMagma(# (G),(G) #), the carrier of multMagma(# (G),(G) #):], the carrier of multMagma(# (G),(G) #):] is set
bool [:[: the carrier of multMagma(# (G),(G) #), the carrier of multMagma(# (G),(G) #):], the carrier of multMagma(# (G),(G) #):] is set
the multF of multMagma(# (G),(G) #) . (a,f1) is Element of the carrier of multMagma(# (G),(G) #)
[a,f1] is set
{a,f1} is non empty set
{a} is non empty set
{{a,f1},{a}} is non empty set
the multF of multMagma(# (G),(G) #) . [a,f1] is set
f1 * a is Element of the carrier of multMagma(# (G),(G) #)
the multF of multMagma(# (G),(G) #) . (f1,a) is Element of the carrier of multMagma(# (G),(G) #)
[f1,a] is set
{f1,a} is non empty set
{f1} is non empty set
{{f1,a},{f1}} is non empty set
the multF of multMagma(# (G),(G) #) . [f1,a] is set
x is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
x * (id the carrier of G) is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
(id the carrier of G) * x is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
x " is Relation-like Function-like set
y1 is Element of the carrier of multMagma(# (G),(G) #)
a * y1 is Element of the carrier of multMagma(# (G),(G) #)
the multF of multMagma(# (G),(G) #) . (a,y1) is Element of the carrier of multMagma(# (G),(G) #)
[a,y1] is set
{a,y1} is non empty set
{{a,y1},{a}} is non empty set
the multF of multMagma(# (G),(G) #) . [a,y1] is set
y1 * a is Element of the carrier of multMagma(# (G),(G) #)
the multF of multMagma(# (G),(G) #) . (y1,a) is Element of the carrier of multMagma(# (G),(G) #)
[y1,a] is set
{y1,a} is non empty set
{y1} is non empty set
{{y1,a},{y1}} is non empty set
the multF of multMagma(# (G),(G) #) . [y1,a] is set
b is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total unity-preserving V102(G,G) Element of bool [: the carrier of G, the carrier of G:]
rng b is Element of bool the carrier of G
bool the carrier of G is set
b " is Relation-like Function-like set
(b ") * b is Relation-like Function-like set
b * (b ") is Relation-like Function-like set
f1 is Element of the carrier of multMagma(# (G),(G) #)
a is Element of the carrier of multMagma(# (G),(G) #)
f1 * a is Element of the carrier of multMagma(# (G),(G) #)
the multF of multMagma(# (G),(G) #) is Relation-like [: the carrier of multMagma(# (G),(G) #), the carrier of multMagma(# (G),(G) #):] -defined the carrier of multMagma(# (G),(G) #) -valued Function-like quasi_total Element of bool [:[: the carrier of multMagma(# (G),(G) #), the carrier of multMagma(# (G),(G) #):], the carrier of multMagma(# (G),(G) #):]
[: the carrier of multMagma(# (G),(G) #), the carrier of multMagma(# (G),(G) #):] is set
[:[: the carrier of multMagma(# (G),(G) #), the carrier of multMagma(# (G),(G) #):], the carrier of multMagma(# (G),(G) #):] is set
bool [:[: the carrier of multMagma(# (G),(G) #), the carrier of multMagma(# (G),(G) #):], the carrier of multMagma(# (G),(G) #):] is set
the multF of multMagma(# (G),(G) #) . (f1,a) is Element of the carrier of multMagma(# (G),(G) #)
[f1,a] is set
{f1,a} is non empty set
{f1} is non empty set
{{f1,a},{f1}} is non empty set
the multF of multMagma(# (G),(G) #) . [f1,a] is set
x is Element of the carrier of multMagma(# (G),(G) #)
(f1 * a) * x is Element of the carrier of multMagma(# (G),(G) #)
the multF of multMagma(# (G),(G) #) . ((f1 * a),x) is Element of the carrier of multMagma(# (G),(G) #)
[(f1 * a),x] is set
{(f1 * a),x} is non empty set
{(f1 * a)} is non empty set
{{(f1 * a),x},{(f1 * a)}} is non empty set
the multF of multMagma(# (G),(G) #) . [(f1 * a),x] is set
a * x is Element of the carrier of multMagma(# (G),(G) #)
the multF of multMagma(# (G),(G) #) . (a,x) is Element of the carrier of multMagma(# (G),(G) #)
[a,x] is set
{a,x} is non empty set
{a} is non empty set
{{a,x},{a}} is non empty set
the multF of multMagma(# (G),(G) #) . [a,x] is set
f1 * (a * x) is Element of the carrier of multMagma(# (G),(G) #)
the multF of multMagma(# (G),(G) #) . (f1,(a * x)) is Element of the carrier of multMagma(# (G),(G) #)
[f1,(a * x)] is set
{f1,(a * x)} is non empty set
{{f1,(a * x)},{f1}} is non empty set
the multF of multMagma(# (G),(G) #) . [f1,(a * x)] is set
q1 is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
b is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
b * q1 is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is set
y1 is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
y1 * b is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
(y1 * b) * q1 is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
y1 * (b * q1) is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
f1 is Element of the carrier of multMagma(# (G),(G) #)
G is non empty strict unital Group-like associative multMagma
(G) is non empty strict unital Group-like associative multMagma
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
the carrier of G is non empty set
(G) is Relation-like [:(G),(G):] -defined (G) -valued Function-like V14([:(G),(G):]) quasi_total Element of bool [:[:(G),(G):],(G):]
[:(G),(G):] is set
[:[:(G),(G):],(G):] is set
bool [:[:(G),(G):],(G):] is set
multMagma(# (G),(G) #) is strict multMagma
the carrier of (G) is non empty set
f is Element of the carrier of (G)
a is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
f1 is Element of the carrier of (G)
x is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
f * f1 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 V14([: the carrier of (G), the carrier of (G):]) quasi_total associative Element of bool [:[: the carrier of (G), the carrier of (G):], the carrier of (G):]
[: the carrier of (G), the carrier of (G):] is set
[:[: the carrier of (G), the carrier of (G):], the carrier of (G):] is set
bool [:[: the carrier of (G), the carrier of (G):], the carrier of (G):] is set
the multF of (G) . (f,f1) is Element of the carrier of (G)
[f,f1] is set
{f,f1} is non empty set
{f} is non empty set
{{f,f1},{f}} is non empty set
the multF of (G) . [f,f1] is set
a * x is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is set
G is non empty strict unital Group-like associative multMagma
the carrier of G is non empty set
id the carrier of G is Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is set
(G) is non empty strict unital Group-like associative multMagma
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
(G) is Relation-like [:(G),(G):] -defined (G) -valued Function-like V14([:(G),(G):]) quasi_total Element of bool [:[:(G),(G):],(G):]
[:(G),(G):] is set
[:[:(G),(G):],(G):] is set
bool [:[:(G),(G):],(G):] is set
multMagma(# (G),(G) #) is strict multMagma
1_ (G) is non being_of_order_0 Element of the carrier of (G)
the carrier of (G) is non empty set
the Element of the carrier of (G) is Element of the carrier of (G)
f1 is Element of the carrier of (G)
a is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
x is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
x * a is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
the Element of the carrier of (G) * f1 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 V14([: the carrier of (G), the carrier of (G):]) quasi_total associative Element of bool [:[: the carrier of (G), the carrier of (G):], the carrier of (G):]
[: the carrier of (G), the carrier of (G):] is set
[:[: the carrier of (G), the carrier of (G):], the carrier of (G):] is set
bool [:[: the carrier of (G), the carrier of (G):], the carrier of (G):] is set
the multF of (G) . ( the Element of the carrier of (G),f1) is Element of the carrier of (G)
[ the Element of the carrier of (G),f1] is set
{ the Element of the carrier of (G),f1} is non empty set
{ the Element of the carrier of (G)} is non empty set
{{ the Element of the carrier of (G),f1},{ the Element of the carrier of (G)}} is non empty set
the multF of (G) . [ the Element of the carrier of (G),f1] is set
G is non empty strict unital Group-like associative multMagma
the carrier of G is non empty set
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
(G) is non empty strict unital Group-like associative multMagma
(G) is Relation-like [:(G),(G):] -defined (G) -valued Function-like V14([:(G),(G):]) quasi_total Element of bool [:[:(G),(G):],(G):]
[:(G),(G):] is set
[:[:(G),(G):],(G):] is set
bool [:[:(G),(G):],(G):] is set
multMagma(# (G),(G) #) is strict multMagma
the carrier of (G) is non empty set
f is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
f " is Relation-like Function-like set
f1 is Element of the carrier of (G)
f1 " is Element of the carrier of (G)
a is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
a * f is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is set
(f1 ") * f1 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 V14([: the carrier of (G), the carrier of (G):]) quasi_total associative Element of bool [:[: the carrier of (G), the carrier of (G):], the carrier of (G):]
[: the carrier of (G), the carrier of (G):] is set
[:[: the carrier of (G), the carrier of (G):], the carrier of (G):] is set
bool [:[: the carrier of (G), the carrier of (G):], the carrier of (G):] is set
the multF of (G) . ((f1 "),f1) is Element of the carrier of (G)
[(f1 "),f1] is set
{(f1 "),f1} is non empty set
{(f1 ")} is non empty set
{{(f1 "),f1},{(f1 ")}} is non empty set
the multF of (G) . [(f1 "),f1] is set
1_ (G) is non being_of_order_0 Element of the carrier of (G)
id the carrier of G is Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
rng f is Element of bool the carrier of G
bool the carrier of G is set
dom f is Element of bool the carrier of G
G is non empty strict unital Group-like associative multMagma
the carrier of G is non empty set
Funcs ( the carrier of G, the carrier of G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
id the carrier of G is Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is set
{ b₁ where b₁ is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of Funcs ( the carrier of G, the carrier of G) : ex b₂ being Element of the carrier of G st
for b₃ being Element of the carrier of G holds b₁ . b₃ = b₃ |^ b₂ } is set
1_ G is non being_of_order_0 Element of the carrier of G
a is non being_of_order_0 Element of the carrier of G
x is Element of the carrier of G
(id the carrier of G) . x is Element of the carrier of G
x |^ a is Element of the carrier of G
a " is Element of the carrier of G
(a ") * 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 V14([: the carrier of G, the carrier of G:]) quasi_total associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . ((a "),x) is Element of the carrier of G
[(a "),x] is set
{(a "),x} is non empty set
{(a ")} is non empty set
{{(a "),x},{(a ")}} is non empty set
the multF of G . [(a "),x] is set
((a ") * x) * a is Element of the carrier of G
the multF of G . (((a ") * x),a) is Element of the carrier of G
[((a ") * x),a] is set
{((a ") * x),a} is non empty set
{((a ") * x)} is non empty set
{{((a ") * x),a},{((a ") * x)}} is non empty set
the multF of G . [((a ") * x),a] is set
x * a is Element of the carrier of G
the multF of G . (x,a) is Element of the carrier of G
[x,a] is set
{x,a} is non empty set
{x} is non empty set
{{x,a},{x}} is non empty set
the multF of G . [x,a] is set
a is Element of the carrier of G
a is set
x is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of Funcs ( the carrier of G, the carrier of G)
y1 is Element of the carrier of G
a is functional non empty set
x is Relation-like Function-like Element of a
y1 is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of Funcs ( the carrier of G, the carrier of G)
b is Element of the carrier of G
x is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
y1 is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of Funcs ( the carrier of G, the carrier of G)
b is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of Funcs ( the carrier of G, the carrier of G)
q1 is Element of the carrier of G
b is Element of the carrier of G
f is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
f1 is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
a is set
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is set
x is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of Funcs ( the carrier of G, the carrier of G)
y1 is Element of the carrier of G
a is set
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is set
x is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of Funcs ( the carrier of G, the carrier of G)
y1 is Element of the carrier of G
G is non empty strict unital Group-like associative multMagma
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
the carrier of G is non empty set
Funcs ( the carrier of G, the carrier of G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
f is set
f1 is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
G is non empty strict unital Group-like associative multMagma
the carrier of G is non empty set
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
f is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
Funcs ( the carrier of G, the carrier of G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
x is Element of the carrier of G
f1 is Element of the carrier of G
a is Element of the carrier of G
f1 * 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 V14([: the carrier of G, the carrier of G:]) quasi_total associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (f1,a) is Element of the carrier of G
[f1,a] is set
{f1,a} is non empty set
{f1} is non empty set
{{f1,a},{f1}} is non empty set
the multF of G . [f1,a] is set
f . (f1 * a) is Element of the carrier of G
(f1 * a) |^ x is Element of the carrier of G
x " is Element of the carrier of G
(x ") * (f1 * a) is Element of the carrier of G
the multF of G . ((x "),(f1 * a)) is Element of the carrier of G
[(x "),(f1 * a)] is set
{(x "),(f1 * a)} is non empty set
{(x ")} is non empty set
{{(x "),(f1 * a)},{(x ")}} is non empty set
the multF of G . [(x "),(f1 * a)] is set
((x ") * (f1 * a)) * x is Element of the carrier of G
the multF of G . (((x ") * (f1 * a)),x) is Element of the carrier of G
[((x ") * (f1 * a)),x] is set
{((x ") * (f1 * a)),x} is non empty set
{((x ") * (f1 * a))} is non empty set
{{((x ") * (f1 * a)),x},{((x ") * (f1 * a))}} is non empty set
the multF of G . [((x ") * (f1 * a)),x] is set
(x ") * f1 is Element of the carrier of G
the multF of G . ((x "),f1) is Element of the carrier of G
[(x "),f1] is set
{(x "),f1} is non empty set
{{(x "),f1},{(x ")}} is non empty set
the multF of G . [(x "),f1] is set
((x ") * f1) * a is Element of the carrier of G
the multF of G . (((x ") * f1),a) is Element of the carrier of G
[((x ") * f1),a] is set
{((x ") * f1),a} is non empty set
{((x ") * f1)} is non empty set
{{((x ") * f1),a},{((x ") * f1)}} is non empty set
the multF of G . [((x ") * f1),a] is set
(((x ") * f1) * a) * x is Element of the carrier of G
the multF of G . ((((x ") * f1) * a),x) is Element of the carrier of G
[(((x ") * f1) * a),x] is set
{(((x ") * f1) * a),x} is non empty set
{(((x ") * f1) * a)} is non empty set
{{(((x ") * f1) * a),x},{(((x ") * f1) * a)}} is non empty set
the multF of G . [(((x ") * f1) * a),x] is set
a * x is Element of the carrier of G
the multF of G . (a,x) is Element of the carrier of G
[a,x] is set
{a,x} is non empty set
{a} is non empty set
{{a,x},{a}} is non empty set
the multF of G . [a,x] is set
((x ") * f1) * (a * x) is Element of the carrier of G
the multF of G . (((x ") * f1),(a * x)) is Element of the carrier of G
[((x ") * f1),(a * x)] is set
{((x ") * f1),(a * x)} is non empty set
{{((x ") * f1),(a * x)},{((x ") * f1)}} is non empty set
the multF of G . [((x ") * f1),(a * x)] is set
1_ G is non being_of_order_0 Element of the carrier of G
((x ") * f1) * (1_ G) is Element of the carrier of G
the multF of G . (((x ") * f1),(1_ G)) is Element of the carrier of G
[((x ") * f1),(1_ G)] is set
{((x ") * f1),(1_ G)} is non empty set
{{((x ") * f1),(1_ G)},{((x ") * f1)}} is non empty set
the multF of G . [((x ") * f1),(1_ G)] is set
(((x ") * f1) * (1_ G)) * (a * x) is Element of the carrier of G
the multF of G . ((((x ") * f1) * (1_ G)),(a * x)) is Element of the carrier of G
[(((x ") * f1) * (1_ G)),(a * x)] is set
{(((x ") * f1) * (1_ G)),(a * x)} is non empty set
{(((x ") * f1) * (1_ G))} is non empty set
{{(((x ") * f1) * (1_ G)),(a * x)},{(((x ") * f1) * (1_ G))}} is non empty set
the multF of G . [(((x ") * f1) * (1_ G)),(a * x)] is set
x * (x ") is Element of the carrier of G
the multF of G . (x,(x ")) is Element of the carrier of G
[x,(x ")] is set
{x,(x ")} is non empty set
{x} is non empty set
{{x,(x ")},{x}} is non empty set
the multF of G . [x,(x ")] is set
((x ") * f1) * (x * (x ")) is Element of the carrier of G
the multF of G . (((x ") * f1),(x * (x "))) is Element of the carrier of G
[((x ") * f1),(x * (x "))] is set
{((x ") * f1),(x * (x "))} is non empty set
{{((x ") * f1),(x * (x "))},{((x ") * f1)}} is non empty set
the multF of G . [((x ") * f1),(x * (x "))] is set
(((x ") * f1) * (x * (x "))) * (a * x) is Element of the carrier of G
the multF of G . ((((x ") * f1) * (x * (x "))),(a * x)) is Element of the carrier of G
[(((x ") * f1) * (x * (x "))),(a * x)] is set
{(((x ") * f1) * (x * (x "))),(a * x)} is non empty set
{(((x ") * f1) * (x * (x ")))} is non empty set
{{(((x ") * f1) * (x * (x "))),(a * x)},{(((x ") * f1) * (x * (x ")))}} is non empty set
the multF of G . [(((x ") * f1) * (x * (x "))),(a * x)] is set
((x ") * f1) * x is Element of the carrier of G
the multF of G . (((x ") * f1),x) is Element of the carrier of G
[((x ") * f1),x] is set
{((x ") * f1),x} is non empty set
{{((x ") * f1),x},{((x ") * f1)}} is non empty set
the multF of G . [((x ") * f1),x] is set
(((x ") * f1) * x) * (x ") is Element of the carrier of G
the multF of G . ((((x ") * f1) * x),(x ")) is Element of the carrier of G
[(((x ") * f1) * x),(x ")] is set
{(((x ") * f1) * x),(x ")} is non empty set
{(((x ") * f1) * x)} is non empty set
{{(((x ") * f1) * x),(x ")},{(((x ") * f1) * x)}} is non empty set
the multF of G . [(((x ") * f1) * x),(x ")] is set
((((x ") * f1) * x) * (x ")) * (a * x) is Element of the carrier of G
the multF of G . (((((x ") * f1) * x) * (x ")),(a * x)) is Element of the carrier of G
[((((x ") * f1) * x) * (x ")),(a * x)] is set
{((((x ") * f1) * x) * (x ")),(a * x)} is non empty set
{((((x ") * f1) * x) * (x "))} is non empty set
{{((((x ") * f1) * x) * (x ")),(a * x)},{((((x ") * f1) * x) * (x "))}} is non empty set
the multF of G . [((((x ") * f1) * x) * (x ")),(a * x)] is set
((((x ") * f1) * x) * (x ")) * a is Element of the carrier of G
the multF of G . (((((x ") * f1) * x) * (x ")),a) is Element of the carrier of G
[((((x ") * f1) * x) * (x ")),a] is set
{((((x ") * f1) * x) * (x ")),a} is non empty set
{{((((x ") * f1) * x) * (x ")),a},{((((x ") * f1) * x) * (x "))}} is non empty set
the multF of G . [((((x ") * f1) * x) * (x ")),a] is set
(((((x ") * f1) * x) * (x ")) * a) * x is Element of the carrier of G
the multF of G . ((((((x ") * f1) * x) * (x ")) * a),x) is Element of the carrier of G
[(((((x ") * f1) * x) * (x ")) * a),x] is set
{(((((x ") * f1) * x) * (x ")) * a),x} is non empty set
{(((((x ") * f1) * x) * (x ")) * a)} is non empty set
{{(((((x ") * f1) * x) * (x ")) * a),x},{(((((x ") * f1) * x) * (x ")) * a)}} is non empty set
the multF of G . [(((((x ") * f1) * x) * (x ")) * a),x] is set
(x ") * a is Element of the carrier of G
the multF of G . ((x "),a) is Element of the carrier of G
[(x "),a] is set
{(x "),a} is non empty set
{{(x "),a},{(x ")}} is non empty set
the multF of G . [(x "),a] is set
(((x ") * f1) * x) * ((x ") * a) is Element of the carrier of G
the multF of G . ((((x ") * f1) * x),((x ") * a)) is Element of the carrier of G
[(((x ") * f1) * x),((x ") * a)] is set
{(((x ") * f1) * x),((x ") * a)} is non empty set
{{(((x ") * f1) * x),((x ") * a)},{(((x ") * f1) * x)}} is non empty set
the multF of G . [(((x ") * f1) * x),((x ") * a)] is set
((((x ") * f1) * x) * ((x ") * a)) * x is Element of the carrier of G
the multF of G . (((((x ") * f1) * x) * ((x ") * a)),x) is Element of the carrier of G
[((((x ") * f1) * x) * ((x ") * a)),x] is set
{((((x ") * f1) * x) * ((x ") * a)),x} is non empty set
{((((x ") * f1) * x) * ((x ") * a))} is non empty set
{{((((x ") * f1) * x) * ((x ") * a)),x},{((((x ") * f1) * x) * ((x ") * a))}} is non empty set
the multF of G . [((((x ") * f1) * x) * ((x ") * a)),x] is set
f1 |^ x is Element of the carrier of G
a |^ x is Element of the carrier of G
((x ") * a) * x is Element of the carrier of G
the multF of G . (((x ") * a),x) is Element of the carrier of G
[((x ") * a),x] is set
{((x ") * a),x} is non empty set
{((x ") * a)} is non empty set
{{((x ") * a),x},{((x ") * a)}} is non empty set
the multF of G . [((x ") * a),x] is set
(f1 |^ x) * (a |^ x) is Element of the carrier of G
the multF of G . ((f1 |^ x),(a |^ x)) is Element of the carrier of G
[(f1 |^ x),(a |^ x)] is set
{(f1 |^ x),(a |^ x)} is non empty set
{(f1 |^ x)} is non empty set
{{(f1 |^ x),(a |^ x)},{(f1 |^ x)}} is non empty set
the multF of G . [(f1 |^ x),(a |^ x)] is set
f . f1 is Element of the carrier of G
(f . f1) * (a |^ x) is Element of the carrier of G
the multF of G . ((f . f1),(a |^ x)) is Element of the carrier of G
[(f . f1),(a |^ x)] is set
{(f . f1),(a |^ x)} is non empty set
{(f . f1)} is non empty set
{{(f . f1),(a |^ x)},{(f . f1)}} is non empty set
the multF of G . [(f . f1),(a |^ x)] is set
f . a is Element of the carrier of G
(f . f1) * (f . a) is Element of the carrier of G
the multF of G . ((f . f1),(f . a)) is Element of the carrier of G
[(f . f1),(f . a)] is set
{(f . f1),(f . a)} is non empty set
{{(f . f1),(f . a)},{(f . f1)}} is non empty set
the multF of G . [(f . f1),(f . a)] is set
bool [: the carrier of G, the carrier of G:] is set
f1 is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total unity-preserving V102(G,G) Element of bool [: the carrier of G, the carrier of G:]
a is set
dom f1 is set
f1 . a is set
x is set
f1 . x is set
dom f1 is Element of bool the carrier of G
bool the carrier of G is set
y1 is Element of the carrier of G
b is Element of the carrier of G
q1 is Element of the carrier of G
f1 . y1 is Element of the carrier of G
b |^ q1 is Element of the carrier of G
q1 " is Element of the carrier of G
(q1 ") * b is Element of the carrier of G
the multF of G . ((q1 "),b) is Element of the carrier of G
[(q1 "),b] is set
{(q1 "),b} is non empty set
{(q1 ")} is non empty set
{{(q1 "),b},{(q1 ")}} is non empty set
the multF of G . [(q1 "),b] is set
((q1 ") * b) * q1 is Element of the carrier of G
the multF of G . (((q1 ") * b),q1) is Element of the carrier of G
[((q1 ") * b),q1] is set
{((q1 ") * b),q1} is non empty set
{((q1 ") * b)} is non empty set
{{((q1 ") * b),q1},{((q1 ") * b)}} is non empty set
the multF of G . [((q1 ") * b),q1] is set
y1 |^ q1 is Element of the carrier of G
(q1 ") * y1 is Element of the carrier of G
the multF of G . ((q1 "),y1) is Element of the carrier of G
[(q1 "),y1] is set
{(q1 "),y1} is non empty set
{{(q1 "),y1},{(q1 ")}} is non empty set
the multF of G . [(q1 "),y1] is set
((q1 ") * y1) * q1 is Element of the carrier of G
the multF of G . (((q1 ") * y1),q1) is Element of the carrier of G
[((q1 ") * y1),q1] is set
{((q1 ") * y1),q1} is non empty set
{((q1 ") * y1)} is non empty set
{{((q1 ") * y1),q1},{((q1 ") * y1)}} is non empty set
the multF of G . [((q1 ") * y1),q1] is set
y1 * q1 is Element of the carrier of G
the multF of G . (y1,q1) is Element of the carrier of G
[y1,q1] is set
{y1,q1} is non empty set
{y1} is non empty set
{{y1,q1},{y1}} is non empty set
the multF of G . [y1,q1] is set
(q1 ") * (y1 * q1) is Element of the carrier of G
the multF of G . ((q1 "),(y1 * q1)) is Element of the carrier of G
[(q1 "),(y1 * q1)] is set
{(q1 "),(y1 * q1)} is non empty set
{{(q1 "),(y1 * q1)},{(q1 ")}} is non empty set
the multF of G . [(q1 "),(y1 * q1)] is set
q1 * ((q1 ") * (y1 * q1)) is Element of the carrier of G
the multF of G . (q1,((q1 ") * (y1 * q1))) is Element of the carrier of G
[q1,((q1 ") * (y1 * q1))] is set
{q1,((q1 ") * (y1 * q1))} is non empty set
{q1} is non empty set
{{q1,((q1 ") * (y1 * q1))},{q1}} is non empty set
the multF of G . [q1,((q1 ") * (y1 * q1))] is set
q1 * (((q1 ") * b) * q1) is Element of the carrier of G
the multF of G . (q1,(((q1 ") * b) * q1)) is Element of the carrier of G
[q1,(((q1 ") * b) * q1)] is set
{q1,(((q1 ") * b) * q1)} is non empty set
{{q1,(((q1 ") * b) * q1)},{q1}} is non empty set
the multF of G . [q1,(((q1 ") * b) * q1)] is set
q1 * (q1 ") is Element of the carrier of G
the multF of G . (q1,(q1 ")) is Element of the carrier of G
[q1,(q1 ")] is set
{q1,(q1 ")} is non empty set
{{q1,(q1 ")},{q1}} is non empty set
the multF of G . [q1,(q1 ")] is set
(q1 * (q1 ")) * (y1 * q1) is Element of the carrier of G
the multF of G . ((q1 * (q1 ")),(y1 * q1)) is Element of the carrier of G
[(q1 * (q1 ")),(y1 * q1)] is set
{(q1 * (q1 ")),(y1 * q1)} is non empty set
{(q1 * (q1 "))} is non empty set
{{(q1 * (q1 ")),(y1 * q1)},{(q1 * (q1 "))}} is non empty set
the multF of G . [(q1 * (q1 ")),(y1 * q1)] is set
b * q1 is Element of the carrier of G
the multF of G . (b,q1) is Element of the carrier of G
[b,q1] is set
{b,q1} is non empty set
{b} is non empty set
{{b,q1},{b}} is non empty set
the multF of G . [b,q1] is set
(q1 ") * (b * q1) is Element of the carrier of G
the multF of G . ((q1 "),(b * q1)) is Element of the carrier of G
[(q1 "),(b * q1)] is set
{(q1 "),(b * q1)} is non empty set
{{(q1 "),(b * q1)},{(q1 ")}} is non empty set
the multF of G . [(q1 "),(b * q1)] is set
q1 * ((q1 ") * (b * q1)) is Element of the carrier of G
the multF of G . (q1,((q1 ") * (b * q1))) is Element of the carrier of G
[q1,((q1 ") * (b * q1))] is set
{q1,((q1 ") * (b * q1))} is non empty set
{{q1,((q1 ") * (b * q1))},{q1}} is non empty set
the multF of G . [q1,((q1 ") * (b * q1))] is set
(q1 * (q1 ")) * (b * q1) is Element of the carrier of G
the multF of G . ((q1 * (q1 ")),(b * q1)) is Element of the carrier of G
[(q1 * (q1 ")),(b * q1)] is set
{(q1 * (q1 ")),(b * q1)} is non empty set
{{(q1 * (q1 ")),(b * q1)},{(q1 * (q1 "))}} is non empty set
the multF of G . [(q1 * (q1 ")),(b * q1)] is set
(1_ G) * (y1 * q1) is Element of the carrier of G
the multF of G . ((1_ G),(y1 * q1)) is Element of the carrier of G
[(1_ G),(y1 * q1)] is set
{(1_ G),(y1 * q1)} is non empty set
{(1_ G)} is non empty set
{{(1_ G),(y1 * q1)},{(1_ G)}} is non empty set
the multF of G . [(1_ G),(y1 * q1)] is set
(1_ G) * (b * q1) is Element of the carrier of G
the multF of G . ((1_ G),(b * q1)) is Element of the carrier of G
[(1_ G),(b * q1)] is set
{(1_ G),(b * q1)} is non empty set
{{(1_ G),(b * q1)},{(1_ G)}} is non empty set
the multF of G . [(1_ G),(b * q1)] is set
(y1 * q1) * (q1 ") is Element of the carrier of G
the multF of G . ((y1 * q1),(q1 ")) is Element of the carrier of G
[(y1 * q1),(q1 ")] is set
{(y1 * q1),(q1 ")} is non empty set
{(y1 * q1)} is non empty set
{{(y1 * q1),(q1 ")},{(y1 * q1)}} is non empty set
the multF of G . [(y1 * q1),(q1 ")] is set
(b * q1) * (q1 ") is Element of the carrier of G
the multF of G . ((b * q1),(q1 ")) is Element of the carrier of G
[(b * q1),(q1 ")] is set
{(b * q1),(q1 ")} is non empty set
{(b * q1)} is non empty set
{{(b * q1),(q1 ")},{(b * q1)}} is non empty set
the multF of G . [(b * q1),(q1 ")] is set
y1 * (q1 * (q1 ")) is Element of the carrier of G
the multF of G . (y1,(q1 * (q1 "))) is Element of the carrier of G
[y1,(q1 * (q1 "))] is set
{y1,(q1 * (q1 "))} is non empty set
{{y1,(q1 * (q1 "))},{y1}} is non empty set
the multF of G . [y1,(q1 * (q1 "))] is set
b * (q1 * (q1 ")) is Element of the carrier of G
the multF of G . (b,(q1 * (q1 "))) is Element of the carrier of G
[b,(q1 * (q1 "))] is set
{b,(q1 * (q1 "))} is non empty set
{{b,(q1 * (q1 "))},{b}} is non empty set
the multF of G . [b,(q1 * (q1 "))] is set
y1 * (1_ G) is Element of the carrier of G
the multF of G . (y1,(1_ G)) is Element of the carrier of G
[y1,(1_ G)] is set
{y1,(1_ G)} is non empty set
{{y1,(1_ G)},{y1}} is non empty set
the multF of G . [y1,(1_ G)] is set
b * (1_ G) is Element of the carrier of G
the multF of G . (b,(1_ G)) is Element of the carrier of G
[b,(1_ G)] is set
{b,(1_ G)} is non empty set
{{b,(1_ G)},{b}} is non empty set
the multF of G . [b,(1_ G)] is set
dom f1 is Element of bool the carrier of G
bool the carrier of G is set
a is set
x is Element of the carrier of G
y1 is Element of the carrier of G
y1 * x is Element of the carrier of G
the multF of G . (y1,x) is Element of the carrier of G
[y1,x] is set
{y1,x} is non empty set
{y1} is non empty set
{{y1,x},{y1}} is non empty set
the multF of G . [y1,x] is set
y1 " is Element of the carrier of G
(y1 * x) * (y1 ") is Element of the carrier of G
the multF of G . ((y1 * x),(y1 ")) is Element of the carrier of G
[(y1 * x),(y1 ")] is set
{(y1 * x),(y1 ")} is non empty set
{(y1 * x)} is non empty set
{{(y1 * x),(y1 ")},{(y1 * x)}} is non empty set
the multF of G . [(y1 * x),(y1 ")] is set
b is Element of the carrier of G
f1 . b is set
q1 is Relation-like Function-like set
dom q1 is set
rng q1 is set
(1_ G) * x is Element of the carrier of G
the multF of G . ((1_ G),x) is Element of the carrier of G
[(1_ G),x] is set
{(1_ G),x} is non empty set
{(1_ G)} is non empty set
{{(1_ G),x},{(1_ G)}} is non empty set
the multF of G . [(1_ G),x] is set
((1_ G) * x) * (1_ G) is Element of the carrier of G
the multF of G . (((1_ G) * x),(1_ G)) is Element of the carrier of G
[((1_ G) * x),(1_ G)] is set
{((1_ G) * x),(1_ G)} is non empty set
{((1_ G) * x)} is non empty set
{{((1_ G) * x),(1_ G)},{((1_ G) * x)}} is non empty set
the multF of G . [((1_ G) * x),(1_ G)] is set
(y1 ") * y1 is Element of the carrier of G
the multF of G . ((y1 "),y1) is Element of the carrier of G
[(y1 "),y1] is set
{(y1 "),y1} is non empty set
{(y1 ")} is non empty set
{{(y1 "),y1},{(y1 ")}} is non empty set
the multF of G . [(y1 "),y1] is set
((y1 ") * y1) * x is Element of the carrier of G
the multF of G . (((y1 ") * y1),x) is Element of the carrier of G
[((y1 ") * y1),x] is set
{((y1 ") * y1),x} is non empty set
{((y1 ") * y1)} is non empty set
{{((y1 ") * y1),x},{((y1 ") * y1)}} is non empty set
the multF of G . [((y1 ") * y1),x] is set
(((y1 ") * y1) * x) * (1_ G) is Element of the carrier of G
the multF of G . ((((y1 ") * y1) * x),(1_ G)) is Element of the carrier of G
[(((y1 ") * y1) * x),(1_ G)] is set
{(((y1 ") * y1) * x),(1_ G)} is non empty set
{(((y1 ") * y1) * x)} is non empty set
{{(((y1 ") * y1) * x),(1_ G)},{(((y1 ") * y1) * x)}} is non empty set
the multF of G . [(((y1 ") * y1) * x),(1_ G)] is set
(((y1 ") * y1) * x) * ((y1 ") * y1) is Element of the carrier of G
the multF of G . ((((y1 ") * y1) * x),((y1 ") * y1)) is Element of the carrier of G
[(((y1 ") * y1) * x),((y1 ") * y1)] is set
{(((y1 ") * y1) * x),((y1 ") * y1)} is non empty set
{{(((y1 ") * y1) * x),((y1 ") * y1)},{(((y1 ") * y1) * x)}} is non empty set
the multF of G . [(((y1 ") * y1) * x),((y1 ") * y1)] is set
(((y1 ") * y1) * x) * (y1 ") is Element of the carrier of G
the multF of G . ((((y1 ") * y1) * x),(y1 ")) is Element of the carrier of G
[(((y1 ") * y1) * x),(y1 ")] is set
{(((y1 ") * y1) * x),(y1 ")} is non empty set
{{(((y1 ") * y1) * x),(y1 ")},{(((y1 ") * y1) * x)}} is non empty set
the multF of G . [(((y1 ") * y1) * x),(y1 ")] is set
((((y1 ") * y1) * x) * (y1 ")) * y1 is Element of the carrier of G
the multF of G . (((((y1 ") * y1) * x) * (y1 ")),y1) is Element of the carrier of G
[((((y1 ") * y1) * x) * (y1 ")),y1] is set
{((((y1 ") * y1) * x) * (y1 ")),y1} is non empty set
{((((y1 ") * y1) * x) * (y1 "))} is non empty set
{{((((y1 ") * y1) * x) * (y1 ")),y1},{((((y1 ") * y1) * x) * (y1 "))}} is non empty set
the multF of G . [((((y1 ") * y1) * x) * (y1 ")),y1] is set
x * (y1 ") is Element of the carrier of G
the multF of G . (x,(y1 ")) is Element of the carrier of G
[x,(y1 ")] is set
{x,(y1 ")} is non empty set
{x} is non empty set
{{x,(y1 ")},{x}} is non empty set
the multF of G . [x,(y1 ")] is set
((y1 ") * y1) * (x * (y1 ")) is Element of the carrier of G
the multF of G . (((y1 ") * y1),(x * (y1 "))) is Element of the carrier of G
[((y1 ") * y1),(x * (y1 "))] is set
{((y1 ") * y1),(x * (y1 "))} is non empty set
{{((y1 ") * y1),(x * (y1 "))},{((y1 ") * y1)}} is non empty set
the multF of G . [((y1 ") * y1),(x * (y1 "))] is set
(((y1 ") * y1) * (x * (y1 "))) * y1 is Element of the carrier of G
the multF of G . ((((y1 ") * y1) * (x * (y1 "))),y1) is Element of the carrier of G
[(((y1 ") * y1) * (x * (y1 "))),y1] is set
{(((y1 ") * y1) * (x * (y1 "))),y1} is non empty set
{(((y1 ") * y1) * (x * (y1 ")))} is non empty set
{{(((y1 ") * y1) * (x * (y1 "))),y1},{(((y1 ") * y1) * (x * (y1 ")))}} is non empty set
the multF of G . [(((y1 ") * y1) * (x * (y1 "))),y1] is set
y1 * (x * (y1 ")) is Element of the carrier of G
the multF of G . (y1,(x * (y1 "))) is Element of the carrier of G
[y1,(x * (y1 "))] is set
{y1,(x * (y1 "))} is non empty set
{{y1,(x * (y1 "))},{y1}} is non empty set
the multF of G . [y1,(x * (y1 "))] is set
(y1 ") * (y1 * (x * (y1 "))) is Element of the carrier of G
the multF of G . ((y1 "),(y1 * (x * (y1 ")))) is Element of the carrier of G
[(y1 "),(y1 * (x * (y1 ")))] is set
{(y1 "),(y1 * (x * (y1 ")))} is non empty set
{{(y1 "),(y1 * (x * (y1 ")))},{(y1 ")}} is non empty set
the multF of G . [(y1 "),(y1 * (x * (y1 ")))] is set
((y1 ") * (y1 * (x * (y1 ")))) * y1 is Element of the carrier of G
the multF of G . (((y1 ") * (y1 * (x * (y1 ")))),y1) is Element of the carrier of G
[((y1 ") * (y1 * (x * (y1 ")))),y1] is set
{((y1 ") * (y1 * (x * (y1 ")))),y1} is non empty set
{((y1 ") * (y1 * (x * (y1 "))))} is non empty set
{{((y1 ") * (y1 * (x * (y1 ")))),y1},{((y1 ") * (y1 * (x * (y1 "))))}} is non empty set
the multF of G . [((y1 ") * (y1 * (x * (y1 ")))),y1] is set
b |^ y1 is Element of the carrier of G
(y1 ") * b is Element of the carrier of G
the multF of G . ((y1 "),b) is Element of the carrier of G
[(y1 "),b] is set
{(y1 "),b} is non empty set
{{(y1 "),b},{(y1 ")}} is non empty set
the multF of G . [(y1 "),b] is set
((y1 ") * b) * y1 is Element of the carrier of G
the multF of G . (((y1 ") * b),y1) is Element of the carrier of G
[((y1 ") * b),y1] is set
{((y1 ") * b),y1} is non empty set
{((y1 ") * b)} is non empty set
{{((y1 ") * b),y1},{((y1 ") * b)}} is non empty set
the multF of G . [((y1 ") * b),y1] is set
f1 . b is Element of the carrier of G
rng f1 is Element of bool the carrier of G
G is non empty strict unital Group-like associative multMagma
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
the carrier of G is non empty set
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
f is set
f1 is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
G is non empty strict unital Group-like associative multMagma
the carrier of G is non empty set
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
(G) is Relation-like [:(G),(G):] -defined (G) -valued Function-like V14([:(G),(G):]) quasi_total Element of bool [:[:(G),(G):],(G):]
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
[:(G),(G):] is set
[:[:(G),(G):],(G):] is set
bool [:[:(G),(G):],(G):] is set
f is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
f1 is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
(G) . (f,f1) is set
[f,f1] is set
{f,f1} is functional non empty set
{f} is functional non empty set
{{f,f1},{f}} is non empty set
(G) . [f,f1] is Relation-like Function-like set
f * f1 is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is set
G is non empty strict unital Group-like associative multMagma
the carrier of G is non empty set
id the carrier of G is Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is set
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
1_ G is non being_of_order_0 Element of the carrier of G
f1 is non being_of_order_0 Element of the carrier of G
a is Element of the carrier of G
(id the carrier of G) . a is Element of the carrier of G
a |^ f1 is Element of the carrier of G
f1 " is Element of the carrier of G
(f1 ") * 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 V14([: the carrier of G, the carrier of G:]) quasi_total associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . ((f1 "),a) is Element of the carrier of G
[(f1 "),a] is set
{(f1 "),a} is non empty set
{(f1 ")} is non empty set
{{(f1 "),a},{(f1 ")}} is non empty set
the multF of G . [(f1 "),a] is set
((f1 ") * a) * f1 is Element of the carrier of G
the multF of G . (((f1 ") * a),f1) is Element of the carrier of G
[((f1 ") * a),f1] is set
{((f1 ") * a),f1} is non empty set
{((f1 ") * a)} is non empty set
{{((f1 ") * a),f1},{((f1 ") * a)}} is non empty set
the multF of G . [((f1 ") * a),f1] is set
a * f1 is Element of the carrier of G
the multF of G . (a,f1) is Element of the carrier of G
[a,f1] is set
{a,f1} is non empty set
{a} is non empty set
{{a,f1},{a}} is non empty set
the multF of G . [a,f1] is set
Funcs ( the carrier of G, the carrier of G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
f1 is Element of the carrier of G
G is non empty strict unital Group-like associative multMagma
the carrier of G is non empty set
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
f is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
f " is Relation-like Function-like set
Funcs ( the carrier of G, the carrier of G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
f1 is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of Funcs ( the carrier of G, the carrier of G)
a is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of Funcs ( the carrier of G, the carrier of G)
x is Element of the carrier of G
x " is Element of the carrier of G
y1 is Element of the carrier of G
b is Element of the carrier of G
(f ") . b is set
b |^ y1 is Element of the carrier of G
y1 " is Element of the carrier of G
(y1 ") * 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 V14([: the carrier of G, the carrier of G:]) quasi_total associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . ((y1 "),b) is Element of the carrier of G
[(y1 "),b] is set
{(y1 "),b} is non empty set
{(y1 ")} is non empty set
{{(y1 "),b},{(y1 ")}} is non empty set
the multF of G . [(y1 "),b] is set
((y1 ") * b) * y1 is Element of the carrier of G
the multF of G . (((y1 ") * b),y1) is Element of the carrier of G
[((y1 ") * b),y1] is set
{((y1 ") * b),y1} is non empty set
{((y1 ") * b)} is non empty set
{{((y1 ") * b),y1},{((y1 ") * b)}} is non empty set
the multF of G . [((y1 ") * b),y1] is set
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
bool [: the carrier of G, the carrier of G:] is set
q1 is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total unity-preserving V102(G,G) Element of bool [: the carrier of G, the carrier of G:]
g is Element of the carrier of G
q1 . g is Element of the carrier of G
q1 " is Relation-like Function-like set
(q1 ") . b is set
1_ G is non being_of_order_0 Element of the carrier of G
(1_ G) * g is Element of the carrier of G
the multF of G . ((1_ G),g) is Element of the carrier of G
[(1_ G),g] is set
{(1_ G),g} is non empty set
{(1_ G)} is non empty set
{{(1_ G),g},{(1_ G)}} is non empty set
the multF of G . [(1_ G),g] is set
((1_ G) * g) * (1_ G) is Element of the carrier of G
the multF of G . (((1_ G) * g),(1_ G)) is Element of the carrier of G
[((1_ G) * g),(1_ G)] is set
{((1_ G) * g),(1_ G)} is non empty set
{((1_ G) * g)} is non empty set
{{((1_ G) * g),(1_ G)},{((1_ G) * g)}} is non empty set
the multF of G . [((1_ G) * g),(1_ G)] is set
x * (x ") is Element of the carrier of G
the multF of G . (x,(x ")) is Element of the carrier of G
[x,(x ")] is set
{x,(x ")} is non empty set
{x} is non empty set
{{x,(x ")},{x}} is non empty set
the multF of G . [x,(x ")] is set
(x * (x ")) * g is Element of the carrier of G
the multF of G . ((x * (x ")),g) is Element of the carrier of G
[(x * (x ")),g] is set
{(x * (x ")),g} is non empty set
{(x * (x "))} is non empty set
{{(x * (x ")),g},{(x * (x "))}} is non empty set
the multF of G . [(x * (x ")),g] is set
((x * (x ")) * g) * (1_ G) is Element of the carrier of G
the multF of G . (((x * (x ")) * g),(1_ G)) is Element of the carrier of G
[((x * (x ")) * g),(1_ G)] is set
{((x * (x ")) * g),(1_ G)} is non empty set
{((x * (x ")) * g)} is non empty set
{{((x * (x ")) * g),(1_ G)},{((x * (x ")) * g)}} is non empty set
the multF of G . [((x * (x ")) * g),(1_ G)] is set
((x * (x ")) * g) * (x * (x ")) is Element of the carrier of G
the multF of G . (((x * (x ")) * g),(x * (x "))) is Element of the carrier of G
[((x * (x ")) * g),(x * (x "))] is set
{((x * (x ")) * g),(x * (x "))} is non empty set
{{((x * (x ")) * g),(x * (x "))},{((x * (x ")) * g)}} is non empty set
the multF of G . [((x * (x ")) * g),(x * (x "))] is set
((x * (x ")) * g) * x is Element of the carrier of G
the multF of G . (((x * (x ")) * g),x) is Element of the carrier of G
[((x * (x ")) * g),x] is set
{((x * (x ")) * g),x} is non empty set
{{((x * (x ")) * g),x},{((x * (x ")) * g)}} is non empty set
the multF of G . [((x * (x ")) * g),x] is set
(((x * (x ")) * g) * x) * (x ") is Element of the carrier of G
the multF of G . ((((x * (x ")) * g) * x),(x ")) is Element of the carrier of G
[(((x * (x ")) * g) * x),(x ")] is set
{(((x * (x ")) * g) * x),(x ")} is non empty set
{(((x * (x ")) * g) * x)} is non empty set
{{(((x * (x ")) * g) * x),(x ")},{(((x * (x ")) * g) * x)}} is non empty set
the multF of G . [(((x * (x ")) * g) * x),(x ")] is set
g * x is Element of the carrier of G
the multF of G . (g,x) is Element of the carrier of G
[g,x] is set
{g,x} is non empty set
{g} is non empty set
{{g,x},{g}} is non empty set
the multF of G . [g,x] is set
(x * (x ")) * (g * x) is Element of the carrier of G
the multF of G . ((x * (x ")),(g * x)) is Element of the carrier of G
[(x * (x ")),(g * x)] is set
{(x * (x ")),(g * x)} is non empty set
{{(x * (x ")),(g * x)},{(x * (x "))}} is non empty set
the multF of G . [(x * (x ")),(g * x)] is set
((x * (x ")) * (g * x)) * (x ") is Element of the carrier of G
the multF of G . (((x * (x ")) * (g * x)),(x ")) is Element of the carrier of G
[((x * (x ")) * (g * x)),(x ")] is set
{((x * (x ")) * (g * x)),(x ")} is non empty set
{((x * (x ")) * (g * x))} is non empty set
{{((x * (x ")) * (g * x)),(x ")},{((x * (x ")) * (g * x))}} is non empty set
the multF of G . [((x * (x ")) * (g * x)),(x ")] is set
(x ") * (g * x) is Element of the carrier of G
the multF of G . ((x "),(g * x)) is Element of the carrier of G
[(x "),(g * x)] is set
{(x "),(g * x)} is non empty set
{(x ")} is non empty set
{{(x "),(g * x)},{(x ")}} is non empty set
the multF of G . [(x "),(g * x)] is set
x * ((x ") * (g * x)) is Element of the carrier of G
the multF of G . (x,((x ") * (g * x))) is Element of the carrier of G
[x,((x ") * (g * x))] is set
{x,((x ") * (g * x))} is non empty set
{{x,((x ") * (g * x))},{x}} is non empty set
the multF of G . [x,((x ") * (g * x))] is set
(x * ((x ") * (g * x))) * (x ") is Element of the carrier of G
the multF of G . ((x * ((x ") * (g * x))),(x ")) is Element of the carrier of G
[(x * ((x ") * (g * x))),(x ")] is set
{(x * ((x ") * (g * x))),(x ")} is non empty set
{(x * ((x ") * (g * x)))} is non empty set
{{(x * ((x ") * (g * x))),(x ")},{(x * ((x ") * (g * x)))}} is non empty set
the multF of G . [(x * ((x ") * (g * x))),(x ")] is set
g |^ x is Element of the carrier of G
(x ") * g is Element of the carrier of G
the multF of G . ((x "),g) is Element of the carrier of G
[(x "),g] is set
{(x "),g} is non empty set
{{(x "),g},{(x ")}} is non empty set
the multF of G . [(x "),g] is set
((x ") * g) * x is Element of the carrier of G
the multF of G . (((x ") * g),x) is Element of the carrier of G
[((x ") * g),x] is set
{((x ") * g),x} is non empty set
{((x ") * g)} is non empty set
{{((x ") * g),x},{((x ") * g)}} is non empty set
the multF of G . [((x ") * g),x] is set
x * (g |^ x) is Element of the carrier of G
the multF of G . (x,(g |^ x)) is Element of the carrier of G
[x,(g |^ x)] is set
{x,(g |^ x)} is non empty set
{{x,(g |^ x)},{x}} is non empty set
the multF of G . [x,(g |^ x)] is set
(x * (g |^ x)) * (x ") is Element of the carrier of G
the multF of G . ((x * (g |^ x)),(x ")) is Element of the carrier of G
[(x * (g |^ x)),(x ")] is set
{(x * (g |^ x)),(x ")} is non empty set
{(x * (g |^ x))} is non empty set
{{(x * (g |^ x)),(x ")},{(x * (g |^ x))}} is non empty set
the multF of G . [(x * (g |^ x)),(x ")] is set
x * b is Element of the carrier of G
the multF of G . (x,b) is Element of the carrier of G
[x,b] is set
{x,b} is non empty set
{{x,b},{x}} is non empty set
the multF of G . [x,b] is set
(x * b) * (x ") is Element of the carrier of G
the multF of G . ((x * b),(x ")) is Element of the carrier of G
[(x * b),(x ")] is set
{(x * b),(x ")} is non empty set
{(x * b)} is non empty set
{{(x * b),(x ")},{(x * b)}} is non empty set
the multF of G . [(x * b),(x ")] is set
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is set
x is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total unity-preserving V102(G,G) Element of bool [: the carrier of G, the carrier of G:]
y1 is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total unity-preserving V102(G,G) Element of bool [: the carrier of G, the carrier of G:]
rng y1 is Element of bool the carrier of G
bool the carrier of G is set
b is Element of the carrier of G
G is non empty strict unital Group-like associative multMagma
the carrier of G is non empty set
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
f1 is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
f is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
f * f1 is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is set
Funcs ( the carrier of G, the carrier of G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
a is Element of the carrier of G
x is Element of the carrier of G
a * 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 V14([: the carrier of G, the carrier of G:]) quasi_total associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (a,x) is Element of the carrier of G
[a,x] is set
{a,x} is non empty set
{a} is non empty set
{{a,x},{a}} is non empty set
the multF of G . [a,x] is set
y1 is Element of the carrier of G
b is Element of the carrier of G
(f * f1) . b is Element of the carrier of G
b |^ y1 is Element of the carrier of G
y1 " is Element of the carrier of G
(y1 ") * b is Element of the carrier of G
the multF of G . ((y1 "),b) is Element of the carrier of G
[(y1 "),b] is set
{(y1 "),b} is non empty set
{(y1 ")} is non empty set
{{(y1 "),b},{(y1 ")}} is non empty set
the multF of G . [(y1 "),b] is set
((y1 ") * b) * y1 is Element of the carrier of G
the multF of G . (((y1 ") * b),y1) is Element of the carrier of G
[((y1 ") * b),y1] is set
{((y1 ") * b),y1} is non empty set
{((y1 ") * b)} is non empty set
{{((y1 ") * b),y1},{((y1 ") * b)}} is non empty set
the multF of G . [((y1 ") * b),y1] is set
f1 . b is Element of the carrier of G
f . (f1 . b) is Element of the carrier of G
b |^ 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 set
{(a ")} is non empty set
{{(a "),b},{(a ")}} is non empty set
the multF of G . [(a "),b] is set
((a ") * b) * a is Element of the carrier of G
the multF of G . (((a ") * b),a) is Element of the carrier of G
[((a ") * b),a] is set
{((a ") * b),a} is non empty set
{((a ") * b)} is non empty set
{{((a ") * b),a},{((a ") * b)}} is non empty set
the multF of G . [((a ") * b),a] is set
f . (b |^ a) is Element of the carrier of G
(((a ") * b) * a) |^ x is Element of the carrier of G
x " is Element of the carrier of G
(x ") * (((a ") * b) * a) is Element of the carrier of G
the multF of G . ((x "),(((a ") * b) * a)) is Element of the carrier of G
[(x "),(((a ") * b) * a)] is set
{(x "),(((a ") * b) * a)} is non empty set
{(x ")} is non empty set
{{(x "),(((a ") * b) * a)},{(x ")}} is non empty set
the multF of G . [(x "),(((a ") * b) * a)] is set
((x ") * (((a ") * b) * a)) * x is Element of the carrier of G
the multF of G . (((x ") * (((a ") * b) * a)),x) is Element of the carrier of G
[((x ") * (((a ") * b) * a)),x] is set
{((x ") * (((a ") * b) * a)),x} is non empty set
{((x ") * (((a ") * b) * a))} is non empty set
{{((x ") * (((a ") * b) * a)),x},{((x ") * (((a ") * b) * a))}} is non empty set
the multF of G . [((x ") * (((a ") * b) * a)),x] is set
(((a ") * b) * a) * x is Element of the carrier of G
the multF of G . ((((a ") * b) * a),x) is Element of the carrier of G
[(((a ") * b) * a),x] is set
{(((a ") * b) * a),x} is non empty set
{(((a ") * b) * a)} is non empty set
{{(((a ") * b) * a),x},{(((a ") * b) * a)}} is non empty set
the multF of G . [(((a ") * b) * a),x] is set
(x ") * ((((a ") * b) * a) * x) is Element of the carrier of G
the multF of G . ((x "),((((a ") * b) * a) * x)) is Element of the carrier of G
[(x "),((((a ") * b) * a) * x)] is set
{(x "),((((a ") * b) * a) * x)} is non empty set
{{(x "),((((a ") * b) * a) * x)},{(x ")}} is non empty set
the multF of G . [(x "),((((a ") * b) * a) * x)] 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 set
{b} is non empty set
{{b,a},{b}} is non empty set
the multF of G . [b,a] is set
(a ") * (b * a) is Element of the carrier of G
the multF of G . ((a "),(b * a)) is Element of the carrier of G
[(a "),(b * a)] is set
{(a "),(b * a)} is non empty set
{{(a "),(b * a)},{(a ")}} is non empty set
the multF of G . [(a "),(b * a)] is set
((a ") * (b * a)) * x is Element of the carrier of G
the multF of G . (((a ") * (b * a)),x) is Element of the carrier of G
[((a ") * (b * a)),x] is set
{((a ") * (b * a)),x} is non empty set
{((a ") * (b * a))} is non empty set
{{((a ") * (b * a)),x},{((a ") * (b * a))}} is non empty set
the multF of G . [((a ") * (b * a)),x] is set
(x ") * (((a ") * (b * a)) * x) is Element of the carrier of G
the multF of G . ((x "),(((a ") * (b * a)) * x)) is Element of the carrier of G
[(x "),(((a ") * (b * a)) * x)] is set
{(x "),(((a ") * (b * a)) * x)} is non empty set
{{(x "),(((a ") * (b * a)) * x)},{(x ")}} is non empty set
the multF of G . [(x "),(((a ") * (b * a)) * x)] is set
(b * a) * x is Element of the carrier of G
the multF of G . ((b * a),x) is Element of the carrier of G
[(b * a),x] is set
{(b * a),x} is non empty set
{(b * a)} is non empty set
{{(b * a),x},{(b * a)}} is non empty set
the multF of G . [(b * a),x] is set
(a ") * ((b * a) * x) is Element of the carrier of G
the multF of G . ((a "),((b * a) * x)) is Element of the carrier of G
[(a "),((b * a) * x)] is set
{(a "),((b * a) * x)} is non empty set
{{(a "),((b * a) * x)},{(a ")}} is non empty set
the multF of G . [(a "),((b * a) * x)] is set
(x ") * ((a ") * ((b * a) * x)) is Element of the carrier of G
the multF of G . ((x "),((a ") * ((b * a) * x))) is Element of the carrier of G
[(x "),((a ") * ((b * a) * x))] is set
{(x "),((a ") * ((b * a) * x))} is non empty set
{{(x "),((a ") * ((b * a) * x))},{(x ")}} is non empty set
the multF of G . [(x "),((a ") * ((b * a) * x))] is set
(x ") * (a ") is Element of the carrier of G
the multF of G . ((x "),(a ")) is Element of the carrier of G
[(x "),(a ")] is set
{(x "),(a ")} is non empty set
{{(x "),(a ")},{(x ")}} is non empty set
the multF of G . [(x "),(a ")] is set
((x ") * (a ")) * ((b * a) * x) is Element of the carrier of G
the multF of G . (((x ") * (a ")),((b * a) * x)) is Element of the carrier of G
[((x ") * (a ")),((b * a) * x)] is set
{((x ") * (a ")),((b * a) * x)} is non empty set
{((x ") * (a "))} is non empty set
{{((x ") * (a ")),((b * a) * x)},{((x ") * (a "))}} is non empty set
the multF of G . [((x ") * (a ")),((b * a) * x)] is set
b * (a * x) is Element of the carrier of G
the multF of G . (b,(a * x)) is Element of the carrier of G
[b,(a * x)] is set
{b,(a * x)} is non empty set
{{b,(a * x)},{b}} is non empty set
the multF of G . [b,(a * x)] is set
((x ") * (a ")) * (b * (a * x)) is Element of the carrier of G
the multF of G . (((x ") * (a ")),(b * (a * x))) is Element of the carrier of G
[((x ") * (a ")),(b * (a * x))] is set
{((x ") * (a ")),(b * (a * x))} is non empty set
{{((x ") * (a ")),(b * (a * x))},{((x ") * (a "))}} is non empty set
the multF of G . [((x ") * (a ")),(b * (a * x))] is set
((x ") * (a ")) * b is Element of the carrier of G
the multF of G . (((x ") * (a ")),b) is Element of the carrier of G
[((x ") * (a ")),b] is set
{((x ") * (a ")),b} is non empty set
{{((x ") * (a ")),b},{((x ") * (a "))}} is non empty set
the multF of G . [((x ") * (a ")),b] is set
(((x ") * (a ")) * b) * (a * x) is Element of the carrier of G
the multF of G . ((((x ") * (a ")) * b),(a * x)) is Element of the carrier of G
[(((x ") * (a ")) * b),(a * x)] is set
{(((x ") * (a ")) * b),(a * x)} is non empty set
{(((x ") * (a ")) * b)} is non empty set
{{(((x ") * (a ")) * b),(a * x)},{(((x ") * (a ")) * b)}} is non empty set
the multF of G . [(((x ") * (a ")) * b),(a * x)] is set
a is Element of the carrier of G
G is non empty strict unital Group-like associative multMagma
(G) is non empty strict unital Group-like associative multMagma
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
the carrier of G is non empty set
(G) is Relation-like [:(G),(G):] -defined (G) -valued Function-like V14([:(G),(G):]) quasi_total Element of bool [:[:(G),(G):],(G):]
[:(G),(G):] is set
[:[:(G),(G):],(G):] is set
bool [:[:(G),(G):],(G):] is set
multMagma(# (G),(G) #) is strict multMagma
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
f is set
bool f is set
f1 is Element of bool f
[:f1,f1:] is set
a is set
(G) . a is Relation-like Function-like set
x is set
y1 is set
[x,y1] is set
{x,y1} is non empty set
{x} is non empty set
{{x,y1},{x}} is non empty set
q1 is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
b is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
b * q1 is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is set
(G) . (b,q1) is set
[b,q1] is set
{b,q1} is functional non empty set
{b} is functional non empty set
{{b,q1},{b}} is non empty set
(G) . [b,q1] is Relation-like Function-like set
[:f,f:] is set
[:(G),(G):] is set
[:[:(G),(G):],(G):] is set
bool [:[:(G),(G):],(G):] is set
(G) || (G) is set
(G) | [:(G),(G):] is Relation-like Function-like set
a is Relation-like [:(G),(G):] -defined (G) -valued Function-like V14([:(G),(G):]) quasi_total Element of bool [:[:(G),(G):],(G):]
multMagma(# (G),a #) is strict multMagma
the carrier of multMagma(# (G),a #) is set
q1 is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
g is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
[q1,g] is set
{q1,g} is functional non empty set
{q1} is functional non empty set
{{q1,g},{q1}} is non empty set
y1 is Element of the carrier of multMagma(# (G),a #)
b is Element of the carrier of multMagma(# (G),a #)
y1 * b is Element of the carrier of multMagma(# (G),a #)
the multF of multMagma(# (G),a #) is Relation-like [: the carrier of multMagma(# (G),a #), the carrier of multMagma(# (G),a #):] -defined the carrier of multMagma(# (G),a #) -valued Function-like quasi_total Element of bool [:[: the carrier of multMagma(# (G),a #), the carrier of multMagma(# (G),a #):], the carrier of multMagma(# (G),a #):]
[: the carrier of multMagma(# (G),a #), the carrier of multMagma(# (G),a #):] is set
[:[: the carrier of multMagma(# (G),a #), the carrier of multMagma(# (G),a #):], the carrier of multMagma(# (G),a #):] is set
bool [:[: the carrier of multMagma(# (G),a #), the carrier of multMagma(# (G),a #):], the carrier of multMagma(# (G),a #):] is set
the multF of multMagma(# (G),a #) . (y1,b) is Element of the carrier of multMagma(# (G),a #)
[y1,b] is set
{y1,b} is non empty set
{y1} is non empty set
{{y1,b},{y1}} is non empty set
the multF of multMagma(# (G),a #) . [y1,b] is set
(G) . (q1,g) is set
(G) . [q1,g] is Relation-like Function-like set
q1 * g is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is set
y1 is Element of the carrier of multMagma(# (G),a #)
b is Element of the carrier of multMagma(# (G),a #)
y1 * b is Element of the carrier of multMagma(# (G),a #)
the multF of multMagma(# (G),a #) . (y1,b) is Element of the carrier of multMagma(# (G),a #)
[y1,b] is set
{y1,b} is non empty set
{y1} is non empty set
{{y1,b},{y1}} is non empty set
the multF of multMagma(# (G),a #) . [y1,b] is set
q1 is Element of the carrier of multMagma(# (G),a #)
(y1 * b) * q1 is Element of the carrier of multMagma(# (G),a #)
the multF of multMagma(# (G),a #) . ((y1 * b),q1) is Element of the carrier of multMagma(# (G),a #)
[(y1 * b),q1] is set
{(y1 * b),q1} is non empty set
{(y1 * b)} is non empty set
{{(y1 * b),q1},{(y1 * b)}} is non empty set
the multF of multMagma(# (G),a #) . [(y1 * b),q1] is set
b * q1 is Element of the carrier of multMagma(# (G),a #)
the multF of multMagma(# (G),a #) . (b,q1) is Element of the carrier of multMagma(# (G),a #)
[b,q1] is set
{b,q1} is non empty set
{b} is non empty set
{{b,q1},{b}} is non empty set
the multF of multMagma(# (G),a #) . [b,q1] is set
y1 * (b * q1) is Element of the carrier of multMagma(# (G),a #)
the multF of multMagma(# (G),a #) . (y1,(b * q1)) is Element of the carrier of multMagma(# (G),a #)
[y1,(b * q1)] is set
{y1,(b * q1)} is non empty set
{{y1,(b * q1)},{y1}} is non empty set
the multF of multMagma(# (G),a #) . [y1,(b * q1)] is set
g is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
b is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
b * g is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
g is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
g * b is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
(g * b) * g is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
g * (b * g) is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
id the carrier of G is Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
y1 is Element of the carrier of multMagma(# (G),a #)
b is Element of the carrier of multMagma(# (G),a #)
b * y1 is Element of the carrier of multMagma(# (G),a #)
the multF of multMagma(# (G),a #) . (b,y1) is Element of the carrier of multMagma(# (G),a #)
[b,y1] is set
{b,y1} is non empty set
{b} is non empty set
{{b,y1},{b}} is non empty set
the multF of multMagma(# (G),a #) . [b,y1] is set
y1 * b is Element of the carrier of multMagma(# (G),a #)
the multF of multMagma(# (G),a #) . (y1,b) is Element of the carrier of multMagma(# (G),a #)
[y1,b] is set
{y1,b} is non empty set
{y1} is non empty set
{{y1,b},{y1}} is non empty set
the multF of multMagma(# (G),a #) . [y1,b] is set
q1 is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
q1 * (id the carrier of G) is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
(id the carrier of G) * q1 is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
q1 " is Relation-like Function-like set
g is Element of the carrier of multMagma(# (G),a #)
b * g is Element of the carrier of multMagma(# (G),a #)
the multF of multMagma(# (G),a #) . (b,g) is Element of the carrier of multMagma(# (G),a #)
[b,g] is set
{b,g} is non empty set
{{b,g},{b}} is non empty set
the multF of multMagma(# (G),a #) . [b,g] is set
g * b is Element of the carrier of multMagma(# (G),a #)
the multF of multMagma(# (G),a #) . (g,b) is Element of the carrier of multMagma(# (G),a #)
[g,b] is set
{g,b} is non empty set
{g} is non empty set
{{g,b},{g}} is non empty set
the multF of multMagma(# (G),a #) . [g,b] is set
b is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
g is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total unity-preserving V102(G,G) Element of bool [: the carrier of G, the carrier of G:]
rng g is Element of bool the carrier of G
bool the carrier of G is set
g " is Relation-like Function-like set
(g ") * g is Relation-like Function-like set
g * (g ") is Relation-like Function-like set
b is Element of the carrier of multMagma(# (G),a #)
y1 is non empty unital Group-like associative multMagma
the carrier of y1 is non empty set
the carrier of (G) is non empty set
b is non empty strict unital Group-like associative Subgroup of (G)
the carrier of b is non empty set
g is Element of the carrier of (G)
q1 is Element of the carrier of (G)
g |^ q1 is Element of the carrier of (G)
q1 " is Element of the carrier of (G)
(q1 ") * g is Element of the carrier of (G)
the multF of (G) is Relation-like [: the carrier of (G), the carrier of (G):] -defined the carrier of (G) -valued Function-like V14([: the carrier of (G), the carrier of (G):]) quasi_total associative Element of bool [:[: the carrier of (G), the carrier of (G):], the carrier of (G):]
[: the carrier of (G), the carrier of (G):] is set
[:[: the carrier of (G), the carrier of (G):], the carrier of (G):] is set
bool [:[: the carrier of (G), the carrier of (G):], the carrier of (G):] is set
the multF of (G) . ((q1 "),g) is Element of the carrier of (G)
[(q1 "),g] is set
{(q1 "),g} is non empty set
{(q1 ")} is non empty set
{{(q1 "),g},{(q1 ")}} is non empty set
the multF of (G) . [(q1 "),g] is set
((q1 ") * g) * q1 is Element of the carrier of (G)
the multF of (G) . (((q1 ") * g),q1) is Element of the carrier of (G)
[((q1 ") * g),q1] is set
{((q1 ") * g),q1} is non empty set
{((q1 ") * g)} is non empty set
{{((q1 ") * g),q1},{((q1 ") * g)}} is non empty set
the multF of (G) . [((q1 ") * g),q1] is set
b is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
g is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
g1 is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
Funcs ( the carrier of G, the carrier of G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
a is Element of the carrier of G
b " is Relation-like Function-like set
g1 * (b ") is Relation-like Function-like set
b * (g1 * (b ")) is Relation-like Function-like set
rng b is Element of bool the carrier of G
bool the carrier of G is set
dom b is Element of bool the carrier of G
C is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total unity-preserving V102(G,G) Element of bool [: the carrier of G, the carrier of G:]
C * b is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
id the carrier of G is Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
q is Element of the carrier of G
(b * (g1 * (b "))) . q is set
g1 * b is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
(g1 * b) * (b ") is Relation-like Function-like set
((g1 * b) * (b ")) . q is set
(g1 * b) . q is Element of the carrier of G
(b ") . ((g1 * b) . q) is set
b . q is Element of the carrier of G
g1 . (b . q) is Element of the carrier of G
(b ") . (g1 . (b . q)) is set
(b . q) |^ a is Element of the carrier of G
a " is Element of the carrier of G
(a ") * (b . q) 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 V14([: the carrier of G, the carrier of G:]) quasi_total associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . ((a "),(b . q)) is Element of the carrier of G
[(a "),(b . q)] is set
{(a "),(b . q)} is non empty set
{(a ")} is non empty set
{{(a "),(b . q)},{(a ")}} is non empty set
the multF of G . [(a "),(b . q)] is set
((a ") * (b . q)) * a is Element of the carrier of G
the multF of G . (((a ") * (b . q)),a) is Element of the carrier of G
[((a ") * (b . q)),a] is set
{((a ") * (b . q)),a} is non empty set
{((a ") * (b . q))} is non empty set
{{((a ") * (b . q)),a},{((a ") * (b . q))}} is non empty set
the multF of G . [((a ") * (b . q)),a] is set
(b ") . ((b . q) |^ a) is set
C . ((a ") * (b . q)) is Element of the carrier of G
C . a is Element of the carrier of G
(C . ((a ") * (b . q))) * (C . a) is Element of the carrier of G
the multF of G . ((C . ((a ") * (b . q))),(C . a)) is Element of the carrier of G
[(C . ((a ") * (b . q))),(C . a)] is set
{(C . ((a ") * (b . q))),(C . a)} is non empty set
{(C . ((a ") * (b . q)))} is non empty set
{{(C . ((a ") * (b . q))),(C . a)},{(C . ((a ") * (b . q)))}} is non empty set
the multF of G . [(C . ((a ") * (b . q))),(C . a)] is set
C . (a ") is Element of the carrier of G
C . (b . q) is Element of the carrier of G
(C . (a ")) * (C . (b . q)) is Element of the carrier of G
the multF of G . ((C . (a ")),(C . (b . q))) is Element of the carrier of G
[(C . (a ")),(C . (b . q))] is set
{(C . (a ")),(C . (b . q))} is non empty set
{(C . (a "))} is non empty set
{{(C . (a ")),(C . (b . q))},{(C . (a "))}} is non empty set
the multF of G . [(C . (a ")),(C . (b . q))] is set
((C . (a ")) * (C . (b . q))) * (C . a) is Element of the carrier of G
the multF of G . (((C . (a ")) * (C . (b . q))),(C . a)) is Element of the carrier of G
[((C . (a ")) * (C . (b . q))),(C . a)] is set
{((C . (a ")) * (C . (b . q))),(C . a)} is non empty set
{((C . (a ")) * (C . (b . q)))} is non empty set
{{((C . (a ")) * (C . (b . q))),(C . a)},{((C . (a ")) * (C . (b . q)))}} is non empty set
the multF of G . [((C . (a ")) * (C . (b . q))),(C . a)] is set
(C * b) . q is Element of the carrier of G
(C . (a ")) * ((C * b) . q) is Element of the carrier of G
the multF of G . ((C . (a ")),((C * b) . q)) is Element of the carrier of G
[(C . (a ")),((C * b) . q)] is set
{(C . (a ")),((C * b) . q)} is non empty set
{{(C . (a ")),((C * b) . q)},{(C . (a "))}} is non empty set
the multF of G . [(C . (a ")),((C * b) . q)] is set
((C . (a ")) * ((C * b) . q)) * (C . a) is Element of the carrier of G
the multF of G . (((C . (a ")) * ((C * b) . q)),(C . a)) is Element of the carrier of G
[((C . (a ")) * ((C * b) . q)),(C . a)] is set
{((C . (a ")) * ((C * b) . q)),(C . a)} is non empty set
{((C . (a ")) * ((C * b) . q))} is non empty set
{{((C . (a ")) * ((C * b) . q)),(C . a)},{((C . (a ")) * ((C * b) . q))}} is non empty set
the multF of G . [((C . (a ")) * ((C * b) . q)),(C . a)] is set
(C . (a ")) * q is Element of the carrier of G
the multF of G . ((C . (a ")),q) is Element of the carrier of G
[(C . (a ")),q] is set
{(C . (a ")),q} is non empty set
{{(C . (a ")),q},{(C . (a "))}} is non empty set
the multF of G . [(C . (a ")),q] is set
((C . (a ")) * q) * (C . a) is Element of the carrier of G
the multF of G . (((C . (a ")) * q),(C . a)) is Element of the carrier of G
[((C . (a ")) * q),(C . a)] is set
{((C . (a ")) * q),(C . a)} is non empty set
{((C . (a ")) * q)} is non empty set
{{((C . (a ")) * q),(C . a)},{((C . (a ")) * q)}} is non empty set
the multF of G . [((C . (a ")) * q),(C . a)] is set
q |^ (C . a) is Element of the carrier of G
(C . a) " is Element of the carrier of G
((C . a) ") * q is Element of the carrier of G
the multF of G . (((C . a) "),q) is Element of the carrier of G
[((C . a) "),q] is set
{((C . a) "),q} is non empty set
{((C . a) ")} is non empty set
{{((C . a) "),q},{((C . a) ")}} is non empty set
the multF of G . [((C . a) "),q] is set
(((C . a) ") * q) * (C . a) is Element of the carrier of G
the multF of G . ((((C . a) ") * q),(C . a)) is Element of the carrier of G
[(((C . a) ") * q),(C . a)] is set
{(((C . a) ") * q),(C . a)} is non empty set
{(((C . a) ") * q)} is non empty set
{{(((C . a) ") * q),(C . a)},{(((C . a) ") * q)}} is non empty set
the multF of G . [(((C . a) ") * q),(C . a)] is set
g * (b ") is Relation-like Function-like set
b * (g * (b ")) is Relation-like Function-like set
q is set
D is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
C is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
C * D is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
carr b is Element of bool the carrier of (G)
bool the carrier of (G) is set
q1 is non empty strict unital Group-like associative normal Subgroup of (G)
the carrier of q1 is non empty set
f is non empty strict unital Group-like associative normal Subgroup of (G)
the carrier of f is non empty set
f1 is non empty strict unital Group-like associative normal Subgroup of (G)
the carrier of f1 is non empty set
G is non empty strict unital Group-like associative multMagma
(G) is non empty strict unital Group-like associative normal Subgroup of (G)
(G) is non empty strict unital Group-like associative multMagma
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
the carrier of G is non empty set
(G) is Relation-like [:(G),(G):] -defined (G) -valued Function-like V14([:(G),(G):]) quasi_total Element of bool [:[:(G),(G):],(G):]
[:(G),(G):] is set
[:[:(G),(G):],(G):] is set
bool [:[:(G),(G):],(G):] is set
multMagma(# (G),(G) #) is strict multMagma
the carrier of (G) is non empty set
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
f is Element of the carrier of (G)
f1 is Element of the carrier of (G)
f * f1 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 V14([: the carrier of (G), the carrier of (G):]) quasi_total associative Element of bool [:[: the carrier of (G), the carrier of (G):], the carrier of (G):]
[: the carrier of (G), the carrier of (G):] is set
[:[: the carrier of (G), the carrier of (G):], the carrier of (G):] is set
bool [:[: the carrier of (G), the carrier of (G):], the carrier of (G):] is set
the multF of (G) . (f,f1) is Element of the carrier of (G)
[f,f1] is set
{f,f1} is non empty set
{f} is non empty set
{{f,f1},{f}} is non empty set
the multF of (G) . [f,f1] is set
a is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
x is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
a * x is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is set
the carrier of (G) is non empty set
y1 is Element of the carrier of (G)
b is Element of the carrier of (G)
q1 is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
g is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
y1 * 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 V14([: the carrier of (G), the carrier of (G):]) quasi_total associative Element of bool [:[: the carrier of (G), the carrier of (G):], the carrier of (G):]
[: the carrier of (G), the carrier of (G):] is set
[:[: the carrier of (G), the carrier of (G):], the carrier of (G):] is set
bool [:[: the carrier of (G), the carrier of (G):], the carrier of (G):] is set
the multF of (G) . (y1,b) is Element of the carrier of (G)
[y1,b] is set
{y1,b} is non empty set
{y1} is non empty set
{{y1,b},{y1}} is non empty set
the multF of (G) . [y1,b] is set
q1 * g is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
G is non empty strict unital Group-like associative multMagma
the carrier of G is non empty set
id the carrier of G is Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is set
(G) is non empty strict unital Group-like associative normal Subgroup of (G)
(G) is non empty strict unital Group-like associative multMagma
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
(G) is Relation-like [:(G),(G):] -defined (G) -valued Function-like V14([:(G),(G):]) quasi_total Element of bool [:[:(G),(G):],(G):]
[:(G),(G):] is set
[:[:(G),(G):],(G):] is set
bool [:[:(G),(G):],(G):] is set
multMagma(# (G),(G) #) is strict multMagma
1_ (G) is non being_of_order_0 Element of the carrier of (G)
the carrier of (G) is non empty set
1_ (G) is non being_of_order_0 Element of the carrier of (G)
the carrier of (G) is non empty set
G is non empty strict unital Group-like associative multMagma
the carrier of G is non empty set
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
(G) is non empty strict unital Group-like associative normal Subgroup of (G)
(G) is non empty strict unital Group-like associative multMagma
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
(G) is Relation-like [:(G),(G):] -defined (G) -valued Function-like V14([:(G),(G):]) quasi_total Element of bool [:[:(G),(G):],(G):]
[:(G),(G):] is set
[:[:(G),(G):],(G):] is set
bool [:[:(G),(G):],(G):] is set
multMagma(# (G),(G) #) is strict multMagma
the carrier of (G) is non empty set
f is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
f " is Relation-like Function-like set
f1 is Element of the carrier of (G)
f1 " is Element of the carrier of (G)
the carrier of (G) is non empty set
a is Element of the carrier of (G)
x is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
x " is Relation-like Function-like set
a " is Element of the carrier of (G)
G is non empty strict unital Group-like associative multMagma
the carrier of G is non empty set
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
f is Element of the carrier of G
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is set
f1 is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
Funcs ( the carrier of G, the carrier of G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
a is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
x is Element of the carrier of G
a . x is Element of the carrier of G
x |^ f is Element of the carrier of G
f " is Element of the carrier of G
(f ") * 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 V14([: the carrier of G, the carrier of G:]) quasi_total associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . ((f "),x) is Element of the carrier of G
[(f "),x] is set
{(f "),x} is non empty set
{(f ")} is non empty set
{{(f "),x},{(f ")}} is non empty set
the multF of G . [(f "),x] is set
((f ") * x) * f is Element of the carrier of G
the multF of G . (((f ") * x),f) is Element of the carrier of G
[((f ") * x),f] is set
{((f ") * x),f} is non empty set
{((f ") * x)} is non empty set
{{((f ") * x),f},{((f ") * x)}} is non empty set
the multF of G . [((f ") * x),f] is set
f1 is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
a is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
x is Element of the carrier of G
f1 . x is Element of the carrier of G
a . x is Element of the carrier of G
x |^ f is Element of the carrier of G
f " is Element of the carrier of G
(f ") * 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 V14([: the carrier of G, the carrier of G:]) quasi_total associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . ((f "),x) is Element of the carrier of G
[(f "),x] is set
{(f "),x} is non empty set
{(f ")} is non empty set
{{(f "),x},{(f ")}} is non empty set
the multF of G . [(f "),x] is set
((f ") * x) * f is Element of the carrier of G
the multF of G . (((f ") * x),f) is Element of the carrier of G
[((f ") * x),f] is set
{((f ") * x),f} is non empty set
{((f ") * x)} is non empty set
{{((f ") * x),f},{((f ") * x)}} is non empty set
the multF of G . [((f ") * x),f] is set
G is non empty strict unital Group-like associative multMagma
the carrier of G is non empty set
f is Element of the carrier of G
(G,f) is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
f1 is Element of the carrier of G
f * f1 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 V14([: the carrier of G, the carrier of G:]) quasi_total associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (f,f1) is Element of the carrier of G
[f,f1] is set
{f,f1} is non empty set
{f} is non empty set
{{f,f1},{f}} is non empty set
the multF of G . [f,f1] is set
(G,(f * f1)) is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
(G,f1) is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
(G,f1) * (G,f) is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
bool [: the carrier of G, the carrier of G:] is set
y1 is Element of the carrier of G
(G,(f * f1)) . y1 is Element of the carrier of G
y1 |^ f is Element of the carrier of G
f " is Element of the carrier of G
(f ") * y1 is Element of the carrier of G
the multF of G . ((f "),y1) is Element of the carrier of G
[(f "),y1] is set
{(f "),y1} is non empty set
{(f ")} is non empty set
{{(f "),y1},{(f ")}} is non empty set
the multF of G . [(f "),y1] is set
((f ") * y1) * f is Element of the carrier of G
the multF of G . (((f ") * y1),f) is Element of the carrier of G
[((f ") * y1),f] is set
{((f ") * y1),f} is non empty set
{((f ") * y1)} is non empty set
{{((f ") * y1),f},{((f ") * y1)}} is non empty set
the multF of G . [((f ") * y1),f] is set
(y1 |^ f) |^ f1 is Element of the carrier of G
f1 " is Element of the carrier of G
(f1 ") * (y1 |^ f) is Element of the carrier of G
the multF of G . ((f1 "),(y1 |^ f)) is Element of the carrier of G
[(f1 "),(y1 |^ f)] is set
{(f1 "),(y1 |^ f)} is non empty set
{(f1 ")} is non empty set
{{(f1 "),(y1 |^ f)},{(f1 ")}} is non empty set
the multF of G . [(f1 "),(y1 |^ f)] is set
((f1 ") * (y1 |^ f)) * f1 is Element of the carrier of G
the multF of G . (((f1 ") * (y1 |^ f)),f1) is Element of the carrier of G
[((f1 ") * (y1 |^ f)),f1] is set
{((f1 ") * (y1 |^ f)),f1} is non empty set
{((f1 ") * (y1 |^ f))} is non empty set
{{((f1 ") * (y1 |^ f)),f1},{((f1 ") * (y1 |^ f))}} is non empty set
the multF of G . [((f1 ") * (y1 |^ f)),f1] is set
y1 |^ (f * f1) is Element of the carrier of G
(f * f1) " is Element of the carrier of G
((f * f1) ") * y1 is Element of the carrier of G
the multF of G . (((f * f1) "),y1) is Element of the carrier of G
[((f * f1) "),y1] is set
{((f * f1) "),y1} is non empty set
{((f * f1) ")} is non empty set
{{((f * f1) "),y1},{((f * f1) ")}} is non empty set
the multF of G . [((f * f1) "),y1] is set
(((f * f1) ") * y1) * (f * f1) is Element of the carrier of G
the multF of G . ((((f * f1) ") * y1),(f * f1)) is Element of the carrier of G
[(((f * f1) ") * y1),(f * f1)] is set
{(((f * f1) ") * y1),(f * f1)} is non empty set
{(((f * f1) ") * y1)} is non empty set
{{(((f * f1) ") * y1),(f * f1)},{(((f * f1) ") * y1)}} is non empty set
the multF of G . [(((f * f1) ") * y1),(f * f1)] is set
y1 is Element of the carrier of G
(G,(f * f1)) . y1 is Element of the carrier of G
y1 |^ f is Element of the carrier of G
f " is Element of the carrier of G
(f ") * y1 is Element of the carrier of G
the multF of G . ((f "),y1) is Element of the carrier of G
[(f "),y1] is set
{(f "),y1} is non empty set
{(f ")} is non empty set
{{(f "),y1},{(f ")}} is non empty set
the multF of G . [(f "),y1] is set
((f ") * y1) * f is Element of the carrier of G
the multF of G . (((f ") * y1),f) is Element of the carrier of G
[((f ") * y1),f] is set
{((f ") * y1),f} is non empty set
{((f ") * y1)} is non empty set
{{((f ") * y1),f},{((f ") * y1)}} is non empty set
the multF of G . [((f ") * y1),f] is set
(G,f1) . (y1 |^ f) is Element of the carrier of G
(y1 |^ f) |^ f1 is Element of the carrier of G
f1 " is Element of the carrier of G
(f1 ") * (y1 |^ f) is Element of the carrier of G
the multF of G . ((f1 "),(y1 |^ f)) is Element of the carrier of G
[(f1 "),(y1 |^ f)] is set
{(f1 "),(y1 |^ f)} is non empty set
{(f1 ")} is non empty set
{{(f1 "),(y1 |^ f)},{(f1 ")}} is non empty set
the multF of G . [(f1 "),(y1 |^ f)] is set
((f1 ") * (y1 |^ f)) * f1 is Element of the carrier of G
the multF of G . (((f1 ") * (y1 |^ f)),f1) is Element of the carrier of G
[((f1 ") * (y1 |^ f)),f1] is set
{((f1 ") * (y1 |^ f)),f1} is non empty set
{((f1 ") * (y1 |^ f))} is non empty set
{{((f1 ") * (y1 |^ f)),f1},{((f1 ") * (y1 |^ f))}} is non empty set
the multF of G . [((f1 ") * (y1 |^ f)),f1] is set
y1 is Element of the carrier of G
(G,(f * f1)) . y1 is Element of the carrier of G
(G,f) . y1 is Element of the carrier of G
(G,f1) . ((G,f) . y1) is Element of the carrier of G
y1 |^ f is Element of the carrier of G
f " is Element of the carrier of G
(f ") * y1 is Element of the carrier of G
the multF of G . ((f "),y1) is Element of the carrier of G
[(f "),y1] is set
{(f "),y1} is non empty set
{(f ")} is non empty set
{{(f "),y1},{(f ")}} is non empty set
the multF of G . [(f "),y1] is set
((f ") * y1) * f is Element of the carrier of G
the multF of G . (((f ") * y1),f) is Element of the carrier of G
[((f ") * y1),f] is set
{((f ") * y1),f} is non empty set
{((f ") * y1)} is non empty set
{{((f ") * y1),f},{((f ") * y1)}} is non empty set
the multF of G . [((f ") * y1),f] is set
(G,f1) . (y1 |^ f) is Element of the carrier of G
y1 is Element of the carrier of G
(G,(f * f1)) . y1 is Element of the carrier of G
((G,f1) * (G,f)) . y1 is Element of the carrier of G
(G,f) . y1 is Element of the carrier of G
(G,f1) . ((G,f) . y1) is Element of the carrier of G
G is non empty strict unital Group-like associative multMagma
the carrier of G is non empty set
1_ G is non being_of_order_0 Element of the carrier of G
(G,(1_ G)) is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
id the carrier of G is Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is set
f is Element of the carrier of G
(G,(1_ G)) . f is Element of the carrier of G
f |^ (1_ G) is Element of the carrier of G
(1_ G) " is Element of the carrier of G
((1_ G) ") * f 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 V14([: the carrier of G, the carrier of G:]) quasi_total associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (((1_ G) "),f) is Element of the carrier of G
[((1_ G) "),f] is set
{((1_ G) "),f} is non empty set
{((1_ G) ")} is non empty set
{{((1_ G) "),f},{((1_ G) ")}} is non empty set
the multF of G . [((1_ G) "),f] is set
(((1_ G) ") * f) * (1_ G) is Element of the carrier of G
the multF of G . ((((1_ G) ") * f),(1_ G)) is Element of the carrier of G
[(((1_ G) ") * f),(1_ G)] is set
{(((1_ G) ") * f),(1_ G)} is non empty set
{(((1_ G) ") * f)} is non empty set
{{(((1_ G) ") * f),(1_ G)},{(((1_ G) ") * f)}} is non empty set
the multF of G . [(((1_ G) ") * f),(1_ G)] is set
f is set
(G,(1_ G)) . f is set
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
dom (G,(1_ G)) is Element of bool the carrier of G
bool the carrier of G is set
G is non empty strict unital Group-like associative multMagma
the carrier of G is non empty set
1_ G is non being_of_order_0 Element of the carrier of G
(G,(1_ G)) is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
f is Element of the carrier of G
(G,(1_ G)) . f is Element of the carrier of G
f |^ (1_ G) is Element of the carrier of G
(1_ G) " is Element of the carrier of G
((1_ G) ") * f 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 V14([: the carrier of G, the carrier of G:]) quasi_total associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (((1_ G) "),f) is Element of the carrier of G
[((1_ G) "),f] is set
{((1_ G) "),f} is non empty set
{((1_ G) ")} is non empty set
{{((1_ G) "),f},{((1_ G) ")}} is non empty set
the multF of G . [((1_ G) "),f] is set
(((1_ G) ") * f) * (1_ G) is Element of the carrier of G
the multF of G . ((((1_ G) ") * f),(1_ G)) is Element of the carrier of G
[(((1_ G) ") * f),(1_ G)] is set
{(((1_ G) ") * f),(1_ G)} is non empty set
{(((1_ G) ") * f)} is non empty set
{{(((1_ G) ") * f),(1_ G)},{(((1_ G) ") * f)}} is non empty set
the multF of G . [(((1_ G) ") * f),(1_ G)] is set
G is non empty strict unital Group-like associative multMagma
the carrier of G is non empty set
1_ G is non being_of_order_0 Element of the carrier of G
(G,(1_ G)) is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
f is Element of the carrier of G
f " is Element of the carrier of G
(G,(f ")) is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
(G,f) is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
(G,f) * (G,(f ")) is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is set
x is Element of the carrier of G
((G,f) * (G,(f "))) . x is Element of the carrier of G
(G,(f ")) . x is Element of the carrier of G
(G,f) . ((G,(f ")) . x) is Element of the carrier of G
x |^ (f ") is Element of the carrier of G
(f ") " is Element of the carrier of G
((f ") ") * 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 V14([: the carrier of G, the carrier of G:]) quasi_total associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (((f ") "),x) is Element of the carrier of G
[((f ") "),x] is set
{((f ") "),x} is non empty set
{((f ") ")} is non empty set
{{((f ") "),x},{((f ") ")}} is non empty set
the multF of G . [((f ") "),x] is set
(((f ") ") * x) * (f ") is Element of the carrier of G
the multF of G . ((((f ") ") * x),(f ")) is Element of the carrier of G
[(((f ") ") * x),(f ")] is set
{(((f ") ") * x),(f ")} is non empty set
{(((f ") ") * x)} is non empty set
{{(((f ") ") * x),(f ")},{(((f ") ") * x)}} is non empty set
the multF of G . [(((f ") ") * x),(f ")] is set
(G,f) . (x |^ (f ")) is Element of the carrier of G
(x |^ (f ")) |^ f is Element of the carrier of G
(f ") * (x |^ (f ")) is Element of the carrier of G
the multF of G . ((f "),(x |^ (f "))) is Element of the carrier of G
[(f "),(x |^ (f "))] is set
{(f "),(x |^ (f "))} is non empty set
{(f ")} is non empty set
{{(f "),(x |^ (f "))},{(f ")}} is non empty set
the multF of G . [(f "),(x |^ (f "))] is set
((f ") * (x |^ (f "))) * f is Element of the carrier of G
the multF of G . (((f ") * (x |^ (f "))),f) is Element of the carrier of G
[((f ") * (x |^ (f "))),f] is set
{((f ") * (x |^ (f "))),f} is non empty set
{((f ") * (x |^ (f ")))} is non empty set
{{((f ") * (x |^ (f "))),f},{((f ") * (x |^ (f ")))}} is non empty set
the multF of G . [((f ") * (x |^ (f "))),f] is set
x is Element of the carrier of G
((G,f) * (G,(f "))) . x is Element of the carrier of G
(G,(1_ G)) . x is Element of the carrier of G
G is non empty strict unital Group-like associative multMagma
the carrier of G is non empty set
1_ G is non being_of_order_0 Element of the carrier of G
(G,(1_ G)) is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
f is Element of the carrier of G
(G,f) is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
f " is Element of the carrier of G
(G,(f ")) is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
(G,(f ")) * (G,f) is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is set
x is Element of the carrier of G
((G,(f ")) * (G,f)) . x is Element of the carrier of G
(G,f) . x is Element of the carrier of G
(G,(f ")) . ((G,f) . x) is Element of the carrier of G
x |^ f is Element of the carrier of G
(f ") * 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 V14([: the carrier of G, the carrier of G:]) quasi_total associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . ((f "),x) is Element of the carrier of G
[(f "),x] is set
{(f "),x} is non empty set
{(f ")} is non empty set
{{(f "),x},{(f ")}} is non empty set
the multF of G . [(f "),x] is set
((f ") * x) * f is Element of the carrier of G
the multF of G . (((f ") * x),f) is Element of the carrier of G
[((f ") * x),f] is set
{((f ") * x),f} is non empty set
{((f ") * x)} is non empty set
{{((f ") * x),f},{((f ") * x)}} is non empty set
the multF of G . [((f ") * x),f] is set
(G,(f ")) . (x |^ f) is Element of the carrier of G
(x |^ f) |^ (f ") is Element of the carrier of G
(f ") " is Element of the carrier of G
((f ") ") * (x |^ f) is Element of the carrier of G
the multF of G . (((f ") "),(x |^ f)) is Element of the carrier of G
[((f ") "),(x |^ f)] is set
{((f ") "),(x |^ f)} is non empty set
{((f ") ")} is non empty set
{{((f ") "),(x |^ f)},{((f ") ")}} is non empty set
the multF of G . [((f ") "),(x |^ f)] is set
(((f ") ") * (x |^ f)) * (f ") is Element of the carrier of G
the multF of G . ((((f ") ") * (x |^ f)),(f ")) is Element of the carrier of G
[(((f ") ") * (x |^ f)),(f ")] is set
{(((f ") ") * (x |^ f)),(f ")} is non empty set
{(((f ") ") * (x |^ f))} is non empty set
{{(((f ") ") * (x |^ f)),(f ")},{(((f ") ") * (x |^ f))}} is non empty set
the multF of G . [(((f ") ") * (x |^ f)),(f ")] is set
x is Element of the carrier of G
((G,(f ")) * (G,f)) . x is Element of the carrier of G
(G,(1_ G)) . x is Element of the carrier of G
G is non empty strict unital Group-like associative multMagma
the carrier of G is non empty set
f is Element of the carrier of G
f " is Element of the carrier of G
(G,(f ")) is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
(G,f) is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
(G,f) " is Relation-like Function-like set
(G,(f ")) * (G,f) is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is set
1_ G is non being_of_order_0 Element of the carrier of G
(G,(1_ G)) is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
id the carrier of G is Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
rng (G,f) is Element of bool the carrier of G
bool the carrier of G is set
dom (G,f) is Element of bool the carrier of G
G is non empty strict unital Group-like associative multMagma
the carrier of G is non empty set
1_ G is non being_of_order_0 Element of the carrier of G
(G,(1_ G)) is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
f is Element of the carrier of G
(G,f) is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
(G,f) * (G,(1_ G)) is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is set
(G,(1_ G)) * (G,f) is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
id the carrier of G is Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
G is non empty strict unital Group-like associative multMagma
the carrier of G is non empty set
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
1_ G is non being_of_order_0 Element of the carrier of G
(G,(1_ G)) is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
f is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
f * (G,(1_ G)) is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is set
(G,(1_ G)) * f is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
id the carrier of G is Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
G is non empty strict unital Group-like associative multMagma
(G) is non empty strict unital Group-like associative normal Subgroup of (G)
(G) is non empty strict unital Group-like associative multMagma
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
the carrier of G is non empty set
(G) is Relation-like [:(G),(G):] -defined (G) -valued Function-like V14([:(G),(G):]) quasi_total Element of bool [:[:(G),(G):],(G):]
[:(G),(G):] is set
[:[:(G),(G):],(G):] is set
bool [:[:(G),(G):],(G):] is set
multMagma(# (G),(G) #) is strict multMagma
center G is non empty strict unital Group-like associative normal Subgroup of G
G ./. (center G) is non empty strict unital Group-like associative multMagma
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
[: the carrier of G,(G):] is set
bool [: the carrier of G,(G):] is set
f is Relation-like the carrier of G -defined (G) -valued Function-like non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G,(G):]
the carrier of (G) is non empty set
[: the carrier of G, the carrier of (G):] is set
bool [: the carrier of G, the carrier of (G):] is set
f1 is Relation-like the carrier of G -defined the carrier of (G) -valued Function-like non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of (G):]
a is Element of the carrier of G
x is Element of the carrier of G
a * 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 V14([: the carrier of G, the carrier of G:]) quasi_total associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (a,x) is Element of the carrier of G
[a,x] is set
{a,x} is non empty set
{a} is non empty set
{{a,x},{a}} is non empty set
the multF of G . [a,x] is set
f1 . (a * x) is Element of the carrier of (G)
(a * x) " is Element of the carrier of G
(G,((a * x) ")) is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
x " is Element of the carrier of G
a " is Element of the carrier of G
(x ") * (a ") is Element of the carrier of G
the multF of G . ((x "),(a ")) is Element of the carrier of G
[(x "),(a ")] is set
{(x "),(a ")} is non empty set
{(x ")} is non empty set
{{(x "),(a ")},{(x ")}} is non empty set
the multF of G . [(x "),(a ")] is set
(G,((x ") * (a "))) is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
(G,(x ")) is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
(G,(a ")) is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
(G,(a ")) * (G,(x ")) is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
bool [: the carrier of G, the carrier of G:] is set
y1 is Element of the carrier of (G)
f1 . a is Element of the carrier of (G)
b is Element of the carrier of (G)
f1 . x is Element of the carrier of (G)
(f1 . a) * (f1 . 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 V14([: the carrier of (G), the carrier of (G):]) quasi_total associative Element of bool [:[: the carrier of (G), the carrier of (G):], the carrier of (G):]
[: the carrier of (G), the carrier of (G):] is set
[:[: the carrier of (G), the carrier of (G):], the carrier of (G):] is set
bool [:[: the carrier of (G), the carrier of (G):], the carrier of (G):] is set
the multF of (G) . ((f1 . a),(f1 . x)) is Element of the carrier of (G)
[(f1 . a),(f1 . x)] is set
{(f1 . a),(f1 . x)} is non empty set
{(f1 . a)} is non empty set
{{(f1 . a),(f1 . x)},{(f1 . a)}} is non empty set
the multF of (G) . [(f1 . a),(f1 . x)] is set
a is Relation-like the carrier of G -defined the carrier of (G) -valued Function-like non empty V14( the carrier of G) quasi_total unity-preserving V102(G,(G)) Element of bool [: the carrier of G, the carrier of (G):]
Ker a is non empty strict unital Group-like associative normal Subgroup of G
{ b₁ where b₁ is Element of the carrier of G : for b₂ being Element of the carrier of G holds b₁ * b₂ = b₂ * b₁ } is set
the carrier of (Ker a) is non empty set
1_ (G) is non being_of_order_0 Element of the carrier of (G)
{ b₁ where b₁ is Element of the carrier of G : a . b₁ = 1_ (G) } is set
b is set
id the carrier of G is Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
q1 is Element of the carrier of G
a . q1 is Element of the carrier of (G)
q1 " is Element of the carrier of G
(G,(q1 ")) is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
g is Element of the carrier of G
(G,(q1 ")) . g is Element of the carrier of G
(id the carrier of G) . g is Element of the carrier of G
g is Element of the carrier of G
g |^ (q1 ") is Element of the carrier of G
(q1 ") " is Element of the carrier of G
((q1 ") ") * g is Element of the carrier of G
the multF of G . (((q1 ") "),g) is Element of the carrier of G
[((q1 ") "),g] is set
{((q1 ") "),g} is non empty set
{((q1 ") ")} is non empty set
{{((q1 ") "),g},{((q1 ") ")}} is non empty set
the multF of G . [((q1 ") "),g] is set
(((q1 ") ") * g) * (q1 ") is Element of the carrier of G
the multF of G . ((((q1 ") ") * g),(q1 ")) is Element of the carrier of G
[(((q1 ") ") * g),(q1 ")] is set
{(((q1 ") ") * g),(q1 ")} is non empty set
{(((q1 ") ") * g)} is non empty set
{{(((q1 ") ") * g),(q1 ")},{(((q1 ") ") * g)}} is non empty set
the multF of G . [(((q1 ") ") * g),(q1 ")] is set
(G,(q1 ")) . g is Element of the carrier of G
g is Element of the carrier of G
q1 * g is Element of the carrier of G
the multF of G . (q1,g) is Element of the carrier of G
[q1,g] is set
{q1,g} is non empty set
{q1} is non empty set
{{q1,g},{q1}} is non empty set
the multF of G . [q1,g] is set
g * q1 is Element of the carrier of G
the multF of G . (g,q1) is Element of the carrier of G
[g,q1] is set
{g,q1} is non empty set
{g} is non empty set
{{g,q1},{g}} is non empty set
the multF of G . [g,q1] is set
g |^ (q1 ") is Element of the carrier of G
(q1 ") " is Element of the carrier of G
((q1 ") ") * g is Element of the carrier of G
the multF of G . (((q1 ") "),g) is Element of the carrier of G
[((q1 ") "),g] is set
{((q1 ") "),g} is non empty set
{((q1 ") ")} is non empty set
{{((q1 ") "),g},{((q1 ") ")}} is non empty set
the multF of G . [((q1 ") "),g] is set
(((q1 ") ") * g) * (q1 ") is Element of the carrier of G
the multF of G . ((((q1 ") ") * g),(q1 ")) is Element of the carrier of G
[(((q1 ") ") * g),(q1 ")] is set
{(((q1 ") ") * g),(q1 ")} is non empty set
{(((q1 ") ") * g)} is non empty set
{{(((q1 ") ") * g),(q1 ")},{(((q1 ") ") * g)}} is non empty set
the multF of G . [(((q1 ") ") * g),(q1 ")] is set
(q1 * g) * (q1 ") is Element of the carrier of G
the multF of G . ((q1 * g),(q1 ")) is Element of the carrier of G
[(q1 * g),(q1 ")] is set
{(q1 * g),(q1 ")} is non empty set
{(q1 * g)} is non empty set
{{(q1 * g),(q1 ")},{(q1 * g)}} is non empty set
the multF of G . [(q1 * g),(q1 ")] is set
((q1 * g) * (q1 ")) * q1 is Element of the carrier of G
the multF of G . (((q1 * g) * (q1 ")),q1) is Element of the carrier of G
[((q1 * g) * (q1 ")),q1] is set
{((q1 * g) * (q1 ")),q1} is non empty set
{((q1 * g) * (q1 "))} is non empty set
{{((q1 * g) * (q1 ")),q1},{((q1 * g) * (q1 "))}} is non empty set
the multF of G . [((q1 * g) * (q1 ")),q1] is set
(q1 ") * q1 is Element of the carrier of G
the multF of G . ((q1 "),q1) is Element of the carrier of G
[(q1 "),q1] is set
{(q1 "),q1} is non empty set
{(q1 ")} is non empty set
{{(q1 "),q1},{(q1 ")}} is non empty set
the multF of G . [(q1 "),q1] is set
(q1 * g) * ((q1 ") * q1) is Element of the carrier of G
the multF of G . ((q1 * g),((q1 ") * q1)) is Element of the carrier of G
[(q1 * g),((q1 ") * q1)] is set
{(q1 * g),((q1 ") * q1)} is non empty set
{{(q1 * g),((q1 ") * q1)},{(q1 * g)}} is non empty set
the multF of G . [(q1 * g),((q1 ") * q1)] is set
1_ G is non being_of_order_0 Element of the carrier of G
(q1 * g) * (1_ G) is Element of the carrier of G
the multF of G . ((q1 * g),(1_ G)) is Element of the carrier of G
[(q1 * g),(1_ G)] is set
{(q1 * g),(1_ G)} is non empty set
{{(q1 * g),(1_ G)},{(q1 * g)}} is non empty set
the multF of G . [(q1 * g),(1_ G)] is set
b is set
q1 is Element of the carrier of G
q1 " is Element of the carrier of G
(G,(q1 ")) is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
g is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
b is Element of the carrier of G
(G,(q1 ")) . b is Element of the carrier of G
q1 * b is Element of the carrier of G
the multF of G . (q1,b) is Element of the carrier of G
[q1,b] is set
{q1,b} is non empty set
{q1} is non empty set
{{q1,b},{q1}} is non empty set
the multF of G . [q1,b] is set
(q1 * b) * (q1 ") is Element of the carrier of G
the multF of G . ((q1 * b),(q1 ")) is Element of the carrier of G
[(q1 * b),(q1 ")] is set
{(q1 * b),(q1 ")} is non empty set
{(q1 * b)} is non empty set
{{(q1 * b),(q1 ")},{(q1 * b)}} is non empty set
the multF of G . [(q1 * b),(q1 ")] is set
b * q1 is Element of the carrier of G
the multF of G . (b,q1) is Element of the carrier of G
[b,q1] is set
{b,q1} is non empty set
{b} is non empty set
{{b,q1},{b}} is non empty set
the multF of G . [b,q1] is set
(b * q1) * (q1 ") is Element of the carrier of G
the multF of G . ((b * q1),(q1 ")) is Element of the carrier of G
[(b * q1),(q1 ")] is set
{(b * q1),(q1 ")} is non empty set
{(b * q1)} is non empty set
{{(b * q1),(q1 ")},{(b * q1)}} is non empty set
the multF of G . [(b * q1),(q1 ")] is set
q1 * (q1 ") is Element of the carrier of G
the multF of G . (q1,(q1 ")) is Element of the carrier of G
[q1,(q1 ")] is set
{q1,(q1 ")} is non empty set
{{q1,(q1 ")},{q1}} is non empty set
the multF of G . [q1,(q1 ")] is set
b * (q1 * (q1 ")) is Element of the carrier of G
the multF of G . (b,(q1 * (q1 "))) is Element of the carrier of G
[b,(q1 * (q1 "))] is set
{b,(q1 * (q1 "))} is non empty set
{{b,(q1 * (q1 "))},{b}} is non empty set
the multF of G . [b,(q1 * (q1 "))] is set
1_ G is non being_of_order_0 Element of the carrier of G
b * (1_ G) is Element of the carrier of G
the multF of G . (b,(1_ G)) is Element of the carrier of G
[b,(1_ G)] is set
{b,(1_ G)} is non empty set
{{b,(1_ G)},{b}} is non empty set
the multF of G . [b,(1_ G)] is set
b |^ (q1 ") is Element of the carrier of G
(q1 ") " is Element of the carrier of G
((q1 ") ") * b is Element of the carrier of G
the multF of G . (((q1 ") "),b) is Element of the carrier of G
[((q1 ") "),b] is set
{((q1 ") "),b} is non empty set
{((q1 ") ")} is non empty set
{{((q1 ") "),b},{((q1 ") ")}} is non empty set
the multF of G . [((q1 ") "),b] is set
(((q1 ") ") * b) * (q1 ") is Element of the carrier of G
the multF of G . ((((q1 ") ") * b),(q1 ")) is Element of the carrier of G
[(((q1 ") ") * b),(q1 ")] is set
{(((q1 ") ") * b),(q1 ")} is non empty set
{(((q1 ") ") * b)} is non empty set
{{(((q1 ") ") * b),(q1 ")},{(((q1 ") ") * b)}} is non empty set
the multF of G . [(((q1 ") ") * b),(q1 ")] is set
id the carrier of G is Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
b is Element of the carrier of G
(id the carrier of G) . b is Element of the carrier of G
g . b is Element of the carrier of G
a . q1 is Element of the carrier of (G)
x is set
y1 is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
Funcs ( the carrier of G, the carrier of G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
b is Element of the carrier of G
b " is Element of the carrier of G
q1 is Element of the carrier of G
a . q1 is set
a . q1 is Element of the carrier of (G)
(b ") " is Element of the carrier of G
(G,((b ") ")) is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
(G,b) is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
rng a is Element of bool the carrier of (G)
bool the carrier of (G) is set
Image a is non empty strict unital Group-like associative Subgroup of (G)
G is non empty strict unital Group-like associative multMagma
(G) is non empty strict unital Group-like associative normal Subgroup of (G)
(G) is non empty strict unital Group-like associative multMagma
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
the carrier of G is non empty set
(G) is Relation-like [:(G),(G):] -defined (G) -valued Function-like V14([:(G),(G):]) quasi_total Element of bool [:[:(G),(G):],(G):]
[:(G),(G):] is set
[:[:(G),(G):],(G):] is set
bool [:[:(G),(G):],(G):] is set
multMagma(# (G),(G) #) is strict multMagma
the carrier of (G) is non empty set
1_ (G) is non being_of_order_0 Element of the carrier of (G)
f is Element of the carrier of (G)
(G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
f1 is Relation-like the carrier of G -defined the carrier of G -valued Function-like V14( the carrier of G) quasi_total Element of (G)
Funcs ( the carrier of G, the carrier of G) is functional non empty FUNCTION_DOMAIN of the carrier of G, the carrier of G
a is Element of the carrier of G
x is Element of the carrier of G
f1 . x is Element of the carrier of G
x |^ a is Element of the carrier of G
a " is Element of the carrier of G
(a ") * 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 V14([: the carrier of G, the carrier of G:]) quasi_total associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . ((a "),x) is Element of the carrier of G
[(a "),x] is set
{(a "),x} is non empty set
{(a ")} is non empty set
{{(a "),x},{(a ")}} is non empty set
the multF of G . [(a "),x] is set
((a ") * x) * a is Element of the carrier of G
the multF of G . (((a ") * x),a) is Element of the carrier of G
[((a ") * x),a] is set
{((a ") * x),a} is non empty set
{((a ") * x)} is non empty set
{{((a ") * x),a},{((a ") * x)}} is non empty set
the multF of G . [((a ") * x),a] is set
id the carrier of G is Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one non empty V14( the carrier of G) quasi_total Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is set
x is Element of the carrier of G
f1 . x is Element of the carrier of G
(id the carrier of G) . x is Element of the carrier of G