let L be non empty ZeroStr ; :: thesis: for z0, z1 being Element of L holds len <%z0,z1%> <= 2
let z0, z1 be Element of L; :: thesis: len <%z0,z1%> <= 2
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;

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