:: Convergent Sequences in Complex Unitary Space
:: by Noboru Endou
::
:: Received February 10, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users


begin

deffunc H1( ComplexUnitarySpace) ->  Element of the carrier of $1 = 0. $1;

definition
let X be ComplexUnitarySpace;
let seq be sequence of X;
attrseq is convergent  means :Def1: :: CLVECT_2:def 1
 ex g being Point of X st
for r being Real st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq . n),g) < r;
end;

:: deftheorem Def1 defines convergent CLVECT_2:def_1_:_
 for X being ComplexUnitarySpace
for seq being sequence of X holds
( seq is convergent iff ex g being Point of X st
for r being Real st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq . n),g) < r );

theorem Th1: :: CLVECT_2:1
for X being ComplexUnitarySpace
for seq being sequence of X st seq is constant holds
seq is convergent
proofend;

theorem Th2: :: CLVECT_2:2
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is convergent &amp; ex k being Element of NAT st
for n being Element of NAT st k <= n holds
seq2 . n = seq1 . n holds
seq2 is convergent
proofend;

theorem Th3: :: CLVECT_2:3
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is convergent &amp; seq2 is convergent holds
seq1 + seq2 is convergent
proofend;

theorem Th4: :: CLVECT_2:4
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is convergent &amp; seq2 is convergent holds
seq1 - seq2 is convergent
proofend;

theorem Th5: :: CLVECT_2:5
for X being ComplexUnitarySpace
for z being Complex
for seq being sequence of X st seq is convergent holds
z * seq is convergent
proofend;

theorem Th6: :: CLVECT_2:6
for X being ComplexUnitarySpace
for seq being sequence of X st seq is convergent holds
- seq is convergent
proofend;

theorem Th7: :: CLVECT_2:7
for X being ComplexUnitarySpace
for x being Point of X
for seq being sequence of X st seq is convergent holds
seq + x is convergent
proofend;

theorem Th8: :: CLVECT_2:8
for X being ComplexUnitarySpace
for x being Point of X
for seq being sequence of X st seq is convergent holds
seq - x is convergent
proofend;

theorem Th9: :: CLVECT_2:9
for X being ComplexUnitarySpace
for seq being sequence of X holds
( seq is convergent iff ex g being Point of X st
for r being Real st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((seq . n) - g).|| < r )
proofend;

definition
let X be ComplexUnitarySpace;
let seq be sequence of X;
assume A1: seq is convergent ;
func lim seq ->  Point of X means :Def2: :: CLVECT_2:def 2
 for r being Real st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq . n),it) < r;
existence
 ex b1 being Point of X st
for r being Real st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq . n),b1) < r by A1, Def1;
uniqueness
 for b1, b2 being Point of X st ( for r being Real st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq . n),b1) < r ) &amp; ( for r being Real st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq . n),b2) < r ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines lim CLVECT_2:def_2_:_
 for X being ComplexUnitarySpace
for seq being sequence of X st seq is convergent holds
for b3 being Point of X holds
( b3 = lim seq iff for r being Real st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq . n),b3) < r );

theorem Th10: :: CLVECT_2:10
for X being ComplexUnitarySpace
for x being Point of X
for seq being sequence of X st seq is constant &amp; x in rng seq holds
lim seq = x
proofend;

theorem :: CLVECT_2:11
for X being ComplexUnitarySpace
for x being Point of X
for seq being sequence of X st seq is constant &amp; ex n being Element of NAT st seq . n = x holds
lim seq = x
proofend;

theorem :: CLVECT_2:12
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is convergent &amp; ex k being Element of NAT st
for n being Element of NAT st n >= k holds
seq2 . n = seq1 . n holds
lim seq1 = lim seq2
proofend;

theorem Th13: :: CLVECT_2:13
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is convergent &amp; seq2 is convergent holds
lim (seq1 + seq2) = (lim seq1) + (lim seq2)
proofend;

theorem Th14: :: CLVECT_2:14
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is convergent &amp; seq2 is convergent holds
lim (seq1 - seq2) = (lim seq1) - (lim seq2)
proofend;

theorem Th15: :: CLVECT_2:15
for X being ComplexUnitarySpace
for z being Complex
for seq being sequence of X st seq is convergent holds
lim (z * seq) = z * (lim seq)
proofend;

