theorem
Th19
:
:: MONOID_1:19
for
X
being
set
for
G
being non
empty
multMagma
for
f
being
Element
of
(
.:
(
G
,
X
)
)
holds
(
dom
f
=
X
&
rng
f
c=
the
carrier
of
G
)