theorem Th17: :: HURWITZ:17

for L being non empty left-distributive doubleLoopStr
for p being Polynomial of L
for x1, x2 being Element of L holds (x1 + x2) * p = (x1 * p) + (x2 * p)