let R be non degenerated comRing; :: thesis: for p being Polynomial of R holds
( p is square-free iff for q being non constant Polynomial of R holds not q `^ 2 divides p )
let p be Polynomial of R; :: thesis: ( p is square-free iff for q being non constant Polynomial of R holds not q `^ 2 divides p )

A: now :: thesis: ( p is square-free implies for q being non constant Polynomial of R holds not q `^ 2 divides p )

assume p is square-free ; :: thesis: for q being non constant Polynomial of R holds not q `^ 2 divides p
then p is_square-free_over R ;
hence for q being non constant Polynomial of R holds not q `^ 2 divides p ; :: thesis: verum

end;

now :: thesis: ( ( for q being non constant Polynomial of R holds not q `^ 2 divides p ) implies p is square-free )

assume for q being non constant Polynomial of R holds not q `^ 2 divides p ; :: thesis: p is square-free
then p is_square-free_over R ;
hence p is square-free ; :: thesis: verum

end;

hence ( p is square-free iff for q being non constant Polynomial of R holds not q `^ 2 divides p ) by A; :: thesis: verum