theorem Th15: :: POLYVIE1:15

for L being Field
for p being non-zero Polynomial of L
for a being Element of L
for b being non zero Element of L st not - (a / b) in Roots p holds
card (Roots (<%a,b%> *' p)) = 1 + (card (Roots p))