reconsider E = F as FieldExtension of F by FIELD_4:6;
reconsider b = a as Element of E ;
reconsider n1 = n - 1 as Nat ;
set p = (X- a) `^ n;
reconsider q = (X- b) `^ n as Polynomial of E ;
reconsider q = q as non constant Polynomial of E ;
reconsider p = (X- a) `^ n as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
deg ((X- a) `^ n) > 0 by RATFUNC1:def 2;
then reconsider p = p as non constant Element of the carrier of (Polynom-Ring F) by RING_4:def 4;
H1: Roots (E,p) = Roots q by FIELD_7:13
.= {b} by Lm12b ;
H2: Roots (E,p) = { a where a is Element of E : a is_a_root_of p,E } by FIELD_4:def 4;
b in Roots (E,p) by H1, TARSKI:def 1;
then consider c being Element of E such that
H7: ( b = c & c is_a_root_of p,E ) by H2;
n >= 1 + 1 by NAT_2:29;
then E: ( n + 1 > n & n > 1 ) by NAT_1:13;
F: n = multiplicity (q,b) by ro0
.= multiplicity (p,b) by FIELD_14:def 6 ;
n1 + 1 = n ;
then p = ((X- a) `^ n1) *' (X- a) by POLYNOM5:19;
hence ( not (X- a) |^ n is separable & not (X- a) |^ n is irreducible ) by F, E, sp, H7, ThSep0; :: thesis: verum