theorem Th5: :: FUNCT_1:5

for X being set st X <> {} holds
for y being object ex f being Function st
( dom f = X & rng f = {y} )