reconsider cf = REAL --> (In (0,REAL)) as Function of REAL,REAL ;
take f = cf; :: thesis: f is RestFunc-like
thus f is total ; :: according to FDIFF_1:def 2 :: thesis: for h being non-zero 0 -convergent Real_Sequence holds
( (h ") (#) (f /* h) is convergent & lim ((h ") (#) (f /* h)) = 0 )
now :: thesis: for h being non-zero 0 -convergent Real_Sequence holds
( (h ") (#) (f /* h) is convergent & lim ((h ") (#) (f /* h)) = 0 )
let h be non-zero 0 -convergent Real_Sequence; :: thesis: ( (h ") (#) (f /* h) is convergent & lim ((h ") (#) (f /* h)) = 0 )
now :: thesis: for n being Nat holds ((h ") (#) (f /* h)) . n = In (0,REAL)
let n be Nat; :: thesis: ((h ") (#) (f /* h)) . n = In (0,REAL)
A2: rng h c= dom f ;
A4: n in NAT by ORDINAL1:def 12;
thus ((h ") (#) (f /* h)) . n = ((h ") . n) * ((f /* h) . n) by SEQ_1:8
.= ((h ") . n) * (f . (h . n)) by A4, A2, FUNCT_2:108
.= ((h ") . n) * 0
.= In (0,REAL) ; :: thesis: verum
end;
then ( (h ") (#) (f /* h) is V8() & ((h ") (#) (f /* h)) . 0 = 0 ) by VALUED_0:def 18;
hence ( (h ") (#) (f /* h) is convergent & lim ((h ") (#) (f /* h)) = 0 ) by SEQ_4:25; :: thesis: verum
end;
hence for h being non-zero 0 -convergent Real_Sequence holds
( (h ") (#) (f /* h) is convergent & lim ((h ") (#) (f /* h)) = 0 ) ; :: thesis: verum