let R be domRing; :: thesis: for a, b being Element of R holds
( rpoly (1,a) divides rpoly (1,b) iff a = b )
let a, b be Element of R; :: thesis: ( rpoly (1,a) divides rpoly (1,b) iff a = b )
X: now :: thesis: ( rpoly (1,a) divides rpoly (1,b) implies a = b )
assume rpoly (1,a) divides rpoly (1,b) ; :: thesis: a = b
then consider p being Polynomial of R such that
A: (rpoly (1,a)) *' p = rpoly (1,b) by RING_4:1;
B: {b} = Roots (rpoly (1,b)) by ro4
.= (Roots (rpoly (1,a))) \/ (Roots p) by A, UPROOTS:23 ;
a in {a} by TARSKI:def 1;
then a in Roots (rpoly (1,a)) by ro4;
then a in {b} by B, XBOOLE_0:def 3;
hence a = b by TARSKI:def 1; :: thesis: verum
end;
now :: thesis: ( a = b implies rpoly (1,a) divides rpoly (1,b) )
assume a = b ; :: thesis: rpoly (1,a) divides rpoly (1,b)
then (rpoly (1,a)) *' (1_. R) = rpoly (1,b) ;
hence rpoly (1,a) divides rpoly (1,b) by RING_4:1; :: thesis: verum
end;
hence ( rpoly (1,a) divides rpoly (1,b) iff a = b ) by X; :: thesis: verum