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 )

A1: now

let n be Nat; :: thesis: ((h " ) (#) (f /* h)) . n = 0c
X: n in NAT by ORDINAL1:def 13;
dom f = COMPLEX by PARTFUN1:def 4;
then A2: rng h c= dom f ;
thus ((h " ) (#) (f /* h)) . n = ((h " ) . n) * ((f /* h) . n) by VALUED_1:5
.= ((h " ) . n) * (f /. (h . n)) by A2, FUNCT_2:185, X
.= ((h " ) . n) * 0c by FUNCOP_1:13
.= 0c ; :: thesis: verum

end;

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