:: deftheorem defines right_invertible ALGSTR_0:def 28 :
for M being multLoopStr
for x being Element of M holds
( x is right_invertible iff ex y being Element of M st x * y = 1. M );