A1: dom f = the carrier of X by FUNCT_2:def 1;
consider x being Element of dom f;
f . x in rng f by A1, 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