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