:: deftheorem defines -concatenation MONOID_0:def 36 :
for D being set holds D -concatenation = the multF of (D *+^);