let F be Field; :: thesis: for p being non constant Element of the carrier of (Polynom-Ring F) holds
( p is separable iff p gcd ((Deriv F) . p) = 1_. F )
let p be non constant Element of the carrier of (Polynom-Ring F); :: thesis: ( p is separable iff p gcd ((Deriv F) . p) = 1_. F )

A: now :: thesis: ( p is separable implies p gcd ((Deriv F) . p) = 1_. F )

assume AS: p is separable ; :: thesis: p gcd ((Deriv F) . p) = 1_. F
set K = the SplittingField of p;
B: p splits_in the SplittingField of p by FIELD_8:def 1;
for a being Element of the SplittingField of p holds not multiplicity (p,a) > 1 by AS, ThSep02;
hence p gcd ((Deriv F) . p) = 1_. F by B, lemsep3; :: thesis: verum

end;

now :: thesis: ( p gcd ((Deriv F) . p) = 1_. F implies p is separable )

assume AS: p gcd ((Deriv F) . p) = 1_. F ; :: thesis: p is separable
set K = the SplittingField of p;
p splits_in the SplittingField of p by FIELD_8:def 1;
then for a being Element of the SplittingField of p holds multiplicity (p,a) <= 1 by AS, lemsep3;
hence p is separable by ThSep01; :: thesis: verum

end;

hence ( p is separable iff p gcd ((Deriv F) . p) = 1_. F ) by A; :: thesis: verum