:: deftheorem defines <% POLYNOM5:def 5 :
for L being non empty ZeroStr
for z0, z1 being Element of L holds <%z0,z1%> = ((0_. L) +* (0,z0)) +* (1,z1);