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;