for x, a being Element of F_Complex st x is algebraic & a <> 0. F_Complex & a in the carrier of (FQ_Ring x) holds
ex f, g being Element of (Polynom-Ring F_Rat) st
( {f} -Ideal = Ann_Poly (x,F_Rat) & not g in Ann_Poly (x,F_Rat) & a = (hom_Ext_eval (x,F_Rat)) . g & {f} -Ideal ,{g} -Ideal are_co-prime )