consider x0 being Point of S such that

A1: x0 <> 0. S by STRUCT_0:def 18;

deffunc H_{1}( 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_{1}(n)
from FUNCT_2:sch 4();

A3: for n being Nat holds s1 . n = H_{1}(n)

A5: lim s1 = 0. S by A3, Th20;

s1 is convergent by A3, Th19;

then s1 is 0. S -convergent by A5;

hence s1 is 0. S -convergent ; :: thesis: verum

A1: x0 <> 0. S by STRUCT_0:def 18;

deffunc H

consider s1 being sequence of S such that

A2: for n being Element of NAT holds s1 . n = H

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

proof

take
s1
; :: thesis: ( s1 is non-zero & s1 is 0. S -convergent )
let n be Nat; :: thesis: s1 . n = H_{1}(n)

n in NAT by ORDINAL1:def 12;

hence s1 . n = H_{1}(n)
by A2; :: thesis: verum

end;n in NAT by ORDINAL1:def 12;

hence s1 . n = H

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

hence
s1 is non-zero
by Th7; :: thesis: s1 is 0. S -convergent let n be Nat; :: thesis: s1 . n <> 0. S

(n + 1) " <> 0 ;

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

thus s1 . n <> 0. S :: thesis: verum

end;(n + 1) " <> 0 ;

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

thus s1 . n <> 0. S :: thesis: verum

proof

assume
s1 . n = 0. S
; :: thesis: contradiction

then (1 / (n + 1)) * x0 = 0. S by A3;

hence contradiction by A1, A4, RLVECT_1:11; :: thesis: verum

end;then (1 / (n + 1)) * x0 = 0. S by A3;

hence contradiction by A1, A4, RLVECT_1:11; :: thesis: verum

A5: lim s1 = 0. S by A3, Th20;

s1 is convergent by A3, Th19;

then s1 is 0. S -convergent by A5;

hence s1 is 0. S -convergent ; :: thesis: verum