let F be domRing; :: thesis: for p being non zero Polynomial of F
for b being non zero Element of F holds BRoots (b * p) = BRoots p
let p be non zero Polynomial of F; :: thesis: for b being non zero Element of F holds BRoots (b * p) = BRoots p
let b be non zero Element of F; :: thesis: BRoots (b * p) = BRoots p

now :: thesis: for a being Element of F holds (BRoots (b * p)) . a = (BRoots p) . a

let a be Element of F; :: thesis: (BRoots (b * p)) . a = (BRoots p) . a
multiplicity (p,a) = multiplicity ((b * p),a) by multip1d;
hence (BRoots (b * p)) . a = multiplicity (p,a) by UPROOTS:def 9
.= (BRoots p) . a by UPROOTS:def 9 ;
:: thesis: verum

end;

then for o being object st o in the carrier of F holds
(BRoots (b * p)) . o = (BRoots p) . o ;
hence BRoots (b * p) = BRoots p by PBOOLE:3; :: thesis: verum