set g = the Element of G;
take multLoopStr(# H₁(G),H₂(G), the Element of G #) ; :: thesis: 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 #)
thus 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 #) ; :: thesis: verum