theorem :: MONOID_0:59

for D being non empty set holds D *+^ = multMagma(# (D *),(D -concatenation) #) by Def34;