for L being non empty right-distributive doubleLoopStr
for p1, p2 being Polynomial of L
for x being Element of L holds x * (p1 + p2) = (x * p1) + (x * p2)