let f be complex-valued Function; :: thesis: (f ^ ) " {0 } = {}
assume A1: (f ^ ) " {0 } <> {} ; :: thesis: contradiction
consider x being Element of (f ^ ) " {0 };
A2: ( x in dom (f ^ ) & (f ^ ) . x in {0 } ) by A1, FUNCT_1:def 13;
then (f ^ ) . x = 0 by TARSKI:def 1;
then A3: (f . x) " = 0 by A2, Def8;
x in (dom f) \ (f " {0 }) by A2, Def8;
then ( x in dom f & not x in f " {0 } ) by XBOOLE_0:def 5;
then not f . x in {0 } by FUNCT_1:def 13;
hence contradiction by A3, TARSKI:def 1, XCMPLX_1:203; :: thesis: verum