theorem :: FUNCT_2:1

for f being Function holds f is Function of (dom f),(rng f)