let F be domRing; :: thesis: for p being non zero Polynomial of F
for a being Element of F
for b being non zero Element of F holds
( rpoly (1,a) divides p iff rpoly (1,a) divides b * p )
let p be non zero Polynomial of F; :: thesis: for a being Element of F
for b being non zero Element of F holds
( rpoly (1,a) divides p iff rpoly (1,a) divides b * p )
let a be Element of F; :: thesis: for b being non zero Element of F holds
( rpoly (1,a) divides p iff rpoly (1,a) divides b * p )
let b be non zero Element of F; :: thesis: ( rpoly (1,a) divides p iff rpoly (1,a) divides b * p )
set q = rpoly (1,a);

now :: thesis: ( rpoly (1,a) divides b * p implies rpoly (1,a) divides p )

assume rpoly (1,a) divides b * p ; :: thesis: rpoly (1,a) divides p
then 0. F = eval ((b * p),a) by Th9
.= b * (eval (p,a)) by Th30 ;
then eval (p,a) = 0. F by VECTSP_2:def 1;
hence rpoly (1,a) divides p by Th9; :: thesis: verum

end;

hence ( rpoly (1,a) divides p iff rpoly (1,a) divides b * p ) by divi1; :: thesis: verum