take f = REAL --> (0. F); :: thesis: f is REST-like
thus f is total ; :: according to NDIFF_3:def 1 :: thesis: for h being convergent_to_0 Real_Sequence holds
( (h ") (#) (f /* h) is convergent & lim ((h ") (#) (f /* h)) = 0. F )
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. F )

now

let n be Nat; :: thesis: ((h ") (#) (f /* h)) . n = 0. F
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 NDIFF_1:def 2
.= ((h ") . n) * (f . (h . n)) by A3, A2, FUNCT_2:108
.= 0. F by FUNCOP_1:7, RLVECT_1:10 ;
:: thesis: verum

end;

then ( (h ") (#) (f /* h) is constant & ((h ") (#) (f /* h)) . 0 = 0. F ) by VALUED_0:def 18;
hence ( (h ") (#) (f /* h) is convergent & lim ((h ") (#) (f /* h)) = 0. F ) by NDIFF_1:18; :: thesis: verum

end;

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