consider g being Element of G;
take M = multLoopStr(# H₁(G),H₂(G),g #); :: thesis: multMagma(# the carrier of M,the multF of M #) = multMagma(# the carrier of G,the multF of G #)
thus multMagma(# the carrier of M,the multF of M #) = multMagma(# the carrier of G,the multF of G #) ; :: thesis: verum