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)%>;
set j = multiplicity (<%(- x),(1. L)%>,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 <%(- x),(1. L)%> = (<%(- x),(1. L)%> `^ k) *' q } and
A2: multiplicity (<%(- x),(1. L)%>,x) = max F by Def7;
multiplicity (<%(- x),(1. L)%>,x) in F by A2, XXREAL_2:def 8;
then consider k being Element of NAT such that
A3: k = multiplicity (<%(- x),(1. L)%>,x) and
A4: ex q being Polynomial of L st <%(- x),(1. L)%> = (<%(- x),(1. L)%> `^ k) *' q by A1;
consider q being Polynomial of L such that
A5: <%(- x),(1. L)%> = (<%(- x),(1. L)%> `^ k) *' q by A4;
A6: len <%(- x),(1. L)%> = 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 <%(- x),(1. L)%> = 0_. L by A5, POLYNOM4:2;
hence contradiction by A6, POLYNOM4:3; :: thesis: verum
end;
then A8: q is non-zero by Th14;
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, Th37; :: thesis: verum
end;
<%(- x),(1. L)%> = <%(- x),(1. L)%> `^ 1 by POLYNOM5:16;
then <%(- x),(1. L)%> = (<%(- x),(1. L)%> `^ 1) *' (1_. L) by POLYNOM3:35;
then 1 in F by A1;
then multiplicity (<%(- x),(1. L)%>,x) >= 1 by A2, XXREAL_2:def 8;
hence multiplicity (<%(- x),(1. L)%>,x) = 1 by A3, A9, XXREAL_0:1; :: thesis: verum