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

H_{1}(G) is having_a_unity
by MONOID_0:def 10;

then A1: {(the_unity_wrt H_{1}(G))} is_a_unity_wrt H_{1}(G) .:^2
by Th53;

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

hence bool G is non empty strict well-unital multLoopStr by A1, MONOID_0:def 21; :: thesis: verum

H

then A1: {(the_unity_wrt H

( 1. multLoopStr(# (bool H

hence bool G is non empty strict well-unital multLoopStr by A1, MONOID_0:def 21; :: thesis: verum