theorem :: FIELD_4:22

for R, S being Ring
for a being Element of S st S is RingExtension of R holds
Ext_eval ((0_. R),a) = 0. S by ALGNUM_1:13;