let i be Nat; :: thesis: for R being non empty ZeroStr

for p being AlgSequence of R st i >= len p holds

p . i = 0. R

let R be non empty ZeroStr ; :: thesis: for p being AlgSequence of R st i >= len p holds

p . i = 0. R

let p be AlgSequence of R; :: thesis: ( i >= len p implies p . i = 0. R )

assume A1: i >= len p ; :: thesis: p . i = 0. R

len p is_at_least_length_of p by Def3;

hence p . i = 0. R by A1; :: thesis: verum

for p being AlgSequence of R st i >= len p holds

p . i = 0. R

let R be non empty ZeroStr ; :: thesis: for p being AlgSequence of R st i >= len p holds

p . i = 0. R

let p be AlgSequence of R; :: thesis: ( i >= len p implies p . i = 0. R )

assume A1: i >= len p ; :: thesis: p . i = 0. R

len p is_at_least_length_of p by Def3;

hence p . i = 0. R by A1; :: thesis: verum