take f = cf; :: thesis: f is REST-like
A1: dom f = REAL by FUNCOP_1:19;
thus f is total ; :: according to FDIFF_1:def 3 :: thesis: for h being convergent_to_0 Real_Sequence holds
( (h " ) (#) (f /* h) is convergent & lim ((h " ) (#) (f /* h)) = 0 )

now

let h be convergent_to_0 Real_Sequence; :: thesis: ( (h " ) (#) (f /* h) is convergent & lim ((h " ) (#) (f /* h)) = 0 )

A2: now

let n be Nat; :: thesis: ((h " ) (#) (f /* h)) . n = 0
X: n in NAT by ORDINAL1:def 13;
A3: rng h c= dom f by A1;
thus ((h " ) (#) (f /* h)) . n = ((h " ) . n) * ((f /* h) . n) by X, SEQ_1:12
.= ((h " ) . n) * (f . (h . n)) by A3, X, FUNCT_2:185
.= ((h " ) . n) * 0 by FUNCOP_1:13
.= 0 ; :: thesis: verum

end;

then A4: (h " ) (#) (f /* h) is V8() by VALUED_0:def 18;
((h " ) (#) (f /* h)) . 0 = 0 by A2;
hence ( (h " ) (#) (f /* h) is convergent & lim ((h " ) (#) (f /* h)) = 0 ) by A4, SEQ_4:40; :: thesis: verum

end;

hence for h being convergent_to_0 Real_Sequence holds
( (h " ) (#) (f /* h) is convergent & lim ((h " ) (#) (f /* h)) = 0 ) ; :: thesis: verum