let R be domRing; :: thesis: for S being non empty finite Subset of R
for p being Ppoly of R,S holds Roots p = S
let S be non empty finite Subset of R; :: thesis: for p being Ppoly of R,S holds Roots p = S
let p be Ppoly of R,S; :: thesis: Roots p = S

A0: now :: thesis: for o being object st o in S holds
o in Roots p

let o be object ; :: thesis: ( o in S implies o in Roots p )
assume AS: o in S ; :: thesis: o in Roots p
then reconsider x = o as Element of R ;
eval (p,x) = 0. R by AS, m1;
then x is_a_root_of p by POLYNOM5:def 7;
hence o in Roots p by POLYNOM5:def 10; :: thesis: verum

end;

then card ((Roots p) \ S) = (card (Roots p)) - (card S) by TARSKI:def 3, CARD_2:44;
then B: ((card (Roots p)) - (card S)) + (card S) >= 0 + (card S) by XREAL_1:6;
card (Roots p) <= deg p by degpoly;
then card (Roots p) <= card S by m00;
then card S = card (Roots p) by B, XXREAL_0:1;
hence Roots p = S by A0, CARD_2:102, TARSKI:def 3; :: thesis: verum