:: deftheorem defines / ALGSTR_0:def 42 :
for M being multLoopStr
for x, y being Element of M holds x / y = x * (/ y);