theorem divfin2h: :: FIELD_14:54

for F being Field
for a being Element of F holds MonicDivisors (rpoly (1,a)) = {(1_. F),(rpoly (1,a))}