let L be non empty ZeroStr ; :: thesis: for s being AlgSequence of L st len s > 0 holds
s . ((len s) - 1) <> 0. L
let s be AlgSequence of L; :: thesis: ( len s > 0 implies s . ((len s) - 1) <> 0. L )
assume len s > 0 ; :: thesis: s . ((len s) - 1) <> 0. L
then len s >= 0 + 1 by NAT_1:13;
then (len s) - 1 >= 1 - 1 by XREAL_1:9;
then reconsider l = (len s) - 1 as Element of NAT by INT_1:3;
assume A1: s . ((len s) - 1) = 0. L ; :: thesis: contradiction

now :: thesis: for i being Nat st i >= l holds
s . i = 0. L

let i be Nat; :: thesis: ( i >= l implies s . b₁ = 0. L )
assume A2: i >= l ; :: thesis: s . b₁ = 0. L

per cases ( i = l or i > l ) by A2, XXREAL_0:1;

suppose i = l ; :: thesis: s . b₁ = 0. L

hence s . i = 0. L by A1; :: thesis: verum

end;

suppose i > l ; :: thesis: s . b₁ = 0. L

then i >= l + 1 by NAT_1:13;
hence s . i = 0. L by ALGSEQ_1:8; :: thesis: verum

end;

end;

end;

then A3: l is_at_least_length_of s by ALGSEQ_1:def 2;
len s < (len s) + 1 by NAT_1:13;
then (len s) - 1 < ((len s) + 1) - 1 by XREAL_1:9;
hence contradiction by A3, ALGSEQ_1:def 3; :: thesis: verum