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
{ b1 where b1 is Relation-like G -defined G -valued Function-like one-to-one V17(G) quasi_total onto bijective Element of K10(([#] (G,G))) : verum } is set
G is set
(G) is set
[#] (G,G) is set
K10(([#] (G,G))) is set
{ b1 where b1 is Relation-like G -defined G -valued Function-like one-to-one V17(G) quasi_total onto bijective Element of K10(([#] (G,G))) : verum } is set
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
{ b1 where b1 is Relation-like G -defined G -valued Function-like one-to-one V17(G) quasi_total onto bijective Element of K10(([#] (G,G))) : verum } is set
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
{ b1 where b1 is Relation-like Seg G -defined Seg G -valued Function-like one-to-one V17( Seg G) quasi_total onto bijective Element of K10(([#] ((Seg G),(Seg G)))) : verum } is set
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
{ b1 where b1 is Relation-like G -defined G -valued Function-like one-to-one V17(G) quasi_total onto bijective Element of K10(([#] (G,G))) : verum } is set
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
{ b1 where b1 is Relation-like G -defined G -valued Function-like one-to-one V17(G) quasi_total onto bijective Element of K10(([#] (G,G))) : verum } is set
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
{ b1 where b1 is Relation-like {} -defined {} -valued Function-like one-to-one V17( {} ) quasi_total onto bijective Element of K10(([#] ({},{}))) : verum } is set
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
{ b1 where b1 is Relation-like G -defined G -valued Function-like one-to-one V17(G) quasi_total onto bijective Element of K10(([#] (G,G))) : verum } is set
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
{ b1 where b1 is Relation-like G -defined G -valued Function-like one-to-one V17(G) quasi_total onto bijective Element of K10(([#] (G,G))) : verum } is set
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
{ b1 where b1 is Relation-like G -defined G -valued Function-like one-to-one V17(G) quasi_total onto bijective Element of K10(([#] (G,G))) : verum } is set
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
{ b1 where b1 is Relation-like G -defined G -valued Function-like one-to-one V17(G) quasi_total onto bijective Element of K10(([#] (G,G))) : verum } is set
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
{ b1 where b1 is Relation-like G -defined G -valued Function-like one-to-one V17(G) quasi_total onto bijective Element of K10(([#] (G,G))) : verum } is set
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
{ b1 where b1 is Relation-like Seg G -defined Seg G -valued Function-like one-to-one V17( Seg G) quasi_total onto bijective Element of K10(([#] ((Seg G),(Seg G)))) : verum } is set
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
{ b1 where b1 is Relation-like G -defined G -valued Function-like one-to-one V17(G) quasi_total onto bijective Element of K10(([#] (G,G))) : verum } is set
({}) 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
{ b1 where b1 is Relation-like f -defined f -valued Function-like one-to-one V17(f) quasi_total onto bijective Element of K10(([#] (f,f))) : verum } is set
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
{ b1 where b1 is Relation-like G -defined G -valued Function-like one-to-one V17(G) quasi_total onto bijective Element of K10(([#] (G,G))) : verum } is set
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
{ b1 where b1 is 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))) : verum } is set
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))