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

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

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

then
card ((Roots p) \ S) = (card (Roots p)) - (card S)
by TARSKI:def 3, CARD_2:44;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;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

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