let X be ComplexUnitarySpace; :: thesis: for seq, seq1 being sequence of X st seq is convergent & ex k being Nat st seq = seq1 ^\ k holds
seq1 is convergent
let seq, seq1 be sequence of X; :: thesis: ( seq is convergent & ex k being Nat st seq = seq1 ^\ k implies seq1 is convergent )
assume that
A1: seq is convergent and
A2: ex k being Nat st seq = seq1 ^\ k ; :: thesis: seq1 is convergent
consider k being Nat such that
A3: seq = seq1 ^\ k by A2;
consider g1 being Point of X such that
A4: for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
||.((seq . n) - g1).|| < r by A1, Th9;

now :: thesis: ex g being Point of X st
for r being Real st r > 0 holds
ex m being set st
for n being Nat st n >= m holds
||.((seq1 . n) - g).|| < r

take g = g1; :: thesis: for r being Real st r > 0 holds
ex m being set st
for n being Nat st n >= m holds
||.((seq1 . n) - g).|| < r
let r be Real; :: thesis: ( r > 0 implies ex m being set st
for n being Nat st n >= m holds
||.((seq1 . n) - g).|| < r )
assume r > 0 ; :: thesis: ex m being set st
for n being Nat st n >= m holds
||.((seq1 . n) - g).|| < r
then consider m1 being Nat such that
A5: for n being Nat st n >= m1 holds
||.((seq . n) - g).|| < r by A4;
take m = m1 + k; :: thesis: for n being Nat st n >= m holds
||.((seq1 . n) - g).|| < r
let n be Nat; :: thesis: ( n >= m implies ||.((seq1 . n) - g).|| < r )
assume A6: n >= m ; :: thesis: ||.((seq1 . n) - g).|| < r
then consider m2 being Nat such that
A7: n = (m1 + k) + m2 by NAT_1:10;
reconsider m2 = m2 as Nat ;
n - k = m1 + m2 by A7;
then consider l being Nat such that
A8: l = n - k ;

now :: thesis: not l < m1

assume l < m1 ; :: thesis: contradiction
then l + k < m1 + k by XREAL_1:6;
hence contradiction by A6, A8; :: thesis: verum

end;

then A9: ||.((seq . l) - g).|| < r by A5;
l + k = n by A8;
hence ||.((seq1 . n) - g).|| < r by A3, A9, NAT_1:def 3; :: thesis: verum

end;

hence seq1 is convergent by Th9; :: thesis: verum