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

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