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

1 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
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
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in carr f & b2 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
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in K102( the carrier of G,f1) & b2 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

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
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in carr f & b2 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
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in K102( the carrier of G,a) & b2 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
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in K102( the carrier of G,(a ")) & b2 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
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in (a ") * f & b2 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
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in K102( the carrier of G,(a ")) & b2 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
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in K102( the carrier of G,((a ") * a)) & b2 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
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in K102( the carrier of G,(1_ G)) & b2 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
{ (b1 |^ b2) where b1, b2 is Element of the carrier of G : ( b1 in carr f & b2 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
{ (b1 * b2) where b1, b2 is Element of the carrier of G : ( b1 in (a ") * (carr f) & b2 in K102( the carrier of G,a) ) } is set

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

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
{ b1 where b1 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 b2 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
( b1 = b2 & b2 is one-to-one & b2 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

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

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

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:]

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

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)

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:]

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)

[: 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:]

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:]

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

f1 . (a,x) is Relation-like Function-like 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

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

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

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

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

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)

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

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
{ b1 where b1 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 b2 being Element of the carrier of G st
for b3 being Element of the carrier of G holds b1 . b3 = b3 |^ b2
}
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

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

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