let x, a be Element of F_Complex; ( 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)
; 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; verum