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 ;

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

hence
rpoly (1,a) is Ppoly of R, Bag {a}
by A, dpp; :: thesis: verumlet c be Element of R; :: thesis: multiplicity (p,b_{1}) = (Bag {a}) . b_{1}

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

end;

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

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;thus multiplicity (p,c) = 1 by B, BR5aa

.= (Bag {a}) . c by C, UPROOTS:7 ; :: thesis: verum

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

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;thus multiplicity (p,c) = 0 by B, BR5aaa

.= (Bag {a}) . c by C, UPROOTS:6 ; :: thesis: verum