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