let M be MonoidalExtension of G; :: thesis: M is constituted-Functions
let a be Element of M; :: according to MONOID_0:def 1 :: thesis: a is Function
multMagma(# the carrier of M, the multF of M #) = multMagma(# the carrier of G, the multF of G #) by Def22;
hence a is Function ; :: thesis: verum