let X be ComplexNormSpace; :: thesis: for seq, seq1 being sequence of X st seq is convergent & ex k being Element of NAT st seq = seq1 ^\ k holds
seq1 is convergent
let seq, seq1 be sequence of X; :: thesis: ( seq is convergent & ex k being Element of NAT st seq = seq1 ^\ k implies seq1 is convergent )
assume that
A1: seq is convergent and
A2: ex k being Element of NAT st seq = seq1 ^\ k ; :: thesis: seq1 is convergent
consider k being Element of NAT such that
A3: seq = seq1 ^\ k by A2;
consider g1 being Element of X such that
A4: for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - g1).|| < p by A1, CLVECT_1:def 16;
take g = g1; :: according to CLVECT_1:def 16 :: thesis: for b₁ being Element of REAL holds
( b₁ <= 0 or ex b₂ being Element of NAT st
for b₃ being Element of NAT holds
( not b₂ <= b₃ or not b₁ <= ||.((seq1 . b₃) - g).|| ) )
let p be Real; :: thesis: ( p <= 0 or ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not p <= ||.((seq1 . b₂) - g).|| ) )
assume 0 < p ; :: thesis: ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not p <= ||.((seq1 . b₂) - g).|| )
then consider n1 being Element of NAT such that
A5: for m being Element of NAT st n1 <= m holds
||.((seq . m) - g1).|| < p by A4;
take n = n1 + k; :: thesis: for b₁ being Element of NAT holds
( not n <= b₁ or not p <= ||.((seq1 . b₁) - g).|| )
let m be Element of NAT ; :: thesis: ( not n <= m or not p <= ||.((seq1 . m) - g).|| )
assume A6: n <= m ; :: thesis: not p <= ||.((seq1 . m) - g).||
then consider l being Nat such that
A7: m = (n1 + k) + l by NAT_1:10;
reconsider l = l as Element of NAT by ORDINAL1:def 13;
m - k = (n1 + l) + 0 by A7;
then consider m1 being Element of NAT such that
A8: m1 = m - k ;

A9: now

assume not n1 <= m1 ; :: thesis: contradiction
then m1 + k < n1 + k by XREAL_1:8;
hence contradiction by A6, A8; :: thesis: verum

end;

A10: m1 + k = m by A8;
||.((seq . m1) - g1).|| < p by A5, A9;
hence not p <= ||.((seq1 . m) - g).|| by A3, A10, NAT_1:def 3; :: thesis: verum