let D be non empty set ; :: thesis: ( D -concatenation is having_a_unity & the_unity_wrt (D -concatenation) = {} & D -concatenation is associative )
multMagma(# (D *),(D -concatenation) #) = D *+^ by Def34;
hence ( D -concatenation is having_a_unity & the_unity_wrt (D -concatenation) = {} & D -concatenation is associative ) by Th60; :: thesis: verum