theorem
Th55
:
:: MONOID_1:55
for
G
being non
empty
multMagma
holds
( the
carrier
of
(
bool
G
)
=
bool
the
carrier
of
G
& the
multF
of
(
bool
G
)
=
the
multF
of
G
.:^2
)