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