theorem :: FUNCT_1:7

for y being object
for f, g being Function st dom f = dom g & rng f = {y} & rng g = {y} holds
f = g