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

now

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

now

let n be Nat; :: thesis: ((h ") (#) (f /* h)) . n = 0
A2: rng h c= dom f by A1;
A3: n in NAT by ORDINAL1:def 12;
hence ((h ") (#) (f /* h)) . n = ((h ") . n) * ((f /* h) . n) by SEQ_1:8
.= ((h ") . n) * (f . (h . n)) by A3, A2, FUNCT_2:108
.= ((h ") . n) * 0 by FUNCOP_1:7
.= 0 ;
:: thesis: verum

end;

then ( (h ") (#) (f /* h) is constant & ((h ") (#) (f /* h)) . 0 = 0 ) by VALUED_0:def 18;
hence ( (h ") (#) (f /* h) is convergent & lim ((h ") (#) (f /* h)) = 0 ) by SEQ_4:25; :: 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