let k be Nat; :: thesis: for R being non empty ZeroStr
for p being AlgSequence of R st ( for i being Nat st i < k holds
p . i <> 0. R ) holds
len p >= k
let R be non empty ZeroStr ; :: thesis: for p being AlgSequence of R st ( for i being Nat st i < k holds
p . i <> 0. R ) holds
len p >= k
let p be AlgSequence of R; :: thesis: ( ( for i being Nat st i < k holds
p . i <> 0. R ) implies len p >= k )
assume A1: for i being Nat st i < k holds
p . i <> 0. R ; :: thesis: len p >= k
for i being Nat st i < k holds
len p > i

proof

let i be Nat; :: thesis: ( i < k implies len p > i )
assume i < k ; :: thesis: len p > i
then p . i <> 0. R by A1;
hence len p > i by Th1; :: thesis: verum

end;

hence len p >= k ; :: thesis: verum