let R be non empty ZeroStr ; :: thesis: for p being AlgSequence of R ex m being Nat st m is_at_least_length_of p
let p be AlgSequence of R; :: thesis: ex m being Nat st m is_at_least_length_of p
consider n being Nat such that
A1: for i being Nat st i >= n holds
p . i = 0. R by Def1;
take n ; :: thesis: n is_at_least_length_of p
thus n is_at_least_length_of p by A1; :: thesis: verum