:: deftheorem defines left-invertible MONOID_0:def 14 :
for IT being non empty multMagma holds
( IT is left-invertible iff the multF of IT is left-invertible );