let K, L be Field; :: thesis: for w being Element of L st K is Subring of L holds
ex g being Element of (Polynom-Ring K) st {g} -Ideal = Ann_Poly (w,K)
let w be Element of L; :: thesis: ( K is Subring of L implies ex g being Element of (Polynom-Ring K) st {g} -Ideal = Ann_Poly (w,K) )
assume A0: K is Subring of L ; :: thesis: ex g being Element of (Polynom-Ring K) st {g} -Ideal = Ann_Poly (w,K)
A1: Polynom-Ring K is PID ;
Ann_Poly (w,K) is Ideal of (Polynom-Ring K) by A0, Th33;
hence ex g being Element of (Polynom-Ring K) st {g} -Ideal = Ann_Poly (w,K) by A1, IDEAL_1:def 27; :: thesis: verum