let F be Field; :: thesis: for q being Polynomial of F
for p being non zero Polynomial of F
for b being non zero Element of F holds
( q divides p iff 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 holds
( q divides p iff q divides b * p )
let p be non zero Polynomial of F; :: thesis: for b being non zero Element of F holds
( q divides p iff q divides b * p )
let b be non zero Element of F; :: thesis: ( q divides p iff q divides b * p )
X: b <> 0. F ;

now :: thesis: ( q divides b * p implies q divides p )

assume q divides b * p ; :: thesis: q divides p
then consider r being Polynomial of F such that
A: b * p = q *' r by RING_4:1;
q *' ((b ") * r) = (b ") * (q *' r) by HURWITZ:19
.= ((b ") * b) * p by A, HURWITZ:14
.= (1. F) * p by X, VECTSP_1:def 10
.= p ;
hence q divides p by RING_4:1; :: thesis: verum

end;

hence ( q divides p iff q divides b * p ) by divi1; :: thesis: verum