A: 2 -' 1 = 2 - 1 by XREAL_0:def 2;
len <%b,(1. R)%> = 2 by POLYNOM5:40;
then <%b,(1. R)%> . ((len <%b,(1. R)%>) -' 1) = 1. R by A, POLYNOM5:38;
then LC <%b,(1. R)%> = 1. R by RATFUNC1:def 6;
hence ( <%b,(1. R)%> is monic & <%b,(1. R)%> is linear ) by RATFUNC1:def 7; :: thesis: verum