for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of L st len p <> 0 holds
ex q being Polynomial of L st
( len q < len p & p = q + (Leading-Monomial p) & ( for n being Element of NAT st n < (len p) - 1 holds
q . n = p . n ) )