let R be non degenerated comRing; :: thesis: for p, q being Polynomial of R
for a being Element of R st a is_a_root_of p holds
a is_a_root_of p *' q
let p, q be Polynomial of R; :: thesis: for a being Element of R st a is_a_root_of p holds
a is_a_root_of p *' q
let a be Element of R; :: thesis: ( a is_a_root_of p implies a is_a_root_of p *' q )
assume a is_a_root_of p ; :: thesis: a is_a_root_of p *' q
then eval (p,a) = 0. R by POLYNOM5:def 7;
then eval ((p *' q),a) = (0. R) * (eval (q,a)) by POLYNOM4:24
.= 0. R ;
hence a is_a_root_of p *' q by POLYNOM5:def 7; :: thesis: verum