theorem :: UPROOTS:32
for L being non empty right_complementable right-distributive well-unital add-associative right_zeroed doubleLoopStr
for p being Polynomial of L holds p *' <%(1. L)%> = p