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 Th42
.= <%z0%> by A1, Th34 ;
:: thesis: verum

end;

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

then A3: len <%z0%> = 0 + 1 by Th33;

A4: now :: thesis: for n being Nat st n < len <%z0%> holds
<%z0,(0. L)%> . n = <%z0%> . n

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 A5: n = 0 by A3, NAT_1:13;
hence <%z0,(0. L)%> . n = z0 by Th38
.= <%z0%> . n by A5, ALGSEQ_1:def 5 ;
:: thesis: verum

end;

len <%z0,(0. L)%> = 1 by A2, Th41;
hence <%z0,(0. L)%> = <%z0%> by A2, A4, Th33, ALGSEQ_1:12; :: thesis: verum

end;

end;