theorem
:: MONOID_1:42
for
A
being non
empty
set
for
p
being
FinSequence
of
A
holds
|.
p
.|
is
Element
of
(
finite-MultiSet_over
A
)