let L be non empty ZeroStr ; :: thesis: for z0, z1, z2 being Element of L st z2 <> 0. L holds
len <%z0,z1,z2%> = 3
let z0, z1, z2 be Element of L; :: thesis: ( z2 <> 0. L implies len <%z0,z1,z2%> = 3 )
assume z2 <> 0. L ; :: thesis: len <%z0,z1,z2%> = 3
then <%z0,z1,z2%> . 2 <> 0. L by Th23;
then A1: for n being Nat st n is_at_least_length_of <%z0,z1,z2%> holds
2 + 1 <= n by NAT_1:13;
3 is_at_least_length_of <%z0,z1,z2%> by Th24;
hence len <%z0,z1,z2%> = 3 by A1, ALGSEQ_1:def 3; :: thesis: verum