:: deftheorem defines / QUOFIELD:def 17 :
for F being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr
for x, y being Element of F holds x / y = x * (y ");