theorem Th16: :: MONOID_0:16

for M being non empty multLoopStr holds
( M is well-unital iff for a being Element of M holds
( (1. M) * a = a & a * (1. M) = a ) ) ;