deffunc H_{1}( Nat) -> set = 1 / (c_{1} + 1);

consider s1 being Real_Sequence such that

A1: for n being Nat holds s1 . n = H_{1}(n)
from SEQ_1:sch 1();

take s1 ; :: thesis: ( s1 is 0 -convergent & s1 is non-zero )

( 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

consider s1 being Real_Sequence such that

A1: for n being Nat holds s1 . n = H

take s1 ; :: thesis: ( s1 is 0 -convergent & s1 is non-zero )

now :: thesis: for n being Nat holds s1 . n <> 0

then A2:
s1 is non-zero
by SEQ_1:5;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;(n + 1) " <> 0 ;

then 1 / (n + 1) <> 0 by XCMPLX_1:215;

hence s1 . n <> 0 by A1; :: thesis: verum

( 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