for L being non empty ZeroStr
for p being AlgSequence of L
for i being Element of NAT st p . i <> 0. L holds
len p >= i + 1