let F be Field; :: thesis: for a being Element of F holds MonicDivisors (rpoly (1,a)) = {(1_. F),(rpoly (1,a))}
let a be Element of F; :: thesis: MonicDivisors (rpoly (1,a)) = {(1_. F),(rpoly (1,a))}
set M = {(1_. F),(rpoly (1,a))};
H: ( 1_. F is Element of the carrier of (Polynom-Ring F) & rpoly (1,a) is Element of the carrier of (Polynom-Ring F) ) by POLYNOM3:def 10;

A: now :: thesis: for o being object st o in {(1_. F),(rpoly (1,a))} holds
o in MonicDivisors (rpoly (1,a))

let o be object ; :: thesis: ( o in {(1_. F),(rpoly (1,a))} implies b₁ in MonicDivisors (rpoly (1,a)) )
assume o in {(1_. F),(rpoly (1,a))} ; :: thesis: b₁ in MonicDivisors (rpoly (1,a))

per cases then ( o = 1_. F or o = rpoly (1,a) ) by TARSKI:def 2;

suppose B: o = 1_. F ; :: thesis: b₁ in MonicDivisors (rpoly (1,a))

(1_. F) *' (rpoly (1,a)) = rpoly (1,a) ;
then 1_. F divides rpoly (1,a) by RING_4:1;
hence o in MonicDivisors (rpoly (1,a)) by B, H; :: thesis: verum

end;

suppose B: o = rpoly (1,a) ; :: thesis: b₁ in MonicDivisors (rpoly (1,a))

(1_. F) *' (rpoly (1,a)) = rpoly (1,a) ;
then rpoly (1,a) divides rpoly (1,a) by RING_4:1;
hence o in MonicDivisors (rpoly (1,a)) by B, H; :: thesis: verum

end;

end;

end;

now :: thesis: for o being object st o in MonicDivisors (rpoly (1,a)) holds
o in {(1_. F),(rpoly (1,a))}

let o be object ; :: thesis: ( o in MonicDivisors (rpoly (1,a)) implies b₁ in {(1_. F),(rpoly (1,a))} )
assume o in MonicDivisors (rpoly (1,a)) ; :: thesis: b₁ in {(1_. F),(rpoly (1,a))}
then consider q being monic Element of the carrier of (Polynom-Ring F) such that
B1: ( o = q & q divides rpoly (1,a) ) ;
deg q <= deg (rpoly (1,a)) by B1, RING_5:13;
then deg q <= 1 by HURWITZ:27;

per cases then ( deg q = 1 or deg q < 1 ) by XXREAL_0:1;

suppose deg q = 1 ; :: thesis: b₁ in {(1_. F),(rpoly (1,a))}

then consider x, b being Element of F such that
B2: ( x <> 0. F & q = x * (rpoly (1,b)) ) by HURWITZ:28;
B3: 1. F = LC q by RATFUNC1:def 7
.= x * (LC (rpoly (1,b))) by B2, RING_5:5
.= x * (1. F) by RATFUNC1:def 7 ;
then a = b by B1, B2, RING_5:21;
hence o in {(1_. F),(rpoly (1,a))} by B1, B2, B3, TARSKI:def 2; :: thesis: verum

end;

suppose deg q < 1 ; :: thesis: b₁ in {(1_. F),(rpoly (1,a))}

then (deg q) + 1 <= 1 by INT_1:7;
then ((deg q) + 1) - 1 <= 1 - 1 by XREAL_1:9;
then consider b being Element of F such that
B2: q = b | F by RING_4:def 4, RING_4:20;
1. F = LC q by RATFUNC1:def 7
.= b by B2, RING_5:6 ;
then q = 1_. F by B2, RING_4:14;
hence o in {(1_. F),(rpoly (1,a))} by B1, TARSKI:def 2; :: thesis: verum

end;

end;

end;

hence MonicDivisors (rpoly (1,a)) = {(1_. F),(rpoly (1,a))} by A, TARSKI:2; :: thesis: verum