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 Def10, Def12, Th69; :: thesis: verum