theorem Th16: :: CLVECT_2:16
for X being ComplexUnitarySpace
for seq being sequence of X st seq is convergent holds
lim (- seq) = - (lim seq)
proofend;

theorem Th17: :: CLVECT_2:17
for X being ComplexUnitarySpace
for x being Point of X
for seq being sequence of X st seq is convergent holds
lim (seq + x) = (lim seq) + x
proofend;

theorem :: CLVECT_2:18
for X being ComplexUnitarySpace
for x being Point of X
for seq being sequence of X st seq is convergent holds
lim (seq - x) = (lim seq) - x
proofend;

theorem Th19: :: CLVECT_2:19
for X being ComplexUnitarySpace
for g being Point of X
for seq being sequence of X st seq is convergent holds
( lim seq = g iff for r being Real st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((seq . n) - g).|| < r )
proofend;

definition
let X be ComplexUnitarySpace;
let seq be sequence of X;
func||.seq.|| ->  Real_Sequence means :Def3: :: CLVECT_2:def 3
 for n being Element of NAT holds it . n = ||.(seq . n).||;
existence
 ex b1 being Real_Sequence st
for n being Element of NAT holds b1 . n = ||.(seq . n).||
proofend;
uniqueness
 for b1, b2 being Real_Sequence st ( for n being Element of NAT holds b1 . n = ||.(seq . n).|| ) &amp; ( for n being Element of NAT holds b2 . n = ||.(seq . n).|| ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines ||. CLVECT_2:def_3_:_
 for X being ComplexUnitarySpace
for seq being sequence of X
for b3 being Real_Sequence holds
( b3 = ||.seq.|| iff for n being Element of NAT holds b3 . n = ||.(seq . n).|| );

theorem Th20: :: CLVECT_2:20
for X being ComplexUnitarySpace
for seq being sequence of X st seq is convergent holds
||.seq.|| is convergent
proofend;

theorem Th21: :: CLVECT_2:21
for X being ComplexUnitarySpace
for g being Point of X
for seq being sequence of X st seq is convergent &amp; lim seq = g holds
( ||.seq.|| is convergent &amp; lim ||.seq.|| = ||.g.|| )
proofend;

theorem Th22: :: CLVECT_2:22
for X being ComplexUnitarySpace
for g being Point of X
for seq being sequence of X st seq is convergent &amp; lim seq = g holds
( ||.(seq - g).|| is convergent &amp; lim ||.(seq - g).|| = 0 )
proofend;

definition
let X be ComplexUnitarySpace;
let seq be sequence of X;
let x be Point of X;
func dist (seq,x) ->  Real_Sequence means :Def4: :: CLVECT_2:def 4
 for n being Element of NAT holds it . n = dist ((seq . n),x);
existence
 ex b1 being Real_Sequence st
for n being Element of NAT holds b1 . n = dist ((seq . n),x)
proofend;
uniqueness
 for b1, b2 being Real_Sequence st ( for n being Element of NAT holds b1 . n = dist ((seq . n),x) ) &amp; ( for n being Element of NAT holds b2 . n = dist ((seq . n),x) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines dist CLVECT_2:def_4_:_
 for X being ComplexUnitarySpace
for seq being sequence of X
for x being Point of X
for b4 being Real_Sequence holds
( b4 = dist (seq,x) iff for n being Element of NAT holds b4 . n = dist ((seq . n),x) );

theorem Th23: :: CLVECT_2:23
for X being ComplexUnitarySpace
for g being Point of X
for seq being sequence of X st seq is convergent &amp; lim seq = g holds
dist (seq,g) is convergent
proofend;

theorem Th24: :: CLVECT_2:24
for X being ComplexUnitarySpace
for g being Point of X
for seq being sequence of X st seq is convergent &amp; lim seq = g holds
( dist (seq,g) is convergent &amp; lim (dist (seq,g)) = 0 )
proofend;

theorem :: CLVECT_2:25
for X being ComplexUnitarySpace
for g1, g2 being Point of X
for seq1, seq2 being sequence of X st seq1 is convergent &amp; lim seq1 = g1 &amp; seq2 is convergent &amp; lim seq2 = g2 holds
( ||.(seq1 + seq2).|| is convergent &amp; lim ||.(seq1 + seq2).|| = ||.(g1 + g2).|| )
proofend;

theorem :: CLVECT_2:26
for X being ComplexUnitarySpace
for g1, g2 being Point of X
for seq1, seq2 being sequence of X st seq1 is convergent &amp; lim seq1 = g1 &amp; seq2 is convergent &amp; lim seq2 = g2 holds
( ||.((seq1 + seq2) - (g1 + g2)).|| is convergent &amp; lim ||.((seq1 + seq2) - (g1 + g2)).|| = 0 )
proofend;

theorem :: CLVECT_2:27
for X being ComplexUnitarySpace
for g1, g2 being Point of X
for seq1, seq2 being sequence of X st seq1 is convergent &amp; lim seq1 = g1 &amp; seq2 is convergent &amp; lim seq2 = g2 holds
( ||.(seq1 - seq2).|| is convergent &amp; lim ||.(seq1 - seq2).|| = ||.(g1 - g2).|| )
proofend;

theorem :: CLVECT_2:28
for X being ComplexUnitarySpace
for g1, g2 being Point of X
for seq1, seq2 being sequence of X st seq1 is convergent &amp; lim seq1 = g1 &amp; seq2 is convergent &amp; lim seq2 = g2 holds
( ||.((seq1 - seq2) - (g1 - g2)).|| is convergent &amp; lim ||.((seq1 - seq2) - (g1 - g2)).|| = 0 )
proofend;

theorem :: CLVECT_2:29
for X being ComplexUnitarySpace
for g being Point of X
for z being Complex
for seq being sequence of X st seq is convergent &amp; lim seq = g holds
( ||.(z * seq).|| is convergent &amp; lim ||.(z * seq).|| = ||.(z * g).|| )
proofend;

theorem :: CLVECT_2:30
for X being ComplexUnitarySpace
for g being Point of X
for z being Complex
for seq being sequence of X st seq is convergent &amp; lim seq = g holds
( ||.((z * seq) - (z * g)).|| is convergent &amp; lim ||.((z * seq) - (z * g)).|| = 0 )
proofend;

theorem :: CLVECT_2:31
for X being ComplexUnitarySpace
for g being Point of X
for seq being sequence of X st seq is convergent &amp; lim seq = g holds
( ||.(- seq).|| is convergent &amp; lim ||.(- seq).|| = ||.(- g).|| )
proofend;

theorem :: CLVECT_2:32
for X being ComplexUnitarySpace
for g being Point of X
for seq being sequence of X st seq is convergent &amp; lim seq = g holds
( ||.((- seq) - (- g)).|| is convergent &amp; lim ||.((- seq) - (- g)).|| = 0 )
proofend;

Lm1:  for X being ComplexUnitarySpace
for g, x being Point of X
for seq being sequence of X st seq is convergent &amp; lim seq = g holds
( ||.(seq + x).|| is convergent &amp; lim ||.(seq + x).|| = ||.(g + x).|| )
proofend;

theorem Th33: :: CLVECT_2:33
for X being ComplexUnitarySpace
for g, x being Point of X
for seq being sequence of X st seq is convergent &amp; lim seq = g holds
( ||.((seq + x) - (g + x)).|| is convergent &amp; lim ||.((seq + x) - (g + x)).|| = 0 )
proofend;

theorem :: CLVECT_2:34
for X being ComplexUnitarySpace
for g, x being Point of X
for seq being sequence of X st seq is convergent &amp; lim seq = g holds
( ||.(seq - x).|| is convergent &amp; lim ||.(seq - x).|| = ||.(g - x).|| )
proofend;

theorem :: CLVECT_2:35
for X being ComplexUnitarySpace
for g, x being Point of X
for seq being sequence of X st seq is convergent &amp; lim seq = g holds
( ||.((seq - x) - (g - x)).|| is convergent &amp; lim ||.((seq - x) - (g - x)).|| = 0 )
proofend;

theorem :: CLVECT_2:36
for X being ComplexUnitarySpace
for g1, g2 being Point of X
for seq1, seq2 being sequence of X st seq1 is convergent &amp; lim seq1 = g1 &amp; seq2 is convergent &amp; lim seq2 = g2 holds
( dist ((seq1 + seq2),(g1 + g2)) is convergent &amp; lim (dist ((seq1 + seq2),(g1 + g2))) = 0 )
proofend;

theorem :: CLVECT_2:37
for X being ComplexUnitarySpace
for g1, g2 being Point of X
for seq1, seq2 being sequence of X st seq1 is convergent &amp; lim seq1 = g1 &amp; seq2 is convergent &amp; lim seq2 = g2 holds
( dist ((seq1 - seq2),(g1 - g2)) is convergent &amp; lim (dist ((seq1 - seq2),(g1 - g2))) = 0 )
proofend;

theorem :: CLVECT_2:38
for X being ComplexUnitarySpace
for g being Point of X
for z being Complex
for seq being sequence of X st seq is convergent &amp; lim seq = g holds
( dist ((z * seq),(z * g)) is convergent &amp; lim (dist ((z * seq),(z * g))) = 0 )
proofend;

theorem :: CLVECT_2:39
for X being ComplexUnitarySpace
for g, x being Point of X
for seq being sequence of X st seq is convergent &amp; lim seq = g holds
( dist ((seq + x),(g + x)) is convergent &amp; lim (dist ((seq + x),(g + x))) = 0 )
proofend;

definition
let X be ComplexUnitarySpace;
let x be Point of X;
let r be Real;
func Ball (x,r) ->  Subset of X equals :: CLVECT_2:def 5
 {  y where y is Point of X : ||.(x - y).|| < r  }  ;
coherence
  {  y where y is Point of X : ||.(x - y).|| < r  }  is Subset of X
proofend;
func cl_Ball (x,r) ->  Subset of X equals :: CLVECT_2:def 6
 {  y where y is Point of X : ||.(x - y).|| <= r  }  ;
coherence
  {  y where y is Point of X : ||.(x - y).|| <= r  }  is Subset of X
proofend;
func Sphere (x,r) ->  Subset of X equals :: CLVECT_2:def 7
 {  y where y is Point of X : ||.(x - y).|| = r  }  ;
coherence
  {  y where y is Point of X : ||.(x - y).|| = r  }  is Subset of X
proofend;
end;

:: deftheorem  defines Ball CLVECT_2:def_5_:_
 for X being ComplexUnitarySpace
for x being Point of X
for r being Real holds Ball (x,r) =  {  y where y is Point of X : ||.(x - y).|| < r  }  ;

:: deftheorem  defines cl_Ball CLVECT_2:def_6_:_
 for X being ComplexUnitarySpace
for x being Point of X
for r being Real holds cl_Ball (x,r) =  {  y where y is Point of X : ||.(x - y).|| <= r  }  ;

:: deftheorem  defines Sphere CLVECT_2:def_7_:_
 for X being ComplexUnitarySpace
for x being Point of X
for r being Real holds Sphere (x,r) =  {  y where y is Point of X : ||.(x - y).|| = r  }  ;

theorem Th40: :: CLVECT_2:40
for X being ComplexUnitarySpace
for w, x being Point of X
for r being Real holds
( w in Ball (x,r) iff ||.(x - w).|| < r )
proofend;

theorem Th41: :: CLVECT_2:41
for X being ComplexUnitarySpace
for w, x being Point of X
for r being Real holds
( w in Ball (x,r) iff dist (x,w) < r )
proofend;

theorem :: CLVECT_2:42
for X being ComplexUnitarySpace
for x being Point of X
for r being Real st r > 0 holds
x in Ball (x,r)
proofend;

theorem :: CLVECT_2:43
for X being ComplexUnitarySpace
for y, x, w being Point of X
for r being Real st y in Ball (x,r) &amp; w in Ball (x,r) holds
dist (y,w) < 2 * r
proofend;

theorem :: CLVECT_2:44
for X being ComplexUnitarySpace
for y, x, w being Point of X
for r being Real st y in Ball (x,r) holds
y - w in Ball ((x - w),r)
proofend;

theorem :: CLVECT_2:45
for X being ComplexUnitarySpace
for y, x being Point of X
for r being Real st y in Ball (x,r) holds
y - x in Ball ((0. X),r)
proofend;

theorem :: CLVECT_2:46
for X being ComplexUnitarySpace
for y, x being Point of X
for r, q being Real st y in Ball (x,r) &amp; r <= q holds
y in Ball (x,q)
proofend;

theorem Th47: :: CLVECT_2:47
for X being ComplexUnitarySpace
for w, x being Point of X
for r being Real holds
( w in cl_Ball (x,r) iff ||.(x - w).|| <= r )
proofend;

theorem Th48: :: CLVECT_2:48
for X being ComplexUnitarySpace
for w, x being Point of X
for r being Real holds
( w in cl_Ball (x,r) iff dist (x,w) <= r )
proofend;

theorem :: CLVECT_2:49
for X being ComplexUnitarySpace
for x being Point of X
for r being Real st r >= 0 holds
x in cl_Ball (x,r)
proofend;

theorem Th50: :: CLVECT_2:50
for X being ComplexUnitarySpace
for y, x being Point of X
for r being Real st y in Ball (x,r) holds
y in cl_Ball (x,r)
proofend;

theorem Th51: :: CLVECT_2:51
for X being ComplexUnitarySpace
for w, x being Point of X
for r being Real holds
( w in Sphere (x,r) iff ||.(x - w).|| = r )
proofend;

theorem :: CLVECT_2:52
for X being ComplexUnitarySpace
for w, x being Point of X
for r being Real holds
( w in Sphere (x,r) iff dist (x,w) = r )
proofend;

theorem :: CLVECT_2:53
for X being ComplexUnitarySpace
for y, x being Point of X
for r being Real st y in Sphere (x,r) holds
y in cl_Ball (x,r)
proofend;

theorem Th54: :: CLVECT_2:54
for X being ComplexUnitarySpace
for x being Point of X
for r being Real holds Ball (x,r) c= cl_Ball (x,r)
proofend;

theorem Th55: :: CLVECT_2:55
for X being ComplexUnitarySpace
for x being Point of X
for r being Real holds Sphere (x,r) c= cl_Ball (x,r)
proofend;

theorem :: CLVECT_2:56
for X being ComplexUnitarySpace
for x being Point of X
for r being Real holds (Ball (x,r)) \/ (Sphere (x,r)) = cl_Ball (x,r)
proofend;

begin

deffunc H2( ComplexUnitarySpace) ->  Element of the carrier of $1 = 0. $1;

definition
let X be ComplexUnitarySpace;
let seq be sequence of X;
attrseq is Cauchy  means :Def8: :: CLVECT_2:def 8
 for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k &amp; m >= k holds
dist ((seq . n),(seq . m)) < r;
end;

:: deftheorem Def8 defines Cauchy CLVECT_2:def_8_:_
 for X being ComplexUnitarySpace
for seq being sequence of X holds
( seq is Cauchy iff for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k &amp; m >= k holds
dist ((seq . n),(seq . m)) < r );

theorem :: CLVECT_2:57
for X being ComplexUnitarySpace
for seq being sequence of X st seq is constant holds
seq is Cauchy
proofend;

theorem :: CLVECT_2:58
for X being ComplexUnitarySpace
for seq being sequence of X holds
( seq is Cauchy iff for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k &amp; m >= k holds
||.((seq . n) - (seq . m)).|| < r )
proofend;

theorem :: CLVECT_2:59
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is Cauchy &amp; seq2 is Cauchy holds
seq1 + seq2 is Cauchy
proofend;

theorem :: CLVECT_2:60
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is Cauchy &amp; seq2 is Cauchy holds
seq1 - seq2 is Cauchy
proofend;

theorem Th61: :: CLVECT_2:61
for X being ComplexUnitarySpace
for z being Complex
for seq being sequence of X st seq is Cauchy holds
z * seq is Cauchy
proofend;

theorem :: CLVECT_2:62
for X being ComplexUnitarySpace
for seq being sequence of X st seq is Cauchy holds
- seq is Cauchy
proofend;

theorem Th63: :: CLVECT_2:63
for X being ComplexUnitarySpace
for x being Point of X
for seq being sequence of X st seq is Cauchy holds
seq + x is Cauchy
proofend;

theorem :: CLVECT_2:64
for X being ComplexUnitarySpace
for x being Point of X
for seq being sequence of X st seq is Cauchy holds
seq - x is Cauchy
proofend;

theorem :: CLVECT_2:65
for X being ComplexUnitarySpace
for seq being sequence of X st seq is convergent holds
seq is Cauchy
proofend;

definition
let X be ComplexUnitarySpace;
let seq1, seq2 be sequence of X;
predseq1 is_compared_to seq2 means :Def9: :: CLVECT_2:def 9
 for r being Real st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq1 . n),(seq2 . n)) < r;
