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

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