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