theorem alg0: :: FIELD_6:41

for R being Ring
for S being RingExtension of R
for a being Element of S holds Ann_Poly (a,R) = ker (hom_Ext_eval (a,R))