theorem :: FUNCT_3:79

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