theorem ZZ3x: :: FIELD_14:35
for F being Field
for p being monic Polynomial of F st p divides 1_. F holds
p = 1_. F