let G be non empty unital multMagma ; :: thesis: 1. (bool G) = {(the_unity_wrt the multF of G)}

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

hence 1. (bool G) = {(the_unity_wrt the multF of G)} ; :: thesis: verum

bool G = multLoopStr(# (bool H

hence 1. (bool G) = {(the_unity_wrt the multF of G)} ; :: thesis: verum