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;

then f . x = 0 by TARSKI:def 1;

hence contradiction by A2; :: thesis: verum

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;

then f . x = 0 by TARSKI:def 1;

hence contradiction by A2; :: thesis: verum