end;

:: deftheorem Def9 defines is_compared_to CLVECT_2:def_9_:_
 for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X holds
( seq1 is_compared_to seq2 iff for r being Real st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq1 . n),(seq2 . n)) < r );

theorem Th66: :: CLVECT_2:66
for X being ComplexUnitarySpace
for seq being sequence of X holds seq is_compared_to seq
proofend;

theorem Th67: :: CLVECT_2:67
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is_compared_to seq2 holds
seq2 is_compared_to seq1
proofend;

definition
let X be ComplexUnitarySpace;
let seq1, seq2 be sequence of X;
:: original:is_compared_to
redefine predseq1 is_compared_to seq2;
reflexivity
 for seq1 being sequence of X holds (X,b1,b1) by Th66;
symmetry
 for seq1, seq2 being sequence of X st (X,b1,b2) holds
(X,b2,b1) by Th67;
end;

theorem :: CLVECT_2:68
for X being ComplexUnitarySpace
for seq1, seq2, seq3 being sequence of X st seq1 is_compared_to seq2 &amp; seq2 is_compared_to seq3 holds
seq1 is_compared_to seq3
proofend;

theorem :: CLVECT_2:69
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X holds
( seq1 is_compared_to seq2 iff for r being Real st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((seq1 . n) - (seq2 . n)).|| < r )
proofend;

