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 } = {}
assume A1: (f ^ ) " {0 } <> {} ; :: thesis: contradiction
consider x being Element of (f ^ ) " {0c };
A2: ( x in dom (f ^ ) & (f ^ ) /. x in {0c } ) by A1, Lm1;
then reconsider x = x as Element of C ;
(f ^ ) /. x = 0c by A2, TARSKI:def 1;
then A3: (f /. x) " = 0c by A2, Def2;
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 not f /. x in {0c } by PARTFUN2:44;
hence contradiction by A3, TARSKI:def 1, XCMPLX_1:203; :: thesis: verum