reconsider p = rpoly (1,(1. R)) as non constant Polynomial of R ;
take p ; :: thesis: p is square-free

now :: thesis: for q being non constant Polynomial of R holds not q `^ 2 divides p

assume ex q being non constant Polynomial of R st q `^ 2 divides p ; :: thesis: contradiction
then consider q being non constant Polynomial of R such that
H: q `^ 2 divides p ;
consider r being Polynomial of R such that
A: p = (q `^ 2) *' r by H, RING_4:1;
F: ( q `^ 2 = q *' q & q <> 0_. R ) by POLYNOM5:17;
then C: deg (q `^ 2) = (deg q) + (deg q) by HURWITZ:23;
deg q >= 1 + 0 by NAT_1:13, RATFUNC1:def 2;
then E: deg (q `^ 2) >= 1 + 1 by C, XREAL_1:7;
r <> 0_. R by A;
then D: deg p = (deg (q `^ 2)) + (deg r) by A, F, HURWITZ:23;
not r is zero by A;
then I: deg p >= 2 + 0 by D, E, XREAL_1:7;
deg p = 1 by HURWITZ:27;
hence contradiction by I; :: thesis: verum

end;

hence p is square-free by lemsq; :: thesis: verum