theorem
Th40
:
:: MONOID_1:40
for
A
being non
empty
set
for
p
,
q
being
FinSequence
of
A
holds
|.
(
p
^
q
)
.|
=
|.
p
.|
[*]
|.
q
.|