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

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

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

then A3:
l is_at_least_length_of s
by ALGSEQ_1:def 2;s . i = 0. L

let i be Nat; :: thesis: ( i >= l implies s . b_{1} = 0. L )

assume A2: i >= l ; :: thesis: s . b_{1} = 0. L

end;assume A2: i >= l ; :: thesis: s . b

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