let H be non empty SubStr 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 Th23;
then a is Element of G ;
hence a is Function ; :: thesis: verum