let L be non empty right_complementable add-associative right_zeroed unital doubleLoopStr ; :: thesis: for p being Polynomial of L st deg p = 0 holds
not p is with_roots
let p be Polynomial of L; :: thesis: ( deg p = 0 implies not p is with_roots )
assume A1: deg p = 0 ; :: thesis: not p is with_roots
then A2: p = <%(p . 0)%> by ALGSEQ_1:def 5;
now :: thesis: not p is with_roots
assume p is with_roots ; :: thesis: contradiction
then consider x being Element of L such that
A3: x is_a_root_of p by POLYNOM5:def 8;
0. L = eval (p,x) by A3, POLYNOM5:def 7
.= p . 0 by A2, POLYNOM5:37 ;
hence contradiction by A1, A2, ALGSEQ_1:14; :: thesis: verum
end;
hence not p is with_roots ; :: thesis: verum