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:24;
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 7;
then eval (f,x) = 0. F_Complex by A2;
hence x is_a_root_of f by POLYNOM5:def 7; :: 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 7;
then eval (f,x) = 0. F_Complex by A2;
hence x is_a_root_of f by POLYNOM5:def 7; :: thesis: verum
end;
end;