let F be Field; :: thesis: for S being non empty finite Subset of F
for a being Element of F
for p being Ppoly of F,(S \/ {a})
for q being non constant Polynomial of F st p = (rpoly (1,a)) *' q & not a in S holds
q is Ppoly of F,S
let S be non empty finite Subset of F; :: thesis: for a being Element of F
for p being Ppoly of F,(S \/ {a})
for q being non constant Polynomial of F st p = (rpoly (1,a)) *' q & not a in S holds
q is Ppoly of F,S
let a be Element of F; :: thesis: for p being Ppoly of F,(S \/ {a})
for q being non constant Polynomial of F st p = (rpoly (1,a)) *' q & not a in S holds
q is Ppoly of F,S
let p be Ppoly of F,(S \/ {a}); :: thesis: for q being non constant Polynomial of F st p = (rpoly (1,a)) *' q & not a in S holds
q is Ppoly of F,S
let q be non constant Polynomial of F; :: thesis: ( p = (rpoly (1,a)) *' q & not a in S implies q is Ppoly of F,S )
assume A: ( p = (rpoly (1,a)) *' q & not a in S ) ; :: thesis: q is Ppoly of F,S
B1: Roots (rpoly (1,a)) = {a} by RING_5:18;
B2: rpoly (1,a) is Ppoly of F by RING_5:51;

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

let b be Element of F; :: thesis: ( b is_a_root_of rpoly (1,a) implies multiplicity ((rpoly (1,a)),b) = 1 )
assume b is_a_root_of rpoly (1,a) ; :: thesis: multiplicity ((rpoly (1,a)),b) = 1
then b in Roots (rpoly (1,a)) by POLYNOM5:def 10;
then b = a by B1, TARSKI:def 1;
hence multiplicity ((rpoly (1,a)),b) = 1 by RING_5:34; :: thesis: verum

end;

B3: rpoly (1,a) is Ppoly of F,{a} by B1, B2, B6, ZZ1;
B8: S \/ {a} = Roots p by RING_5:63;
B10: p is Ppoly of F,(Roots p) by RING_5:63;
B9: a in Roots (rpoly (1,a)) by B1, TARSKI:def 1;
B7: for b being Element of F st b is_a_root_of (rpoly (1,a)) *' q holds
multiplicity (((rpoly (1,a)) *' q),b) = 1 by A, B10, ZZ1;
C: S = Roots q

proof

C1: now :: thesis: for o being object st o in S holds
o in Roots q

let o be object ; :: thesis: ( o in S implies o in Roots q )
assume C2: o in S ; :: thesis: o in Roots q
then reconsider b = o as Element of F ;
b in S \/ {a} by C2, XBOOLE_0:def 3;
then b in Roots p by RING_5:63;
then C4: b is_a_root_of (rpoly (1,a)) *' q by A, POLYNOM5:def 10;
not b in {a} by C2, A, TARSKI:def 1;
then not b in Roots (rpoly (1,a)) by RING_5:18;
then not b is_a_root_of rpoly (1,a) by POLYNOM5:def 10;
then b is_a_root_of q by C4, ZZ1e;
hence o in Roots q by POLYNOM5:def 10; :: thesis: verum

end;

now :: thesis: for o being object st o in Roots q holds
o in S

let o be object ; :: thesis: ( o in Roots q implies o in S )
assume C2: o in Roots q ; :: thesis: o in S
then reconsider b = o as Element of F ;
C3: Roots q c= Roots p by A, ZZ1f;

now :: thesis: not b = a

assume b = a ; :: thesis: contradiction
then b in (Roots (rpoly (1,a))) /\ (Roots q) by B9, C2;
hence contradiction by B7, ZZ1d; :: thesis: verum

end;

then not b in {a} by TARSKI:def 1;
hence o in S by C2, C3, B8, XBOOLE_0:def 3; :: thesis: verum

end;

hence S = Roots q by C1, TARSKI:2; :: thesis: verum

end;

then ( not q is zero & q is with_roots & p is Ppoly of F,({a} \/ S) ) ;
hence q is Ppoly of F,S by A, B3, C, ZZ1a; :: thesis: verum