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

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