set p = (rpoly (1,(0. R))) *' (rpoly (1,(0. R)));
reconsider a = (rpoly (1,(0. R))) *' (rpoly (1,(0. R))) as Element of (Polynom-Ring R) by POLYNOM3:def 10;
take a ; :: thesis: not a is constant
deg ((rpoly (1,(0. R))) *' (rpoly (1,(0. R)))) = (deg (rpoly (1,(0. R)))) + (deg (rpoly (1,(0. R)))) by HURWITZ:23
.= 1 + (deg (rpoly (1,(0. R)))) by HURWITZ:27
.= 1 + 1 by HURWITZ:27 ;
hence not a is constant ; :: thesis: verum