:: deftheorem Def32 defines right_invertible ALGSTR_0:def 32 :
for M being multLoopStr holds
( M is right_invertible iff for x being Element of M holds x is right_invertible );