h is non-empty by FDIFF_1:def 1;
then A1: - h is non-empty by SEQ_1:45;
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:10;
- h is convergent by A2, SEQ_2:9;
hence - h is convergent_to_0 Real_Sequence by A1, A3, FDIFF_1:def 1; :: thesis: verum