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