let A be Ring; :: thesis: for B being comRing
for z being Element of B
for p, x being Element of (Polynom-Ring A) st A is Subring of B & x in Ann_Poly (z,A) holds
p * x in Ann_Poly (z,A)
let B be comRing; :: thesis: for z being Element of B
for p, x being Element of (Polynom-Ring A) st A is Subring of B & x in Ann_Poly (z,A) holds
p * x in Ann_Poly (z,A)
let w be Element of B; :: thesis: for p, x being Element of (Polynom-Ring A) st A is Subring of B & x in Ann_Poly (w,A) holds
p * x in Ann_Poly (w,A)
let p, x be Element of (Polynom-Ring A); :: thesis: ( A is Subring of B & x in Ann_Poly (w,A) implies p * x in Ann_Poly (w,A) )
assume that
A0: A is Subring of B and
A1: x in Ann_Poly (w,A) ; :: thesis: p * x in Ann_Poly (w,A)
set M = { p where p is Polynomial of A : Ext_eval (p,w) = 0. B } ;
reconsider p1 = p, x1 = x as Polynomial of A by POLYNOM3:def 10;
consider x2 being Polynomial of A such that
A2: x2 = x1 and
A3: Ext_eval (x2,w) = 0. B by A1;
Ext_eval ((p1 *' x1),w) = (Ext_eval (p1,w)) * (0. B) by A0, A2, A3, Th24
.= 0. B ;
then consider t being Polynomial of A such that
A4: t = p1 *' x1 and
A5: Ext_eval (t,w) = 0. B ;
p1 *' x1 in { p where p is Polynomial of A : Ext_eval (p,w) = 0. B } by A4, A5;
hence p * x in Ann_Poly (w,A) by POLYNOM3:def 10; :: thesis: verum