let F be Field; :: thesis: for p being non zero Element of the carrier of (Polynom-Ring F)
for a being Element of F st a is_a_root_of p holds
( ( multiplicity (p,a) = 1 implies eval (((Deriv F) . p),a) <> 0. F ) & ( eval (((Deriv F) . p),a) <> 0. F implies multiplicity (p,a) = 1 ) & ( multiplicity (p,a) > 1 implies eval (((Deriv F) . p),a) = 0. F ) & ( eval (((Deriv F) . p),a) = 0. F implies multiplicity (p,a) > 1 ) )
let p be non zero Element of the carrier of (Polynom-Ring F); :: thesis: for a being Element of F st a is_a_root_of p holds
( ( multiplicity (p,a) = 1 implies eval (((Deriv F) . p),a) <> 0. F ) & ( eval (((Deriv F) . p),a) <> 0. F implies multiplicity (p,a) = 1 ) & ( multiplicity (p,a) > 1 implies eval (((Deriv F) . p),a) = 0. F ) & ( eval (((Deriv F) . p),a) = 0. F implies multiplicity (p,a) > 1 ) )
let a be Element of F; :: thesis: ( a is_a_root_of p implies ( ( multiplicity (p,a) = 1 implies eval (((Deriv F) . p),a) <> 0. F ) & ( eval (((Deriv F) . p),a) <> 0. F implies multiplicity (p,a) = 1 ) & ( multiplicity (p,a) > 1 implies eval (((Deriv F) . p),a) = 0. F ) & ( eval (((Deriv F) . p),a) = 0. F implies multiplicity (p,a) > 1 ) ) )
assume H: a is_a_root_of p ; :: thesis: ( ( multiplicity (p,a) = 1 implies eval (((Deriv F) . p),a) <> 0. F ) & ( eval (((Deriv F) . p),a) <> 0. F implies multiplicity (p,a) = 1 ) & ( multiplicity (p,a) > 1 implies eval (((Deriv F) . p),a) = 0. F ) & ( eval (((Deriv F) . p),a) = 0. F implies multiplicity (p,a) > 1 ) )
then AS: multiplicity (p,a) >= 1 by UPROOTS:52;
reconsider n = multiplicity (p,a) as non zero Element of NAT by H, UPROOTS:52;
consider r1 being Polynomial of F such that
H0: ((X- a) `^ n) *' r1 = p by RING_4:1, FIELD_14:67;
reconsider r = r1 as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
set R = Polynom-Ring F;
H4: ( r1 *' (1_. F) = r * (1. (Polynom-Ring F)) & (X- a) * ((Deriv F) . r) = (X- a) *' ((Deriv F) . r) ) by POLYNOM3:def 10;
H5: (Deriv F) . (X- a) = 1_. F by FIELD_14:61
.= 1. (Polynom-Ring F) by POLYNOM3:def 10 ;
H6: (Deriv F) . p = (Deriv F) . (((X- a) |^ n) * r) by H0, POLYNOM3:def 10
.= (r * ((Deriv F) . ((X- a) |^ n))) + (((X- a) |^ n) * ((Deriv F) . r)) by RINGDER1:def 1
.= (r * (n * (((X- a) |^ (n - 1)) * ((Deriv F) . (X- a))))) + (((X- a) |^ n) * ((Deriv F) . r)) by FIELD_14:63 ;

A: now :: thesis: ( multiplicity (p,a) = 1 implies eval (((Deriv F) . p),a) <> 0. F )

assume multiplicity (p,a) = 1 ; :: thesis: eval (((Deriv F) . p),a) <> 0. F
then (Deriv F) . p = (r * (((X- a) |^ 0) * ((Deriv F) . (X- a)))) + (((X- a) |^ 1) * ((Deriv F) . r)) by H6, BINOM:13
.= (r * ((1_ (Polynom-Ring F)) * ((Deriv F) . (X- a)))) + (((X- a) |^ 1) * ((Deriv F) . r)) by BINOM:8
.= (r * ((Deriv F) . (X- a))) + ((X- a) * ((Deriv F) . r)) by BINOM:8
.= (r1 *' (1_. F)) + ((X- a) *' ((Deriv F) . r)) by H5, H4, POLYNOM3:def 10 ;
then eval (((Deriv F) . p),a) = (eval ((r1 *' (1_. F)),a)) + (eval (((X- a) *' ((Deriv F) . r)),a)) by POLYNOM4:19
.= (eval (r1,a)) + ((eval ((X- a),a)) * (eval (((Deriv F) . r),a))) by POLYNOM4:24
.= (eval (r1,a)) + ((a - a) * (eval (((Deriv F) . r),a))) by HURWITZ:29
.= (eval (r1,a)) + ((0. F) * (eval (((Deriv F) . r),a))) by RLVECT_1:15
.= eval (r1,a) ;
hence eval (((Deriv F) . p),a) <> 0. F by multi4b, H0; :: thesis: verum

end;

B: now :: thesis: ( multiplicity (p,a) <> 1 implies eval (((Deriv F) . p),a) = 0. F )

assume I: multiplicity (p,a) <> 1 ; :: thesis: eval (((Deriv F) . p),a) = 0. F
reconsider n1 = n - 1 as Element of NAT by INT_1:3;
reconsider n1 = n1 as non zero Element of NAT by I;
B1: eval (((X- a) `^ n),a) = (power F) . ((eval ((rpoly (1,a)),a)),n) by POLYNOM5:22
.= (power F) . ((a - a),n) by HURWITZ:29
.= (0. F) |^ n by RLVECT_1:5
.= 0. F ;
B7: eval ((((X- a) `^ n) *' ((Deriv F) . r)),a) = (eval (((X- a) `^ n),a)) * (eval (((Deriv F) . r),a)) by POLYNOM4:24
.= 0. F by B1 ;
B2: eval (((X- a) `^ n1),a) = (power F) . ((eval ((rpoly (1,a)),a)),(n - 1)) by POLYNOM5:22
.= (power F) . ((a - a),(n - 1)) by HURWITZ:29
.= (0. F) |^ n1 by RLVECT_1:5
.= 0. F ;
B3: eval ((((X- a) `^ n1) *' ((Deriv F) . (X- a))),a) = (eval (((X- a) `^ n1),a)) * (eval (((Deriv F) . (X- a)),a)) by POLYNOM4:24
.= 0. F by B2 ;
reconsider h1 = ((X- a) `^ n1) *' ((Deriv F) . (X- a)) as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
reconsider h = n * h1 as Polynomial of F by POLYNOM3:def 10;
B5: eval (h,a) = 0. F by B3, multi4d;
B6: eval ((r1 *' h),a) = (eval (r1,a)) * (eval (h,a)) by POLYNOM4:24
.= 0. F by B5 ;
B8: ((X- a) |^ n) * ((Deriv F) . r) = ((X- a) `^ n) *' ((Deriv F) . r) by POLYNOM3:def 10;
h1 = ((X- a) |^ n1) * ((Deriv F) . (X- a)) by POLYNOM3:def 10;
then r1 *' h = r * (n * (((X- a) |^ (n - 1)) * ((Deriv F) . (X- a)))) by POLYNOM3:def 10;
then (Deriv F) . p = (r1 *' h) + (((X- a) `^ n) *' ((Deriv F) . r)) by B8, H6, POLYNOM3:def 10;
then eval (((Deriv F) . p),a) = (eval ((r1 *' h),a)) + (eval ((((X- a) `^ n) *' ((Deriv F) . r)),a)) by POLYNOM4:19;
hence eval (((Deriv F) . p),a) = 0. F by B6, B7; :: thesis: verum

end;

hence ( multiplicity (p,a) = 1 iff eval (((Deriv F) . p),a) <> 0. F ) by A; :: thesis: ( multiplicity (p,a) > 1 iff eval (((Deriv F) . p),a) = 0. F )
thus ( multiplicity (p,a) > 1 iff eval (((Deriv F) . p),a) = 0. F ) by A, B, AS, XXREAL_0:1; :: thesis: verum