A1: the carrier of (Image f) = rng f by Th10;
then ( the carrier of (Image f) | f = f & the carrier of X = dom f ) by FUNCT_2:def 1, RELAT_1:125;
hence f is Function of X,(Image f) by A1, FUNCT_2:3; :: thesis: verum