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₃(G)),(H₁(G) .:^2),{(the_unity_wrt H₁(G))} #) or bool G = multMagma(# (bool the carrier of G),(H₁(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