len <%b,a%> = 2 by POLYNOM5:40;
then deg <%b,a%> = 2 - 1 by HURWITZ:def 2;
hence <%b,a%> is linear by FIELD_5:def 1; :: thesis: verum