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;

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

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

then A8:
q is non-zero
by Th14;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 q = 0_. L by POLYNOM4:5;

then <%(- x),(1. L)%> = 0_. L by A5, POLYNOM4:2;

hence contradiction by A6, POLYNOM4:3; :: thesis: verum

A9: now :: thesis: not k > 1

<%(- x),(1. L)%> = <%(- x),(1. L)%> `^ 1
by POLYNOM5:16;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;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

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