let F be 0 -characteristic Field; :: thesis: for p being irreducible Element of the carrier of (Polynom-Ring F) holds p gcd ((Deriv F) . p) = 1_. F
let p be irreducible Element of the carrier of (Polynom-Ring F); :: thesis: p gcd ((Deriv F) . p) = 1_. F
reconsider e = 1_. F as Element of (Polynom-Ring F) by POLYNOM3:def 10;
reconsider q1 = p, q2 = (Deriv F) . p as Element of (Polynom-Ring F) ;
H: ( q1 <> 0_. F & e is Element of the carrier of (Polynom-Ring F) ) ;
e * q1 = (1_. F) *' p by POLYNOM3:def 10
.= q1 ;
then A: e divides q1 by GCD_1:def 1;
e * q2 = (1_. F) *' ((Deriv F) . p) by POLYNOM3:def 10
.= q2 ;
then B: e divides q2 by GCD_1:def 1;

now :: thesis: for r1 being Element of (Polynom-Ring F) st r1 divides q1 & r1 divides q2 holds
r1 divides e

let r1 be Element of (Polynom-Ring F); :: thesis: ( r1 divides q1 & r1 divides q2 implies b₁ divides e )
assume C1: ( r1 divides q1 & r1 divides q2 ) ; :: thesis: b₁ divides e
reconsider r = r1 as Element of the carrier of (Polynom-Ring F) ;
consider u1 being Element of (Polynom-Ring F) such that
C2: q1 = r1 * u1 by C1, GCD_1:def 1;
reconsider u = u1 as Element of the carrier of (Polynom-Ring F) ;
C3: p = r *' u by C2, POLYNOM3:def 10;
consider u2 being Element of (Polynom-Ring F) such that
C5: q2 = r1 * u2 by C1, GCD_1:def 1;
reconsider v = u2 as Element of the carrier of (Polynom-Ring F) ;
C7: (Deriv F) . p = r *' v by C5, POLYNOM3:def 10;

per cases ( deg r < 1 + 0 or deg r >= deg p ) by C3, RING_4:1, RING_4:41;

suppose deg r < 1 + 0 ; :: thesis: b₁ divides e

then r is constant by INT_1:7, RING_4:def 4;
then consider a being Element of F such that
D1: r = a | F by RING_4:20;
D2: a <> 0. F by C3, D1;
reconsider v = (a ") | F as Element of (Polynom-Ring F) by POLYNOM3:def 10;
r1 * v = r *' ((a ") | F) by POLYNOM3:def 10
.= (a * (a ")) | F by D1, RING_4:18
.= (1. F) | F by D2, VECTSP_1:def 10
.= 1_. F by RING_4:14 ;
hence r1 divides e by GCD_1:def 1; :: thesis: verum

end;

suppose D1: deg r >= deg p ; :: thesis: b₁ divides e

deg r <= deg p by C3, RING_4:1, RING_5:13;
then D2: deg r = deg p by D1, XXREAL_0:1;
(Deriv F) . p <> 0_. F by mm6b;
then not (Deriv F) . p is zero by UPROOTS:def 5;
then deg r <= deg ((Deriv F) . p) by C7, RING_4:1, RING_5:13;
hence r1 divides e by D2, mm6a; :: thesis: verum

end;

end;

end;

then e is q1,q2 -gcd by A, B, RING_4:def 10;
then 1_. F = q1 gcd q2 by H, RING_4:def 11;
hence p gcd ((Deriv F) . p) = 1_. F by RING_4:def 12; :: thesis: verum