A: 3 -' 1 = 3 - 1 by XREAL_0:def 2;
len <%c,b,(1. R)%> = 3 by qua3;
then <%c,b,(1. R)%> . ((len <%c,b,(1. R)%>) -' 1) = 1. R by A, qua1;
then LC <%c,b,(1. R)%> = 1. R by RATFUNC1:def 6;
hence ( <%c,b,(1. R)%> is quadratic & <%c,b,(1. R)%> is monic ) by RATFUNC1:def 7; :: thesis: verum