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

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

is non empty trivial finite V34() set
G is 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

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

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

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

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

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)

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

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

the carrier of g1 is set

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

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

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

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

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)

G is set

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

G is set

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)

[#] (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
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)

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)

G is V27() set

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

G is V27() set
Seg G is Element of K10(K100())

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

the carrier of () 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))

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 Element of K10(([#] (([#] ( the carrier of (), the carrier of ())), the carrier of ())))
[#] ( the carrier of (), the carrier of ()) is set
[#] (([#] ( the carrier of (), the carrier of ())), the carrier of ()) is set
K10(([#] (([#] ( the carrier of (), the carrier of ())), the carrier of ()))) is set
the multF of () . (f,g1) is set
G is finite set

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

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

[#] (,) 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)))

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

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)

g2 * (x * g1) is Relation-like Function-like set
[#] (G,G) is set
K10(([#] (G,G))) is set

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)

(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

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

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

x * (g1 * 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))))

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
[#] (f,G) is set
K10(([#] (f,G))) is 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

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

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

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)

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

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

the carrier of G is non empty set

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)

the carrier of G is non empty set

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

the carrier of G is non empty set

(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