:: deftheorem Def9 defines almost_left_invertible VECTSP_1:def 9 :
for IT being non empty multLoopStr_0 holds
( IT is almost_left_invertible iff for x being Element of IT st x <> 0. IT holds
ex y being Element of IT st y * x = 1. IT );