for R being non degenerated Ring
for S being RingExtension of R
for a being Element of S holds Ext_eval ((1_. R),a) = 1. S