h is non-empty by FDIFF_1:def 1;
then A1: - h is non-empty by SEQ_1:53;
A2: h is convergent by FDIFF_1:def 1;
lim h = 0 by FDIFF_1:def 1;
then A3: lim (- h) = - 0 by A2, SEQ_2:24;
- h is convergent by A2, SEQ_2:23;
hence - h is convergent_to_0 Real_Sequence by A1, A3, FDIFF_1:def 1; :: thesis: verum