take f = cf; :: thesis: ( f is total & f is REST-like )
thus f is total ; :: thesis: f is REST-like
let h be convergent_to_0 Complex_Sequence; :: according to CFDIFF_1:def 3 :: thesis: ( (h ") (#) (f /* h) is convergent & lim ((h ") (#) (f /* h)) = 0 )

now

let n be Nat; :: thesis: ((h ") (#) (f /* h)) . n = 0c
dom f = COMPLEX by PARTFUN1:def 2;
then A1: ( n in NAT & rng h c= dom f ) by ORDINAL1:def 12;
thus ((h ") (#) (f /* h)) . n = ((h ") . n) * ((f /* h) . n) by VALUED_1:5
.= ((h ") . n) * (f /. (h . n)) by A1, FUNCT_2:108
.= ((h ") . n) * 0c by FUNCOP_1:7
.= 0c ; :: thesis: verum

end;

then ( (h ") (#) (f /* h) is constant & ((h ") (#) (f /* h)) . 0 = 0c ) by VALUED_0:def 18;
hence ( (h ") (#) (f /* h) is convergent & lim ((h ") (#) (f /* h)) = 0c ) by CFCONT_1:26, CFCONT_1:27; :: thesis: verum