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