theorem Th35: :: UPROOTS:38

for L being non empty non degenerated right_complementable well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for r being Element of L
for q being non-zero Polynomial of L holds len (<%r,(1. L)%> *' q) = (len q) + 1