let L be Field; :: thesis: for a being Element of L
for b being non zero Element of L holds multiplicity (<%a,b%>,(- (a / b))) = 1
let a be Element of L; :: thesis: for b being non zero Element of L holds multiplicity (<%a,b%>,(- (a / b))) = 1
let b be non zero Element of L; :: thesis: multiplicity (<%a,b%>,(- (a / b))) = 1
set p = <%a,b%>;
set x = - (a / b);
set r = <%(- (- (a / b))),(1. L)%>;
set j = multiplicity (<%a,b%>,(- (a / b)));
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 <%a,b%> = (<%(- (- (a / b))),(1. L)%> `^ k) *' q } and
A2: multiplicity (<%a,b%>,(- (a / b))) = max F by UPROOTS:def 8;
multiplicity (<%a,b%>,(- (a / b))) in F by A2, XXREAL_2:def 8;
then consider k being Element of NAT such that
A3: k = multiplicity (<%a,b%>,(- (a / b))) and
A4: ex q being Polynomial of L st <%a,b%> = (<%(- (- (a / b))),(1. L)%> `^ k) *' q by A1;
consider q being Polynomial of L such that
A5: <%a,b%> = (<%(- (- (a / b))),(1. L)%> `^ k) *' q by A4;
b <> 0. L ;
then A6: len <%a,b%> = 2 by POLYNOM5:40;

A7: now :: thesis: not len q = 0

assume len q = 0 ; :: thesis: contradiction
then q = 0_. L by POLYNOM4:5;
then <%a,b%> = 0_. L by A5, POLYNOM4:2;
hence contradiction by A6, POLYNOM4:3; :: thesis: verum

end;

then A8: q is non-zero by UPROOTS:17;

A9: now :: thesis: not k > 1

assume k > 1 ; :: thesis: contradiction
then k >= 1 + 1 by NAT_1:13;
then k + (len q) > 2 + 0 by A7, XREAL_1:8;
hence contradiction by A6, A5, A8, UPROOTS:40; :: thesis: verum

end;

multiplicity (<%a,b%>,(- (a / b))) >= 1 by Th9, UPROOTS:52;
then k = 1 by A3, A9, XXREAL_0:1;
then 1 in F by A1, A5;
then multiplicity (<%a,b%>,(- (a / b))) >= 1 by A2, XXREAL_2:def 8;
hence multiplicity (<%a,b%>,(- (a / b))) = 1 by A3, A9, XXREAL_0:1; :: thesis: verum