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