let H be non empty MonoidalSubStr of G; :: thesis: H is constituted-FinSeqs
let a be Element of H; :: according to MONOID_0:def 2 :: thesis: a is FinSequence
H₁(H) c= H₁(G) by Th25;
then a is Element of G by TARSKI:def 3;
hence a is FinSequence ; :: thesis: verum