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