:: deftheorem defines almost_right_invertible ALGSTR_0:def 39 :
for M being multLoopStr_0 holds
( M is almost_right_invertible iff for x being Element of M st x <> 0. M holds
x is right_invertible );