let L be Field; 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; for b being non zero Element of L holds multiplicity (<%a,b%>,(- (a / b))) = 1
let b be non zero Element of L; 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;
then A8:
q is non-zero
by UPROOTS:17;
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; verum