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

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