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

now :: thesis: for h being non-zero 0 -convergent Real_Sequence holds
( (h ") (#) (f /* h) is convergent & lim ((h ") (#) (f /* h)) = 0 )

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

now :: thesis: for n being Nat holds ((h ") (#) (f /* h)) . n = In (0,REAL)

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

end;

then ( (h ") (#) (f /* h) is V8() & ((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 non-zero 0 -convergent Real_Sequence holds
( (h ") (#) (f /* h) is convergent & lim ((h ") (#) (f /* h)) = 0 ) ; :: thesis: verum