let F be Field; :: thesis: for p, q being Polynomial of F
for r being non zero Polynomial of F st r *' q divides r *' p holds
q divides p
let p, q be Polynomial of F; :: thesis: for r being non zero Polynomial of F st r *' q divides r *' p holds
q divides p
let r be non zero Polynomial of F; :: thesis: ( r *' q divides r *' p implies q divides p )
assume r *' q divides r *' p ; :: thesis: q divides p
then consider u being Polynomial of F such that
A: (r *' q) *' u = r *' p by RING_4:1;
r *' p = r *' (q *' u) by A, POLYNOM3:33;
hence q divides p by RING_4:1, RATFUNC1:7; :: thesis: verum