set M = multLoopStr(# (bool H₃(G)),(H₁(G) .:^2),{(the_unity_wrt H₁(G))} #);
H₁(G) is having_a_unity by MONOID_0:def 10;
then A1: {(the_unity_wrt H₁(G))} is_a_unity_wrt H₁(G) .:^2 by Th53;
( 1. multLoopStr(# (bool H₃(G)),(H₁(G) .:^2),{(the_unity_wrt H₁(G))} #) = {(the_unity_wrt H₁(G))} & bool G = multLoopStr(# (bool H₃(G)),(H₁(G) .:^2),{(the_unity_wrt H₁(G))} #) ) by Def9;
hence bool G is non empty strict well-unital multLoopStr by A1, MONOID_0:def 21; :: thesis: verum