let F be Field; :: thesis: for p being non zero Element of the carrier of (Polynom-Ring F) st p gcd ((Deriv F) . p) = 1_. F holds
p is square-free
let p be non zero Element of the carrier of (Polynom-Ring F); :: thesis: ( p gcd ((Deriv F) . p) = 1_. F implies p is square-free )

now :: thesis: ( not p is square-free implies p gcd ((Deriv F) . p) <> 1_. F )

assume not p is square-free ; :: thesis: p gcd ((Deriv F) . p) <> 1_. F
then consider q1 being non constant Polynomial of F such that
A1: q1 `^ 2 divides p by lemsq;
consider r1 being Polynomial of F such that
A2: p = (q1 `^ 2) *' r1 by A1, RING_4:1;
reconsider r = r1, q = q1 as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
q1 `^ 2 = q1 *' q1 by POLYNOM5:17
.= q * q by POLYNOM3:def 10 ;
then A3: p = (q * q) * r by A2, POLYNOM3:def 10
.= q * (q * r) by GROUP_1:def 3 ;
A4: p = (q1 *' q1) *' r1 by A2, POLYNOM5:17
.= q1 *' (q1 *' r) by POLYNOM3:33 ;
reconsider u = ((Deriv F) . (q * r)) + (r * ((Deriv F) . q)) as Polynomial of F by POLYNOM3:def 10;
(Deriv F) . p = (q * ((Deriv F) . (q * r))) + ((q * r) * ((Deriv F) . q)) by A3, RINGDER1:def 1
.= (q * ((Deriv F) . (q * r))) + (q * (r * ((Deriv F) . q))) by GROUP_1:def 3
.= q * (((Deriv F) . (q * r)) + (r * ((Deriv F) . q))) by VECTSP_1:def 2
.= q1 *' u by POLYNOM3:def 10 ;
then A5: ( q1 divides p & q1 divides (Deriv F) . p ) by A4, RING_4:1;
( deg q1 > 0 & deg (1_. F) <= 0 ) by RATFUNC1:def 2;
hence p gcd ((Deriv F) . p) <> 1_. F by A5, RING_5:13, RING_4:52; :: thesis: verum

end;

hence ( p gcd ((Deriv F) . p) = 1_. F implies p is square-free ) ; :: thesis: verum