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 Th45;
then A1: support (BRoots <%(- x),(1. L)%>) = {x} by Def8;
A2: x in {x} by TARSKI:def 1;
now :: thesis: for i being object st i in the carrier of L holds
(BRoots <%(- x),(1. L)%>) . i = (({x},1) -bag) . i
let i be object ; :: thesis: ( i in the carrier of L implies (BRoots <%(- x),(1. L)%>) . b1 = (({x},1) -bag) . b1 )
assume i in the carrier of L ; :: thesis: (BRoots <%(- x),(1. L)%>) . b1 = (({x},1) -bag) . b1
then reconsider i1 = i as Element of L ;
per cases ( i = x or i <> x ) ;
suppose A3: i = x ; :: thesis: (BRoots <%(- x),(1. L)%>) . b1 = (({x},1) -bag) . b1
thus (BRoots <%(- x),(1. L)%>) . i = multiplicity (<%(- x),(1. L)%>,i1) by Def8
.= 1 by A3, Th50
.= (({x},1) -bag) . i by A2, A3, Th4 ; :: thesis: verum
end;
suppose i <> x ; :: thesis: (BRoots <%(- x),(1. L)%>) . b1 = (({x},1) -bag) . b1
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, Th3 ;
:: thesis: verum
end;
end;
end;
hence BRoots <%(- x),(1. L)%> = ({x},1) -bag by PBOOLE:3; :: thesis: verum