:: deftheorem defines -composition MONOID_0:def 39 :
for X being set holds X -composition = the multF of (GPFuncs X);