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