let R be domRing; :: thesis: for S being non empty finite Subset of R
for p being Ppoly of R,S
for a being Element of R st a in S holds
( rpoly (1,a) divides p & not (rpoly (1,a)) `^ 2 divides p )
let S be non empty finite Subset of R; :: thesis: for p being Ppoly of R,S
for a being Element of R st a in S holds
( rpoly (1,a) divides p & not (rpoly (1,a)) `^ 2 divides p )
let p be Ppoly of R,S; :: thesis: for a being Element of R st a in S holds
( rpoly (1,a) divides p & not (rpoly (1,a)) `^ 2 divides p )
let a be Element of R; :: thesis: ( a in S implies ( rpoly (1,a) divides p & not (rpoly (1,a)) `^ 2 divides p ) )
assume a in S ; :: thesis: ( rpoly (1,a) divides p & not (rpoly (1,a)) `^ 2 divides p )
then A: (Bag S) . a = 1 by UPROOTS:7;
X: ( (rpoly (1,a)) `^ ((Bag S) . a) divides p & not (rpoly (1,a)) `^ (((Bag S) . a) + 1) divides p ) by pf1;
hence rpoly (1,a) divides p by A, POLYNOM5:16; :: thesis: not (rpoly (1,a)) `^ 2 divides p
thus not (rpoly (1,a)) `^ 2 divides p by A, X; :: thesis: verum