:: deftheorem defines is_a_root_of FIELD_4:def 2 :
for R being Ring
for S being RingExtension of R
for p being Element of the carrier of (Polynom-Ring R)
for a being Element of S holds
( a is_a_root_of p,S iff Ext_eval (p,a) = 0. S );