let L be non empty ZeroStr ; :: thesis: for z0 being Element of L st z0 <> 0. L holds
len <%z0,(0. L)%> = 1
let z0 be Element of L; :: thesis: ( z0 <> 0. L implies len <%z0,(0. L)%> = 1 )
A1: 1 is_at_least_length_of <%z0,(0. L)%>
proof
let n be Nat; :: according to ALGSEQ_1:def 2 :: thesis: ( not 1 <= n or <%z0,(0. L)%> . n = 0. L )
assume A2: n >= 1 ; :: thesis: <%z0,(0. L)%> . n = 0. L
per cases ( n = 1 or n > 1 ) by A2, XXREAL_0:1;
suppose n = 1 ; :: thesis: <%z0,(0. L)%> . n = 0. L
hence <%z0,(0. L)%> . n = 0. L by Th38; :: thesis: verum
end;
suppose n > 1 ; :: thesis: <%z0,(0. L)%> . n = 0. L
then n >= 1 + 1 by NAT_1:13;
hence <%z0,(0. L)%> . n = 0. L by Th38; :: thesis: verum
end;
end;
end;
assume z0 <> 0. L ; :: thesis: len <%z0,(0. L)%> = 1
then <%z0,(0. L)%> . 0 <> 0. L by Th38;
then for n being Nat st n is_at_least_length_of <%z0,(0. L)%> holds
0 + 1 <= n by NAT_1:13;
hence len <%z0,(0. L)%> = 1 by A1, ALGSEQ_1:def 3; :: thesis: verum