reconsider f = the carrier of S --> (0. T) as PartFunc of S,T ;
take f ; :: thesis: f is REST-like
thus f is total ; :: according to NDIFF_1:def 5 :: thesis: for h being convergent_to_0 sequence of S holds
( (||.h.|| ") (#) (f /* h) is convergent & lim ((||.h.|| ") (#) (f /* h)) = 0. T )
A1: dom f = the carrier of S by FUNCOP_1:13;

now

let h be convergent_to_0 sequence of S; :: thesis: ( (||.h.|| ") (#) (f /* h) is convergent & lim ((||.h.|| ") (#) (f /* h)) = 0. T )

now

let n be Nat; :: thesis: ((||.h.|| ") (#) (f /* h)) . n = 0. T
A2: f /. (h . n) = f . (h . n) by A1, PARTFUN1:def 6
.= 0. T by FUNCOP_1:7 ;
A3: rng h c= dom f by A1;
A4: n in NAT by ORDINAL1:def 12;
hence ((||.h.|| ") (#) (f /* h)) . n = ((||.h.|| ") . n) * ((f /* h) . n) by Def2
.= ((||.h.|| ") . n) * (f /. (h . n)) by A3, A4, FUNCT_2:109
.= 0. T by A2, RLVECT_1:10 ;
:: thesis: verum

end;

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

end;

hence for h being convergent_to_0 sequence of S holds
( (||.h.|| ") (#) (f /* h) is convergent & lim ((||.h.|| ") (#) (f /* h)) = 0. T ) ; :: thesis: verum