theorem
Th17
:
:: MONOID_1:17
for
X
being
set
for
G
being non
empty
multMagma
holds
( the
carrier
of
(
.:
(
G
,
X
)
)
=
Funcs
(
X
, the
carrier
of
G
) & the
multF
of
(
.:
(
G
,
X
)
)
=
( the
multF
of
G
, the
carrier
of
G
)
.:
X
)