let F be Field; :: thesis: for S being non empty finite Subset of F
for p being Ppoly of F,S
for q being non zero with_roots Polynomial of F st p *' q is Ppoly of F,(S \/ (Roots q)) holds
q is Ppoly of F,(Roots q)
let S be non empty finite Subset of F; :: thesis: for p being Ppoly of F,S
for q being non zero with_roots Polynomial of F st p *' q is Ppoly of F,(S \/ (Roots q)) holds
q is Ppoly of F,(Roots q)
let p be Ppoly of F,S; :: thesis: for q being non zero with_roots Polynomial of F st p *' q is Ppoly of F,(S \/ (Roots q)) holds
q is Ppoly of F,(Roots q)
let q be non zero with_roots Polynomial of F; :: thesis: ( p *' q is Ppoly of F,(S \/ (Roots q)) implies q is Ppoly of F,(Roots q) )
assume AS: p *' q is Ppoly of F,(S \/ (Roots q)) ; :: thesis: q is Ppoly of F,(Roots q)
then ( q *' p is Ppoly of F,(S \/ (Roots q)) & q is monic ) by ZZ3y;
then A: q is Ppoly of F by FIELD_8:10;
S = Roots p by RING_5:63;
then H: S \/ (Roots q) = Roots (p *' q) by UPROOTS:23;

now :: thesis: for a being Element of F st a is_a_root_of q holds
multiplicity (q,a) = 1

let a be Element of F; :: thesis: ( a is_a_root_of q implies multiplicity (q,a) = 1 )
assume B: a is_a_root_of q ; :: thesis: multiplicity (q,a) = 1
D: multiplicity (q,a) >= 1 by B, UPROOTS:52;

now :: thesis: not multiplicity (q,a) > 1

assume E: multiplicity (q,a) > 1 ; :: thesis: contradiction
multiplicity (q,a) <= multiplicity ((p *' q),a) by ZZ7;
hence contradiction by B, H, E, AS, ZZ1, ro1; :: thesis: verum

end;

hence multiplicity (q,a) = 1 by D, XXREAL_0:1; :: thesis: verum

end;

hence q is Ppoly of F,(Roots q) by A, ZZ1; :: thesis: verum