let L be domRing; :: thesis: for x being Element of L holds BRoots <%(- x),(1. L)%> = {x},1 -bag
let x be Element of L; :: thesis: BRoots <%(- x),(1. L)%> = {x},1 -bag
set r = <%(- x),(1. L)%>;
Roots <%(- x),(1. L)%> = {x} by Th50;
then A1: support (BRoots <%(- x),(1. L)%>) = {x} by Def9;
A2: x in {x} by TARSKI:def 1;

now

let i be set ; :: thesis: ( i in the carrier of L implies (BRoots <%(- x),(1. L)%>) . b₁ = ({x},1 -bag ) . b₁ )
assume i in the carrier of L ; :: thesis: (BRoots <%(- x),(1. L)%>) . b₁ = ({x},1 -bag ) . b₁
then reconsider i1 = i as Element of L ;

per cases ( i = x or i <> x ) ;

suppose A3: i = x ; :: thesis: (BRoots <%(- x),(1. L)%>) . b₁ = ({x},1 -bag ) . b₁

thus (BRoots <%(- x),(1. L)%>) . i = multiplicity <%(- x),(1. L)%>,i1 by Def9
.= 1 by A3, Th55
.= ({x},1 -bag ) . i by A2, A3, Th9 ; :: thesis: verum

end;

suppose i <> x ; :: thesis: (BRoots <%(- x),(1. L)%>) . b₁ = ({x},1 -bag ) . b₁

then A4: not i in {x} by TARSKI:def 1;
hence (BRoots <%(- x),(1. L)%>) . i = 0 by A1, PRE_POLY:def 7
.= ({x},1 -bag ) . i by A4, Th8 ;
:: thesis: verum

end;

end;

end;

hence BRoots <%(- x),(1. L)%> = {x},1 -bag by PBOOLE:3; :: thesis: verum