let q be Polynomial of R; :: thesis: ( not q is zero & q is with_roots implies not q is constant )
assume AS: ( not q is zero & q is with_roots ) ; :: thesis: not q is constant
reconsider p = q as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 10;
reconsider degp = deg p as Element of NAT by AS, T8;
consider x being Element of R such that
X: x is_a_root_of p by AS, POLYNOM5:def 8;
H: eval (p,x) = 0. R by X, POLYNOM5:def 7;
now :: thesis: not p is constant
assume A: p is constant ; :: thesis: contradiction
then consider a being Element of R such that
B: p = a | R by RING_4:20;
degp = 0 by A;
then a <> 0. R by B, RING_4:21;
hence contradiction by H, B, evconst; :: thesis: verum
end;
hence not q is constant ; :: thesis: verum