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