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

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