let R be domRing; :: thesis: for p being Polynomial of R
for b being non zero Element of R holds Roots (b * p) = Roots p
let p be Polynomial of R; :: thesis: for b being non zero Element of R holds Roots (b * p) = Roots p
let b be non zero Element of R; :: thesis: Roots (b * p) = Roots p

A: now :: thesis: for o being object st o in Roots p holds
o in Roots (b * p)

let o be object ; :: thesis: ( o in Roots p implies o in Roots (b * p) )
assume B0: o in Roots p ; :: thesis: o in Roots (b * p)
then reconsider a = o as Element of R ;
a is_a_root_of p by B0, POLYNOM5:def 10;
then 0. R = eval (p,a) by POLYNOM5:def 7;
then eval ((b * p),a) = b * (0. R) by Th30
.= 0. R ;
then a is_a_root_of b * p by POLYNOM5:def 7;
hence o in Roots (b * p) by POLYNOM5:def 10; :: thesis: verum

end;

now :: thesis: for o being object st o in Roots (b * p) holds
o in Roots p

let o be object ; :: thesis: ( o in Roots (b * p) implies o in Roots p )
assume B0: o in Roots (b * p) ; :: thesis: o in Roots p
then reconsider a = o as Element of R ;
a is_a_root_of b * p by B0, POLYNOM5:def 10;
then 0. R = eval ((b * p),a) by POLYNOM5:def 7
.= b * (eval (p,a)) by Th30 ;
then eval (p,a) = 0. R by VECTSP_2:def 1;
then a is_a_root_of p by POLYNOM5:def 7;
hence o in Roots p by POLYNOM5:def 10; :: thesis: verum

end;

hence Roots (b * p) = Roots p by A, TARSKI:2; :: thesis: verum