theorem :: CLVECT_2:70
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st ex k being Element of NAT st
for n being Element of NAT st n >= k holds
seq1 . n = seq2 . n holds
seq1 is_compared_to seq2
proofend;

theorem :: CLVECT_2:71
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is Cauchy &amp; seq1 is_compared_to seq2 holds
seq2 is Cauchy
proofend;

theorem :: CLVECT_2:72
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is convergent &amp; seq1 is_compared_to seq2 holds
seq2 is convergent
proofend;

theorem :: CLVECT_2:73
for X being ComplexUnitarySpace
for g being Point of X
for seq1, seq2 being sequence of X st seq1 is convergent &amp; lim seq1 = g &amp; seq1 is_compared_to seq2 holds
( seq2 is convergent &amp; lim seq2 = g )
proofend;

definition
let X be ComplexUnitarySpace;
let seq be sequence of X;
attrseq is bounded  means :Def10: :: CLVECT_2:def 10
 ex M being Real st
( M > 0 &amp; ( for n being Element of NAT holds ||.(seq . n).|| <= M ) );
end;

:: deftheorem Def10 defines bounded CLVECT_2:def_10_:_
 for X being ComplexUnitarySpace
for seq being sequence of X holds
( seq is bounded iff ex M being Real st
( M > 0 &amp; ( for n being Element of NAT holds ||.(seq . n).|| <= M ) ) );

