theorem :: FIELD_9:16

for L being non empty ZeroStr
for a, b, c being Element of L holds
( <%c,b,a%> . 0 = c & <%c,b,a%> . 1 = b & <%c,b,a%> . 2 = a & ( for n being Nat st n >= 3 holds
<%c,b,a%> . n = 0. L ) ) by qua1;