let K, L be Field; :: thesis: 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
let z be Element of L; :: thesis: 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
let f, g be Element of (Polynom-Ring K); :: thesis: ( z is_integral_over K & {f} -Ideal = Ann_Poly (z,K) & f = NormPolynomial f & {g} -Ideal = Ann_Poly (z,K) & g = NormPolynomial g implies f = g )
assume that
A1: z is_integral_over K and
A2: {f} -Ideal = Ann_Poly (z,K) and
A3: f = NormPolynomial f and
A4: {g} -Ideal = Ann_Poly (z,K) and
A5: g = NormPolynomial g ; :: thesis: f = g
reconsider f = f as Element of the carrier of (Polynom-Ring K) ;
NormPolynomial f <> 0. (Polynom-Ring K) by A3, A2, A1, Th35, IDEAL_1:47;
then f <> 0_. K by A3, POLYNOM3:def 10;
then A6: f is non zero Element of the carrier of (Polynom-Ring K) by Lm37;
reconsider g = g as Element of the carrier of (Polynom-Ring K) ;
NormPolynomial g <> 0. (Polynom-Ring K) by A5, A4, A1, Th35, IDEAL_1:47;
then g <> 0_. K by A5, POLYNOM3:def 10;
then g is non zero Element of the carrier of (Polynom-Ring K) by Lm37;
hence f = g by A3, A6, A5, RING_2:21, RING_4:30, A4, A2; :: thesis: verum