theorem :: POLYNOM5:43

for L being non empty ZeroStr
for z0 being Element of L holds <%z0,(0. L)%> = <%z0%>