let x, a be Element of F_Complex; :: thesis: ( x is algebraic & a <> 0. F_Complex & a in the carrier of (FQ_Ring x) implies 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 ) )
assume that
A1: x is algebraic and
A2: a <> 0. F_Complex and
A3: a in the carrier of (FQ_Ring x) ; :: thesis: 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 )
consider f being Element of (Polynom-Ring F_Rat) such that
A4: {f} -Ideal = Ann_Poly (x,F_Rat) by Th34, Th3;
consider g being Element of (Polynom-Ring F_Rat) such that
A5: not g in Ann_Poly (x,F_Rat) and
A6: a = (hom_Ext_eval (x,F_Rat)) . g by Th83, A2, A3;
A7: {f} -Ideal is prime by A4, A1, Th3, Th39;
A8: f <> 0. (Polynom-Ring F_Rat) by A1, A4, Th35, IDEAL_1:47;
{f} -Ideal ,{g} -Ideal are_co-prime by A4, A5, A7, A8, Th81;
hence 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 ) by A4, A5, A6; :: thesis: verum