take f = REAL --> (0. F); :: thesis: f is RestFunc-like
thus f is total ; :: according to NDIFF_3:def 1 :: thesis: for h being non-zero 0 -convergent Real_Sequence holds
( (h ") (#) (f /* h) is convergent & lim ((h ") (#) (f /* h)) = 0. F )

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

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

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

let n be Nat; :: thesis: ((h ") (#) (f /* h)) . n = 0. F
A2: rng h c= dom f ;
A3: n in NAT by ORDINAL1:def 12;
thus ((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 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 non-zero 0 -convergent Real_Sequence holds
( (h ") (#) (f /* h) is convergent & lim ((h ") (#) (f /* h)) = 0. F ) ; :: thesis: verum