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 ;

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 )

hence
( q divides p iff q divides b * p )
by divi1; :: thesis: verumassume
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;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