reconsider p = Char F as Prime ;
consider n being non zero Nat such that
A: order F = p |^ n by FIELD_15:92;
F is p -characteristic by RING_3:def 6;
hence for b₁ being non constant Element of the carrier of (Polynom-Ring F) st b₁ = X^ ((order F),F) holds
b₁ is separable by A; :: thesis: verum