let L be non degenerated comRing; :: thesis: for p being non-zero Polynomial of L
for x being Element of L holds
( x is_a_root_of p iff multiplicity p,x >= 1 )
let p be non-zero Polynomial of L; :: thesis: for x being Element of L holds
( x is_a_root_of p iff multiplicity p,x >= 1 )
let x be Element of L; :: thesis: ( x is_a_root_of p iff multiplicity p,x >= 1 )
set r = <%(- x),(1. L)%>;
set m = multiplicity p,x;
consider F being non empty finite Subset of NAT such that
A1: F = { k where k is Element of NAT : ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ k) *' q } and
A2: multiplicity p,x = max F by Def8;
multiplicity p,x in F by A2, XXREAL_2:def 8;
then consider k being Element of NAT such that
A3: multiplicity p,x = k and
A4: ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ k) *' q by A1;

hereby :: thesis: ( multiplicity p,x >= 1 implies x is_a_root_of p )

assume x is_a_root_of p ; :: thesis: multiplicity p,x >= 1
then A5: p = <%(- x),(1. L)%> *' (poly_quotient p,x) by Th52;
<%(- x),(1. L)%> `^ 1 = <%(- x),(1. L)%> by POLYNOM5:17;
then 1 in F by A1, A5;
hence multiplicity p,x >= 1 by A2, XXREAL_2:def 8; :: thesis: verum

end;

consider q being Polynomial of L such that
A6: p = (<%(- x),(1. L)%> `^ k) *' q by A4;
assume multiplicity p,x >= 1 ; :: thesis: x is_a_root_of p
then consider k1 being Nat such that
A7: k = k1 + 1 by A3, NAT_1:6;
reconsider k1 = k1 as Element of NAT by ORDINAL1:def 13;
p = (<%(- x),(1. L)%> *' (<%(- x),(1. L)%> `^ k1)) *' q by A6, A7, POLYNOM5:20
.= <%(- x),(1. L)%> *' ((<%(- x),(1. L)%> `^ k1) *' q) by POLYNOM3:34 ;
hence x is_a_root_of p by Th51; :: thesis: verum