let L be non empty ZeroStr ; :: thesis: for p being AlgSequence of L st len p > 0 holds
p . ((len p) -' 1) <> 0. L
let p be AlgSequence of L; :: thesis: ( len p > 0 implies p . ((len p) -' 1) <> 0. L )
assume len p > 0 ; :: thesis: p . ((len p) -' 1) <> 0. L
then ex k being Nat st len p = k + 1 by NAT_1:6;
then len p = ((len p) -' 1) + 1 by NAT_D:34;
hence p . ((len p) -' 1) <> 0. L by ALGSEQ_1:10; :: thesis: verum