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
; ( M is well-unital & M is strict )
thus
H3(M) is_a_unity_wrt H2(M)
by Th4; MONOID_0:def 21 M is strict
thus
M is strict
; verum