let K, L be Field; :: thesis: for z being Element of L st z is_integral_over K holds
Ann_Poly (z,K) <> {(0. (Polynom-Ring K))}
let z be Element of L; :: thesis: ( z is_integral_over K implies Ann_Poly (z,K) <> {(0. (Polynom-Ring K))} )
assume A1: z is_integral_over K ; :: thesis: Ann_Poly (z,K) <> {(0. (Polynom-Ring K))}
set M = { p where p is Polynomial of K : Ext_eval (p,z) = 0. L } ;
consider f being Polynomial of K such that
A2: LC f = 1. K and
A3: Ext_eval (f,z) = 0. L by A1;
not f in {(0. (Polynom-Ring K))}
proof
assume A5: f in {(0. (Polynom-Ring K))} ; :: thesis: contradiction
reconsider f = f as Element of (Polynom-Ring K) by POLYNOM3:def 10;
f in {(0. (Polynom-Ring K))} -Ideal by A5, IDEAL_1:47;
then f in { ((0. (Polynom-Ring K)) * g) where g is Element of (Polynom-Ring K) : verum } by IDEAL_1:64;
then consider g1 being Element of (Polynom-Ring K) such that
A6: f = (0. (Polynom-Ring K)) * g1 ;
reconsider g2 = g1 as Polynomial of K by POLYNOM3:def 10;
reconsider h2 = 0. (Polynom-Ring K) as Polynomial of K by POLYNOM3:def 10;
f = 0_. K by POLYNOM3:def 10, A6;
hence contradiction by FUNCOP_1:7, A2; :: thesis: verum
end;
hence Ann_Poly (z,K) <> {(0. (Polynom-Ring K))} by A3; :: thesis: verum