reconsider r = p * q as Element of the carrier of (Polynom-Ring R) ;
A: ( deg q > 0 & deg p > 0 ) by RING_4:def 4;
( q <> 0_. R & p <> 0_. R ) ;
then (deg p) + (deg q) = deg (p *' q) by HURWITZ:23
.= deg r by POLYNOM3:def 10 ;
hence not p * q is constant by A, RING_4:def 4; :: thesis: verum