for k being Nat
for R being non empty ZeroStr
for p being AlgSequence of R st len p = k + 1 holds
p . k <> 0. R