:: deftheorem defines <% FIELD_9:def 5 :
for L being non empty ZeroStr
for a, b, c being Element of L holds <%c,b,a%> = (((0_. L) +* (0,c)) +* (1,b)) +* (2,a);