Lm1:
for R being non empty ZeroStr
for p being AlgSequence of R ex m being Nat st m is_at_least_length_of p
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
Lm2:
for R being non empty ZeroStr
for p being AlgSequence of R st p = <%(0. R)%> holds
len p = 0
canceled;