let C be non empty set ; :: thesis: for f being PartFunc of C,REAL holds
( f ^ is total iff ( f " {0 } = {} & f is total ) )
let f be PartFunc of C,REAL ; :: 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 by PARTFUN1:def 4;
f " {0 } c= C ;
then f " {0 } c= (dom f) \ (f " {0 }) by A1, Def8;
hence f " {0 } = {} by XBOOLE_1:38; :: thesis: f is total
then C = (dom f) \ {} by A1, Def8;
hence dom f = C ; :: according to PARTFUN1:def 4 :: thesis: verum

end;

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