( dom f = [#] R & rng f c= [#] S ) by FUNCT_2:def 1;
then f is Function of ([#] R),(rng f) by FUNCT_2:2;
hence f " is Function of (rng f),R by FUNCT_2:25; :: thesis: verum