:: deftheorem Def2 defines is_at_least_length_of ALGSEQ_1:def 2 :
for R being non empty ZeroStr
for p being AlgSequence of R
for k being Nat holds
( k is_at_least_length_of p iff for i being Nat st i >= k holds
p . i = 0. R );