theorem Th83: :: ALGNUM_1:52

for x, a being Element of F_Complex st a <> 0. F_Complex & a in the carrier of (FQ_Ring x) holds
ex g being Element of (Polynom-Ring F_Rat) st
( not g in Ann_Poly (x,F_Rat) & a = (hom_Ext_eval (x,F_Rat)) . g )