theorem Th3: :: POLYNOM8:3

for L being non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr
for z, z1 being Element of L st z <> 0. L holds
z1 = (z1 * z) / z