:: deftheorem Def40 defines GFuncs MONOID_0:def 40 :
for X being set
for b₂ being strict SubStr of GPFuncs X holds
( b₂ = GFuncs X iff the carrier of b₂ = Funcs (X,X) );