consider x being Element of dom f;
dom f = the carrier of X by FUNCT_2:def 1;
then f . x in rng f by FUNCT_1:def 5;
then reconsider A = rng f as non empty Subset of Y ;
the carrier of (Image f) = [#] (Image f)
.= A by PRE_TOPC:def 10 ;
hence not the carrier of (Image f) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum