let R be non degenerated Ring; :: thesis: for a being Element of R holds Roots (rpoly (1,a)) = {a}
let a be Element of R; :: thesis: Roots (rpoly (1,a)) = {a}
set p = rpoly (1,a);
A: now :: thesis: for u being object st u in {a} holds
u in Roots (rpoly (1,a))
let u be object ; :: thesis: ( u in {a} implies u in Roots (rpoly (1,a)) )
assume u in {a} ; :: thesis: u in Roots (rpoly (1,a))
then A: u = a by TARSKI:def 1;
eval ((rpoly (1,a)),a) = a - a by HURWITZ:29
.= 0. R by RLVECT_1:15 ;
then a is_a_root_of rpoly (1,a) by POLYNOM5:def 7;
hence u in Roots (rpoly (1,a)) by A, POLYNOM5:def 10; :: thesis: verum
end;
now :: thesis: for u being object st u in Roots (rpoly (1,a)) holds
u in {a}
let u be object ; :: thesis: ( u in Roots (rpoly (1,a)) implies u in {a} )
assume B: u in Roots (rpoly (1,a)) ; :: thesis: u in {a}
then reconsider x = u as Element of R ;
x is_a_root_of rpoly (1,a) by B, POLYNOM5:def 10;
then 0. R = eval ((rpoly (1,a)),x) by POLYNOM5:def 7
.= x - a by HURWITZ:29 ;
then a = x by RLVECT_1:21;
hence u in {a} by TARSKI:def 1; :: thesis: verum
end;
hence Roots (rpoly (1,a)) = {a} by A, TARSKI:2; :: thesis: verum