let F be Field; :: thesis: for p, q being non zero Polynomial of F holds BRoots p divides BRoots (p *' q)
let p, q be non zero Polynomial of F; :: thesis: BRoots p divides BRoots (p *' q)

now :: thesis: for o being object holds (BRoots p) . o <= (BRoots (p *' q)) . o

let o be object ; :: thesis: (BRoots p) . b₁ <= (BRoots (p *' q)) . b₁

per cases ( o in support (BRoots p) or not o in support (BRoots p) ) ;

suppose o in support (BRoots p) ; :: thesis: (BRoots p) . b₁ <= (BRoots (p *' q)) . b₁

then reconsider a = o as Element of the carrier of F ;
( (BRoots p) . a = multiplicity (p,a) & (BRoots (p *' q)) . a = multiplicity ((p *' q),a) ) by UPROOTS:def 9;
hence (BRoots p) . o <= (BRoots (p *' q)) . o by ZZ7; :: thesis: verum

end;

suppose not o in support (BRoots p) ; :: thesis: (BRoots p) . b₁ <= (BRoots (p *' q)) . b₁

hence (BRoots p) . o <= (BRoots (p *' q)) . o by PRE_POLY:def 7; :: thesis: verum

end;

end;

end;

hence BRoots p divides BRoots (p *' q) by PRE_POLY:def 11; :: thesis: verum