theorem Th2: :: FUNCT_2:2

for Y being set
for f being Function st rng f c= Y holds
f is Function of (dom f),Y