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);

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 )

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