deg (x * <%c,b,a%>) = deg <%c,b,a%> by RING_5:4
.= 2 by qua4 ;
hence x * <%c,b,a%> is quadratic ; :: thesis: verum