dom r = X by defr;
then r is Function of X,(rng r) by FUNCT_2:2;
hence r " is Function of (rng r),X by FUNCT_2:25; :: thesis: verum