for A, B being Ring
for x being Element of B holds Ext_eval ((0_. A),x) = 0. B