let R be domRing; :: thesis: for p, q being non zero Polynomial of R holds card (BRoots (p *' q)) = (card (BRoots p)) + (card (BRoots q))
let p, q be non zero Polynomial of R; :: thesis: card (BRoots (p *' q)) = (card (BRoots p)) + (card (BRoots q))
thus card (BRoots (p *' q)) = card ((BRoots p) + (BRoots q)) by UPROOTS:56
.= (card (BRoots p)) + (card (BRoots q)) by UPROOTS:15 ; :: thesis: verum