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; verum