let G be non empty unital multMagma ; :: thesis: 1. (bool G) = {(the_unity_wrt the multF of G)}
bool G = multLoopStr(# (bool H₃(G)),(H₁(G) .:^2),{(the_unity_wrt H₁(G))} #) by Def9;
hence 1. (bool G) = {(the_unity_wrt the multF of G)} ; :: thesis: verum