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

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