for n being Nat
for L being non empty ZeroStr
for x being Element of L holds n + 1 is_at_least_length_of seq (n,x)