theorem Th4: :: POLYVIE1:4

for L being non trivial right_unital associative doubleLoopStr
for a, b being Element of L st b is left_invertible & b is right_mult-cancelable & b * (/ b) = (/ b) * b holds
(a * b) / b = a