theorem Th19: :: MONOID_0:19

for G being non empty multMagma
for M being MonoidalExtension of G holds
( ( G is unital implies M is unital ) & ( G is commutative implies M is commutative ) & ( G is associative implies M is associative ) & ( G is invertible implies M is invertible ) & ( G is uniquely-decomposable implies M is uniquely-decomposable ) & ( G is cancelable implies M is cancelable ) )