deffunc H₁( Nat) -> set = 1 / (c₁ + 1);
consider s1 being Real_Sequence such that
A1: for n being Nat holds s1 . n = H₁(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