let G be non empty multMagma ; :: thesis: ( the carrier of (bool G) = bool the carrier of G & the multF of (bool G) = the multF of G .:^2 )

( bool G = multLoopStr(# (bool H_{3}(G)),(H_{1}(G) .:^2),{(the_unity_wrt H_{1}(G))} #) or bool G = multMagma(# (bool the carrier of G),(H_{1}(G) .:^2) #) )
by Def9;

hence ( the carrier of (bool G) = bool the carrier of G & the multF of (bool G) = the multF of G .:^2 ) ; :: thesis: verum

( bool G = multLoopStr(# (bool H

hence ( the carrier of (bool G) = bool the carrier of G & the multF of (bool G) = the multF of G .:^2 ) ; :: thesis: verum