let M be MonoidalExtension of G; :: thesis: not M is empty
multMagma(# the carrier of M, the multF of M #) = multMagma(# the carrier of G, the multF of G #) by Def22;
hence not the carrier of M is empty ; :: according to STRUCT_0:def 1 :: thesis: verum