let F be Field; :: thesis: for p, q being non zero Polynomial of F
for a being Element of F st a is_a_root_of p *' q & not a is_a_root_of p holds
a is_a_root_of q
let p, q be non zero Polynomial of F; :: thesis: for a being Element of F st a is_a_root_of p *' q & not a is_a_root_of p holds
a is_a_root_of q
let a be Element of F; :: thesis: ( a is_a_root_of p *' q & not a is_a_root_of p implies a is_a_root_of q )
assume A: ( a is_a_root_of p *' q & not a is_a_root_of p ) ; :: thesis: a is_a_root_of q
C: eval (p,a) <> 0. F by A, POLYNOM5:def 7;
eval ((p *' q),a) = (eval (p,a)) * (eval (q,a)) by POLYNOM4:24;
then eval (q,a) = 0. F by C, A, POLYNOM5:def 7, VECTSP_2:def 1;
hence a is_a_root_of q by POLYNOM5:def 7; :: thesis: verum