for f being Function holds (pr1 ((dom f),(rng f))) .: f = dom f