:: deftheorem Def31 defines left_invertible ALGSTR_0:def 31 :
for M being multLoopStr holds
( M is left_invertible iff for x being Element of M holds x is left_invertible );