consider x0 being Point of S such that
A1: x0 <> 0. S by STRUCT_0:def 18;
deffunc H1( 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 = H1(n) from A3: for n being Nat holds s1 . n = H1(n)
proof
let n be Nat; :: thesis: s1 . n = H1(n)
n in NAT by ORDINAL1:def 12;
hence s1 . n = H1(n) by A2; :: thesis: verum
end;
take s1 ; :: thesis: ( s1 is non-zero & s1 is 0. S -convergent )
now :: thesis: for n being Nat holds s1 . n <> 0. S
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
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;
end;
hence s1 is non-zero by Th7; :: thesis: s1 is 0. S -convergent
A5: lim s1 = 0. S by ;
s1 is convergent by ;
then s1 is 0. S -convergent by A5;
hence s1 is 0. S -convergent ; :: thesis: verum