set x0 = the Point of S;

deffunc H_{1}( Nat) -> Element of the carrier of S = (1 / (S + 1)) * the Point of S;

consider s1 being sequence of S such that

A1: for n being Element of NAT holds s1 . n = H_{1}(n)
from FUNCT_2:sch 4();

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

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

s1 is convergent by A2, Th19;

then s1 is 0. S -convergent by A3;

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

deffunc H

consider s1 being sequence of S such that

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

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

proof

take
s1
; :: thesis: 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 A1; :: thesis: verum

end;n in NAT by ORDINAL1:def 12;

hence s1 . n = H

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

s1 is convergent by A2, Th19;

then s1 is 0. S -convergent by A3;

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