let R be domRing; :: thesis: for a being Element of R holds rpoly (1,a) is Ppoly of R, Bag {a}
let a be Element of R; :: thesis: rpoly (1,a) is Ppoly of R, Bag {a}
reconsider p = rpoly (1,a) as Ppoly of R by lemppoly1;
A: deg p = 1 by HURWITZ:27
.= card {a} by CARD_1:30
.= card (({a},1) -bag) by UPROOTS:13 ;
now :: thesis: for c being Element of R holds multiplicity (p,c) = (Bag {a}) . c
let c be Element of R; :: thesis: multiplicity (p,b1) = (Bag {a}) . b1
per cases ( c = a or c <> a ) ;
suppose B: c = a ; :: thesis: multiplicity (p,b1) = (Bag {a}) . b1
then C: c in {a} by TARSKI:def 1;
thus multiplicity (p,c) = 1 by B, BR5aa
.= (Bag {a}) . c by C, UPROOTS:7 ; :: thesis: verum
end;
end;
end;
hence rpoly (1,a) is Ppoly of R, Bag {a} by A, dpp; :: thesis: verum