assume not f " {0} is empty ; :: thesis: contradiction
then consider x being object such that
A1: x in f " {0} by XBOOLE_0:def 1;
x in dom f by A1, FUNCT_1:def 7;
then A2: f . x in rng f by FUNCT_1:def 3;
f . x in {0} by A1, FUNCT_1:def 7;
hence contradiction by A2, TARSKI:def 1; :: thesis: verum