:: deftheorem Def22 defines MonoidalExtension MONOID_0:def 22 :
for G being multMagma
for b₂ being multLoopStr holds
( b₂ is MonoidalExtension of G iff multMagma(# the carrier of b₂, the multF of b₂ #) = multMagma(# the carrier of G, the multF of G #) );