theorem
Th20
:
:: MONOID_1:20
for
X
being
set
for
G
being non
empty
multMagma
for
f
,
g
being
Element
of
(
.:
(
G
,
X
)
)
st ( for
x
being
object
st
x
in
X
holds
f
.
x
=
g
.
x
) holds
f
=
g