rng f = the carrier of S by FUNCT_2:def 3;
then reconsider g = f " as Function of the carrier of S, the carrier of R by FUNCT_2:25;
g is Function of S,R ;
hence f " is Function of S,R ; :: thesis: verum