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;
then a is Element of G ;
hence a is Function ; :: thesis: verum