for G being non empty unital multMagma
for M1, M2 being strict well-unital MonoidalExtension of G holds M1 = M2