let L be non empty ZeroStr ; :: thesis: for z0 being Element of L holds <%z0,(0. L)%> = <%z0%>
let z0 be Element of L; :: thesis: <%z0,(0. L)%> = <%z0%>

per cases ( z0 = 0. L or z0 <> 0. L ) ;

suppose A1: z0 = 0. L ; :: thesis: <%z0,(0. L)%> = <%z0%>

hence <%z0,(0. L)%> = 0_. L by Th43
.= <%z0%> by A1, Th35 ;
:: thesis: verum

end;

suppose A2: z0 <> 0. L ; :: thesis: <%z0,(0. L)%> = <%z0%>

then A3: len <%z0%> = 0 + 1 by Th34;
A4: len <%z0,(0. L)%> = 1 by A2, Th42;

now

let n be Nat; :: thesis: ( n < len <%z0%> implies <%z0,(0. L)%> . n = <%z0%> . n )
assume n < len <%z0%> ; :: thesis: <%z0,(0. L)%> . n = <%z0%> . n
then n <= 0 by A3, NAT_1:13;
then A5: n = 0 ;
hence <%z0,(0. L)%> . n = z0 by Th39
.= <%z0%> . n by A5, ALGSEQ_1:def 6 ;
:: thesis: verum

end;

hence <%z0,(0. L)%> = <%z0%> by A3, A4, ALGSEQ_1:28; :: thesis: verum

end;

end;