set q = the non constant Polynomial of R;
( the non constant Polynomial of R `^ 2 = the non constant Polynomial of R *' the non constant Polynomial of R & the non constant Polynomial of R <> 0_. R ) by POLYNOM5:17;
then C: deg ( the non constant Polynomial of R `^ 2) = (deg the non constant Polynomial of R) + (deg the non constant Polynomial of R) by HURWITZ:23;
deg the non constant Polynomial of R >= 1 + 0 by NAT_1:13, RATFUNC1:def 2;
then reconsider r = the non constant Polynomial of R `^ 2 as non constant Polynomial of R by C, RATFUNC1:def 2;
take r ; :: thesis: not r is square-free
the non constant Polynomial of R `^ 2 = ( the non constant Polynomial of R `^ 2) *' (1_. R) ;
hence not r is square-free by lemsq, RING_4:1; :: thesis: verum