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

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

hence
len p >= k
; :: thesis: verum
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;assume i < k ; :: thesis: len p > i

then p . i <> 0. R by A1;

hence len p > i by Th1; :: thesis: verum