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

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