let L be domRing; :: thesis: for p being non-zero Polynomial of L st Roots p = {} holds
SumRoots p = 0. L
let p be non-zero Polynomial of L; :: thesis: ( Roots p = {} implies SumRoots p = 0. L )
assume A1: Roots p = {} ; :: thesis: SumRoots p = 0. L
canFS (Roots p) is Enumeration of Roots p by Th2;
then (BRoots p) (++) (canFS (Roots p)) = {} by A1, Th18;
then len ((BRoots p) (++) (canFS (Roots p))) = 0 ;
hence SumRoots p = 0. L by RLVECT_1:75; :: thesis: verum