for U being Grothendieck
for f being Function st dom f in U & rng f c= U holds
rng f in U