theorem :: MONOID_0:72

for X, Y being set st Y c= X holds
GPFuncs Y is SubStr of GPFuncs X