theorem :: FUNCT_1:86

for Y being set
for f, g, h being Function st Y = rng f & dom g = Y & dom h = Y & g * f = h * f holds
g = h