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