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;

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

hence
not q is constant
; :: thesis: verumassume 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;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