for L being non empty ZeroStr
for z0, z1, z2 being Element of L holds <%z0,z1,z2%> . 2 = z2