theorem Th1: :: CQC_SIM1:1

for x, y being set
for f being Function holds Im ((f +* (x .--> y)),x) = {y}