let C be non empty set ; :: thesis: for f being PartFunc of C,COMPLEX holds (f ^ ) " {0 } = {}
let f be PartFunc of C,COMPLEX ; :: thesis: (f ^ ) " {0 } = {}
consider x being Element of (f ^ ) " {0c };
assume A1: (f ^ ) " {0 } <> {} ; :: thesis: contradiction
then A2: x in dom (f ^ ) by Lm1;
A3: (f ^ ) /. x in {0c } by A1, Lm1;
reconsider x = x as Element of C by A2;
x in (dom f) \ (f " {0c }) by A2, Def2;
then ( x in dom f & not x in f " {0c } ) by XBOOLE_0:def 5;
then A4: not f /. x in {0c } by PARTFUN2:44;
(f ^ ) /. x = 0c by A3, TARSKI:def 1;
then (f /. x) " = 0c by A2, Def2;
hence contradiction by A4, TARSKI:def 1, XCMPLX_1:203; :: thesis: verum