let F be non degenerated comRing; :: thesis: for q being Polynomial of F
for p being non zero Polynomial of F
for b being non zero Element of F st q divides p holds
q divides b * p
let q be Polynomial of F; :: thesis: for p being non zero Polynomial of F
for b being non zero Element of F st q divides p holds
q divides b * p
let p be non zero Polynomial of F; :: thesis: for b being non zero Element of F st q divides p holds
q divides b * p
let b be non zero Element of F; :: thesis: ( q divides p implies q divides b * p )
assume q divides p ; :: thesis: q divides b * p
then consider r being Polynomial of F such that
A: p = q *' r by RING_4:1;
b * (r *' q) = (b * r) *' q by HURWITZ:19;
hence q divides b * p by A, RING_4:1; :: thesis: verum