theorem Th14: :: HURWITZ:14

for L being non empty associative doubleLoopStr
for p being Polynomial of L
for x1, x2 being Element of L holds x1 * (x2 * p) = (x1 * x2) * p