theorem Th2: :: ALGSEQ_1:9

for k being Nat
for R being non empty ZeroStr
for p being AlgSequence of R st ( for i being Nat st i < k holds
p . i <> 0. R ) holds
len p >= k