let X be ComplexUnitarySpace; :: thesis:
let seq, seq1 be sequence of X; :: thesis:
assume that
A1: seq is convergent and
A2: ex k being Nat st seq = seq1 ^\ k ; :: thesis:
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;

take g = g1; :: thesis:
let r be Real; :: thesis:
assume r > 0 ; :: thesis:
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:
let n be Nat; :: thesis:
assume A6: n >= m ; :: thesis:
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 ;

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:

end;