for L being non empty non degenerated multLoopStr_0
for n being Element of NAT
for p being Polynomial of L st n <= len p holds
(len (poly_shift (p,n))) + n = len p