let L be non empty ZeroStr ; :: thesis: for p being AlgSequence of L
for i being Element of NAT st p . i <> 0. L holds
len p >= i + 1
let p be AlgSequence of L; :: thesis: for i being Element of NAT st p . i <> 0. L holds
len p >= i + 1
let i be Element of NAT ; :: thesis: ( p . i <> 0. L implies len p >= i + 1 )
A1: len p is_at_least_length_of p by ALGSEQ_1:def 3;
assume p . i <> 0. L ; :: thesis: len p >= i + 1
then len p > i by A1, ALGSEQ_1:def 2;
hence len p >= i + 1 by NAT_1:13; :: thesis: verum