theorem Th17: :: ALGNUM_1:13

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