theorem :: MONOID_0:59

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