let L be non empty right_complementable unital right-distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for p being Polynomial of L st deg p = 0 holds
for x being Element of L holds eval (p,x) <> 0. L
let p be Polynomial of L; :: thesis: ( deg p = 0 implies for x being Element of L holds eval (p,x) <> 0. L )
assume AS: deg p = 0 ; :: thesis: for x being Element of L holds eval (p,x) <> 0. L
let x be Element of L; :: thesis: eval (p,x) <> 0. L
assume eval (p,x) = 0. L ; :: thesis: contradiction
then x is_a_root_of p by POLYNOM5:def 6;
then p is with_roots by POLYNOM5:def 7;
hence contradiction by AS, HURWITZ:24; :: thesis: verum