assume not f " {0 } is empty ; :: thesis: contradiction
then consider x being set such that
A1: x in f " {0 } by XBOOLE_0:def 1;
x in dom f by A1, FUNCT_1:def 13;
then A2: f . x in rng f by FUNCT_1:def 5;
f . x in {0 } by A1, FUNCT_1:def 13;
then f . x = 0 by TARSKI:def 1;
hence contradiction by A2, RELAT_1:def 9; :: thesis: verum