reconsider f = the carrier of S --> (0. T) as PartFunc of S,T ;
take f ; :: thesis: f is RestFunc-like
thus f is total ; :: according to NDIFF_1:def 5 :: thesis: for h being 0. S -convergent sequence of S st h is non-zero holds
( (||.h.|| ") (#) (f /* h) is convergent & lim ((||.h.|| ") (#) (f /* h)) = 0. T )
A1: dom f = the carrier of S ;
now :: thesis: for h being 0. S -convergent sequence of S st h is non-zero holds
( (||.h.|| ") (#) (f /* h) is convergent & lim ((||.h.|| ") (#) (f /* h)) = 0. T )
let h be 0. S -convergent sequence of S; :: thesis: ( h is non-zero implies ( (||.h.|| ") (#) (f /* h) is convergent & lim ((||.h.|| ") (#) (f /* h)) = 0. T ) )
assume h is non-zero ; :: thesis: ( (||.h.|| ") (#) (f /* h) is convergent & lim ((||.h.|| ") (#) (f /* h)) = 0. T )
now :: thesis: for n being Nat holds ((||.h.|| ") (#) (f /* h)) . n = 0. T
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 ;
A3: rng h c= dom f ;
A4: n in NAT by ORDINAL1:def 12;
thus ((||.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 Th18; :: thesis: verum
end;
hence for h being 0. S -convergent sequence of S st h is non-zero holds
( (||.h.|| ") (#) (f /* h) is convergent & lim ((||.h.|| ") (#) (f /* h)) = 0. T ) ; :: thesis: verum