let C be non empty set ; :: thesis: for f being PartFunc of C,COMPLEX holds
( f ^ is total iff ( f " {0} = {} & f is total ) )
let f be PartFunc of C,COMPLEX; :: thesis: ( f ^ is total iff ( f " {0} = {} & f is total ) )
thus ( f ^ is total implies ( f " {0} = {} & f is total ) ) :: thesis: ( f " {0} = {} & f is total implies f ^ is total )

proof

assume f ^ is total ; :: thesis: ( f " {0} = {} & f is total )
then A1: dom (f ^) = C ;
f " {0c} c= C ;
then f " {0c} c= (dom f) \ (f " {0c}) by A1, Def2;
hence f " {0} = {} by XBOOLE_1:38; :: thesis: f is total
then C = (dom f) \ {} by A1, Def2;
hence dom f = C ; :: according to PARTFUN1:def 2 :: thesis: verum

end;

assume A2: ( f " {0} = {} & f is total ) ; :: thesis: f ^ is total
thus dom (f ^) = (dom f) \ (f " {0c}) by Def2
.= C by A2 ; :: according to PARTFUN1:def 2 :: thesis: verum