let K, L be Field; :: thesis: for w being Element of L st K is Subring of L & w is_integral_over K holds
Ann_Poly (w,K) is maximal
let w be Element of L; :: thesis: ( K is Subring of L & w is_integral_over K implies Ann_Poly (w,K) is maximal )
assume A1: ( K is Subring of L & w is_integral_over K ) ; :: thesis: Ann_Poly (w,K) is maximal
then consider g being Element of (Polynom-Ring K) such that
A2: ( g <> 0_. K & {g} -Ideal = Ann_Poly (w,K) & g = NormPolynomial g ) by ALGNUM_1:33;
A3: g <> 0. (Polynom-Ring K) by A2, POLYNOM3:def 10;
reconsider g1 = g as non zero Element of (Polynom-Ring K) by A3, STRUCT_0:def 12;
Ann_Poly (w,K) is prime by A1, ALGNUM_1:32;
then g1 is prime by A2, RING_2:24;
hence Ann_Poly (w,K) is maximal by A2, RING_2:26; :: thesis: verum