deffunc H₁( Element of NAT ) -> Element of REAL = 1 / (c₁ + 1);
consider s1 being Real_Sequence such that
A1: for n being Element of NAT holds s1 . n = H₁(n) from SEQ_1:sch 1();
take s1 ; :: thesis: s1 is convergent_to_0

now

let n be Element of NAT ; :: thesis: s1 . n <> 0
(n + 1) " <> 0 ;
then 1 / (n + 1) <> 0 by XCMPLX_1:215;
hence s1 . n <> 0 by A1; :: thesis: verum

end;

hence s1 is non-zero by SEQ_1:5; :: according to FDIFF_1:def 1 :: thesis: ( s1 is convergent & lim s1 = 0 )
thus ( s1 is convergent & lim s1 = 0 ) by A1, SEQ_4:30; :: thesis: verum