:: deftheorem Def37 defines GPFuncs MONOID_0:def 37 :
for X being set
for b₂ being strict constituted-Functions multMagma holds
( b₂ = GPFuncs X iff ( the carrier of b₂ = PFuncs (X,X) & ( for f, g being Element of b₂ holds f [*] g = g (*) f ) ) );