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 )