:: deftheorem defines is_a_root_of POLYNOM5:def 7 :
for L being non empty unital doubleLoopStr
for p being Polynomial of L
for x being Element of L holds
( x is_a_root_of p iff eval (p,x) = 0. L );