theorem Th41: :: ALGNUM_1:34

for K, L being Field
for z being Element of L
for f, g being Element of (Polynom-Ring K) st z is_integral_over K & {f} -Ideal = Ann_Poly (z,K) & f = NormPolynomial f & {g} -Ideal = Ann_Poly (z,K) & g = NormPolynomial g holds
f = g