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

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