theorem ID2: :: FIELD_16:11

for R being domRing
for S being domRingExtension of R
for p being non zero Element of the carrier of (Polynom-Ring R) holds card (Roots (S,p)) <= deg p