let F be 0 -characteristic Field; :: thesis: for p being irreducible Element of the carrier of (Polynom-Ring F)
for E being FieldExtension of F
for a being Element of E st a is_a_root_of p,E holds
multiplicity (p,a) = 1
let p be irreducible Element of the carrier of (Polynom-Ring F); :: thesis: for E being FieldExtension of F
for a being Element of E st a is_a_root_of p,E holds
multiplicity (p,a) = 1
let E be FieldExtension of F; :: thesis: for a being Element of E st a is_a_root_of p,E holds
multiplicity (p,a) = 1
let a be Element of E; :: thesis: ( a is_a_root_of p,E implies multiplicity (p,a) = 1 )
assume AS: a is_a_root_of p,E ; :: thesis: multiplicity (p,a) = 1
the carrier of (Polynom-Ring F) c= the carrier of (Polynom-Ring E) by FIELD_4:10;
then reconsider p1 = p as Element of the carrier of (Polynom-Ring E) ;
p <> 0_. F ;
then p1 <> 0_. E by FIELD_4:12;
then reconsider p1 = p1 as non zero Element of the carrier of (Polynom-Ring E) by UPROOTS:def 5;
reconsider a1 = a as Element of E ;
A: 0. E = Ext_eval (p,a) by AS, FIELD_4:def 2
.= eval (p1,a1) by FIELD_4:26 ;
B: (Deriv E) . p1 = (Deriv F) . p by mm5;
p gcd ((Deriv F) . p) = 1_. F by mm6;
then p1 gcd ((Deriv E) . p1) = 1_. F by B, lemgcd
.= 1_. E by FIELD_4:14 ;
then C: p1 is square-free by mm4i;

D: now :: thesis: not multiplicity (p1,a1) > 1

assume multiplicity (p1,a1) > 1 ; :: thesis: contradiction
then E: multiplicity (p1,a1) >= 1 + 1 by INT_1:7;
(X- a1) `^ (multiplicity (p1,a1)) divides p1 by multi2;
then (X- a1) `^ 2 divides p1 by E, multi1;
hence contradiction by C, lemsq; :: thesis: verum

end;

multiplicity (p1,a1) >= 1 by A, POLYNOM5:def 7, UPROOTS:52;
hence multiplicity (p,a) = 1 by D, XXREAL_0:1, defM; :: thesis: verum