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