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 A1: len p = 1 ; :: thesis: Roots p = {}
assume Roots p <> {} ; :: thesis: contradiction
then consider x being set such that
A2: x in Roots p by XBOOLE_0:def 1;
A3: ( p = <%(p . 0 )%> & p . 0 <> 0. L ) by A1, Th21;
reconsider x = x as Element of L by A2;
x is_a_root_of p by A2, POLYNOM5:def 9;
then eval p,x = 0. L by POLYNOM5:def 6;
hence contradiction by A3, POLYNOM5:38; :: thesis: verum