theorem Th74: :: CLVECT_2:74
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is bounded &amp; seq2 is bounded holds
seq1 + seq2 is bounded
proofend;

theorem Th75: :: CLVECT_2:75
for X being ComplexUnitarySpace
for seq being sequence of X st seq is bounded holds
- seq is bounded
proofend;

theorem :: CLVECT_2:76
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is bounded &amp; seq2 is bounded holds
seq1 - seq2 is bounded
proofend;

theorem :: CLVECT_2:77
for X being ComplexUnitarySpace
for z being Complex
for seq being sequence of X st seq is bounded holds
z * seq is bounded
proofend;

theorem :: CLVECT_2:78
for X being ComplexUnitarySpace
for seq being sequence of X st seq is constant holds
seq is bounded
proofend;

theorem Th79: :: CLVECT_2:79
for X being ComplexUnitarySpace
for seq being sequence of X
for m being Element of NAT ex M being Real st
( M > 0 &amp; ( for n being Element of NAT st n <= m holds
||.(seq . n).|| < M ) )
proofend;

theorem Th80: :: CLVECT_2:80
for X being ComplexUnitarySpace
for seq being sequence of X st seq is convergent holds
seq is bounded
proofend;

theorem :: CLVECT_2:81
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is bounded &amp; seq1 is_compared_to seq2 holds
seq2 is bounded
proofend;

