theorem Th17: :: POLYVIE1:17

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
for E being Enumeration of Roots (<%a,b%> *' p) st E = (canFS (Roots p)) ^ <*(- (a / b))*> holds
( len E = 1 + (card (Roots p)) & E . (1 + (card (Roots p))) = - (a / b) & ( for n being Nat st 1 <= n & n <= card (Roots p) holds
E . n = (canFS (Roots p)) . n ) )