theorem Th18: :: MONOID_0:18

for G being non empty multMagma
for M being MonoidalExtension of G holds
( the carrier of M = the carrier of G & the multF of M = the multF of G & ( for a, b being Element of M
for a9, b9 being Element of G st a = a9 & b = b9 holds
a * b = a9 * b9 ) )