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;

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

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

assume i in the carrier of L ; :: thesis: (BRoots <%(- x),(1. L)%>) . b_{1} = (({x},1) -bag) . b_{1}

then reconsider i1 = i as Element of L ;

end;assume i in the carrier of L ; :: thesis: (BRoots <%(- x),(1. L)%>) . b

then reconsider i1 = i as Element of L ;