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

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