let L be non empty ZeroStr ; :: thesis: for z0 being Element of L st z0 <> 0. L holds
len <%z0%> = 1
let z0 be Element of L; :: thesis: ( z0 <> 0. L implies len <%z0%> = 1 )
assume z0 <> 0. L ; :: thesis: len <%z0%> = 1
then <%z0%> . 0 <> 0. L by ALGSEQ_1:def 5;
then <%z0%> <> <%(0. L)%> by ALGSEQ_1:def 5;
then len <%z0%> <> 0 by ALGSEQ_1:14;
then A1: len <%z0%> >= 0 + 1 by NAT_1:13;
assume len <%z0%> <> 1 ; :: thesis: contradiction
then len <%z0%> > 1 by A1, XXREAL_0:1;
hence contradiction by ALGSEQ_1:def 5; :: thesis: verum