theorem Th4: :: FUNCT_1:4

for x being object
for f being Function st dom f = {x} holds
rng f = {(f . x)}