let L be non empty right_complementable right-distributive add-associative right_zeroed unital 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 A1: 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 7;
then p is with_roots by POLYNOM5:def 8;
hence contradiction by A1, HURWITZ:24; :: thesis: verum