theorem :: MONOID_0:67

for D being set holds
( D -concatenation is having_a_unity & the_unity_wrt (D -concatenation) = {} & D -concatenation is associative )