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 A1: <%z0,z1%> . 1 <> 0. L by Th39;
A2: 2 is_at_least_length_of <%z0,z1%>

proof

let n be Nat; :: according to ALGSEQ_1:def 3 :: thesis: ( not 2 <= n or <%z0,z1%> . n = 0. L )
thus ( not 2 <= n or <%z0,z1%> . n = 0. L ) by Th39; :: thesis: verum

end;

now

let n be Nat; :: thesis: ( n is_at_least_length_of <%z0,z1%> implies 1 + 1 <= n )
assume n is_at_least_length_of <%z0,z1%> ; :: thesis: 1 + 1 <= n
then 1 < n by A1, ALGSEQ_1:def 3;
hence 1 + 1 <= n by NAT_1:13; :: thesis: verum

end;

hence len <%z0,z1%> = 2 by A2, ALGSEQ_1:def 4; :: thesis: verum