let f be complex-valued Function; :: thesis: (f ^ ) " {0 } = {}
consider x being Element of (f ^ ) " {0 };
assume A1: (f ^ ) " {0 } <> {} ; :: thesis: contradiction
then A2: x in dom (f ^ ) by FUNCT_1:def 13;
then A3: x in (dom f) \ (f " {0 }) by Def8;
then not x in f " {0 } by XBOOLE_0:def 5;
then A4: not f . x in {0 } by A3, FUNCT_1:def 13;
(f ^ ) . x in {0 } by A1, FUNCT_1:def 13;
then (f ^ ) . x = 0 by TARSKI:def 1;
then (f . x) " = 0 by A2, Def8;
hence contradiction by A4, TARSKI:def 1, XCMPLX_1:203; :: thesis: verum