theorem Th71: :: MCART_1:87

for R being non empty Relation
for x being object holds Im (R,x) = { (I `2) where I is Element of R : I `1 = x }