deffunc H1( Nat) -> set = 1 / (c1 + 1);
consider s1 being Real_Sequence such that
A1: for n being Nat holds s1 . n = H1(n) from SEQ_1:sch 1();
 take s1 ; :: thesis: ( s1 is 0 -convergent & s1 is non-zero )
now :: thesis: for n being Nat holds s1 . n <> 0
let n be 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;
then A2: s1 is non-zero by SEQ_1:5;
( lim s1 = 0 & s1 is convergent ) by A1, SEQ_4:31;
then s1 is 0 -convergent ;
hence ( s1 is 0 -convergent & s1 is non-zero ) by A2; :: thesis: verum