theorem Th82: :: CLVECT_2:82
for X being ComplexUnitarySpace
for seq, seq1 being sequence of X st seq is bounded &amp; seq1 is subsequence of seq holds
seq1 is bounded
proofend;

theorem Th83: :: CLVECT_2:83
for X being ComplexUnitarySpace
for seq, seq1 being sequence of X st seq is convergent &amp; seq1 is subsequence of seq holds
seq1 is convergent
proofend;

theorem Th84: :: CLVECT_2:84
for X being ComplexUnitarySpace
for seq1, seq being sequence of X st seq1 is subsequence of seq &amp; seq is convergent holds
lim seq1 = lim seq
proofend;

theorem Th85: :: CLVECT_2:85
for X being ComplexUnitarySpace
for seq, seq1 being sequence of X st seq is Cauchy &amp; seq1 is subsequence of seq holds
seq1 is Cauchy
proofend;

theorem Th86: :: CLVECT_2:86
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X
for k being Element of NAT holds (seq1 + seq2) ^\ k = (seq1 ^\ k) + (seq2 ^\ k)
proofend;

theorem Th87: :: CLVECT_2:87
for X being ComplexUnitarySpace
for seq being sequence of X
for k being Element of NAT holds (- seq) ^\ k = - (seq ^\ k)
proofend;

