let L be Field; :: thesis: for a being Element of L
for b being non zero Element of L holds BRoots <%a,b%> = ({(- (a / b))},1) -bag
let a be Element of L; :: thesis: for b being non zero Element of L holds BRoots <%a,b%> = ({(- (a / b))},1) -bag
let b be non zero Element of L; :: thesis: BRoots <%a,b%> = ({(- (a / b))},1) -bag
set r = <%a,b%>;
Roots <%a,b%> = {(- (a / b))} by Th10;
then A1: support (BRoots <%a,b%>) = {(- (a / b))} by UPROOTS:def 9;
A2: - (a / b) in {(- (a / b))} by TARSKI:def 1;

now :: thesis: for i being object st i in the carrier of L holds
(BRoots <%a,b%>) . i = (({(- (a / b))},1) -bag) . i

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

per cases ( i = - (a / b) or i <> - (a / b) ) ;

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

thus (BRoots <%a,b%>) . i = multiplicity (<%a,b%>,i1) by UPROOTS:def 9
.= 1 by A3, Th11
.= (({(- (a / b))},1) -bag) . i by A2, A3, UPROOTS:7 ; :: thesis: verum

end;

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

then A4: not i in {(- (a / b))} by TARSKI:def 1;
hence (BRoots <%a,b%>) . i = 0 by A1, PRE_POLY:def 7
.= (({(- (a / b))},1) -bag) . i by A4, UPROOTS:6 ;
:: thesis: verum

end;

end;

end;

hence BRoots <%a,b%> = ({(- (a / b))},1) -bag by PBOOLE:3; :: thesis: verum