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

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)

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

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

o in Roots p

hence
Roots (b * p) = Roots p
by A, TARSKI:2; :: thesis: verumo 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;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