( the carrier of (Image f) = rng f & the carrier of X = dom f ) by Th9, FUNCT_2:def 1;
hence f is Function of X,(Image f) by FUNCT_2:1; :: thesis: verum