theorem :: CLVECT_2:88
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X
for k being Element of NAT holds (seq1 - seq2) ^\ k = (seq1 ^\ k) - (seq2 ^\ k)
proofend;

theorem :: CLVECT_2:89
for X being ComplexUnitarySpace
for z being Complex
for seq being sequence of X
for k being Element of NAT holds (z * seq) ^\ k = z * (seq ^\ k)
proofend;

theorem :: CLVECT_2:90
for X being ComplexUnitarySpace
for seq being sequence of X
for k being Element of NAT st seq is convergent holds
( seq ^\ k is convergent &amp; lim (seq ^\ k) = lim seq ) by Th83, Th84;

theorem :: CLVECT_2:91
for X being ComplexUnitarySpace
for seq, seq1 being sequence of X st seq is convergent &amp; ex k being Element of NAT st seq = seq1 ^\ k holds
seq1 is convergent
proofend;

theorem :: CLVECT_2:92
for X being ComplexUnitarySpace
for seq, seq1 being sequence of X st seq is Cauchy &amp; ex k being Element of NAT st seq = seq1 ^\ k holds
seq1 is Cauchy
proofend;

theorem :: CLVECT_2:93
for X being ComplexUnitarySpace
for seq being sequence of X
for k being Element of NAT st seq is Cauchy holds
seq ^\ k is Cauchy by Th85;

theorem :: CLVECT_2:94
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X
for k being Element of NAT st seq1 is_compared_to seq2 holds
seq1 ^\ k is_compared_to seq2 ^\ k
proofend;

theorem :: CLVECT_2:95
for X being ComplexUnitarySpace
for seq being sequence of X
for k being Element of NAT st seq is bounded holds
seq ^\ k is bounded by Th82;

theorem :: CLVECT_2:96
for X being ComplexUnitarySpace
for seq being sequence of X
for k being Element of NAT st seq is constant holds
seq ^\ k is constant ;

definition
let X be ComplexUnitarySpace;
attrX is complete  means :Def11: :: CLVECT_2:def 11
 for seq being sequence of X st seq is Cauchy holds
seq is convergent ;
end;

:: deftheorem Def11 defines complete CLVECT_2:def_11_:_
 for X being ComplexUnitarySpace holds
( X is complete iff for seq being sequence of X st seq is Cauchy holds
seq is convergent );

theorem :: CLVECT_2:97
for X being ComplexUnitarySpace
for seq being sequence of X st X is complete &amp; seq is Cauchy holds
seq is bounded
proofend;