let f, g, h be Polynomial of F_Complex ; :: thesis: ( f = g *' h implies for x being Element of F_Complex st ( x is_a_root_of g or x is_a_root_of h ) holds
x is_a_root_of f )
assume A1: f = g *' h ; :: thesis: for x being Element of F_Complex st ( x is_a_root_of g or x is_a_root_of h ) holds
x is_a_root_of f
let x be Element of F_Complex ; :: thesis: ( ( x is_a_root_of g or x is_a_root_of h ) implies x is_a_root_of f )
A2: eval f,x = (eval g,x) * (eval h,x) by A1, POLYNOM4:27;
assume A3: ( x is_a_root_of g or x is_a_root_of h ) ; :: thesis: x is_a_root_of f

per cases ( x is_a_root_of g or x is_a_root_of h ) by A3;

suppose x is_a_root_of g ; :: thesis: x is_a_root_of f

then eval g,x = 0. F_Complex by POLYNOM5:def 6;
then eval f,x = 0. F_Complex by A2, VECTSP_1:39;
hence x is_a_root_of f by POLYNOM5:def 6; :: thesis: verum

end;

suppose x is_a_root_of h ; :: thesis: x is_a_root_of f

then eval h,x = 0. F_Complex by POLYNOM5:def 6;
then eval f,x = 0. F_Complex by A2, VECTSP_1:36;
hence x is_a_root_of f by POLYNOM5:def 6; :: thesis: verum

end;

end;