(Deriv F) . (X- a) = 1_. F by FIELD_14:61;
hence ( X- a is separable & X- a is irreducible ) by main1; :: thesis: verum