theorem
:: MONOID_1:18
for
x
,
X
being
set
for
G
being non
empty
multMagma
holds
(
x
is
Element
of
(
.:
(
G
,
X
)
)
iff
x
is
Function
of
X
, the
carrier
of
G
)