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

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

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

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

(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

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

(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

(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

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

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

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

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

( b

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

for b

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