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

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