let R be domRing; :: thesis: for a being Element of R holds card (BRoots (rpoly (1,a))) = 1
let a be Element of R; :: thesis: card (BRoots (rpoly (1,a))) = 1
BRoots (rpoly (1,a)) = BRoots <%(- a),(1. R)%> by repr
.= ({a},1) -bag by UPROOTS:54 ;
then card (BRoots (rpoly (1,a))) = card {a} by UPROOTS:13;
hence card (BRoots (rpoly (1,a))) = 1 by CARD_1:30; :: thesis: verum