:: CAYLEY semantic presentation

K100() is Element of K10(K96())

K96() is set

K10(K96()) is set

K95() is set

K10(K95()) is set

K10(K100()) is set

1 is non empty set

2 is non empty set

K97() is set

K98() is set

K99() is set

[#] (K96(),K96()) is set

K10(([#] (K96(),K96()))) is set

K408() is non empty strict multMagma

the carrier of K408() is non empty set

<REAL,+> is non empty strict unital Group-like associative commutative left-invertible right-invertible invertible left-cancelable right-cancelable V206() multMagma

K414() is non empty strict associative commutative left-cancelable right-cancelable V206() SubStr of <REAL,+>

<NAT,+> is non empty strict unital associative commutative left-cancelable right-cancelable V206() uniquely-decomposable SubStr of K414()

<REAL,*> is non empty strict unital associative commutative multMagma

<NAT,*> is non empty strict unital associative commutative uniquely-decomposable SubStr of <REAL,*>

K478() is set

[#] (1,1) is set

K10(([#] (1,1))) is set

[#] (([#] (1,1)),1) is set

K10(([#] (([#] (1,1)),1))) is set

{} is empty trivial Function-like functional finite V34() set

the empty trivial Function-like functional finite V34() set is empty trivial Function-like functional finite V34() set

{{}} is non empty trivial finite V34() set

G is set

{} (G,{}) is empty trivial Relation-like G -defined {} -valued Function-like one-to-one constant functional finite finite-yielding V34() Element of K10(([#] (G,{})))

[#] (G,{}) is empty trivial Function-like functional finite V34() set

K10(([#] (G,{}))) is finite V34() set

rng ({} (G,{})) is trivial functional finite V34() Element of K10({})

K10({}) is finite V34() set

G is set

f is set

g1 is V27() set

Seg g1 is Element of K10(K100())

[#] ((Seg g1),(Seg g1)) is set

K10(([#] ((Seg g1),(Seg g1)))) is set

G is set

[#] (G,G) is set

K10(([#] (G,G))) is set

{ b

G is set

(G) is set

[#] (G,G) is set

K10(([#] (G,G))) is set

{ b

f is set

g1 is Relation-like G -defined G -valued Function-like one-to-one V17(G) quasi_total onto bijective Element of K10(([#] (G,G)))

G is set

(G) is set

[#] (G,G) is set

K10(([#] (G,G))) is set

{ b

Funcs (G,G) is non empty functional set

f is set

G is V27() set

Seg G is Element of K10(K100())

((Seg G)) is set

[#] ((Seg G),(Seg G)) is set

K10(([#] ((Seg G),(Seg G)))) is set

{ b

Permutations G is non empty functional permutational set

f is set

f is set

G is set

(G) is set

[#] (G,G) is set

K10(([#] (G,G))) is set

{ b

the Relation-like G -defined G -valued Function-like one-to-one V17(G) quasi_total onto bijective Element of K10(([#] (G,G))) is Relation-like G -defined G -valued Function-like one-to-one V17(G) quasi_total onto bijective Element of K10(([#] (G,G)))

f is set

G is finite set

(G) is non empty functional set

[#] (G,G) is finite set

K10(([#] (G,G))) is finite V34() set

{ b

Funcs (G,G) is non empty functional finite set

({}) is non empty functional finite set

[#] ({},{}) is empty trivial Function-like functional finite V34() set

K10(([#] ({},{}))) is finite V34() set

{ b

f is set

f is set

{} ({},{}) is empty trivial Relation-like {} -defined {} -valued Function-like one-to-one constant functional V17( {} ) quasi_total onto bijective finite finite-yielding V34() Element of K10(([#] ({},{})))

G is set

(G) is non empty functional set

[#] (G,G) is set

K10(([#] (G,G))) is set

{ b

g1 is Relation-like Function-like Element of (G)

g2 is Relation-like Function-like Element of (G)

g1 * g2 is Relation-like Function-like set

g1 is Relation-like G -defined G -valued Function-like one-to-one V17(G) quasi_total onto bijective Element of K10(([#] (G,G)))

g2 is Relation-like G -defined G -valued Function-like one-to-one V17(G) quasi_total onto bijective Element of K10(([#] (G,G)))

g2 * g1 is Relation-like G -defined G -valued Function-like one-to-one V17(G) quasi_total onto bijective Element of K10(([#] (G,G)))

[#] ((G),(G)) is set

[#] (([#] ((G),(G))),(G)) is set

K10(([#] (([#] ((G),(G))),(G)))) is set

g1 is Relation-like [#] ((G),(G)) -defined (G) -valued Function-like V17( [#] ((G),(G))) quasi_total Element of K10(([#] (([#] ((G),(G))),(G))))

multMagma(# (G),g1 #) is strict multMagma

the carrier of multMagma(# (G),g1 #) is set

g1 is Element of the carrier of multMagma(# (G),g1 #)

g1 is strict constituted-Functions multMagma

the carrier of g1 is set

g2 is Relation-like Function-like Element of the carrier of g1

x is Relation-like Function-like Element of the carrier of g1

g2 * x is Relation-like Function-like Element of the carrier of g1

the multF of g1 is Relation-like [#] ( the carrier of g1, the carrier of g1) -defined the carrier of g1 -valued Function-like quasi_total Element of K10(([#] (([#] ( the carrier of g1, the carrier of g1)), the carrier of g1)))

[#] ( the carrier of g1, the carrier of g1) is set

[#] (([#] ( the carrier of g1, the carrier of g1)), the carrier of g1) is set

K10(([#] (([#] ( the carrier of g1, the carrier of g1)), the carrier of g1))) is set

the multF of g1 . (g2,x) is Relation-like Function-like Element of the carrier of g1

g2 * x is Relation-like Function-like set

g1 is strict constituted-Functions multMagma

the carrier of g1 is set

g2 is strict constituted-Functions multMagma

the carrier of g2 is set

g1 is Relation-like Function-like Element of the carrier of g1

g2 is Relation-like Function-like Element of the carrier of g1

the multF of g1 is Relation-like [#] ( the carrier of g1, the carrier of g1) -defined the carrier of g1 -valued Function-like quasi_total Element of K10(([#] (([#] ( the carrier of g1, the carrier of g1)), the carrier of g1)))

[#] ( the carrier of g1, the carrier of g1) is set

[#] (([#] ( the carrier of g1, the carrier of g1)), the carrier of g1) is set

K10(([#] (([#] ( the carrier of g1, the carrier of g1)), the carrier of g1))) is set

the multF of g1 . (g1,g2) is Relation-like Function-like Element of the carrier of g1

g1 * g2 is Relation-like Function-like Element of the carrier of g1

g1 * g2 is Relation-like Function-like set

x is Relation-like Function-like Element of the carrier of g2

y is Relation-like Function-like Element of the carrier of g2

x * y is Relation-like Function-like Element of the carrier of g2

the multF of g2 is Relation-like [#] ( the carrier of g2, the carrier of g2) -defined the carrier of g2 -valued Function-like quasi_total Element of K10(([#] (([#] ( the carrier of g2, the carrier of g2)), the carrier of g2)))

[#] ( the carrier of g2, the carrier of g2) is set

[#] (([#] ( the carrier of g2, the carrier of g2)), the carrier of g2) is set

K10(([#] (([#] ( the carrier of g2, the carrier of g2)), the carrier of g2))) is set

the multF of g2 . (x,y) is Relation-like Function-like Element of the carrier of g2

the multF of g2 . (g1,g2) is set

G is set

(G) is strict constituted-Functions multMagma

the carrier of (G) is set

[#] (G,G) is set

K10(([#] (G,G))) is set

f is Relation-like Function-like Element of the carrier of (G)

(G) is non empty functional set

{ b

G is set

(G) is strict constituted-Functions multMagma

the carrier of (G) is set

(G) is non empty functional set

[#] (G,G) is set

K10(([#] (G,G))) is set

{ b

f is Relation-like Function-like Element of the carrier of (G)

g1 is Relation-like Function-like Element of the carrier of (G)

f * g1 is Relation-like Function-like 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 quasi_total Element of K10(([#] (([#] ( 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

K10(([#] (([#] ( the carrier of (G), the carrier of (G))), the carrier of (G)))) is set

the multF of (G) . (f,g1) is Relation-like Function-like Element of the carrier of (G)

g2 is Relation-like Function-like Element of the carrier of (G)

(f * g1) * g2 is Relation-like Function-like Element of the carrier of (G)

the multF of (G) . ((f * g1),g2) is Relation-like Function-like Element of the carrier of (G)

g1 * g2 is Relation-like Function-like Element of the carrier of (G)

the multF of (G) . (g1,g2) is Relation-like Function-like Element of the carrier of (G)

f * (g1 * g2) is Relation-like Function-like Element of the carrier of (G)

the multF of (G) . (f,(g1 * g2)) is Relation-like Function-like Element of the carrier of (G)

(f * g1) * g2 is Relation-like Function-like set

f * g1 is Relation-like Function-like set

(f * g1) * g2 is Relation-like Function-like set

g1 * g2 is Relation-like Function-like set

f * (g1 * g2) is Relation-like Function-like set

f * (g1 * g2) is Relation-like Function-like set

id G is Relation-like G -defined G -valued Function-like one-to-one V17(G) quasi_total onto bijective V116() V118() V119() V123() Element of K10(([#] (G,G)))

g1 is Relation-like Function-like Element of the carrier of (G)

g2 is Relation-like Function-like Element of the carrier of (G)

g2 * g1 is Relation-like Function-like 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 quasi_total Element of K10(([#] (([#] ( 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

K10(([#] (([#] ( the carrier of (G), the carrier of (G))), the carrier of (G)))) is set

the multF of (G) . (g2,g1) is Relation-like Function-like Element of the carrier of (G)

g1 * g2 is Relation-like Function-like Element of the carrier of (G)

the multF of (G) . (g1,g2) is Relation-like Function-like Element of the carrier of (G)

g1 is Relation-like G -defined G -valued Function-like one-to-one V17(G) quasi_total onto bijective Element of K10(([#] (G,G)))

g1 * g1 is Relation-like Function-like set

g1 * g1 is Relation-like Function-like set

g1 " is Relation-like G -defined G -valued Function-like one-to-one V17(G) quasi_total onto bijective Element of K10(([#] (G,G)))

g2 is Relation-like Function-like Element of the carrier of (G)

g2 * g2 is Relation-like Function-like Element of the carrier of (G)

the multF of (G) . (g2,g2) is Relation-like Function-like Element of the carrier of (G)

g2 * g2 is Relation-like Function-like Element of the carrier of (G)

the multF of (G) . (g2,g2) is Relation-like Function-like Element of the carrier of (G)

g2 * g2 is Relation-like Function-like set

g2 * g2 is Relation-like Function-like set

G is set

(G) is non empty strict unital Group-like associative constituted-Functions left-invertible right-invertible invertible left-cancelable right-cancelable V206() multMagma

1_ (G) is Relation-like Function-like Element of the carrier of (G)

the carrier of (G) is non empty set

id G is Relation-like G -defined G -valued Function-like one-to-one V17(G) quasi_total onto bijective V116() V118() V119() V123() Element of K10(([#] (G,G)))

[#] (G,G) is set

K10(([#] (G,G))) is set

(G) is non empty functional set

{ b

g2 is Relation-like Function-like Element of the carrier of (G)

g1 is Relation-like Function-like Element of the carrier of (G)

g2 * g1 is Relation-like Function-like 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 V17( [#] ( the carrier of (G), the carrier of (G))) quasi_total Element of K10(([#] (([#] ( 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

K10(([#] (([#] ( the carrier of (G), the carrier of (G))), the carrier of (G)))) is set

the multF of (G) . (g2,g1) is Relation-like Function-like Element of the carrier of (G)

g1 is Relation-like G -defined G -valued Function-like one-to-one V17(G) quasi_total onto bijective Element of K10(([#] (G,G)))

g1 * g1 is Relation-like Function-like set

g1 * g2 is Relation-like Function-like Element of the carrier of (G)

the multF of (G) . (g1,g2) is Relation-like Function-like Element of the carrier of (G)

g1 * g1 is Relation-like Function-like set

G is set

(G) is non empty strict unital Group-like associative constituted-Functions left-invertible right-invertible invertible left-cancelable right-cancelable V206() multMagma

the carrier of (G) is non empty set

f is Relation-like Function-like Element of the carrier of (G)

f " is Relation-like Function-like Element of the carrier of (G)

f " is Relation-like Function-like set

[#] (G,G) is set

K10(([#] (G,G))) is set

g1 is Relation-like G -defined G -valued Function-like one-to-one V17(G) quasi_total onto bijective Element of K10(([#] (G,G)))

g1 " is Relation-like G -defined G -valued Function-like one-to-one V17(G) quasi_total onto bijective Element of K10(([#] (G,G)))

(G) is non empty functional set

{ b

1_ (G) is Relation-like Function-like Element of the carrier of (G)

id G is Relation-like G -defined G -valued Function-like one-to-one V17(G) quasi_total onto bijective V116() V118() V119() V123() Element of K10(([#] (G,G)))

g2 is Relation-like Function-like Element of the carrier of (G)

f * g2 is Relation-like Function-like 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 V17( [#] ( the carrier of (G), the carrier of (G))) quasi_total Element of K10(([#] (([#] ( 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

K10(([#] (([#] ( the carrier of (G), the carrier of (G))), the carrier of (G)))) is set

the multF of (G) . (f,g2) is Relation-like Function-like Element of the carrier of (G)

f * g2 is Relation-like Function-like set

g2 * f is Relation-like Function-like Element of the carrier of (G)

the multF of (G) . (g2,f) is Relation-like Function-like Element of the carrier of (G)

g2 * f is Relation-like Function-like set

G is V27() set

Group_of_Perm G is non empty strict unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V206() multMagma

f is set

the carrier of (Group_of_Perm G) is non empty set

Permutations G is non empty functional permutational set

G is V27() set

Seg G is Element of K10(K100())

((Seg G)) is non empty strict unital Group-like associative constituted-Functions left-invertible right-invertible invertible left-cancelable right-cancelable V206() multMagma

Group_of_Perm G is non empty strict unital Group-like associative constituted-Functions left-invertible right-invertible invertible left-cancelable right-cancelable V206() multMagma

the carrier of ((Seg G)) is non empty set

((Seg G)) is non empty functional set

[#] ((Seg G),(Seg G)) is set

K10(([#] ((Seg G),(Seg G)))) is set

{ b

Permutations G is non empty functional permutational set

the carrier of (Group_of_Perm G) is non empty set

f is Relation-like Function-like Element of the carrier of ((Seg G))

g1 is Relation-like Function-like Element of the carrier of ((Seg G))

f * g1 is Relation-like Function-like Element of the carrier of ((Seg G))

the multF of ((Seg G)) is Relation-like [#] ( the carrier of ((Seg G)), the carrier of ((Seg G))) -defined the carrier of ((Seg G)) -valued Function-like V17( [#] ( the carrier of ((Seg G)), the carrier of ((Seg G)))) quasi_total Element of K10(([#] (([#] ( the carrier of ((Seg G)), the carrier of ((Seg G)))), the carrier of ((Seg G)))))

[#] ( the carrier of ((Seg G)), the carrier of ((Seg G))) is set

[#] (([#] ( the carrier of ((Seg G)), the carrier of ((Seg G)))), the carrier of ((Seg G))) is set

K10(([#] (([#] ( the carrier of ((Seg G)), the carrier of ((Seg G)))), the carrier of ((Seg G))))) is set

the multF of ((Seg G)) . (f,g1) is Relation-like Function-like Element of the carrier of ((Seg G))

f * g1 is Relation-like Function-like set

the multF of (Group_of_Perm G) is Relation-like [#] ( the carrier of (Group_of_Perm G), the carrier of (Group_of_Perm G)) -defined the carrier of (Group_of_Perm G) -valued Function-like V17( [#] ( the carrier of (Group_of_Perm G), the carrier of (Group_of_Perm G))) quasi_total Element of K10(([#] (([#] ( the carrier of (Group_of_Perm G), the carrier of (Group_of_Perm G))), the carrier of (Group_of_Perm G))))

[#] ( the carrier of (Group_of_Perm G), the carrier of (Group_of_Perm G)) is set

[#] (([#] ( the carrier of (Group_of_Perm G), the carrier of (Group_of_Perm G))), the carrier of (Group_of_Perm G)) is set

K10(([#] (([#] ( the carrier of (Group_of_Perm G), the carrier of (Group_of_Perm G))), the carrier of (Group_of_Perm G)))) is set

the multF of (Group_of_Perm G) . (f,g1) is set

G is finite set

(G) is non empty strict unital Group-like associative constituted-Functions left-invertible right-invertible invertible left-cancelable right-cancelable V206() multMagma

the carrier of (G) is non empty set

(G) is non empty functional finite set

[#] (G,G) is finite set

K10(([#] (G,G))) is finite V34() set

{ b

({}) is non empty finite strict unital Group-like associative constituted-Functions left-invertible right-invertible invertible left-cancelable right-cancelable V206() multMagma

Trivial-multMagma is multMagma

op2 is Relation-like [#] (1,1) -defined 1 -valued Function-like V17( [#] (1,1)) quasi_total Element of K10(([#] (([#] (1,1)),1)))

K447({},{},{}) is Relation-like [#] ({{}},{{}}) -defined {{}} -valued Function-like V17( [#] ({{}},{{}})) quasi_total finite Element of K10(([#] (([#] ({{}},{{}})),{{}})))

[#] ({{}},{{}}) is finite set

[#] (([#] ({{}},{{}})),{{}}) is finite set

K10(([#] (([#] ({{}},{{}})),{{}}))) is finite V34() set

multMagma(# 1,op2 #) is strict multMagma

the carrier of ({}) is non empty finite set

f is Element of 1

g1 is Element of 1

the multF of ({}) is Relation-like [#] ( the carrier of ({}), the carrier of ({})) -defined the carrier of ({}) -valued Function-like V17( [#] ( the carrier of ({}), the carrier of ({}))) quasi_total finite Element of K10(([#] (([#] ( the carrier of ({}), the carrier of ({}))), the carrier of ({}))))

[#] ( the carrier of ({}), the carrier of ({})) is finite set

[#] (([#] ( the carrier of ({}), the carrier of ({}))), the carrier of ({})) is finite set

K10(([#] (([#] ( the carrier of ({}), the carrier of ({}))), the carrier of ({})))) is finite V34() set

the multF of ({}) . (f,g1) is set

g2 is Relation-like Function-like Element of the carrier of ({})

g1 is Relation-like Function-like Element of the carrier of ({})

g2 * g1 is Relation-like Function-like Element of the carrier of ({})

the multF of ({}) . (g2,g1) is Relation-like Function-like Element of the carrier of ({})

op2 . (f,g1) is Element of 1

G is set

f is set

[#] (G,f) is set

K10(([#] (G,f))) is set

g1 is Relation-like G -defined f -valued Function-like quasi_total Element of K10(([#] (G,f)))

(G) is non empty strict unital Group-like associative constituted-Functions left-invertible right-invertible invertible left-cancelable right-cancelable V206() multMagma

(f) is non empty strict unital Group-like associative constituted-Functions left-invertible right-invertible invertible left-cancelable right-cancelable V206() multMagma

the carrier of (G) is non empty set

the carrier of (f) is non empty set

[#] ( the carrier of (G), the carrier of (f)) is set

K10(([#] ( the carrier of (G), the carrier of (f)))) is set

g1 " is Relation-like Function-like set

dom g1 is Element of K10(G)

K10(G) is set

rng g1 is Element of K10(f)

K10(f) is set

[#] (f,G) is set

K10(([#] (f,G))) is set

g2 is Relation-like f -defined G -valued Function-like quasi_total Element of K10(([#] (f,G)))

rng g2 is Element of K10(G)

x is Relation-like Function-like Element of the carrier of (G)

x * g1 is Relation-like Function-like set

g2 * (x * g1) is Relation-like Function-like set

[#] (G,G) is set

K10(([#] (G,G))) is set

y is Relation-like G -defined G -valued Function-like one-to-one V17(G) quasi_total onto bijective Element of K10(([#] (G,G)))

g1 * y is Relation-like G -defined f -valued Function-like quasi_total Element of K10(([#] (G,f)))

(g1 * y) * g2 is Relation-like f -defined f -valued Function-like Element of K10(([#] (f,f)))

[#] (f,f) is set

K10(([#] (f,f))) is set

rng y is Element of K10(G)

rng (g1 * y) is Element of K10(f)

rng ((g1 * y) * g2) is Element of K10(f)

(f) is non empty functional set

{ b

p1 is Relation-like Function-like Element of the carrier of (f)

x is non empty Relation-like the carrier of (G) -defined the carrier of (f) -valued Function-like V17( the carrier of (G)) quasi_total Element of K10(([#] ( the carrier of (G), the carrier of (f))))

g2 is non empty Relation-like the carrier of (G) -defined the carrier of (f) -valued Function-like V17( the carrier of (G)) quasi_total Element of K10(([#] ( the carrier of (G), the carrier of (f))))

x is non empty Relation-like the carrier of (G) -defined the carrier of (f) -valued Function-like V17( the carrier of (G)) quasi_total Element of K10(([#] ( the carrier of (G), the carrier of (f))))

y is Relation-like Function-like Element of the carrier of (G)

g2 . y is set

x . y is set

g2 . y is Relation-like Function-like Element of the carrier of (f)

y * g1 is Relation-like Function-like set

(g1 ") * (y * g1) is Relation-like Function-like set

x . y is Relation-like Function-like Element of the carrier of (f)

G is non empty set

f is non empty set

[#] (G,f) is set

K10(([#] (G,f))) is set

(G) is non empty strict unital Group-like associative constituted-Functions left-invertible right-invertible invertible left-cancelable right-cancelable V206() multMagma

(f) is non empty strict unital Group-like associative constituted-Functions left-invertible right-invertible invertible left-cancelable right-cancelable V206() multMagma

g1 is non empty Relation-like G -defined f -valued Function-like V17(G) quasi_total Element of K10(([#] (G,f)))

(G,f,g1) is non empty Relation-like the carrier of (G) -defined the carrier of (f) -valued Function-like V17( the carrier of (G)) quasi_total Element of K10(([#] ( the carrier of (G), the carrier of (f))))

the carrier of (G) is non empty set

the carrier of (f) is non empty set

[#] ( the carrier of (G), the carrier of (f)) is set

K10(([#] ( the carrier of (G), the carrier of (f)))) is set

rng g1 is Element of K10(f)

K10(f) is set

g1 is Relation-like Function-like Element of the carrier of (G)

g2 is Relation-like Function-like Element of the carrier of (G)

g1 * g2 is Relation-like Function-like 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 V17( [#] ( the carrier of (G), the carrier of (G))) quasi_total Element of K10(([#] (([#] ( 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

K10(([#] (([#] ( the carrier of (G), the carrier of (G))), the carrier of (G)))) is set

the multF of (G) . (g1,g2) is Relation-like Function-like Element of the carrier of (G)

(G,f,g1) . (g1 * g2) is Relation-like Function-like Element of the carrier of (f)

(G,f,g1) . g1 is Relation-like Function-like Element of the carrier of (f)

(G,f,g1) . g2 is Relation-like Function-like Element of the carrier of (f)

((G,f,g1) . g1) * ((G,f,g1) . g2) is Relation-like Function-like Element of the carrier of (f)

the multF of (f) is Relation-like [#] ( the carrier of (f), the carrier of (f)) -defined the carrier of (f) -valued Function-like V17( [#] ( the carrier of (f), the carrier of (f))) quasi_total Element of K10(([#] (([#] ( the carrier of (f), the carrier of (f))), the carrier of (f))))

[#] ( the carrier of (f), the carrier of (f)) is set

[#] (([#] ( the carrier of (f), the carrier of (f))), the carrier of (f)) is set

K10(([#] (([#] ( the carrier of (f), the carrier of (f))), the carrier of (f)))) is set

the multF of (f) . (((G,f,g1) . g1),((G,f,g1) . g2)) is Relation-like Function-like Element of the carrier of (f)

[#] (f,G) is set

K10(([#] (f,G))) is set

g1 " is Relation-like Function-like set

id G is non empty Relation-like G -defined G -valued Function-like one-to-one V17(G) quasi_total onto bijective V116() V118() V119() V123() Element of K10(([#] (G,G)))

[#] (G,G) is set

K10(([#] (G,G))) is set

x is non empty Relation-like f -defined G -valued Function-like V17(f) quasi_total Element of K10(([#] (f,G)))

x * g1 is non empty Relation-like G -defined G -valued Function-like V17(G) quasi_total Element of K10(([#] (G,G)))

g1 * g1 is Relation-like Function-like set

x * (g1 * g1) is Relation-like Function-like set

g2 * g1 is Relation-like Function-like set

x * (g2 * g1) is Relation-like Function-like set

(g1 * g2) * g1 is Relation-like Function-like set

x * ((g1 * g2) * g1) is Relation-like Function-like set

y is non empty Relation-like G -defined G -valued Function-like one-to-one V17(G) quasi_total onto bijective Element of K10(([#] (G,G)))

g is non empty Relation-like G -defined G -valued Function-like one-to-one V17(G) quasi_total onto bijective Element of K10(([#] (G,G)))

g * y is non empty Relation-like G -defined G -valued Function-like one-to-one V17(G) quasi_total onto bijective Element of K10(([#] (G,G)))

g1 * (g * y) is non empty Relation-like G -defined f -valued Function-like V17(G) quasi_total Element of K10(([#] (G,f)))

(g1 * (g * y)) * x is non empty Relation-like f -defined f -valued Function-like V17(f) quasi_total Element of K10(([#] (f,f)))

[#] (f,f) is set

K10(([#] (f,f))) is set

g * (id G) is non empty Relation-like G -defined G -valued Function-like one-to-one V17(G) quasi_total onto bijective Element of K10(([#] (G,G)))

(g * (id G)) * y is non empty Relation-like G -defined G -valued Function-like one-to-one V17(G) quasi_total onto bijective Element of K10(([#] (G,G)))

g1 * ((g * (id G)) * y) is non empty Relation-like G -defined f -valued Function-like V17(G) quasi_total Element of K10(([#] (G,f)))

(g1 * ((g * (id G)) * y)) * x is non empty Relation-like f -defined f -valued Function-like V17(f) quasi_total Element of K10(([#] (f,f)))

g * x is non empty Relation-like f -defined G -valued Function-like V17(f) quasi_total Element of K10(([#] (f,G)))

(g * x) * g1 is non empty Relation-like G -defined G -valued Function-like V17(G) quasi_total Element of K10(([#] (G,G)))

((g * x) * g1) * y is non empty Relation-like G -defined G -valued Function-like V17(G) quasi_total Element of K10(([#] (G,G)))

g1 * (((g * x) * g1) * y) is non empty Relation-like G -defined f -valued Function-like V17(G) quasi_total Element of K10(([#] (G,f)))

(g1 * (((g * x) * g1) * y)) * x is non empty Relation-like f -defined f -valued Function-like V17(f) quasi_total Element of K10(([#] (f,f)))

g1 * y is non empty Relation-like G -defined f -valued Function-like V17(G) quasi_total Element of K10(([#] (G,f)))

(g * x) * (g1 * y) is non empty Relation-like G -defined G -valued Function-like V17(G) quasi_total Element of K10(([#] (G,G)))

g1 * ((g * x) * (g1 * y)) is non empty Relation-like G -defined f -valued Function-like V17(G) quasi_total Element of K10(([#] (G,f)))

(g1 * ((g * x) * (g1 * y))) * x is non empty Relation-like f -defined f -valued Function-like V17(f) quasi_total Element of K10(([#] (f,f)))

g1 * (g * x) is non empty Relation-like f -defined f -valued Function-like V17(f) quasi_total Element of K10(([#] (f,f)))

(g1 * (g * x)) * (g1 * y) is non empty Relation-like G -defined f -valued Function-like V17(G) quasi_total Element of K10(([#] (G,f)))

((g1 * (g * x)) * (g1 * y)) * x is non empty Relation-like f -defined f -valued Function-like V17(f) quasi_total Element of K10(([#] (f,f)))

(g1 * y) * x is non empty Relation-like f -defined f -valued Function-like V17(f) quasi_total Element of K10(([#] (f,f)))

(g1 * (g * x)) * ((g1 * y) * x) is non empty Relation-like f -defined f -valued Function-like V17(f) quasi_total Element of K10(([#] (f,f)))

g1 * g is non empty Relation-like G -defined f -valued Function-like V17(G) quasi_total Element of K10(([#] (G,f)))

(g1 * g) * x is non empty Relation-like f -defined f -valued Function-like V17(f) quasi_total Element of K10(([#] (f,f)))

((g1 * g) * x) * ((g1 * y) * x) is non empty Relation-like f -defined f -valued Function-like V17(f) quasi_total Element of K10(([#] (f,f)))

G is non empty set

f is non empty set

[#] (G,f) is set

K10(([#] (G,f))) is set

g1 is non empty Relation-like G -defined f -valued Function-like V17(G) quasi_total Element of K10(([#] (G,f)))

(G,f,g1) is non empty Relation-like the carrier of (G) -defined the carrier of (f) -valued Function-like V17( the carrier of (G)) quasi_total Element of K10(([#] ( the carrier of (G), the carrier of (f))))

(G) is non empty strict unital Group-like associative constituted-Functions left-invertible right-invertible invertible left-cancelable right-cancelable V206() multMagma

the carrier of (G) is non empty set

(f) is non empty strict unital Group-like associative constituted-Functions left-invertible right-invertible invertible left-cancelable right-cancelable V206() multMagma

the carrier of (f) is non empty set

[#] ( the carrier of (G), the carrier of (f)) is set

K10(([#] ( the carrier of (G), the carrier of (f)))) is set

rng g1 is Element of K10(f)

K10(f) is set

[#] (f,G) is set

K10(([#] (f,G))) is set

g1 " is Relation-like Function-like set

id G is non empty Relation-like G -defined G -valued Function-like one-to-one V17(G) quasi_total onto bijective V116() V118() V119() V123() Element of K10(([#] (G,G)))

[#] (G,G) is set

K10(([#] (G,G))) is set

g1 is non empty Relation-like f -defined G -valued Function-like V17(f) quasi_total Element of K10(([#] (f,G)))

g1 * g1 is non empty Relation-like G -defined G -valued Function-like V17(G) quasi_total Element of K10(([#] (G,G)))

g2 is set

dom (G,f,g1) is set

x is set

(G,f,g1) . g2 is set

(G,f,g1) . x is set

dom (G,f,g1) is Element of K10( the carrier of (G))

K10( the carrier of (G)) is set

y is Relation-like Function-like Element of the carrier of (G)

g is Relation-like Function-like Element of the carrier of (G)

(G,f,g1) . y is Relation-like Function-like Element of the carrier of (f)

p1 is non empty Relation-like G -defined G -valued Function-like one-to-one V17(G) quasi_total onto bijective Element of K10(([#] (G,G)))

g1 * p1 is non empty Relation-like G -defined f -valued Function-like V17(G) quasi_total Element of K10(([#] (G,f)))

(g1 * p1) * g1 is non empty Relation-like f -defined f -valued Function-like V17(f) quasi_total Element of K10(([#] (f,f)))

[#] (f,f) is set

K10(([#] (f,f))) is set

(G,f,g1) . g is Relation-like Function-like Element of the carrier of (f)

x is non empty Relation-like G -defined G -valued Function-like one-to-one V17(G) quasi_total onto bijective Element of K10(([#] (G,G)))

g1 * x is non empty Relation-like G -defined f -valued Function-like V17(G) quasi_total Element of K10(([#] (G,f)))

(g1 * x) * g1 is non empty Relation-like f -defined f -valued Function-like V17(f) quasi_total Element of K10(([#] (f,f)))

(g1 * p1) * (g1 * g1) is non empty Relation-like G -defined f -valued Function-like V17(G) quasi_total Element of K10(([#] (G,f)))

((g1 * x) * g1) * g1 is non empty Relation-like G -defined f -valued Function-like V17(G) quasi_total Element of K10(([#] (G,f)))

(g1 * x) * (g1 * g1) is non empty Relation-like G -defined f -valued Function-like V17(G) quasi_total Element of K10(([#] (G,f)))

(g1 * x) * (id G) is non empty Relation-like G -defined f -valued Function-like V17(G) quasi_total Element of K10(([#] (G,f)))

g1 * (g1 * p1) is non empty Relation-like G -defined G -valued Function-like V17(G) quasi_total Element of K10(([#] (G,G)))

g1 * (g1 * x) is non empty Relation-like G -defined G -valued Function-like V17(G) quasi_total Element of K10(([#] (G,G)))

(g1 * g1) * p1 is non empty Relation-like G -defined G -valued Function-like V17(G) quasi_total Element of K10(([#] (G,G)))

(g1 * g1) * x is non empty Relation-like G -defined G -valued Function-like V17(G) quasi_total Element of K10(([#] (G,G)))

(id G) * x is non empty Relation-like G -defined G -valued Function-like one-to-one V17(G) quasi_total onto bijective Element of K10(([#] (G,G)))

G is non empty set

f is non empty set

[#] (G,f) is set

K10(([#] (G,f))) is set

(f) is non empty strict unital Group-like associative constituted-Functions left-invertible right-invertible invertible left-cancelable right-cancelable V206() multMagma

the carrier of (f) is non empty set

g1 is non empty Relation-like G -defined f -valued Function-like V17(G) quasi_total Element of K10(([#] (G,f)))

(G,f,g1) is non empty Relation-like the carrier of (G) -defined the carrier of (f) -valued Function-like V17( the carrier of (G)) quasi_total Element of K10(([#] ( the carrier of (G), the carrier of (f))))

(G) is non empty strict unital Group-like associative constituted-Functions left-invertible right-invertible invertible left-cancelable right-cancelable V206() multMagma

the carrier of (G) is non empty set

[#] ( the carrier of (G), the carrier of (f)) is set

K10(([#] ( the carrier of (G), the carrier of (f)))) is set

dom g1 is Element of K10(G)

K10(G) is set

rng (G,f,g1) is Element of K10( the carrier of (f))

K10( the carrier of (f)) is set

x is set

[#] (f,f) is set

K10(([#] (f,f))) is set

y is Relation-like Function-like Element of the carrier of (f)

rng g1 is Element of K10(f)

K10(f) is set

[#] (f,G) is set

K10(([#] (f,G))) is set

g1 " is Relation-like Function-like set

id f is non empty Relation-like f -defined f -valued Function-like one-to-one V17(f) quasi_total onto bijective V116() V118() V119() V123() Element of K10(([#] (f,f)))

p1 is non empty Relation-like f -defined G -valued Function-like V17(f) quasi_total Element of K10(([#] (f,G)))

g1 * p1 is non empty Relation-like f -defined f -valued Function-like V17(f) quasi_total Element of K10(([#] (f,f)))

dom (G,f,g1) is Element of K10( the carrier of (G))

K10( the carrier of (G)) is set

g is non empty Relation-like f -defined f -valued Function-like one-to-one V17(f) quasi_total onto bijective Element of K10(([#] (f,f)))

p1 * g is non empty Relation-like f -defined G -valued Function-like V17(f) quasi_total Element of K10(([#] (f,G)))

(p1 * g) * g1 is non empty Relation-like G -defined G -valued Function-like V17(G) quasi_total Element of K10(([#] (G,G)))

[#] (G,G) is set

K10(([#] (G,G))) is set

rng p1 is Element of K10(G)

rng g is Element of K10(f)

rng (p1 * g) is Element of K10(G)

rng ((p1 * g) * g1) is Element of K10(G)

(G) is non empty functional set

{ b

x is Relation-like Function-like Element of the carrier of (G)

(G,f,g1) . x is Relation-like Function-like Element of the carrier of (f)

x * g1 is Relation-like Function-like set

p1 * (x * g1) is Relation-like Function-like set

g1 * (p1 * g) is non empty Relation-like f -defined f -valued Function-like V17(f) quasi_total Element of K10(([#] (f,f)))

(g1 * (p1 * g)) * g1 is non empty Relation-like G -defined f -valued Function-like V17(G) quasi_total Element of K10(([#] (G,f)))

((g1 * (p1 * g)) * g1) * p1 is non empty Relation-like f -defined f -valued Function-like V17(f) quasi_total Element of K10(([#] (f,f)))

(g1 * (p1 * g)) * (g1 * p1) is non empty Relation-like f -defined f -valued Function-like V17(f) quasi_total Element of K10(([#] (f,f)))

(id f) * g is non empty Relation-like f -defined f -valued Function-like one-to-one V17(f) quasi_total onto bijective Element of K10(([#] (f,f)))

((id f) * g) * (id f) is non empty Relation-like f -defined f -valued Function-like one-to-one V17(f) quasi_total onto bijective Element of K10(([#] (f,f)))

g * (id f) is non empty Relation-like f -defined f -valued Function-like one-to-one V17(f) quasi_total onto bijective Element of K10(([#] (f,f)))

G is set

(G) is non empty strict unital Group-like associative constituted-Functions left-invertible right-invertible invertible left-cancelable right-cancelable V206() multMagma

f is set

(f) is non empty strict unital Group-like associative constituted-Functions left-invertible right-invertible invertible left-cancelable right-cancelable V206() multMagma

g1 is Relation-like Function-like set

dom g1 is set

rng g1 is set

[#] (G,f) is set

K10(([#] (G,f))) is set

g2 is Relation-like G -defined f -valued Function-like quasi_total Element of K10(([#] (G,f)))

the carrier of (G) is non empty set

the carrier of (f) is non empty set

[#] ( the carrier of (G), the carrier of (f)) is set

K10(([#] ( the carrier of (G), the carrier of (f)))) is set

(G,f,g2) is non empty Relation-like the carrier of (G) -defined the carrier of (f) -valued Function-like V17( the carrier of (G)) quasi_total Element of K10(([#] ( the carrier of (G), the carrier of (f))))

g1 is non empty Relation-like the carrier of (G) -defined the carrier of (f) -valued Function-like V17( the carrier of (G)) quasi_total multiplicative Element of K10(([#] ( the carrier of (G), the carrier of (f))))

G is non empty unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V206() multMagma

the carrier of G is non empty set

( the carrier of G) is non empty strict unital Group-like associative constituted-Functions left-invertible right-invertible invertible left-cancelable right-cancelable V206() multMagma

the carrier of ( the carrier of G) is non empty set

[#] ( the carrier of G, the carrier of ( the carrier of G)) is set

K10(([#] ( the carrier of G, the carrier of ( the carrier of G)))) is set

g1 is Element of the carrier of G

* g1 is non empty Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one V17( the carrier of G) quasi_total onto bijective Element of K10(([#] ( the carrier of G, the carrier of G)))

[#] ( the carrier of G, the carrier of G) is set

K10(([#] ( the carrier of G, the carrier of G))) is set

( the carrier of G) is non empty functional set

{ b

g1 is Relation-like Function-like Element of the carrier of ( the carrier of G)

g1 is non empty Relation-like the carrier of G -defined the carrier of ( the carrier of G) -valued Function-like V17( the carrier of G) quasi_total Element of K10(([#] ( the carrier of G, the carrier of ( the carrier of G))))

f is non empty Relation-like the carrier of G -defined the carrier of ( the carrier of G) -valued Function-like V17( the carrier of G) quasi_total Element of K10(([#] ( the carrier of G, the carrier of ( the carrier of G))))

g1 is non empty Relation-like the carrier of G -defined the carrier of ( the carrier of G) -valued Function-like V17( the carrier of G) quasi_total Element of K10(([#] ( the carrier of G, the carrier of ( the carrier of G))))

g2 is Element of the carrier of G

f . g2 is set

g1 . g2 is set

f . g2 is Relation-like Function-like Element of the carrier of ( the carrier of G)

* g2 is non empty Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one V17( the carrier of G) quasi_total onto bijective Element of K10(([#] ( the carrier of G, the carrier of G)))

[#] ( the carrier of G, the carrier of G) is set

K10(([#] ( the carrier of G, the carrier of G))) is set

g1 . g2 is Relation-like Function-like Element of the carrier of ( the carrier of G)

G is non empty unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V206() multMagma

the carrier of G is non empty set

( the carrier of G) is non empty strict unital Group-like associative constituted-Functions left-invertible right-invertible invertible left-cancelable right-cancelable V206() multMagma

(G) is non empty Relation-like the carrier of G -defined the carrier of ( the carrier of G) -valued Function-like V17( the carrier of G) quasi_total Element of K10(([#] ( the carrier of G, the carrier of ( the carrier of G))))

the carrier of ( the carrier of G) is non empty set

[#] ( the carrier of G, the carrier of ( the carrier of G)) is set

K10(([#] ( the carrier of G, the carrier of ( the carrier of G)))) is set

g2 is Element of the carrier of G

g1 is Element of the carrier of G

g2 * g1 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 V17( [#] ( the carrier of G, the carrier of G)) quasi_total Element of K10(([#] (([#] ( 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

K10(([#] (([#] ( the carrier of G, the carrier of G)), the carrier of G))) is set

the multF of G . (g2,g1) is Element of the carrier of G

(G) . (g2 * g1) is Relation-like Function-like Element of the carrier of ( the carrier of G)

(G) . g2 is Relation-like Function-like Element of the carrier of ( the carrier of G)

(G) . g1 is Relation-like Function-like Element of the carrier of ( the carrier of G)

((G) . g2) * ((G) . g1) is Relation-like Function-like Element of the carrier of ( the carrier of G)

the multF of ( the carrier of G) is Relation-like [#] ( the carrier of ( the carrier of G), the carrier of ( the carrier of G)) -defined the carrier of ( the carrier of G) -valued Function-like V17( [#] ( the carrier of ( the carrier of G), the carrier of ( the carrier of G))) quasi_total Element of K10(([#] (([#] ( the carrier of ( the carrier of G), the carrier of ( the carrier of G))), the carrier of ( the carrier of G))))

[#] ( the carrier of ( the carrier of G), the carrier of ( the carrier of G)) is set

[#] (([#] ( the carrier of ( the carrier of G), the carrier of ( the carrier of G))), the carrier of ( the carrier of G)) is set

K10(([#] (([#] ( the carrier of ( the carrier of G), the carrier of ( the carrier of G))), the carrier of ( the carrier of G)))) is set

the multF of ( the carrier of G) . (((G) . g2),((G) . g1)) is Relation-like Function-like Element of the carrier of ( the carrier of G)

K10(([#] ( the carrier of G, the carrier of G))) is set

dom ((G) . (g2 * g1)) is set

dom (((G) . g2) * ((G) . g1)) is set

g2 is set

((G) . (g2 * g1)) . g2 is set

* (g2 * g1) is non empty Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one V17( the carrier of G) quasi_total onto bijective Element of K10(([#] ( the carrier of G, the carrier of G)))

x is Element of the carrier of G

(* (g2 * g1)) . x is Element of the carrier of G

x * (g2 * g1) is Element of the carrier of G

the multF of G . (x,(g2 * g1)) is Element of the carrier of G

x * g2 is Element of the carrier of G

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

(x * g2) * g1 is Element of the carrier of G

the multF of G . ((x * g2),g1) is Element of the carrier of G

* g1 is non empty Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one V17( the carrier of G) quasi_total onto bijective Element of K10(([#] ( the carrier of G, the carrier of G)))

(* g1) . (x * g2) is Element of the carrier of G

* g2 is non empty Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one V17( the carrier of G) quasi_total onto bijective Element of K10(([#] ( the carrier of G, the carrier of G)))

(* g2) . x is Element of the carrier of G

(* g1) . ((* g2) . x) is Element of the carrier of G

(* g1) * (* g2) is non empty Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one V17( the carrier of G) quasi_total onto bijective Element of K10(([#] ( the carrier of G, the carrier of G)))

((* g1) * (* g2)) . x is Element of the carrier of G

(* g2) * ((G) . g1) is Relation-like Function-like set

((* g2) * ((G) . g1)) . x is set

((G) . g2) * ((G) . g1) is Relation-like Function-like set

(((G) . g2) * ((G) . g1)) . g2 is set

(((G) . g2) * ((G) . g1)) . g2 is set

G is non empty unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V206() multMagma

(G) is non empty Relation-like the carrier of G -defined the carrier of ( the carrier of G) -valued Function-like V17( the carrier of G) quasi_total multiplicative Element of K10(([#] ( the carrier of G, the carrier of ( the carrier of G))))

the carrier of G is non empty set

( the carrier of G) is non empty strict unital Group-like associative constituted-Functions left-invertible right-invertible invertible left-cancelable right-cancelable V206() multMagma

the carrier of ( the carrier of G) is non empty set

[#] ( the carrier of G, the carrier of ( the carrier of G)) is set

K10(([#] ( the carrier of G, the carrier of ( the carrier of G)))) is set

g1 is set

dom (G) is set

g2 is set

(G) . g1 is set

(G) . g2 is set

dom (G) is Element of K10( the carrier of G)

K10( the carrier of G) is set

g1 is Element of the carrier of G

(G) . g1 is Relation-like Function-like Element of the carrier of ( the carrier of G)

* g1 is non empty Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one V17( the carrier of G) quasi_total onto bijective Element of K10(([#] ( the carrier of G, the carrier of G)))

[#] ( the carrier of G, the carrier of G) is set

K10(([#] ( the carrier of G, the carrier of G))) is set

g2 is Element of the carrier of G

(G) . g2 is Relation-like Function-like Element of the carrier of ( the carrier of G)

* g2 is non empty Relation-like the carrier of G -defined the carrier of G -valued Function-like one-to-one V17( the carrier of G) quasi_total onto bijective Element of K10(([#] ( the carrier of G, the carrier of G)))

dom (* g1) is Element of K10( the carrier of G)

g1 " is Element of the carrier of G

g2 " is Element of the carrier of G

(* g1) . (g1 ") is Element of the carrier of G

(g1 ") * g1 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 V17( [#] ( the carrier of G, the carrier of G)) quasi_total Element of K10(([#] (([#] ( 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

K10(([#] (([#] ( the carrier of G, the carrier of G)), the carrier of G))) is set

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

1_ G is Element of the carrier of G

(* g2) . (g2 ") is Element of the carrier of G

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

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

G is non empty unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V206() multMagma

the carrier of G is non empty set

( the carrier of G) is non empty strict unital Group-like associative constituted-Functions left-invertible right-invertible invertible left-cancelable right-cancelable V206() multMagma

(G) is non empty Relation-like the carrier of G -defined the carrier of ( the carrier of G) -valued Function-like one-to-one V17( the carrier of G) quasi_total multiplicative Element of K10(([#] ( the carrier of G, the carrier of ( the carrier of G))))

the carrier of ( the carrier of G) is non empty set

[#] ( the carrier of G, the carrier of ( the carrier of G)) is set

K10(([#] ( the carrier of G, the carrier of ( the carrier of G)))) is set

Image (G) is non empty strict unital Group-like associative left-invertible right-invertible invertible left-cancelable right-cancelable V206() M6(( the carrier of G))