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,b₁) = (Bag {a}) . b₁

per cases ( c = a or c <> a ) ;

suppose B: c = a ; :: thesis: multiplicity (p,b₁) = (Bag {a}) . b₁

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;

suppose B: c <> a ; :: thesis: multiplicity (p,b₁) = (Bag {a}) . b₁

then C: not c in {a} by TARSKI:def 1;
thus multiplicity (p,c) = 0 by B, BR5aaa
.= (Bag {a}) . c by C, UPROOTS:6 ; :: thesis: verum

end;

end;

end;

hence rpoly (1,a) is Ppoly of R, Bag {a} by A, dpp; :: thesis: verum