let F be Field; :: thesis: for p being monic Polynomial of F st p divides 1_. F holds
p = 1_. F
let r be monic Polynomial of F; :: thesis: ( r divides 1_. F implies r = 1_. F )
assume AS: r divides 1_. F ; :: thesis: r = 1_. F
reconsider r1 = r as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
deg r1 <= deg (1_. F) by AS, RING_5:13;
then deg r1 <= 0 by RATFUNC1:def 2;
then consider a being Element of F such that
A: r1 = a | F by RING_4:def 4, RING_4:20;
1. F = LC r by RATFUNC1:def 7
.= a by A, RING_5:6 ;
hence r = 1_. F by A, RING_4:14; :: thesis: verum