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 )