let R be Field; :: thesis: for S1, S2 being non empty finite Subset of R
for p being Ppoly of R,S1
for a being Element of R
for q being non constant Polynomial of R st p = (rpoly (1,a)) *' q & S2 = S1 \ {a} holds
q is Ppoly of R,S2
let S1, S2 be non empty finite Subset of R; :: thesis: for p being Ppoly of R,S1
for a being Element of R
for q being non constant Polynomial of R st p = (rpoly (1,a)) *' q & S2 = S1 \ {a} holds
q is Ppoly of R,S2
let p be Ppoly of R,S1; :: thesis: for a being Element of R
for q being non constant Polynomial of R st p = (rpoly (1,a)) *' q & S2 = S1 \ {a} holds
q is Ppoly of R,S2
let a be Element of R; :: thesis: for q being non constant Polynomial of R st p = (rpoly (1,a)) *' q & S2 = S1 \ {a} holds
q is Ppoly of R,S2
let q be non constant Polynomial of R; :: thesis: ( p = (rpoly (1,a)) *' q & S2 = S1 \ {a} implies q is Ppoly of R,S2 )
assume A: ( p = (rpoly (1,a)) *' q & S2 = S1 \ {a} ) ; :: thesis: q is Ppoly of R,S2
then H: Roots (rpoly (1,a)) c= Roots p by ZZ3b, RING_4:1;
Roots (rpoly (1,a)) = {a} by RING_5:18;
then B: {a} c= S1 by H, RING_5:63;

C: now :: thesis: not a in S2

assume a in S2 ; :: thesis: contradiction
then not a in {a} by A, XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis: verum

end;

S2 \/ {a} = S1 \/ {a} by A, XBOOLE_1:39
.= S1 by B, XBOOLE_1:12 ;
hence q is Ppoly of R,S2 by A, C, r59a; :: thesis: verum