consider g being Element of G;
set M = multLoopStr(# H₁(G),H₂(G),g #);
multMagma(# the carrier of multLoopStr(# H₁(G),H₂(G),g #),the multF of multLoopStr(# H₁(G),H₂(G),g #) #) = multMagma(# the carrier of G,the multF of G #) ;
then multLoopStr(# H₁(G),H₂(G),g #) is MonoidalExtension of G by Def22;
hence ex b₁ being MonoidalExtension of G st b₁ is strict ; :: thesis: verum