let L be non degenerated comRing; for x being Element of L holds multiplicity (<%(- x),(1. L)%>,x) = 1
let x be Element of L; 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;
then A8:
q is non-zero
by Th14;
<%(- 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; verum