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 )

A2: f " {0} = {} and

A3: f is total ; :: thesis: f ^ is total

thus dom (f ^) = (dom f) \ (f " {0}) by Def2

.= C by A2, A3 ; :: according to PARTFUN1:def 2 :: thesis: verum

( 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 that
assume
f ^ is total
; :: thesis: ( f " {0} = {} & f is total )

then A1: dom (f ^) = C ;

f " {0} c= C ;

then f " {0} c= (dom f) \ (f " {0}) 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;then A1: dom (f ^) = C ;

f " {0} c= C ;

then f " {0} c= (dom f) \ (f " {0}) 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

A2: f " {0} = {} and

A3: f is total ; :: thesis: f ^ is total

thus dom (f ^) = (dom f) \ (f " {0}) by Def2

.= C by A2, A3 ; :: according to PARTFUN1:def 2 :: thesis: verum