let L be non degenerated comRing; :: thesis: for x being Element of L holds multiplicity <%(- x),(1. L)%>,x = 1
let x be Element of L; :: thesis: multiplicity <%(- x),(1. L)%>,x = 1
set r = <%(- x),(1. L)%>;
A1: len <%(- x),(1. L)%> = 2 by POLYNOM5:41;
consider F being non empty finite Subset of NAT such that
A2: F = { k where k is Element of NAT : ex q being Polynomial of L st <%(- x),(1. L)%> = (<%(- x),(1. L)%> `^ k) *' q } and
A3: multiplicity <%(- x),(1. L)%>,x = max F by Def8;
<%(- x),(1. L)%> = <%(- x),(1. L)%> `^ 1 by POLYNOM5:17;
then <%(- x),(1. L)%> = (<%(- x),(1. L)%> `^ 1) *' (1_. L) by POLYNOM3:36;
then 1 in F by A2;
then A4: multiplicity <%(- x),(1. L)%>,x >= 1 by A3, XXREAL_2:def 8;
set j = multiplicity <%(- x),(1. L)%>,x;
multiplicity <%(- x),(1. L)%>,x in F by A3, XXREAL_2:def 8;
then consider k being Element of NAT such that
A5: k = multiplicity <%(- x),(1. L)%>,x and
A6: ex q being Polynomial of L st <%(- x),(1. L)%> = (<%(- x),(1. L)%> `^ k) *' q by A2;
consider q being Polynomial of L such that
A7: <%(- x),(1. L)%> = (<%(- x),(1. L)%> `^ k) *' q by A6;

B8: now

assume len q = 0 ; :: thesis: contradiction
then q = 0_. L by POLYNOM4:8;
then <%(- x),(1. L)%> = 0_. L by A7, POLYNOM4:5;
hence contradiction by A1, POLYNOM4:6; :: thesis: verum

end;

A9: q is non-zero by Th19, B8;

now

assume k > 1 ; :: thesis: contradiction
then k >= 1 + 1 by NAT_1:13;
then k + (len q) > 2 + 0 by B8, XREAL_1:10;
hence contradiction by A1, A7, A9, Th42; :: thesis: verum

end;

hence multiplicity <%(- x),(1. L)%>,x = 1 by A4, A5, XXREAL_0:1; :: thesis: verum