let G be non empty multMagma ; :: thesis:
let M be MonoidalExtension of G; :: thesis:
A1: multMagma(# the carrier of M, the multF of M #) = multMagma(# the carrier of G, the multF of G #) by Def22;
thus ( G is unital implies M is unital ) by A1; :: thesis:
thus ( G is commutative implies M is commutative ) by A1; :: thesis:
thus ( G is associative implies M is associative ) by A1; :: thesis:
thus ( G is invertible implies M is invertible ) by A1; :: thesis:
thus ( G is uniquely-decomposable implies M is uniquely-decomposable ) by A1; :: thesis:
assume H₂(G) is cancelable ; :: according to MONOID_0:def 19 :: thesis:
hence H₂(M) is cancelable by A1; :: according to MONOID_0:def 19 :: thesis: