let C be non empty set ; for f being PartFunc of C,COMPLEX holds (f ^) " {0} = {}
let f be PartFunc of C,COMPLEX; (f ^) " {0} = {}
set x = the Element of (f ^) " {0c};
assume A1:
(f ^) " {0} <> {}
; contradiction
then A2:
the Element of (f ^) " {0c} in dom (f ^)
by Lm1;
A3:
(f ^) /. the Element of (f ^) " {0c} in {0c}
by A1, Lm1;
reconsider x = the Element of (f ^) " {0c} 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:26;
(f ^) /. x = 0c
by A3, TARSKI:def 1;
then
(f /. x) " = 0c
by A2, Def2;
hence
contradiction
by A4, TARSKI:def 1, XCMPLX_1:202; verum