let L be non degenerated comRing; :: thesis: for p being Polynomial of L st len p = 1 holds
Roots p = {}
let p be Polynomial of L; :: thesis: ( len p = 1 implies Roots p = {} )
assume len p = 1 ; :: thesis: Roots p = {}
then A1: ( p = <%(p . 0)%> & p . 0 <> 0. L ) by Th16;
assume Roots p <> {} ; :: thesis: contradiction
then consider x being object such that
A2: x in Roots p by XBOOLE_0:def 1;
reconsider x = x as Element of L by A2;
x is_a_root_of p by A2, POLYNOM5:def 10;
then eval (p,x) = 0. L ;
hence contradiction by A1, POLYNOM5:37; :: thesis: verum