theorem
:: MONOID_1:1
for
f
,
g
being
Function
for
X
being
set
holds
(
f

X
)
*
g
=
f
*
(
X
`
g
)