let F be Field; :: thesis: for a being Element of F
for p being Ppoly of F,{a} holds p = rpoly (1,a)
let a be Element of F; :: thesis: for p being Ppoly of F,{a} holds p = rpoly (1,a)
let p be Ppoly of F,{a}; :: thesis: p = rpoly (1,a)
deg p = card {a} by RING_5:60
.= 1 by CARD_2:42 ;
then consider x, z being Element of F such that
A: ( x <> 0. F & p = x * (rpoly (1,z)) ) by HURWITZ:28;
B: 1. F = LC p by RATFUNC1:def 7
.= x * (LC (rpoly (1,z))) by A, RING_5:5
.= x * (1. F) by RING_5:9 ;
( {a} = Roots p & Roots (rpoly (1,z)) = {z} ) by RING_5:18, RING_5:63;
then ( {a} = {z} & a in {a} ) by A, B, TARSKI:def 1;
hence p = rpoly (1,a) by A, B, TARSKI:def 1; :: thesis: verum