theorem qua6: :: FIELD_9:19
for R being Ring
for a, b, c, x being Element of R holds x * <%c,b,a%> = <%(x * c),(x * b),(x * a)%>