set q = X^ ((p |^ n),F);
set E = the SplittingField of X^ ((p |^ n),F);
A: X^ ((p |^ n),F) splits_in the SplittingField of X^ ((p |^ n),F) by FIELD_8:def 1;

now :: thesis: not X^ ((p |^ n),F) is inseparable

assume X^ ((p |^ n),F) is inseparable ; :: thesis: contradiction
then ex a being Element of the SplittingField of X^ ((p |^ n),F) st multiplicity ((X^ ((p |^ n),F)),a) > 1 by A, FIELD_15:78;
then B: (X^ ((p |^ n),F)) gcd ((Deriv F) . (X^ ((p |^ n),F))) <> 1_. F by A, FIELD_15:72;
(- (1_. F)) gcd (X^ ((p |^ n),F)) = 1_. F

proof

(1_. F) *' (- (1_. F)) = - (1_. F) ;
then C: 1_. F divides - (1_. F) by RING_4:1;
(1_. F) *' (X^ ((p |^ n),F)) = X^ ((p |^ n),F) ;
then D: 1_. F divides X^ ((p |^ n),F) by RING_4:1;

now :: thesis: for r being Polynomial of F st r divides - (1_. F) & r divides X^ ((p |^ n),F) holds
r divides 1_. F

let r be Polynomial of F; :: thesis: ( r divides - (1_. F) & r divides X^ ((p |^ n),F) implies r divides 1_. F )
assume ( r divides - (1_. F) & r divides X^ ((p |^ n),F) ) ; :: thesis: r divides 1_. F
then consider u being Polynomial of F such that
E: r *' u = - (1_. F) by RING_4:1;
r *' (- u) = - (r *' u) by lemX
.= 1_. F by E ;
hence r divides 1_. F by RING_4:1; :: thesis: verum

end;

hence (- (1_. F)) gcd (X^ ((p |^ n),F)) = 1_. F by C, D, RING_4:53; :: thesis: verum

end;

hence contradiction by B, thX3; :: thesis: verum

end;

hence for b₁ being non constant Element of the carrier of (Polynom-Ring F) st b₁ = X^ ((p |^ n),F) holds
b₁ is separable ; :: thesis: verum