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 ;
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;
assume that
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