let F be Field; :: thesis: for p being non zero Polynomial of F
for q being Polynomial of F
for a being Element of F st p = ((X- a) `^ (multiplicity (p,a))) *' q holds
eval (q,a) <> 0. F
let p be non zero Polynomial of F; :: thesis: for q being Polynomial of F
for a being Element of F st p = ((X- a) `^ (multiplicity (p,a))) *' q holds
eval (q,a) <> 0. F
let q be Polynomial of F; :: thesis: for a being Element of F st p = ((X- a) `^ (multiplicity (p,a))) *' q holds
eval (q,a) <> 0. F
let a be Element of F; :: thesis: ( p = ((X- a) `^ (multiplicity (p,a))) *' q implies eval (q,a) <> 0. F )
assume AS: p = ((X- a) `^ (multiplicity (p,a))) *' q ; :: thesis: eval (q,a) <> 0. F
set n = multiplicity (p,a);

now :: thesis: not eval (q,a) = 0. F

assume eval (q,a) = 0. F ; :: thesis: contradiction
then consider r being Polynomial of F such that
A: q = (rpoly (1,a)) *' r by HURWITZ:33, POLYNOM5:def 7;
p = (((X- a) `^ (multiplicity (p,a))) *' (X- a)) *' r by AS, A, POLYNOM3:33
.= ((X- a) `^ ((multiplicity (p,a)) + 1)) *' r by POLYNOM5:19 ;
hence contradiction by FIELD_14:67, RING_4:1; :: thesis: verum

end;

hence eval (q,a) <> 0. F ; :: thesis: verum