consider x being Element of R such that
A: x is_a_root_of p by POLYNOM5:def 8;
multiplicity (p,x) >= 1 by A, UPROOTS:52;
then (BRoots p) . x >= 1 by UPROOTS:def 9;
hence not BRoots p is zero ; :: thesis: verum