theorem Lm45: :: ALGNUM_1:36

for A, B being Ring
for x being Element of B
for z being object st z in rng (hom_Ext_eval (x,A)) holds
z in B ;