consider x0 being Point of S such that
A1: x0 <> 0. S by STRUCT_0:def 19;
deffunc H₁( Element of NAT ) -> Element of the carrier of S = (1 / (S + 1)) * x0;
consider s1 being sequence of S such that
A2: for n being Element of NAT holds s1 . n = H₁(n) from FUNCT_2:sch 4();
take s1 ; :: thesis: s1 is convergent_to_0

now

let n be Element of NAT ; :: thesis: s1 . n <> 0. S
(n + 1) " <> 0 by NAT_1:5, XCMPLX_1:203;
then A3: 1 / (n + 1) <> 0 by XCMPLX_1:217;
thus s1 . n <> 0. S :: thesis: verum

proof

assume s1 . n = 0. S ; :: thesis: contradiction
then (1 / (n + 1)) * x0 = 0. S by A2;
hence contradiction by A1, A3, RLVECT_1:24; :: thesis: verum

end;

end;

hence s1 is non-zero by Th7; :: according to NDIFF_1:def 4 :: thesis: ( s1 is convergent & lim s1 = 0. S )
thus ( s1 is convergent & lim s1 = 0. S ) by A2, Th22, Th23; :: thesis: verum