set M = multLoopStr(# H1(G),H2(G),(the_unity_wrt H2(G)) #);
multMagma(# the carrier of multLoopStr(# H1(G),H2(G),(the_unity_wrt H2(G)) #), the multF of multLoopStr(# H1(G),H2(G),(the_unity_wrt H2(G)) #) #) = multMagma(# the carrier of G, the multF of G #) ;
then reconsider M = multLoopStr(# H1(G),H2(G),(the_unity_wrt H2(G)) #) as MonoidalExtension of G by Def22;
take M ; :: thesis: ( M is well-unital & M is strict )
thus H3(M) is_a_unity_wrt H2(M) by Th4; :: according to MONOID_0:def 21 :: thesis: M is strict
thus M is strict ; :: thesis: verum