theorem Th8: :: POLYVIE1:8

for L being non empty right_complementable almost_left_invertible add-associative right_zeroed left-distributive well-unital associative commutative doubleLoopStr
for a, b, x being Element of L st b <> 0. L holds
eval (<%a,b%>,(- (a / b))) = 0. L