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