reconsider p1 = p, q1 = q as Polynomial of R ;
( q <> 0_. R & p <> 0_. R ) ;
then B: deg (p1 *' q1) = (deg p) + (deg q) by HURWITZ:23;
deg p = 1 by defl;
hence not p *' q is linear by RATFUNC1:def 2, B; :: thesis: verum