theorem
:: MONOID_1:36
for
A
being non
empty
set
for
a
being
Element
of
A
holds
|.
(
<*>
A
)
.|
.
a
=
0