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

(BRoots (b * p)) . o = (BRoots p) . o ;

hence BRoots (b * p) = BRoots p by PBOOLE:3; :: thesis: verum

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

then
for o being object st o in the carrier of F holds 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;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

(BRoots (b * p)) . o = (BRoots p) . o ;

hence BRoots (b * p) = BRoots p by PBOOLE:3; :: thesis: verum