theorem Th2: :: CLASSES3:2

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