:: CLVECT_2 semantic presentation

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
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X st seq is constant holds
seq is convergent
let seq be sequence of X; ::_thesis: ( seq is constant implies seq is convergent )
assume  seq is constant ; ::_thesis: seq is convergent
then consider x being Point of X such that
A1: for n being Nat holds seq . n = x by VALUED_0:def_18;
take g = x; :: according to CLVECT_2:def_1 ::_thesis: 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
let r be Real; ::_thesis: ( r > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq . n),g) < r )
assume A2: r > 0 ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq . n),g) < r
take m = 0 ; ::_thesis: for n being Element of NAT st n >= m holds
dist ((seq . n),g) < r
let n be Element of NAT ; ::_thesis: ( n >= m implies dist ((seq . n),g) < r )
assume  n >= m ; ::_thesis: dist ((seq . n),g) < r
dist ((seq . n),g) = dist (x,g) by A1
.= 0 by CSSPACE:50 ;
hence  dist ((seq . n),g) < r by A2; ::_thesis: verum
end;

theorem Th2: :: CLVECT_2:2
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is convergent & 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
proof
let X be ComplexUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X st seq1 is convergent & 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
let seq1, seq2 be sequence of X; ::_thesis: ( seq1 is convergent & ex k being Element of NAT st
for n being Element of NAT st k <= n holds
seq2 . n = seq1 . n implies seq2 is convergent )
assume that
A1: seq1 is convergent and
A2: ex k being Element of NAT st
for n being Element of NAT st k <= n holds
seq2 . n = seq1 . n ; ::_thesis: seq2 is convergent
consider k being Element of NAT  such that
A3: for n being Element of NAT st n >= k holds
seq2 . n = seq1 . n by A2;
consider g being Point of X such that
A4: 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),g) < r by A1, Def1;
take h = g; :: according to CLVECT_2:def_1 ::_thesis: 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 ((seq2 . n),h) < r
let r be Real; ::_thesis: ( r > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq2 . n),h) < r )
assume  r > 0 ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq2 . n),h) < r
then consider m1 being Element of NAT  such that
A5: for n being Element of NAT st n >= m1 holds
dist ((seq1 . n),h) < r by A4;
A6: now__::_thesis:_(_m1_<=_k_implies_ex_m_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_n_>=_m_holds_
dist_((seq2_._n),h)_<_r_)
assume A7: m1 <= k ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq2 . n),h) < r
take m = k; ::_thesis: for n being Element of NAT st n >= m holds
dist ((seq2 . n),h) < r
let n be Element of NAT ; ::_thesis: ( n >= m implies dist ((seq2 . n),h) < r )
assume A8: n >= m ; ::_thesis: dist ((seq2 . n),h) < r
then  n >= m1 by A7, XXREAL_0:2;
then  dist ((seq1 . n),g) < r by A5;
hence  dist ((seq2 . n),h) < r by A3, A8; ::_thesis: verum
end;
now__::_thesis:_(_k_<=_m1_implies_ex_m_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_n_>=_m_holds_
dist_((seq2_._n),h)_<_r_)
assume A9: k <= m1 ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq2 . n),h) < r
take m = m1; ::_thesis: for n being Element of NAT st n >= m holds
dist ((seq2 . n),h) < r
let n be Element of NAT ; ::_thesis: ( n >= m implies dist ((seq2 . n),h) < r )
assume A10: n >= m ; ::_thesis: dist ((seq2 . n),h) < r
then  seq2 . n = seq1 . n by A3, A9, XXREAL_0:2;
hence  dist ((seq2 . n),h) < r by A5, A10; ::_thesis: verum
end;
hence  ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq2 . n),h) < r by A6; ::_thesis: verum
end;

theorem Th3: :: CLVECT_2:3
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is convergent & seq2 is convergent holds
seq1 + seq2 is convergent
proof
let X be ComplexUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X st seq1 is convergent & seq2 is convergent holds
seq1 + seq2 is convergent
let seq1, seq2 be sequence of X; ::_thesis: ( seq1 is convergent & seq2 is convergent implies seq1 + seq2 is convergent )
assume that
A1: seq1 is convergent and
A2: seq2 is convergent ; ::_thesis: seq1 + seq2 is convergent
consider g1 being Point of X such that
A3: 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),g1) < r by A1, Def1;
consider g2 being Point of X such that
A4: 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 ((seq2 . n),g2) < r by A2, Def1;
take g = g1 + g2; :: according to CLVECT_2:def_1 ::_thesis: 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 + seq2) . n),g) < r
let r be Real; ::_thesis: ( r > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist (((seq1 + seq2) . n),g) < r )
assume A5: r > 0 ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist (((seq1 + seq2) . n),g) < r
then consider m1 being Element of NAT  such that
A6: for n being Element of NAT st n >= m1 holds
dist ((seq1 . n),g1) < r / 2 by A3, XREAL_1:215;
consider m2 being Element of NAT  such that
A7: for n being Element of NAT st n >= m2 holds
dist ((seq2 . n),g2) < r / 2 by A4, A5, XREAL_1:215;
take k = m1 + m2; ::_thesis: for n being Element of NAT st n >= k holds
dist (((seq1 + seq2) . n),g) < r
let n be Element of NAT ; ::_thesis: ( n >= k implies dist (((seq1 + seq2) . n),g) < r )
assume A8: n >= k ; ::_thesis: dist (((seq1 + seq2) . n),g) < r
 k >= m2 by NAT_1:12;
then  n >= m2 by A8, XXREAL_0:2;
then A9: dist ((seq2 . n),g2) < r / 2 by A7;
 dist (((seq1 + seq2) . n),g) = dist (((seq1 . n) + (seq2 . n)),(g1 + g2)) by NORMSP_1:def_2;
then A10: dist (((seq1 + seq2) . n),g) <= (dist ((seq1 . n),g1)) + (dist ((seq2 . n),g2)) by CSSPACE:56;
 m1 + m2 >= m1 by NAT_1:12;
then  n >= m1 by A8, XXREAL_0:2;
then  dist ((seq1 . n),g1) < r / 2 by A6;
then  (dist ((seq1 . n),g1)) + (dist ((seq2 . n),g2)) < (r / 2) + (r / 2) by A9, XREAL_1:8;
hence  dist (((seq1 + seq2) . n),g) < r by A10, XXREAL_0:2; ::_thesis: verum
end;

theorem Th4: :: CLVECT_2:4
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is convergent & seq2 is convergent holds
seq1 - seq2 is convergent
proof
let X be ComplexUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X st seq1 is convergent & seq2 is convergent holds
seq1 - seq2 is convergent
let seq1, seq2 be sequence of X; ::_thesis: ( seq1 is convergent & seq2 is convergent implies seq1 - seq2 is convergent )
assume that
A1: seq1 is convergent and
A2: seq2 is convergent ; ::_thesis: seq1 - seq2 is convergent
consider g1 being Point of X such that
A3: 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),g1) < r by A1, Def1;
consider g2 being Point of X such that
A4: 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 ((seq2 . n),g2) < r by A2, Def1;
take g = g1 - g2; :: according to CLVECT_2:def_1 ::_thesis: 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 - seq2) . n),g) < r
let r be Real; ::_thesis: ( r > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist (((seq1 - seq2) . n),g) < r )
assume A5: r > 0 ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist (((seq1 - seq2) . n),g) < r
then consider m1 being Element of NAT  such that
A6: for n being Element of NAT st n >= m1 holds
dist ((seq1 . n),g1) < r / 2 by A3, XREAL_1:215;
consider m2 being Element of NAT  such that
A7: for n being Element of NAT st n >= m2 holds
dist ((seq2 . n),g2) < r / 2 by A4, A5, XREAL_1:215;
take k = m1 + m2; ::_thesis: for n being Element of NAT st n >= k holds
dist (((seq1 - seq2) . n),g) < r
let n be Element of NAT ; ::_thesis: ( n >= k implies dist (((seq1 - seq2) . n),g) < r )
assume A8: n >= k ; ::_thesis: dist (((seq1 - seq2) . n),g) < r
 k >= m2 by NAT_1:12;
then  n >= m2 by A8, XXREAL_0:2;
then A9: dist ((seq2 . n),g2) < r / 2 by A7;
 dist (((seq1 - seq2) . n),g) = dist (((seq1 . n) - (seq2 . n)),(g1 - g2)) by NORMSP_1:def_3;
then A10: dist (((seq1 - seq2) . n),g) <= (dist ((seq1 . n),g1)) + (dist ((seq2 . n),g2)) by CSSPACE:57;
 m1 + m2 >= m1 by NAT_1:12;
then  n >= m1 by A8, XXREAL_0:2;
then  dist ((seq1 . n),g1) < r / 2 by A6;
then  (dist ((seq1 . n),g1)) + (dist ((seq2 . n),g2)) < (r / 2) + (r / 2) by A9, XREAL_1:8;
hence  dist (((seq1 - seq2) . n),g) < r by A10, XXREAL_0:2; ::_thesis: verum
end;

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
proof
let X be ComplexUnitarySpace; ::_thesis: for z being Complex
for seq being sequence of X st seq is convergent holds
z * seq is convergent
let z be Complex; ::_thesis: for seq being sequence of X st seq is convergent holds
z * seq is convergent
let seq be sequence of X; ::_thesis: ( seq is convergent implies z * seq is convergent )
assume  seq is convergent ; ::_thesis: z * seq is convergent
then consider g being Point of X such that
A1: 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 by Def1;
take h = z * g; :: according to CLVECT_2:def_1 ::_thesis: 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 (((z * seq) . n),h) < r
A2: now__::_thesis:_(_z_<>_0_implies_for_r_being_Real_st_r_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_n_>=_k_holds_
dist_(((z_*_seq)_._n),h)_<_r_)
A3: 0 / |.z.| = 0 ;
assume A4: z <> 0 ; ::_thesis: for r being Real st r > 0 holds
ex k being Element of NAT st
for n being Element of NAT st n >= k holds
dist (((z * seq) . n),h) < r
then A5: |.z.| > 0 by COMPLEX1:47;
let r be Real; ::_thesis: ( r > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
dist (((z * seq) . n),h) < r )
assume  r > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
dist (((z * seq) . n),h) < r
then consider m1 being Element of NAT  such that
A6: for n being Element of NAT st n >= m1 holds
dist ((seq . n),g) < r / |.z.| by A1, A5, A3, XREAL_1:74;
take k = m1; ::_thesis: for n being Element of NAT st n >= k holds
dist (((z * seq) . n),h) < r
let n be Element of NAT ; ::_thesis: ( n >= k implies dist (((z * seq) . n),h) < r )
assume  n >= k ; ::_thesis: dist (((z * seq) . n),h) < r
then A7: dist ((seq . n),g) < r / |.z.| by A6;
A8: |.z.| <> 0 by A4, COMPLEX1:47;
A9: |.z.| * (r / |.z.|) = |.z.| * ((|.z.| ") * r) by XCMPLX_0:def_9
.= (|.z.| * (|.z.| ")) * r
.= 1 * r by A8, XCMPLX_0:def_7
.= r ;
dist ((z * (seq . n)),(z * g)) = ||.((z * (seq . n)) - (z * g)).|| by CSSPACE:def_16
.= ||.(z * ((seq . n) - g)).|| by CLVECT_1:9
.= |.z.| * ||.((seq . n) - g).|| by CSSPACE:43
.= |.z.| * (dist ((seq . n),g)) by CSSPACE:def_16 ;
then  dist ((z * (seq . n)),h) < r by A5, A7, A9, XREAL_1:68;
hence  dist (((z * seq) . n),h) < r by CLVECT_1:def_14; ::_thesis: verum
end;
now__::_thesis:_(_z_=_0_implies_for_r_being_Real_st_r_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_n_>=_k_holds_
dist_(((z_*_seq)_._n),h)_<_r_)
assume A10: z = 0 ; ::_thesis: for r being Real st r > 0 holds
ex k being Element of NAT st
for n being Element of NAT st n >= k holds
dist (((z * seq) . n),h) < r
let r be Real; ::_thesis: ( r > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
dist (((z * seq) . n),h) < r )
assume  r > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
dist (((z * seq) . n),h) < r
then consider m1 being Element of NAT  such that
A11: for n being Element of NAT st n >= m1 holds
dist ((seq . n),g) < r by A1;
take k = m1; ::_thesis: for n being Element of NAT st n >= k holds
dist (((z * seq) . n),h) < r
let n be Element of NAT ; ::_thesis: ( n >= k implies dist (((z * seq) . n),h) < r )
assume  n >= k ; ::_thesis: dist (((z * seq) . n),h) < r
then A12: dist ((seq . n),g) < r by A11;
dist ((z * (seq . n)),(z * g)) = dist ((0c * (seq . n)),H1(X)) by A10, CLVECT_1:1
.= dist (H1(X),H1(X)) by CLVECT_1:1
.= 0 by CSSPACE:50 ;
then  dist ((z * (seq . n)),h) < r by A12, CSSPACE:53;
hence  dist (((z * seq) . n),h) < r by CLVECT_1:def_14; ::_thesis: verum
end;
hence  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 (((z * seq) . n),h) < r by A2; ::_thesis: verum
end;

theorem Th6: :: CLVECT_2:6
for X being ComplexUnitarySpace
for seq being sequence of X st seq is convergent holds
- seq is convergent
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X st seq is convergent holds
- seq is convergent
let seq be sequence of X; ::_thesis: ( seq is convergent implies - seq is convergent )
assume  seq is convergent ; ::_thesis: - seq is convergent
then  (- 1r) * seq is convergent by Th5;
hence  - seq is convergent by CSSPACE:70; ::_thesis: verum
end;

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
proof
let X be ComplexUnitarySpace; ::_thesis: for x being Point of X
for seq being sequence of X st seq is convergent holds
seq + x is convergent
let x be Point of X; ::_thesis: for seq being sequence of X st seq is convergent holds
seq + x is convergent
let seq be sequence of X; ::_thesis: ( seq is convergent implies seq + x is convergent )
assume  seq is convergent ; ::_thesis: seq + x is convergent
then consider g being Point of X such that
A1: 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 by Def1;
take  g + x ; :: according to CLVECT_2:def_1 ::_thesis: 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 + x) . n),(g + x)) < r
let r be Real; ::_thesis: ( r > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist (((seq + x) . n),(g + x)) < r )
assume  r > 0 ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist (((seq + x) . n),(g + x)) < r
then consider m1 being Element of NAT  such that
A2: for n being Element of NAT st n >= m1 holds
dist ((seq . n),g) < r by A1;
take k = m1; ::_thesis: for n being Element of NAT st n >= k holds
dist (((seq + x) . n),(g + x)) < r
let n be Element of NAT ; ::_thesis: ( n >= k implies dist (((seq + x) . n),(g + x)) < r )
 dist (((seq . n) + x),(g + x)) <= (dist ((seq . n),g)) + (dist (x,x)) by CSSPACE:56;
then A3: dist (((seq . n) + x),(g + x)) <= (dist ((seq . n),g)) + 0 by CSSPACE:50;
assume  n >= k ; ::_thesis: dist (((seq + x) . n),(g + x)) < r
then  dist ((seq . n),g) < r by A2;
then  dist (((seq . n) + x),(g + x)) < r by A3, XXREAL_0:2;
hence  dist (((seq + x) . n),(g + x)) < r by BHSP_1:def_6; ::_thesis: verum
end;

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
proof
let X be ComplexUnitarySpace; ::_thesis: for x being Point of X
for seq being sequence of X st seq is convergent holds
seq - x is convergent
let x be Point of X; ::_thesis: for seq being sequence of X st seq is convergent holds
seq - x is convergent
let seq be sequence of X; ::_thesis: ( seq is convergent implies seq - x is convergent )
assume  seq is convergent ; ::_thesis: seq - x is convergent
then  seq + (- x) is convergent by Th7;
hence  seq - x is convergent by CSSPACE:71; ::_thesis: verum
end;

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 )
proof
let X be ComplexUnitarySpace; ::_thesis: 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 )
let seq be sequence of X; ::_thesis: ( 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 )
thus  ( seq is convergent implies 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 ) ::_thesis: ( 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 implies seq is convergent )
proof
assume  seq is convergent ; ::_thesis: 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
then consider g being Point of X such that
A1: 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 by Def1;
take  g ; ::_thesis: 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
let r be Real; ::_thesis: ( r > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((seq . n) - g).|| < r )
assume  r > 0 ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((seq . n) - g).|| < r
then consider m1 being Element of NAT  such that
A2: for n being Element of NAT st n >= m1 holds
dist ((seq . n),g) < r by A1;
take k = m1; ::_thesis: for n being Element of NAT st n >= k holds
||.((seq . n) - g).|| < r
let n be Element of NAT ; ::_thesis: ( n >= k implies ||.((seq . n) - g).|| < r )
assume  n >= k ; ::_thesis: ||.((seq . n) - g).|| < r
then  dist ((seq . n),g) < r by A2;
hence  ||.((seq . n) - g).|| < r by CSSPACE:def_16; ::_thesis: verum
end;
 ( 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 implies seq is convergent )
proof
given g being Point of X such that A3: 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 ; ::_thesis: seq is convergent
take  g ; :: according to CLVECT_2:def_1 ::_thesis: 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
let r be Real; ::_thesis: ( r > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq . n),g) < r )
assume  r > 0 ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq . n),g) < r
then consider m1 being Element of NAT  such that
A4: for n being Element of NAT st n >= m1 holds
||.((seq . n) - g).|| < r by A3;
take k = m1; ::_thesis: for n being Element of NAT st n >= k holds
dist ((seq . n),g) < r
let n be Element of NAT ; ::_thesis: ( n >= k implies dist ((seq . n),g) < r )
assume  n >= k ; ::_thesis: dist ((seq . n),g) < r
then  ||.((seq . n) - g).|| < r by A4;
hence  dist ((seq . n),g) < r by CSSPACE:def_16; ::_thesis: verum
end;
hence  ( 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 implies seq is convergent ) ; ::_thesis: verum
end;

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 ) & ( 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
proof
 for x, y 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),x) < r ) & ( 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),y) < r ) holds
x = y
proof
given x, y being Point of X such that A2: 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),x) < r and
A3: 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),y) < r and
A4: x <> y ; ::_thesis: contradiction
A5: dist (x,y) > 0 by A4, CSSPACE:54;
then A6: (dist (x,y)) / 4 > 0 / 4 by XREAL_1:74;
then consider m1 being Element of NAT  such that
A7: for n being Element of NAT st n >= m1 holds
dist ((seq . n),x) < (dist (x,y)) / 4 by A2;
consider m2 being Element of NAT  such that
A8: for n being Element of NAT st n >= m2 holds
dist ((seq . n),y) < (dist (x,y)) / 4 by A3, A6;
A9: now__::_thesis:_not_m1_>=_m2
assume  m1 >= m2 ; ::_thesis: contradiction
then A10: dist ((seq . m1),y) < (dist (x,y)) / 4 by A8;
 dist (x,y) = dist ((x - (seq . m1)),(y - (seq . m1))) by CSSPACE:58;
then A11: dist (x,y) <= (dist ((seq . m1),x)) + (dist ((seq . m1),y)) by CSSPACE:59;
 dist ((seq . m1),x) < (dist (x,y)) / 4 by A7;
then  (dist ((seq . m1),x)) + (dist ((seq . m1),y)) < ((dist (x,y)) / 4) + ((dist (x,y)) / 4) by A10, XREAL_1:8;
then  dist (x,y) <= (dist (x,y)) / 2 by A11, XXREAL_0:2;
hence  contradiction by A5, XREAL_1:216; ::_thesis: verum
end;
now__::_thesis:_not_m1_<=_m2
assume  m1 <= m2 ; ::_thesis: contradiction
then A12: dist ((seq . m2),x) < (dist (x,y)) / 4 by A7;
 dist (x,y) = dist ((x - (seq . m2)),(y - (seq . m2))) by CSSPACE:58;
then A13: dist (x,y) <= (dist ((seq . m2),x)) + (dist ((seq . m2),y)) by CSSPACE:59;
 dist ((seq . m2),y) < (dist (x,y)) / 4 by A8;
then  (dist ((seq . m2),x)) + (dist ((seq . m2),y)) < ((dist (x,y)) / 4) + ((dist (x,y)) / 4) by A12, XREAL_1:8;
then  dist (x,y) <= (dist (x,y)) / 2 by A13, XXREAL_0:2;
hence  contradiction by A5, XREAL_1:216; ::_thesis: verum
end;
hence  contradiction by A9; ::_thesis: verum
end;
hence  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 ) & ( 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 ; ::_thesis: verum
end;
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 & x in rng seq holds
lim seq = x
proof
let X be ComplexUnitarySpace; ::_thesis: for x being Point of X
for seq being sequence of X st seq is constant & x in rng seq holds
lim seq = x
let x be Point of X; ::_thesis: for seq being sequence of X st seq is constant & x in rng seq holds
lim seq = x
let seq be sequence of X; ::_thesis: ( seq is constant & x in rng seq implies lim seq = x )
assume that
A1: seq is constant and
A2: x in rng seq ; ::_thesis: lim seq = x
consider y being Point of X such that
A3: rng seq = {y} by A1, FUNCT_2:111;
consider w being Point of X such that
A4: for n being Nat holds seq . n = w by A1, VALUED_0:def_18;
A5: x = y by A2, A3, TARSKI:def_1;
A6: now__::_thesis:_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),x)_<_r
let r be Real; ::_thesis: ( r > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq . n),x) < r )
assume A7: r > 0 ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq . n),x) < r
take m = 0 ; ::_thesis: for n being Element of NAT st n >= m holds
dist ((seq . n),x) < r
let n be Element of NAT ; ::_thesis: ( n >= m implies dist ((seq . n),x) < r )
assume  n >= m ; ::_thesis: dist ((seq . n),x) < r
 n in NAT ;
then  n in dom seq by NORMSP_1:12;
then  seq . n in rng seq by FUNCT_1:def_3;
then  w in rng seq by A4;
then  w = x by A3, A5, TARSKI:def_1;
then  seq . n = x by A4;
hence  dist ((seq . n),x) < r by A7, CSSPACE:50; ::_thesis: verum
end;
 seq is convergent by A1, Th1;
hence  lim seq = x by A6, Def2; ::_thesis: verum
end;

theorem :: CLVECT_2:11
for X being ComplexUnitarySpace
for x being Point of X
for seq being sequence of X st seq is constant & ex n being Element of NAT st seq . n = x holds
lim seq = x
proof
let X be ComplexUnitarySpace; ::_thesis: for x being Point of X
for seq being sequence of X st seq is constant & ex n being Element of NAT st seq . n = x holds
lim seq = x
let x be Point of X; ::_thesis: for seq being sequence of X st seq is constant & ex n being Element of NAT st seq . n = x holds
lim seq = x
let seq be sequence of X; ::_thesis: ( seq is constant & ex n being Element of NAT st seq . n = x implies lim seq = x )
assume that
A1: seq is constant and
A2: ex n being Element of NAT st seq . n = x ; ::_thesis: lim seq = x
consider n being Element of NAT  such that
A3: seq . n = x by A2;
 n in NAT ;
then  n in dom seq by NORMSP_1:12;
then  x in rng seq by A3, FUNCT_1:def_3;
hence  lim seq = x by A1, Th10; ::_thesis: verum
end;

theorem :: CLVECT_2:12
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is convergent & 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
proof
let X be ComplexUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X st seq1 is convergent & 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
let seq1, seq2 be sequence of X; ::_thesis: ( seq1 is convergent & ex k being Element of NAT st
for n being Element of NAT st n >= k holds
seq2 . n = seq1 . n implies lim seq1 = lim seq2 )
assume that
A1: seq1 is convergent and
A2: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
seq2 . n = seq1 . n ; ::_thesis: lim seq1 = lim seq2
consider k being Element of NAT  such that
A3: for n being Element of NAT st n >= k holds
seq2 . n = seq1 . n by A2;
A4: now__::_thesis:_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_((seq2_._n),(lim_seq1))_<_r
let r be Real; ::_thesis: ( r > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq2 . n),(lim seq1)) < r )
assume  r > 0 ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq2 . n),(lim seq1)) < r
then consider m1 being Element of NAT  such that
A5: for n being Element of NAT st n >= m1 holds
dist ((seq1 . n),(lim seq1)) < r by A1, Def2;
A6: now__::_thesis:_(_m1_<=_k_implies_ex_m_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_n_>=_m_holds_
dist_((seq2_._n),(lim_seq1))_<_r_)
assume A7: m1 <= k ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq2 . n),(lim seq1)) < r
take m = k; ::_thesis: for n being Element of NAT st n >= m holds
dist ((seq2 . n),(lim seq1)) < r
let n be Element of NAT ; ::_thesis: ( n >= m implies dist ((seq2 . n),(lim seq1)) < r )
assume A8: n >= m ; ::_thesis: dist ((seq2 . n),(lim seq1)) < r
then  n >= m1 by A7, XXREAL_0:2;
then  dist ((seq1 . n),(lim seq1)) < r by A5;
hence  dist ((seq2 . n),(lim seq1)) < r by A3, A8; ::_thesis: verum
end;
now__::_thesis:_(_k_<=_m1_implies_ex_m_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_n_>=_m_holds_
dist_((seq2_._n),(lim_seq1))_<_r_)
assume A9: k <= m1 ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq2 . n),(lim seq1)) < r
take m = m1; ::_thesis: for n being Element of NAT st n >= m holds
dist ((seq2 . n),(lim seq1)) < r
let n be Element of NAT ; ::_thesis: ( n >= m implies dist ((seq2 . n),(lim seq1)) < r )
assume A10: n >= m ; ::_thesis: dist ((seq2 . n),(lim seq1)) < r
then  seq2 . n = seq1 . n by A3, A9, XXREAL_0:2;
hence  dist ((seq2 . n),(lim seq1)) < r by A5, A10; ::_thesis: verum
end;
hence  ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq2 . n),(lim seq1)) < r by A6; ::_thesis: verum
end;
 seq2 is convergent by A1, A2, Th2;
hence  lim seq1 = lim seq2 by A4, Def2; ::_thesis: verum
end;

theorem Th13: :: CLVECT_2:13
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is convergent & seq2 is convergent holds
lim (seq1 + seq2) = (lim seq1) + (lim seq2)
proof
let X be ComplexUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X st seq1 is convergent & seq2 is convergent holds
lim (seq1 + seq2) = (lim seq1) + (lim seq2)
let seq1, seq2 be sequence of X; ::_thesis: ( seq1 is convergent & seq2 is convergent implies lim (seq1 + seq2) = (lim seq1) + (lim seq2) )
assume that
A1: seq1 is convergent and
A2: seq2 is convergent ; ::_thesis: lim (seq1 + seq2) = (lim seq1) + (lim seq2)
set g2 = lim seq2;
set g1 = lim seq1;
set g = (lim seq1) + (lim seq2);
A3: now__::_thesis:_for_r_being_Real_st_r_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_n_>=_k_holds_
dist_(((seq1_+_seq2)_._n),((lim_seq1)_+_(lim_seq2)))_<_r
let r be Real; ::_thesis: ( r > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
dist (((seq1 + seq2) . n),((lim seq1) + (lim seq2))) < r )
assume  r > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
dist (((seq1 + seq2) . n),((lim seq1) + (lim seq2))) < r
then A4: r / 2 > 0 by XREAL_1:215;
then consider m1 being Element of NAT  such that
A5: for n being Element of NAT st n >= m1 holds
dist ((seq1 . n),(lim seq1)) < r / 2 by A1, Def2;
consider m2 being Element of NAT  such that
A6: for n being Element of NAT st n >= m2 holds
dist ((seq2 . n),(lim seq2)) < r / 2 by A2, A4, Def2;
take k = m1 + m2; ::_thesis: for n being Element of NAT st n >= k holds
dist (((seq1 + seq2) . n),((lim seq1) + (lim seq2))) < r
let n be Element of NAT ; ::_thesis: ( n >= k implies dist (((seq1 + seq2) . n),((lim seq1) + (lim seq2))) < r )
assume A7: n >= k ; ::_thesis: dist (((seq1 + seq2) . n),((lim seq1) + (lim seq2))) < r
 k >= m2 by NAT_1:12;
then  n >= m2 by A7, XXREAL_0:2;
then A8: dist ((seq2 . n),(lim seq2)) < r / 2 by A6;
 dist (((seq1 + seq2) . n),((lim seq1) + (lim seq2))) = dist (((seq1 . n) + (seq2 . n)),((lim seq1) + (lim seq2))) by NORMSP_1:def_2;
then A9: dist (((seq1 + seq2) . n),((lim seq1) + (lim seq2))) <= (dist ((seq1 . n),(lim seq1))) + (dist ((seq2 . n),(lim seq2))) by CSSPACE:56;
 m1 + m2 >= m1 by NAT_1:12;
then  n >= m1 by A7, XXREAL_0:2;
then  dist ((seq1 . n),(lim seq1)) < r / 2 by A5;
then  (dist ((seq1 . n),(lim seq1))) + (dist ((seq2 . n),(lim seq2))) < (r / 2) + (r / 2) by A8, XREAL_1:8;
hence  dist (((seq1 + seq2) . n),((lim seq1) + (lim seq2))) < r by A9, XXREAL_0:2; ::_thesis: verum
end;
 seq1 + seq2 is convergent by A1, A2, Th3;
hence  lim (seq1 + seq2) = (lim seq1) + (lim seq2) by A3, Def2; ::_thesis: verum
end;

theorem Th14: :: CLVECT_2:14
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is convergent & seq2 is convergent holds
lim (seq1 - seq2) = (lim seq1) - (lim seq2)
proof
let X be ComplexUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X st seq1 is convergent & seq2 is convergent holds
lim (seq1 - seq2) = (lim seq1) - (lim seq2)
let seq1, seq2 be sequence of X; ::_thesis: ( seq1 is convergent & seq2 is convergent implies lim (seq1 - seq2) = (lim seq1) - (lim seq2) )
assume that
A1: seq1 is convergent and
A2: seq2 is convergent ; ::_thesis: lim (seq1 - seq2) = (lim seq1) - (lim seq2)
set g2 = lim seq2;
set g1 = lim seq1;
set g = (lim seq1) - (lim seq2);
A3: now__::_thesis:_for_r_being_Real_st_r_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_n_>=_k_holds_
dist_(((seq1_-_seq2)_._n),((lim_seq1)_-_(lim_seq2)))_<_r
let r be Real; ::_thesis: ( r > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
dist (((seq1 - seq2) . n),((lim seq1) - (lim seq2))) < r )
assume  r > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
dist (((seq1 - seq2) . n),((lim seq1) - (lim seq2))) < r
then A4: r / 2 > 0 by XREAL_1:215;
then consider m1 being Element of NAT  such that
A5: for n being Element of NAT st n >= m1 holds
dist ((seq1 . n),(lim seq1)) < r / 2 by A1, Def2;
consider m2 being Element of NAT  such that
A6: for n being Element of NAT st n >= m2 holds
dist ((seq2 . n),(lim seq2)) < r / 2 by A2, A4, Def2;
take k = m1 + m2; ::_thesis: for n being Element of NAT st n >= k holds
dist (((seq1 - seq2) . n),((lim seq1) - (lim seq2))) < r
let n be Element of NAT ; ::_thesis: ( n >= k implies dist (((seq1 - seq2) . n),((lim seq1) - (lim seq2))) < r )
assume A7: n >= k ; ::_thesis: dist (((seq1 - seq2) . n),((lim seq1) - (lim seq2))) < r
 k >= m2 by NAT_1:12;
then  n >= m2 by A7, XXREAL_0:2;
then A8: dist ((seq2 . n),(lim seq2)) < r / 2 by A6;
 dist (((seq1 - seq2) . n),((lim seq1) - (lim seq2))) = dist (((seq1 . n) - (seq2 . n)),((lim seq1) - (lim seq2))) by NORMSP_1:def_3;
then A9: dist (((seq1 - seq2) . n),((lim seq1) - (lim seq2))) <= (dist ((seq1 . n),(lim seq1))) + (dist ((seq2 . n),(lim seq2))) by CSSPACE:57;
 m1 + m2 >= m1 by NAT_1:12;
then  n >= m1 by A7, XXREAL_0:2;
then  dist ((seq1 . n),(lim seq1)) < r / 2 by A5;
then  (dist ((seq1 . n),(lim seq1))) + (dist ((seq2 . n),(lim seq2))) < (r / 2) + (r / 2) by A8, XREAL_1:8;
hence  dist (((seq1 - seq2) . n),((lim seq1) - (lim seq2))) < r by A9, XXREAL_0:2; ::_thesis: verum
end;
 seq1 - seq2 is convergent by A1, A2, Th4;
hence  lim (seq1 - seq2) = (lim seq1) - (lim seq2) by A3, Def2; ::_thesis: verum
end;

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)
proof
let X be ComplexUnitarySpace; ::_thesis: for z being Complex
for seq being sequence of X st seq is convergent holds
lim (z * seq) = z * (lim seq)
let z be Complex; ::_thesis: for seq being sequence of X st seq is convergent holds
lim (z * seq) = z * (lim seq)
let seq be sequence of X; ::_thesis: ( seq is convergent implies lim (z * seq) = z * (lim seq) )
set g = lim seq;
set h = z * (lim seq);
A1: now__::_thesis:_(_z_=_0_implies_for_r_being_Real_st_r_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_n_>=_k_holds_
dist_(((z_*_seq)_._n),(z_*_(lim_seq)))_<_r_)
set m1 = the Element of NAT ;
assume A2: z = 0 ; ::_thesis: for r being Real st r > 0 holds
ex k being Element of NAT st
for n being Element of NAT st n >= k holds
dist (((z * seq) . n),(z * (lim seq))) < r
let r be Real; ::_thesis: ( r > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
dist (((z * seq) . n),(z * (lim seq))) < r )
assume A3: r > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
dist (((z * seq) . n),(z * (lim seq))) < r
take k = the Element of NAT ; ::_thesis: for n being Element of NAT st n >= k holds
dist (((z * seq) . n),(z * (lim seq))) < r
let n be Element of NAT ; ::_thesis: ( n >= k implies dist (((z * seq) . n),(z * (lim seq))) < r )
assume  n >= k ; ::_thesis: dist (((z * seq) . n),(z * (lim seq))) < r
dist ((z * (seq . n)),(z * (lim seq))) = dist ((0c * (seq . n)),H1(X)) by A2, CLVECT_1:1
.= dist (H1(X),H1(X)) by CLVECT_1:1
.= 0 by CSSPACE:50 ;
hence  dist (((z * seq) . n),(z * (lim seq))) < r by A3, CLVECT_1:def_14; ::_thesis: verum
end;
assume A4: seq is convergent ; ::_thesis: lim (z * seq) = z * (lim seq)
A5: now__::_thesis:_(_z_<>_0_implies_for_r_being_Real_st_r_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_n_>=_k_holds_
dist_(((z_*_seq)_._n),(z_*_(lim_seq)))_<_r_)
A6: 0 / |.z.| = 0 ;
assume A7: z <> 0 ; ::_thesis: for r being Real st r > 0 holds
ex k being Element of NAT st
for n being Element of NAT st n >= k holds
dist (((z * seq) . n),(z * (lim seq))) < r
then A8: |.z.| > 0 by COMPLEX1:47;
let r be Real; ::_thesis: ( r > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
dist (((z * seq) . n),(z * (lim seq))) < r )
assume  r > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
dist (((z * seq) . n),(z * (lim seq))) < r
then  r / |.z.| > 0 by A8, A6, XREAL_1:74;
then consider m1 being Element of NAT  such that
A9: for n being Element of NAT st n >= m1 holds
dist ((seq . n),(lim seq)) < r / |.z.| by A4, Def2;
take k = m1; ::_thesis: for n being Element of NAT st n >= k holds
dist (((z * seq) . n),(z * (lim seq))) < r
let n be Element of NAT ; ::_thesis: ( n >= k implies dist (((z * seq) . n),(z * (lim seq))) < r )
assume  n >= k ; ::_thesis: dist (((z * seq) . n),(z * (lim seq))) < r
then A10: dist ((seq . n),(lim seq)) < r / |.z.| by A9;
A11: |.z.| <> 0 by A7, COMPLEX1:47;
A12: |.z.| * (r / |.z.|) = |.z.| * ((|.z.| ") * r) by XCMPLX_0:def_9
.= (|.z.| * (|.z.| ")) * r
.= 1 * r by A11, XCMPLX_0:def_7
.= r ;
dist ((z * (seq . n)),(z * (lim seq))) = ||.((z * (seq . n)) - (z * (lim seq))).|| by CSSPACE:def_16
.= ||.(z * ((seq . n) - (lim seq))).|| by CLVECT_1:9
.= |.z.| * ||.((seq . n) - (lim seq)).|| by CSSPACE:43
.= |.z.| * (dist ((seq . n),(lim seq))) by CSSPACE:def_16 ;
then  dist ((z * (seq . n)),(z * (lim seq))) < r by A8, A10, A12, XREAL_1:68;
hence  dist (((z * seq) . n),(z * (lim seq))) < r by CLVECT_1:def_14; ::_thesis: verum
end;
 z * seq is convergent by A4, Th5;
hence  lim (z * seq) = z * (lim seq) by A1, A5, Def2; ::_thesis: verum
end;

theorem Th16: :: CLVECT_2:16
for X being ComplexUnitarySpace
for seq being sequence of X st seq is convergent holds
lim (- seq) = - (lim seq)
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X st seq is convergent holds
lim (- seq) = - (lim seq)
let seq be sequence of X; ::_thesis: ( seq is convergent implies lim (- seq) = - (lim seq) )
assume  seq is convergent ; ::_thesis: lim (- seq) = - (lim seq)
then  lim ((- 1r) * seq) = (- 1r) * (lim seq) by Th15;
then  lim (- seq) = (- 1r) * (lim seq) by CSSPACE:70;
hence  lim (- seq) = - (lim seq) by CLVECT_1:3; ::_thesis: verum
end;

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
proof
let X be ComplexUnitarySpace; ::_thesis: for x being Point of X
for seq being sequence of X st seq is convergent holds
lim (seq + x) = (lim seq) + x
let x be Point of X; ::_thesis: for seq being sequence of X st seq is convergent holds
lim (seq + x) = (lim seq) + x
let seq be sequence of X; ::_thesis: ( seq is convergent implies lim (seq + x) = (lim seq) + x )
set g = lim seq;
assume A1: seq is convergent ; ::_thesis: lim (seq + x) = (lim seq) + x
A2: now__::_thesis:_for_r_being_Real_st_r_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_n_>=_k_holds_
dist_(((seq_+_x)_._n),((lim_seq)_+_x))_<_r
let r be Real; ::_thesis: ( r > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
dist (((seq + x) . n),((lim seq) + x)) < r )
assume  r > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
dist (((seq + x) . n),((lim seq) + x)) < r
then consider m1 being Element of NAT  such that
A3: for n being Element of NAT st n >= m1 holds
dist ((seq . n),(lim seq)) < r by A1, Def2;
take k = m1; ::_thesis: for n being Element of NAT st n >= k holds
dist (((seq + x) . n),((lim seq) + x)) < r
let n be Element of NAT ; ::_thesis: ( n >= k implies dist (((seq + x) . n),((lim seq) + x)) < r )
assume  n >= k ; ::_thesis: dist (((seq + x) . n),((lim seq) + x)) < r
then A4: dist ((seq . n),(lim seq)) < r by A3;
dist ((seq . n),(lim seq)) = dist (((seq . n) - (- x)),((lim seq) - (- x))) by CSSPACE:58
.= dist (((seq . n) + (- (- x))),((lim seq) - (- x))) by RLVECT_1:def_11
.= dist (((seq . n) + x),((lim seq) - (- x))) by RLVECT_1:17
.= dist (((seq . n) + x),((lim seq) + (- (- x)))) by RLVECT_1:def_11
.= dist (((seq . n) + x),((lim seq) + x)) by RLVECT_1:17 ;
hence  dist (((seq + x) . n),((lim seq) + x)) < r by A4, BHSP_1:def_6; ::_thesis: verum
end;
 seq + x is convergent by A1, Th7;
hence  lim (seq + x) = (lim seq) + x by A2, Def2; ::_thesis: verum
end;

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
proof
let X be ComplexUnitarySpace; ::_thesis: for x being Point of X
for seq being sequence of X st seq is convergent holds
lim (seq - x) = (lim seq) - x
let x be Point of X; ::_thesis: for seq being sequence of X st seq is convergent holds
lim (seq - x) = (lim seq) - x
let seq be sequence of X; ::_thesis: ( seq is convergent implies lim (seq - x) = (lim seq) - x )
assume  seq is convergent ; ::_thesis: lim (seq - x) = (lim seq) - x
then  lim (seq + (- x)) = (lim seq) + (- x) by Th17;
then  lim (seq - x) = (lim seq) + (- x) by CSSPACE:71;
hence  lim (seq - x) = (lim seq) - x by RLVECT_1:def_11; ::_thesis: verum
end;

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 )
proof
let X be ComplexUnitarySpace; ::_thesis: 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 )
let g be Point of X; ::_thesis: 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 )
let seq be sequence of X; ::_thesis: ( seq is convergent implies ( 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 ) )
assume A1: seq is convergent ; ::_thesis: ( 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 )
thus  ( lim seq = g implies 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 ) ::_thesis: ( ( 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 ) implies lim seq = g )
proof
assume A2: lim seq = g ; ::_thesis: 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
let r be Real; ::_thesis: ( r > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((seq . n) - g).|| < r )
assume  r > 0 ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((seq . n) - g).|| < r
then consider m1 being Element of NAT  such that
A3: for n being Element of NAT st n >= m1 holds
dist ((seq . n),g) < r by A1, A2, Def2;
take k = m1; ::_thesis: for n being Element of NAT st n >= k holds
||.((seq . n) - g).|| < r
let n be Element of NAT ; ::_thesis: ( n >= k implies ||.((seq . n) - g).|| < r )
assume  n >= k ; ::_thesis: ||.((seq . n) - g).|| < r
then  dist ((seq . n),g) < r by A3;
hence  ||.((seq . n) - g).|| < r by CSSPACE:def_16; ::_thesis: verum
end;
 ( ( 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 ) implies lim seq = g )
proof
assume A4: 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 ; ::_thesis: lim seq = g
now__::_thesis:_for_r_being_Real_st_r_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_n_>=_k_holds_
dist_((seq_._n),g)_<_r
let r be Real; ::_thesis: ( r > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
dist ((seq . n),g) < r )
assume  r > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
dist ((seq . n),g) < r
then consider m1 being Element of NAT  such that
A5: for n being Element of NAT st n >= m1 holds
||.((seq . n) - g).|| < r by A4;
take k = m1; ::_thesis: for n being Element of NAT st n >= k holds
dist ((seq . n),g) < r
let n be Element of NAT ; ::_thesis: ( n >= k implies dist ((seq . n),g) < r )
assume  n >= k ; ::_thesis: dist ((seq . n),g) < r
then  ||.((seq . n) - g).|| < r by A5;
hence  dist ((seq . n),g) < r by CSSPACE:def_16; ::_thesis: verum
end;
hence  lim seq = g by A1, Def2; ::_thesis: verum
end;
hence  ( ( 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 ) implies lim seq = g ) ; ::_thesis: verum
end;

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).||
proof
deffunc H2( Element of NAT ) ->  Element of REAL = ||.(seq . $1).||;
consider s being Real_Sequence such that
A1: for n being Element of NAT holds s . n = H2(n) from SEQ_1:sch_1();
take  s ; ::_thesis: for n being Element of NAT holds s . n = ||.(seq . n).||
thus  for n being Element of NAT holds s . n = ||.(seq . n).|| by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Real_Sequence st ( for n being Element of NAT holds b1 . n = ||.(seq . n).|| ) & ( for n being Element of NAT holds b2 . n = ||.(seq . n).|| ) holds
b1 = b2
proof
let s, t be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = ||.(seq . n).|| ) & ( for n being Element of NAT holds t . n = ||.(seq . n).|| ) implies s = t )
assume that
A2: for n being Element of NAT holds s . n = ||.(seq . n).|| and
A3: for n being Element of NAT holds t . n = ||.(seq . n).|| ; ::_thesis: s = t
now__::_thesis:_for_n_being_Element_of_NAT_holds_s_._n_=_t_._n
let n be Element of NAT ; ::_thesis: s . n = t . n
 s . n = ||.(seq . n).|| by A2;
hence  s . n = t . n by A3; ::_thesis: verum
end;
hence  s = t by FUNCT_2:63; ::_thesis: verum
end;
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
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X st seq is convergent holds
||.seq.|| is convergent
let seq be sequence of X; ::_thesis: ( seq is convergent implies ||.seq.|| is convergent )
assume  seq is convergent ; ::_thesis: ||.seq.|| is convergent
then consider g being Point of X such that
A1: 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 by Th9;
now__::_thesis:_for_r_being_real_number_st_r_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_k_<=_n_holds_
abs_((||.seq.||_._n)_-_||.g.||)_<_r
let r be real number ; ::_thesis: ( r > 0 implies ex k being Element of NAT st
for n being Element of NAT st k <= n holds
abs ((||.seq.|| . n) - ||.g.||) < r )
assume A2: r > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st k <= n holds
abs ((||.seq.|| . n) - ||.g.||) < r
 r is Real by XREAL_0:def_1;
then consider m1 being Element of NAT  such that
A3: for n being Element of NAT st n >= m1 holds
||.((seq . n) - g).|| < r by A1, A2;
take k = m1; ::_thesis: for n being Element of NAT st k <= n holds
abs ((||.seq.|| . n) - ||.g.||) < r
now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_k_holds_
abs_((||.seq.||_._n)_-_||.g.||)_<_r
let n be Element of NAT ; ::_thesis: ( n >= k implies abs ((||.seq.|| . n) - ||.g.||) < r )
assume  n >= k ; ::_thesis: abs ((||.seq.|| . n) - ||.g.||) < r
then A4: ||.((seq . n) - g).|| < r by A3;
 abs (||.(seq . n).|| - ||.g.||) <= ||.((seq . n) - g).|| by CSSPACE:49;
then  abs (||.(seq . n).|| - ||.g.||) < r by A4, XXREAL_0:2;
hence  abs ((||.seq.|| . n) - ||.g.||) < r by Def3; ::_thesis: verum
end;
hence  for n being Element of NAT st k <= n holds
abs ((||.seq.|| . n) - ||.g.||) < r ; ::_thesis: verum
end;
hence  ||.seq.|| is convergent by SEQ_2:def_6; ::_thesis: verum
end;

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 & lim seq = g holds
( ||.seq.|| is convergent & lim ||.seq.|| = ||.g.|| )
proof
let X be ComplexUnitarySpace; ::_thesis: for g being Point of X
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.seq.|| is convergent & lim ||.seq.|| = ||.g.|| )
let g be Point of X; ::_thesis: for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.seq.|| is convergent & lim ||.seq.|| = ||.g.|| )
let seq be sequence of X; ::_thesis: ( seq is convergent & lim seq = g implies ( ||.seq.|| is convergent & lim ||.seq.|| = ||.g.|| ) )
assume that
A1: seq is convergent and
A2: lim seq = g ; ::_thesis: ( ||.seq.|| is convergent & lim ||.seq.|| = ||.g.|| )
A3: now__::_thesis:_for_r_being_real_number_st_r_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_k_<=_n_holds_
abs_((||.seq.||_._n)_-_||.g.||)_<_r
let r be real number ; ::_thesis: ( r > 0 implies ex k being Element of NAT st
for n being Element of NAT st k <= n holds
abs ((||.seq.|| . n) - ||.g.||) < r )
assume A4: r > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st k <= n holds
abs ((||.seq.|| . n) - ||.g.||) < r
 r is Real by XREAL_0:def_1;
then consider m1 being Element of NAT  such that
A5: for n being Element of NAT st n >= m1 holds
||.((seq . n) - g).|| < r by A1, A2, A4, Th19;
take k = m1; ::_thesis: for n being Element of NAT st k <= n holds
abs ((||.seq.|| . n) - ||.g.||) < r
now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_k_holds_
abs_((||.seq.||_._n)_-_||.g.||)_<_r
let n be Element of NAT ; ::_thesis: ( n >= k implies abs ((||.seq.|| . n) - ||.g.||) < r )
assume  n >= k ; ::_thesis: abs ((||.seq.|| . n) - ||.g.||) < r
then A6: ||.((seq . n) - g).|| < r by A5;
 abs (||.(seq . n).|| - ||.g.||) <= ||.((seq . n) - g).|| by CSSPACE:49;
then  abs (||.(seq . n).|| - ||.g.||) < r by A6, XXREAL_0:2;
hence  abs ((||.seq.|| . n) - ||.g.||) < r by Def3; ::_thesis: verum
end;
hence  for n being Element of NAT st k <= n holds
abs ((||.seq.|| . n) - ||.g.||) < r ; ::_thesis: verum
end;
 ||.seq.|| is convergent by A1, Th20;
hence  ( ||.seq.|| is convergent & lim ||.seq.|| = ||.g.|| ) by A3, SEQ_2:def_7; ::_thesis: verum
end;

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 & lim seq = g holds
( ||.(seq - g).|| is convergent & lim ||.(seq - g).|| = 0 )
proof
let X be ComplexUnitarySpace; ::_thesis: for g being Point of X
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.(seq - g).|| is convergent & lim ||.(seq - g).|| = 0 )
let g be Point of X; ::_thesis: for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.(seq - g).|| is convergent & lim ||.(seq - g).|| = 0 )
let seq be sequence of X; ::_thesis: ( seq is convergent & lim seq = g implies ( ||.(seq - g).|| is convergent & lim ||.(seq - g).|| = 0 ) )
assume that
A1: seq is convergent and
A2: lim seq = g ; ::_thesis: ( ||.(seq - g).|| is convergent & lim ||.(seq - g).|| = 0 )
A3: now__::_thesis:_for_r_being_real_number_st_r_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_n_>=_k_holds_
abs_((||.(seq_-_g).||_._n)_-_0)_<_r
let r be real number ; ::_thesis: ( r > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs ((||.(seq - g).|| . n) - 0) < r )
assume A4: r > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs ((||.(seq - g).|| . n) - 0) < r
 r is Real by XREAL_0:def_1;
then consider m1 being Element of NAT  such that
A5: for n being Element of NAT st n >= m1 holds
||.((seq . n) - g).|| < r by A1, A2, A4, Th19;
take k = m1; ::_thesis: for n being Element of NAT st n >= k holds
abs ((||.(seq - g).|| . n) - 0) < r
let n be Element of NAT ; ::_thesis: ( n >= k implies abs ((||.(seq - g).|| . n) - 0) < r )
assume  n >= k ; ::_thesis: abs ((||.(seq - g).|| . n) - 0) < r
then  ||.((seq . n) - g).|| < r by A5;
then A6: ||.(((seq . n) - g) - H1(X)).|| < r by RLVECT_1:13;
 abs (||.((seq . n) - g).|| - ||.H1(X).||) <= ||.(((seq . n) - g) - H1(X)).|| by CSSPACE:49;
then  abs (||.((seq . n) - g).|| - ||.H1(X).||) < r by A6, XXREAL_0:2;
then  abs (||.((seq . n) - g).|| - 0) < r by CSSPACE:42;
then  abs (||.((seq - g) . n).|| - 0) < r by NORMSP_1:def_4;
hence  abs ((||.(seq - g).|| . n) - 0) < r by Def3; ::_thesis: verum
end;
 ||.(seq - g).|| is convergent by A1, Th8, Th20;
hence  ( ||.(seq - g).|| is convergent & lim ||.(seq - g).|| = 0 ) by A3, SEQ_2:def_7; ::_thesis: verum
end;

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)
proof
deffunc H2( Element of NAT ) ->  Element of REAL = dist ((seq . $1),x);
consider s being Real_Sequence such that
A1: for n being Element of NAT holds s . n = H2(n) from SEQ_1:sch_1();
take  s ; ::_thesis: for n being Element of NAT holds s . n = dist ((seq . n),x)
thus  for n being Element of NAT holds s . n = dist ((seq . n),x) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Real_Sequence st ( for n being Element of NAT holds b1 . n = dist ((seq . n),x) ) & ( for n being Element of NAT holds b2 . n = dist ((seq . n),x) ) holds
b1 = b2
proof
let s, t be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = dist ((seq . n),x) ) & ( for n being Element of NAT holds t . n = dist ((seq . n),x) ) implies s = t )
assume that
A2: for n being Element of NAT holds s . n = dist ((seq . n),x) and
A3: for n being Element of NAT holds t . n = dist ((seq . n),x) ; ::_thesis: s = t
now__::_thesis:_for_n_being_Element_of_NAT_holds_s_._n_=_t_._n
let n be Element of NAT ; ::_thesis: s . n = t . n
 s . n = dist ((seq . n),x) by A2;
hence  s . n = t . n by A3; ::_thesis: verum
end;
hence  s = t by FUNCT_2:63; ::_thesis: verum
end;
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 & lim seq = g holds
dist (seq,g) is convergent
proof
let X be ComplexUnitarySpace; ::_thesis: for g being Point of X
for seq being sequence of X st seq is convergent & lim seq = g holds
dist (seq,g) is convergent
let g be Point of X; ::_thesis: for seq being sequence of X st seq is convergent & lim seq = g holds
dist (seq,g) is convergent
let seq be sequence of X; ::_thesis: ( seq is convergent & lim seq = g implies dist (seq,g) is convergent )
assume A1: ( seq is convergent & lim seq = g ) ; ::_thesis: dist (seq,g) is convergent
now__::_thesis:_for_r_being_real_number_st_r_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_k_<=_n_holds_
abs_(((dist_(seq,g))_._n)_-_0)_<_r
let r be real number ; ::_thesis: ( r > 0 implies ex k being Element of NAT st
for n being Element of NAT st k <= n holds
abs (((dist (seq,g)) . n) - 0) < r )
assume A2: r > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st k <= n holds
abs (((dist (seq,g)) . n) - 0) < r
 r is Real by XREAL_0:def_1;
then consider m1 being Element of NAT  such that
A3: for n being Element of NAT st n >= m1 holds
dist ((seq . n),g) < r by A1, A2, Def2;
take k = m1; ::_thesis: for n being Element of NAT st k <= n holds
abs (((dist (seq,g)) . n) - 0) < r
now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_k_holds_
abs_(((dist_(seq,g))_._n)_-_0)_<_r
let n be Element of NAT ; ::_thesis: ( n >= k implies abs (((dist (seq,g)) . n) - 0) < r )
 dist ((seq . n),g) >= 0 by CSSPACE:53;
then A4: abs ((dist ((seq . n),g)) - 0) = dist ((seq . n),g) by ABSVALUE:def_1;
assume  n >= k ; ::_thesis: abs (((dist (seq,g)) . n) - 0) < r
then  dist ((seq . n),g) < r by A3;
hence  abs (((dist (seq,g)) . n) - 0) < r by A4, Def4; ::_thesis: verum
end;
hence  for n being Element of NAT st k <= n holds
abs (((dist (seq,g)) . n) - 0) < r ; ::_thesis: verum
end;
hence  dist (seq,g) is convergent by SEQ_2:def_6; ::_thesis: verum
end;

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 & lim seq = g holds
( dist (seq,g) is convergent & lim (dist (seq,g)) = 0 )
proof
let X be ComplexUnitarySpace; ::_thesis: for g being Point of X
for seq being sequence of X st seq is convergent & lim seq = g holds
( dist (seq,g) is convergent & lim (dist (seq,g)) = 0 )
let g be Point of X; ::_thesis: for seq being sequence of X st seq is convergent & lim seq = g holds
( dist (seq,g) is convergent & lim (dist (seq,g)) = 0 )
let seq be sequence of X; ::_thesis: ( seq is convergent & lim seq = g implies ( dist (seq,g) is convergent & lim (dist (seq,g)) = 0 ) )
assume A1: ( seq is convergent & lim seq = g ) ; ::_thesis: ( dist (seq,g) is convergent & lim (dist (seq,g)) = 0 )
A2: now__::_thesis:_for_r_being_real_number_st_r_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_n_>=_k_holds_
abs_(((dist_(seq,g))_._n)_-_0)_<_r
let r be real number ; ::_thesis: ( r > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs (((dist (seq,g)) . n) - 0) < r )
assume A3: r > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs (((dist (seq,g)) . n) - 0) < r
 r is Real by XREAL_0:def_1;
then consider m1 being Element of NAT  such that
A4: for n being Element of NAT st n >= m1 holds
dist ((seq . n),g) < r by A1, A3, Def2;
take k = m1; ::_thesis: for n being Element of NAT st n >= k holds
abs (((dist (seq,g)) . n) - 0) < r
let n be Element of NAT ; ::_thesis: ( n >= k implies abs (((dist (seq,g)) . n) - 0) < r )
 dist ((seq . n),g) >= 0 by CSSPACE:53;
then A5: abs ((dist ((seq . n),g)) - 0) = dist ((seq . n),g) by ABSVALUE:def_1;
assume  n >= k ; ::_thesis: abs (((dist (seq,g)) . n) - 0) < r
then  dist ((seq . n),g) < r by A4;
hence  abs (((dist (seq,g)) . n) - 0) < r by A5, Def4; ::_thesis: verum
end;
 dist (seq,g) is convergent by A1, Th23;
hence  ( dist (seq,g) is convergent & lim (dist (seq,g)) = 0 ) by A2, SEQ_2:def_7; ::_thesis: verum
end;

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 & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 holds
( ||.(seq1 + seq2).|| is convergent & lim ||.(seq1 + seq2).|| = ||.(g1 + g2).|| )
proof
let X be ComplexUnitarySpace; ::_thesis: for g1, g2 being Point of X
for seq1, seq2 being sequence of X st seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 holds
( ||.(seq1 + seq2).|| is convergent & lim ||.(seq1 + seq2).|| = ||.(g1 + g2).|| )
let g1, g2 be Point of X; ::_thesis: for seq1, seq2 being sequence of X st seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 holds
( ||.(seq1 + seq2).|| is convergent & lim ||.(seq1 + seq2).|| = ||.(g1 + g2).|| )
let seq1, seq2 be sequence of X; ::_thesis: ( seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 implies ( ||.(seq1 + seq2).|| is convergent & lim ||.(seq1 + seq2).|| = ||.(g1 + g2).|| ) )
assume  ( seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 ) ; ::_thesis: ( ||.(seq1 + seq2).|| is convergent & lim ||.(seq1 + seq2).|| = ||.(g1 + g2).|| )
then  ( seq1 + seq2 is convergent & lim (seq1 + seq2) = g1 + g2 ) by Th3, Th13;
hence  ( ||.(seq1 + seq2).|| is convergent & lim ||.(seq1 + seq2).|| = ||.(g1 + g2).|| ) by Th21; ::_thesis: verum
end;

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 & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 holds
( ||.((seq1 + seq2) - (g1 + g2)).|| is convergent & lim ||.((seq1 + seq2) - (g1 + g2)).|| = 0 )
proof
let X be ComplexUnitarySpace; ::_thesis: for g1, g2 being Point of X
for seq1, seq2 being sequence of X st seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 holds
( ||.((seq1 + seq2) - (g1 + g2)).|| is convergent & lim ||.((seq1 + seq2) - (g1 + g2)).|| = 0 )
let g1, g2 be Point of X; ::_thesis: for seq1, seq2 being sequence of X st seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 holds
( ||.((seq1 + seq2) - (g1 + g2)).|| is convergent & lim ||.((seq1 + seq2) - (g1 + g2)).|| = 0 )
let seq1, seq2 be sequence of X; ::_thesis: ( seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 implies ( ||.((seq1 + seq2) - (g1 + g2)).|| is convergent & lim ||.((seq1 + seq2) - (g1 + g2)).|| = 0 ) )
assume  ( seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 ) ; ::_thesis: ( ||.((seq1 + seq2) - (g1 + g2)).|| is convergent & lim ||.((seq1 + seq2) - (g1 + g2)).|| = 0 )
then  ( seq1 + seq2 is convergent & lim (seq1 + seq2) = g1 + g2 ) by Th3, Th13;
hence  ( ||.((seq1 + seq2) - (g1 + g2)).|| is convergent & lim ||.((seq1 + seq2) - (g1 + g2)).|| = 0 ) by Th22; ::_thesis: verum
end;

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 & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 holds
( ||.(seq1 - seq2).|| is convergent & lim ||.(seq1 - seq2).|| = ||.(g1 - g2).|| )
proof
let X be ComplexUnitarySpace; ::_thesis: for g1, g2 being Point of X
for seq1, seq2 being sequence of X st seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 holds
( ||.(seq1 - seq2).|| is convergent & lim ||.(seq1 - seq2).|| = ||.(g1 - g2).|| )
let g1, g2 be Point of X; ::_thesis: for seq1, seq2 being sequence of X st seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 holds
( ||.(seq1 - seq2).|| is convergent & lim ||.(seq1 - seq2).|| = ||.(g1 - g2).|| )
let seq1, seq2 be sequence of X; ::_thesis: ( seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 implies ( ||.(seq1 - seq2).|| is convergent & lim ||.(seq1 - seq2).|| = ||.(g1 - g2).|| ) )
assume  ( seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 ) ; ::_thesis: ( ||.(seq1 - seq2).|| is convergent & lim ||.(seq1 - seq2).|| = ||.(g1 - g2).|| )
then  ( seq1 - seq2 is convergent & lim (seq1 - seq2) = g1 - g2 ) by Th4, Th14;
hence  ( ||.(seq1 - seq2).|| is convergent & lim ||.(seq1 - seq2).|| = ||.(g1 - g2).|| ) by Th21; ::_thesis: verum
end;

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 & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 holds
( ||.((seq1 - seq2) - (g1 - g2)).|| is convergent & lim ||.((seq1 - seq2) - (g1 - g2)).|| = 0 )
proof
let X be ComplexUnitarySpace; ::_thesis: for g1, g2 being Point of X
for seq1, seq2 being sequence of X st seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 holds
( ||.((seq1 - seq2) - (g1 - g2)).|| is convergent & lim ||.((seq1 - seq2) - (g1 - g2)).|| = 0 )
let g1, g2 be Point of X; ::_thesis: for seq1, seq2 being sequence of X st seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 holds
( ||.((seq1 - seq2) - (g1 - g2)).|| is convergent & lim ||.((seq1 - seq2) - (g1 - g2)).|| = 0 )
let seq1, seq2 be sequence of X; ::_thesis: ( seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 implies ( ||.((seq1 - seq2) - (g1 - g2)).|| is convergent & lim ||.((seq1 - seq2) - (g1 - g2)).|| = 0 ) )
assume  ( seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 ) ; ::_thesis: ( ||.((seq1 - seq2) - (g1 - g2)).|| is convergent & lim ||.((seq1 - seq2) - (g1 - g2)).|| = 0 )
then  ( seq1 - seq2 is convergent & lim (seq1 - seq2) = g1 - g2 ) by Th4, Th14;
hence  ( ||.((seq1 - seq2) - (g1 - g2)).|| is convergent & lim ||.((seq1 - seq2) - (g1 - g2)).|| = 0 ) by Th22; ::_thesis: verum
end;

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 & lim seq = g holds
( ||.(z * seq).|| is convergent & lim ||.(z * seq).|| = ||.(z * g).|| )
proof
let X be ComplexUnitarySpace; ::_thesis: for g being Point of X
for z being Complex
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.(z * seq).|| is convergent & lim ||.(z * seq).|| = ||.(z * g).|| )
let g be Point of X; ::_thesis: for z being Complex
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.(z * seq).|| is convergent & lim ||.(z * seq).|| = ||.(z * g).|| )
let z be Complex; ::_thesis: for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.(z * seq).|| is convergent & lim ||.(z * seq).|| = ||.(z * g).|| )
let seq be sequence of X; ::_thesis: ( seq is convergent & lim seq = g implies ( ||.(z * seq).|| is convergent & lim ||.(z * seq).|| = ||.(z * g).|| ) )
assume  ( seq is convergent & lim seq = g ) ; ::_thesis: ( ||.(z * seq).|| is convergent & lim ||.(z * seq).|| = ||.(z * g).|| )
then  ( z * seq is convergent & lim (z * seq) = z * g ) by Th5, Th15;
hence  ( ||.(z * seq).|| is convergent & lim ||.(z * seq).|| = ||.(z * g).|| ) by Th21; ::_thesis: verum
end;

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 & lim seq = g holds
( ||.((z * seq) - (z * g)).|| is convergent & lim ||.((z * seq) - (z * g)).|| = 0 )
proof
let X be ComplexUnitarySpace; ::_thesis: for g being Point of X
for z being Complex
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.((z * seq) - (z * g)).|| is convergent & lim ||.((z * seq) - (z * g)).|| = 0 )
let g be Point of X; ::_thesis: for z being Complex
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.((z * seq) - (z * g)).|| is convergent & lim ||.((z * seq) - (z * g)).|| = 0 )
let z be Complex; ::_thesis: for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.((z * seq) - (z * g)).|| is convergent & lim ||.((z * seq) - (z * g)).|| = 0 )
let seq be sequence of X; ::_thesis: ( seq is convergent & lim seq = g implies ( ||.((z * seq) - (z * g)).|| is convergent & lim ||.((z * seq) - (z * g)).|| = 0 ) )
assume  ( seq is convergent & lim seq = g ) ; ::_thesis: ( ||.((z * seq) - (z * g)).|| is convergent & lim ||.((z * seq) - (z * g)).|| = 0 )
then  ( z * seq is convergent & lim (z * seq) = z * g ) by Th5, Th15;
hence  ( ||.((z * seq) - (z * g)).|| is convergent & lim ||.((z * seq) - (z * g)).|| = 0 ) by Th22; ::_thesis: verum
end;

theorem :: CLVECT_2:31
for X being ComplexUnitarySpace
for g being Point of X
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.(- seq).|| is convergent & lim ||.(- seq).|| = ||.(- g).|| )
proof
let X be ComplexUnitarySpace; ::_thesis: for g being Point of X
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.(- seq).|| is convergent & lim ||.(- seq).|| = ||.(- g).|| )
let g be Point of X; ::_thesis: for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.(- seq).|| is convergent & lim ||.(- seq).|| = ||.(- g).|| )
let seq be sequence of X; ::_thesis: ( seq is convergent & lim seq = g implies ( ||.(- seq).|| is convergent & lim ||.(- seq).|| = ||.(- g).|| ) )
assume  ( seq is convergent & lim seq = g ) ; ::_thesis: ( ||.(- seq).|| is convergent & lim ||.(- seq).|| = ||.(- g).|| )
then  ( - seq is convergent & lim (- seq) = - g ) by Th6, Th16;
hence  ( ||.(- seq).|| is convergent & lim ||.(- seq).|| = ||.(- g).|| ) by Th21; ::_thesis: verum
end;

theorem :: CLVECT_2:32
for X being ComplexUnitarySpace
for g being Point of X
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.((- seq) - (- g)).|| is convergent & lim ||.((- seq) - (- g)).|| = 0 )
proof
let X be ComplexUnitarySpace; ::_thesis: for g being Point of X
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.((- seq) - (- g)).|| is convergent & lim ||.((- seq) - (- g)).|| = 0 )
let g be Point of X; ::_thesis: for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.((- seq) - (- g)).|| is convergent & lim ||.((- seq) - (- g)).|| = 0 )
let seq be sequence of X; ::_thesis: ( seq is convergent & lim seq = g implies ( ||.((- seq) - (- g)).|| is convergent & lim ||.((- seq) - (- g)).|| = 0 ) )
assume  ( seq is convergent & lim seq = g ) ; ::_thesis: ( ||.((- seq) - (- g)).|| is convergent & lim ||.((- seq) - (- g)).|| = 0 )
then  ( - seq is convergent & lim (- seq) = - g ) by Th6, Th16;
hence  ( ||.((- seq) - (- g)).|| is convergent & lim ||.((- seq) - (- g)).|| = 0 ) by Th22; ::_thesis: verum
end;

Lm1:  for X being ComplexUnitarySpace
for g, x being Point of X
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.(seq + x).|| is convergent & lim ||.(seq + x).|| = ||.(g + x).|| )
proof
let X be ComplexUnitarySpace; ::_thesis: for g, x being Point of X
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.(seq + x).|| is convergent & lim ||.(seq + x).|| = ||.(g + x).|| )
let g, x be Point of X; ::_thesis: for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.(seq + x).|| is convergent & lim ||.(seq + x).|| = ||.(g + x).|| )
let seq be sequence of X; ::_thesis: ( seq is convergent & lim seq = g implies ( ||.(seq + x).|| is convergent & lim ||.(seq + x).|| = ||.(g + x).|| ) )
assume  ( seq is convergent & lim seq = g ) ; ::_thesis: ( ||.(seq + x).|| is convergent & lim ||.(seq + x).|| = ||.(g + x).|| )
then  ( seq + x is convergent & lim (seq + x) = g + x ) by Th7, Th17;
hence  ( ||.(seq + x).|| is convergent & lim ||.(seq + x).|| = ||.(g + x).|| ) by Th21; ::_thesis: verum
end;

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 & lim seq = g holds
( ||.((seq + x) - (g + x)).|| is convergent & lim ||.((seq + x) - (g + x)).|| = 0 )
proof
let X be ComplexUnitarySpace; ::_thesis: for g, x being Point of X
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.((seq + x) - (g + x)).|| is convergent & lim ||.((seq + x) - (g + x)).|| = 0 )
let g, x be Point of X; ::_thesis: for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.((seq + x) - (g + x)).|| is convergent & lim ||.((seq + x) - (g + x)).|| = 0 )
let seq be sequence of X; ::_thesis: ( seq is convergent & lim seq = g implies ( ||.((seq + x) - (g + x)).|| is convergent & lim ||.((seq + x) - (g + x)).|| = 0 ) )
assume  ( seq is convergent & lim seq = g ) ; ::_thesis: ( ||.((seq + x) - (g + x)).|| is convergent & lim ||.((seq + x) - (g + x)).|| = 0 )
then  ( seq + x is convergent & lim (seq + x) = g + x ) by Th7, Th17;
hence  ( ||.((seq + x) - (g + x)).|| is convergent & lim ||.((seq + x) - (g + x)).|| = 0 ) by Th22; ::_thesis: verum
end;

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 & lim seq = g holds
( ||.(seq - x).|| is convergent & lim ||.(seq - x).|| = ||.(g - x).|| )
proof
let X be ComplexUnitarySpace; ::_thesis: for g, x being Point of X
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.(seq - x).|| is convergent & lim ||.(seq - x).|| = ||.(g - x).|| )
let g, x be Point of X; ::_thesis: for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.(seq - x).|| is convergent & lim ||.(seq - x).|| = ||.(g - x).|| )
let seq be sequence of X; ::_thesis: ( seq is convergent & lim seq = g implies ( ||.(seq - x).|| is convergent & lim ||.(seq - x).|| = ||.(g - x).|| ) )
assume A1: ( seq is convergent & lim seq = g ) ; ::_thesis: ( ||.(seq - x).|| is convergent & lim ||.(seq - x).|| = ||.(g - x).|| )
then  lim ||.(seq + (- x)).|| = ||.(g + (- x)).|| by Lm1;
then A2: lim ||.(seq - x).|| = ||.(g + (- x)).|| by CSSPACE:71;
 ||.(seq + (- x)).|| is convergent by A1, Lm1;
hence  ( ||.(seq - x).|| is convergent & lim ||.(seq - x).|| = ||.(g - x).|| ) by A2, CSSPACE:71, RLVECT_1:def_11; ::_thesis: verum
end;

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 & lim seq = g holds
( ||.((seq - x) - (g - x)).|| is convergent & lim ||.((seq - x) - (g - x)).|| = 0 )
proof
let X be ComplexUnitarySpace; ::_thesis: for g, x being Point of X
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.((seq - x) - (g - x)).|| is convergent & lim ||.((seq - x) - (g - x)).|| = 0 )
let g, x be Point of X; ::_thesis: for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.((seq - x) - (g - x)).|| is convergent & lim ||.((seq - x) - (g - x)).|| = 0 )
let seq be sequence of X; ::_thesis: ( seq is convergent & lim seq = g implies ( ||.((seq - x) - (g - x)).|| is convergent & lim ||.((seq - x) - (g - x)).|| = 0 ) )
assume A1: ( seq is convergent & lim seq = g ) ; ::_thesis: ( ||.((seq - x) - (g - x)).|| is convergent & lim ||.((seq - x) - (g - x)).|| = 0 )
then  lim ||.((seq + (- x)) - (g + (- x))).|| = 0 by Th33;
then A2: lim ||.((seq - x) - (g + (- x))).|| = 0 by CSSPACE:71;
 ||.((seq + (- x)) - (g + (- x))).|| is convergent by A1, Th33;
then  ||.((seq - x) - (g + (- x))).|| is convergent by CSSPACE:71;
hence  ( ||.((seq - x) - (g - x)).|| is convergent & lim ||.((seq - x) - (g - x)).|| = 0 ) by A2, RLVECT_1:def_11; ::_thesis: verum
end;

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 & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 holds
( dist ((seq1 + seq2),(g1 + g2)) is convergent & lim (dist ((seq1 + seq2),(g1 + g2))) = 0 )
proof
let X be ComplexUnitarySpace; ::_thesis: for g1, g2 being Point of X
for seq1, seq2 being sequence of X st seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 holds
( dist ((seq1 + seq2),(g1 + g2)) is convergent & lim (dist ((seq1 + seq2),(g1 + g2))) = 0 )
let g1, g2 be Point of X; ::_thesis: for seq1, seq2 being sequence of X st seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 holds
( dist ((seq1 + seq2),(g1 + g2)) is convergent & lim (dist ((seq1 + seq2),(g1 + g2))) = 0 )
let seq1, seq2 be sequence of X; ::_thesis: ( seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 implies ( dist ((seq1 + seq2),(g1 + g2)) is convergent & lim (dist ((seq1 + seq2),(g1 + g2))) = 0 ) )
assume  ( seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 ) ; ::_thesis: ( dist ((seq1 + seq2),(g1 + g2)) is convergent & lim (dist ((seq1 + seq2),(g1 + g2))) = 0 )
then  ( seq1 + seq2 is convergent & lim (seq1 + seq2) = g1 + g2 ) by Th3, Th13;
hence  ( dist ((seq1 + seq2),(g1 + g2)) is convergent & lim (dist ((seq1 + seq2),(g1 + g2))) = 0 ) by Th24; ::_thesis: verum
end;

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 & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 holds
( dist ((seq1 - seq2),(g1 - g2)) is convergent & lim (dist ((seq1 - seq2),(g1 - g2))) = 0 )
proof
let X be ComplexUnitarySpace; ::_thesis: for g1, g2 being Point of X
for seq1, seq2 being sequence of X st seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 holds
( dist ((seq1 - seq2),(g1 - g2)) is convergent & lim (dist ((seq1 - seq2),(g1 - g2))) = 0 )
let g1, g2 be Point of X; ::_thesis: for seq1, seq2 being sequence of X st seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 holds
( dist ((seq1 - seq2),(g1 - g2)) is convergent & lim (dist ((seq1 - seq2),(g1 - g2))) = 0 )
let seq1, seq2 be sequence of X; ::_thesis: ( seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 implies ( dist ((seq1 - seq2),(g1 - g2)) is convergent & lim (dist ((seq1 - seq2),(g1 - g2))) = 0 ) )
assume  ( seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 ) ; ::_thesis: ( dist ((seq1 - seq2),(g1 - g2)) is convergent & lim (dist ((seq1 - seq2),(g1 - g2))) = 0 )
then  ( seq1 - seq2 is convergent & lim (seq1 - seq2) = g1 - g2 ) by Th4, Th14;
hence  ( dist ((seq1 - seq2),(g1 - g2)) is convergent & lim (dist ((seq1 - seq2),(g1 - g2))) = 0 ) by Th24; ::_thesis: verum
end;

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 & lim seq = g holds
( dist ((z * seq),(z * g)) is convergent & lim (dist ((z * seq),(z * g))) = 0 )
proof
let X be ComplexUnitarySpace; ::_thesis: for g being Point of X
for z being Complex
for seq being sequence of X st seq is convergent & lim seq = g holds
( dist ((z * seq),(z * g)) is convergent & lim (dist ((z * seq),(z * g))) = 0 )
let g be Point of X; ::_thesis: for z being Complex
for seq being sequence of X st seq is convergent & lim seq = g holds
( dist ((z * seq),(z * g)) is convergent & lim (dist ((z * seq),(z * g))) = 0 )
let z be Complex; ::_thesis: for seq being sequence of X st seq is convergent & lim seq = g holds
( dist ((z * seq),(z * g)) is convergent & lim (dist ((z * seq),(z * g))) = 0 )
let seq be sequence of X; ::_thesis: ( seq is convergent & lim seq = g implies ( dist ((z * seq),(z * g)) is convergent & lim (dist ((z * seq),(z * g))) = 0 ) )
assume  ( seq is convergent & lim seq = g ) ; ::_thesis: ( dist ((z * seq),(z * g)) is convergent & lim (dist ((z * seq),(z * g))) = 0 )
then  ( z * seq is convergent & lim (z * seq) = z * g ) by Th5, Th15;
hence  ( dist ((z * seq),(z * g)) is convergent & lim (dist ((z * seq),(z * g))) = 0 ) by Th24; ::_thesis: verum
end;

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 & lim seq = g holds
( dist ((seq + x),(g + x)) is convergent & lim (dist ((seq + x),(g + x))) = 0 )
proof
let X be ComplexUnitarySpace; ::_thesis: for g, x being Point of X
for seq being sequence of X st seq is convergent & lim seq = g holds
( dist ((seq + x),(g + x)) is convergent & lim (dist ((seq + x),(g + x))) = 0 )
let g, x be Point of X; ::_thesis: for seq being sequence of X st seq is convergent & lim seq = g holds
( dist ((seq + x),(g + x)) is convergent & lim (dist ((seq + x),(g + x))) = 0 )
let seq be sequence of X; ::_thesis: ( seq is convergent & lim seq = g implies ( dist ((seq + x),(g + x)) is convergent & lim (dist ((seq + x),(g + x))) = 0 ) )
assume  ( seq is convergent & lim seq = g ) ; ::_thesis: ( dist ((seq + x),(g + x)) is convergent & lim (dist ((seq + x),(g + x))) = 0 )
then  ( seq + x is convergent & lim (seq + x) = g + x ) by Th7, Th17;
hence  ( dist ((seq + x),(g + x)) is convergent & lim (dist ((seq + x),(g + x))) = 0 ) by Th24; ::_thesis: verum
end;

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
proof
defpred S1[ Point of X] means ||.(x - $1).|| < r;
  {  y where y is Point of X : S1[y]  }  c= the carrier of X from FRAENKEL:sch_10();
hence   {  y where y is Point of X : ||.(x - y).|| < r  }  is Subset of X ; ::_thesis: verum
end;
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
proof
defpred S1[ Point of X] means ||.(x - $1).|| <= r;
  {  y where y is Point of X : S1[y]  }  c= the carrier of X from FRAENKEL:sch_10();
hence   {  y where y is Point of X : ||.(x - y).|| <= r  }  is Subset of X ; ::_thesis: verum
end;
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
proof
defpred S1[ Point of X] means ||.(x - $1).|| = r;
  {  y where y is Point of X : S1[y]  }  c= the carrier of X from FRAENKEL:sch_10();
hence   {  y where y is Point of X : ||.(x - y).|| = r  }  is Subset of X ; ::_thesis: verum
end;
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 )
proof
let X be ComplexUnitarySpace; ::_thesis: for w, x being Point of X
for r being Real holds
( w in Ball (x,r) iff ||.(x - w).|| < r )
let w, x be Point of X; ::_thesis: for r being Real holds
( w in Ball (x,r) iff ||.(x - w).|| < r )
let r be Real; ::_thesis: ( w in Ball (x,r) iff ||.(x - w).|| < r )
thus  ( w in Ball (x,r) implies ||.(x - w).|| < r ) ::_thesis: ( ||.(x - w).|| < r implies w in Ball (x,r) )
proof
assume  w in Ball (x,r) ; ::_thesis: ||.(x - w).|| < r
then  ex y being Point of X st
( w = y & ||.(x - y).|| < r ) ;
hence  ||.(x - w).|| < r ; ::_thesis: verum
end;
thus  ( ||.(x - w).|| < r implies w in Ball (x,r) ) ; ::_thesis: verum
end;

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 )
proof
let X be ComplexUnitarySpace; ::_thesis: for w, x being Point of X
for r being Real holds
( w in Ball (x,r) iff dist (x,w) < r )
let w, x be Point of X; ::_thesis: for r being Real holds
( w in Ball (x,r) iff dist (x,w) < r )
let r be Real; ::_thesis: ( w in Ball (x,r) iff dist (x,w) < r )
thus  ( w in Ball (x,r) implies dist (x,w) < r ) ::_thesis: ( dist (x,w) < r implies w in Ball (x,r) )
proof
assume  w in Ball (x,r) ; ::_thesis: dist (x,w) < r
then  ||.(x - w).|| < r by Th40;
hence  dist (x,w) < r by CSSPACE:def_16; ::_thesis: verum
end;
assume  dist (x,w) < r ; ::_thesis: w in Ball (x,r)
then  ||.(x - w).|| < r by CSSPACE:def_16;
hence  w in Ball (x,r) ; ::_thesis: verum
end;

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)
proof
let X be ComplexUnitarySpace; ::_thesis: for x being Point of X
for r being Real st r > 0 holds
x in Ball (x,r)
let x be Point of X; ::_thesis: for r being Real st r > 0 holds
x in Ball (x,r)
let r be Real; ::_thesis: ( r > 0 implies x in Ball (x,r) )
A1: dist (x,x) = 0 by CSSPACE:50;
assume  r > 0 ; ::_thesis: x in Ball (x,r)
hence  x in Ball (x,r) by A1, Th41; ::_thesis: verum
end;

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) & w in Ball (x,r) holds
dist (y,w) < 2 * r
proof
let X be ComplexUnitarySpace; ::_thesis: for y, x, w being Point of X
for r being Real st y in Ball (x,r) & w in Ball (x,r) holds
dist (y,w) < 2 * r
let y, x, w be Point of X; ::_thesis: for r being Real st y in Ball (x,r) & w in Ball (x,r) holds
dist (y,w) < 2 * r
let r be Real; ::_thesis: ( y in Ball (x,r) & w in Ball (x,r) implies dist (y,w) < 2 * r )
assume that
A1: y in Ball (x,r) and
A2: w in Ball (x,r) ; ::_thesis: dist (y,w) < 2 * r
 dist (x,w) < r by A2, Th41;
then A3: r + (dist (x,w)) < r + r by XREAL_1:6;
A4: dist (y,w) <= (dist (y,x)) + (dist (x,w)) by CSSPACE:51;
 dist (x,y) < r by A1, Th41;
then  (dist (x,y)) + (dist (x,w)) < r + (dist (x,w)) by XREAL_1:6;
then  (dist (x,y)) + (dist (x,w)) < 2 * r by A3, XXREAL_0:2;
hence  dist (y,w) < 2 * r by A4, XXREAL_0:2; ::_thesis: verum
end;

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)
proof
let X be ComplexUnitarySpace; ::_thesis: 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)
let y, x, w be Point of X; ::_thesis: for r being Real st y in Ball (x,r) holds
y - w in Ball ((x - w),r)
let r be Real; ::_thesis: ( y in Ball (x,r) implies y - w in Ball ((x - w),r) )
assume  y in Ball (x,r) ; ::_thesis: y - w in Ball ((x - w),r)
then A1: dist (x,y) < r by Th41;
 dist ((x - w),(y - w)) = dist (x,y) by CSSPACE:58;
hence  y - w in Ball ((x - w),r) by A1, Th41; ::_thesis: verum
end;

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)
proof
let X be ComplexUnitarySpace; ::_thesis: 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)
let y, x be Point of X; ::_thesis: for r being Real st y in Ball (x,r) holds
y - x in Ball ((0. X),r)
let r be Real; ::_thesis: ( y in Ball (x,r) implies y - x in Ball ((0. X),r) )
assume  y in Ball (x,r) ; ::_thesis: y - x in Ball ((0. X),r)
then  ||.(x - y).|| < r by Th40;
then  ||.((- y) + x).|| < r by RLVECT_1:def_11;
then  ||.(- (y - x)).|| < r by RLVECT_1:33;
then  ||.(H1(X) - (y - x)).|| < r by RLVECT_1:14;
hence  y - x in Ball ((0. X),r) ; ::_thesis: verum
end;

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) & r <= q holds
y in Ball (x,q)
proof
let X be ComplexUnitarySpace; ::_thesis: for y, x being Point of X
for r, q being Real st y in Ball (x,r) & r <= q holds
y in Ball (x,q)
let y, x be Point of X; ::_thesis: for r, q being Real st y in Ball (x,r) & r <= q holds
y in Ball (x,q)
let r, q be Real; ::_thesis: ( y in Ball (x,r) & r <= q implies y in Ball (x,q) )
assume that
A1: y in Ball (x,r) and
A2: r <= q ; ::_thesis: y in Ball (x,q)
 ||.(x - y).|| < r by A1, Th40;
then  ||.(x - y).|| < q by A2, XXREAL_0:2;
hence  y in Ball (x,q) ; ::_thesis: verum
end;

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 )
proof
let X be ComplexUnitarySpace; ::_thesis: for w, x being Point of X
for r being Real holds
( w in cl_Ball (x,r) iff ||.(x - w).|| <= r )
let w, x be Point of X; ::_thesis: for r being Real holds
( w in cl_Ball (x,r) iff ||.(x - w).|| <= r )
let r be Real; ::_thesis: ( w in cl_Ball (x,r) iff ||.(x - w).|| <= r )
thus  ( w in cl_Ball (x,r) implies ||.(x - w).|| <= r ) ::_thesis: ( ||.(x - w).|| <= r implies w in cl_Ball (x,r) )
proof
assume  w in cl_Ball (x,r) ; ::_thesis: ||.(x - w).|| <= r
then  ex y being Point of X st
( w = y & ||.(x - y).|| <= r ) ;
hence  ||.(x - w).|| <= r ; ::_thesis: verum
end;
assume  ||.(x - w).|| <= r ; ::_thesis: w in cl_Ball (x,r)
hence  w in cl_Ball (x,r) ; ::_thesis: verum
end;

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 )
proof
let X be ComplexUnitarySpace; ::_thesis: for w, x being Point of X
for r being Real holds
( w in cl_Ball (x,r) iff dist (x,w) <= r )
let w, x be Point of X; ::_thesis: for r being Real holds
( w in cl_Ball (x,r) iff dist (x,w) <= r )
let r be Real; ::_thesis: ( w in cl_Ball (x,r) iff dist (x,w) <= r )
thus  ( w in cl_Ball (x,r) implies dist (x,w) <= r ) ::_thesis: ( dist (x,w) <= r implies w in cl_Ball (x,r) )
proof
assume  w in cl_Ball (x,r) ; ::_thesis: dist (x,w) <= r
then  ||.(x - w).|| <= r by Th47;
hence  dist (x,w) <= r by CSSPACE:def_16; ::_thesis: verum
end;
assume  dist (x,w) <= r ; ::_thesis: w in cl_Ball (x,r)
then  ||.(x - w).|| <= r by CSSPACE:def_16;
hence  w in cl_Ball (x,r) ; ::_thesis: verum
end;

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)
proof
let X be ComplexUnitarySpace; ::_thesis: for x being Point of X
for r being Real st r >= 0 holds
x in cl_Ball (x,r)
let x be Point of X; ::_thesis: for r being Real st r >= 0 holds
x in cl_Ball (x,r)
let r be Real; ::_thesis: ( r >= 0 implies x in cl_Ball (x,r) )
assume  r >= 0 ; ::_thesis: x in cl_Ball (x,r)
then  dist (x,x) <= r by CSSPACE:50;
hence  x in cl_Ball (x,r) by Th48; ::_thesis: verum
end;

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)
proof
let X be ComplexUnitarySpace; ::_thesis: for y, x being Point of X
for r being Real st y in Ball (x,r) holds
y in cl_Ball (x,r)
let y, x be Point of X; ::_thesis: for r being Real st y in Ball (x,r) holds
y in cl_Ball (x,r)
let r be Real; ::_thesis: ( y in Ball (x,r) implies y in cl_Ball (x,r) )
assume  y in Ball (x,r) ; ::_thesis: y in cl_Ball (x,r)
then  ||.(x - y).|| <= r by Th40;
hence  y in cl_Ball (x,r) ; ::_thesis: verum
end;

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 )
proof
let X be ComplexUnitarySpace; ::_thesis: for w, x being Point of X
for r being Real holds
( w in Sphere (x,r) iff ||.(x - w).|| = r )
let w, x be Point of X; ::_thesis: for r being Real holds
( w in Sphere (x,r) iff ||.(x - w).|| = r )
let r be Real; ::_thesis: ( w in Sphere (x,r) iff ||.(x - w).|| = r )
thus  ( w in Sphere (x,r) implies ||.(x - w).|| = r ) ::_thesis: ( ||.(x - w).|| = r implies w in Sphere (x,r) )
proof
assume  w in Sphere (x,r) ; ::_thesis: ||.(x - w).|| = r
then  ex y being Point of X st
( w = y & ||.(x - y).|| = r ) ;
hence  ||.(x - w).|| = r ; ::_thesis: verum
end;
assume  ||.(x - w).|| = r ; ::_thesis: w in Sphere (x,r)
hence  w in Sphere (x,r) ; ::_thesis: verum
end;

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 )
proof
let X be ComplexUnitarySpace; ::_thesis: for w, x being Point of X
for r being Real holds
( w in Sphere (x,r) iff dist (x,w) = r )
let w, x be Point of X; ::_thesis: for r being Real holds
( w in Sphere (x,r) iff dist (x,w) = r )
let r be Real; ::_thesis: ( w in Sphere (x,r) iff dist (x,w) = r )
thus  ( w in Sphere (x,r) implies dist (x,w) = r ) ::_thesis: ( dist (x,w) = r implies w in Sphere (x,r) )
proof
assume  w in Sphere (x,r) ; ::_thesis: dist (x,w) = r
then  ||.(x - w).|| = r by Th51;
hence  dist (x,w) = r by CSSPACE:def_16; ::_thesis: verum
end;
assume  dist (x,w) = r ; ::_thesis: w in Sphere (x,r)
then  ||.(x - w).|| = r by CSSPACE:def_16;
hence  w in Sphere (x,r) ; ::_thesis: verum
end;

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)
proof
let X be ComplexUnitarySpace; ::_thesis: for y, x being Point of X
for r being Real st y in Sphere (x,r) holds
y in cl_Ball (x,r)
let y, x be Point of X; ::_thesis: for r being Real st y in Sphere (x,r) holds
y in cl_Ball (x,r)
let r be Real; ::_thesis: ( y in Sphere (x,r) implies y in cl_Ball (x,r) )
assume  y in Sphere (x,r) ; ::_thesis: y in cl_Ball (x,r)
then  ||.(x - y).|| = r by Th51;
hence  y in cl_Ball (x,r) ; ::_thesis: verum
end;

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)
proof
let X be ComplexUnitarySpace; ::_thesis: for x being Point of X
for r being Real holds Ball (x,r) c= cl_Ball (x,r)
let x be Point of X; ::_thesis: for r being Real holds Ball (x,r) c= cl_Ball (x,r)
let r be Real; ::_thesis: Ball (x,r) c= cl_Ball (x,r)
 for y being Point of X st y in Ball (x,r) holds
y in cl_Ball (x,r) by Th50;
hence  Ball (x,r) c= cl_Ball (x,r) by SUBSET_1:2; ::_thesis: verum
end;

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)
proof
let X be ComplexUnitarySpace; ::_thesis: for x being Point of X
for r being Real holds Sphere (x,r) c= cl_Ball (x,r)
let x be Point of X; ::_thesis: for r being Real holds Sphere (x,r) c= cl_Ball (x,r)
let r be Real; ::_thesis: Sphere (x,r) c= cl_Ball (x,r)
now__::_thesis:_for_y_being_Point_of_X_st_y_in_Sphere_(x,r)_holds_
y_in_cl_Ball_(x,r)
let y be Point of X; ::_thesis: ( y in Sphere (x,r) implies y in cl_Ball (x,r) )
assume  y in Sphere (x,r) ; ::_thesis: y in cl_Ball (x,r)
then  ||.(x - y).|| = r by Th51;
hence  y in cl_Ball (x,r) ; ::_thesis: verum
end;
hence  Sphere (x,r) c= cl_Ball (x,r) by SUBSET_1:2; ::_thesis: verum
end;

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)
proof
let X be ComplexUnitarySpace; ::_thesis: for x being Point of X
for r being Real holds (Ball (x,r)) \/ (Sphere (x,r)) = cl_Ball (x,r)
let x be Point of X; ::_thesis: for r being Real holds (Ball (x,r)) \/ (Sphere (x,r)) = cl_Ball (x,r)
let r be Real; ::_thesis: (Ball (x,r)) \/ (Sphere (x,r)) = cl_Ball (x,r)
now__::_thesis:_for_y_being_Point_of_X_st_y_in_cl_Ball_(x,r)_holds_
y_in_(Ball_(x,r))_\/_(Sphere_(x,r))
let y be Point of X; ::_thesis: ( y in cl_Ball (x,r) implies y in (Ball (x,r)) \/ (Sphere (x,r)) )
assume  y in cl_Ball (x,r) ; ::_thesis: y in (Ball (x,r)) \/ (Sphere (x,r))
then A1: ||.(x - y).|| <= r by Th47;
now__::_thesis:_(_(_||.(x_-_y).||_<_r_&_y_in_Ball_(x,r)_)_or_(_||.(x_-_y).||_=_r_&_y_in_Sphere_(x,r)_)_)
percases ( ||.(x - y).|| < r or ||.(x - y).|| = r ) by A1, XXREAL_0:1;
case ||.(x - y).|| < r ; ::_thesis: y in Ball (x,r)
hence  y in Ball (x,r) ; ::_thesis: verum
end;
case ||.(x - y).|| = r ; ::_thesis: y in Sphere (x,r)
hence  y in Sphere (x,r) ; ::_thesis: verum
end;
end;
end;
hence  y in (Ball (x,r)) \/ (Sphere (x,r)) by XBOOLE_0:def_3; ::_thesis: verum
end;
then A2: cl_Ball (x,r) c= (Ball (x,r)) \/ (Sphere (x,r)) by SUBSET_1:2;
 ( Ball (x,r) c= cl_Ball (x,r) & Sphere (x,r) c= cl_Ball (x,r) ) by Th54, Th55;
then  (Ball (x,r)) \/ (Sphere (x,r)) c= cl_Ball (x,r) by XBOOLE_1:8;
hence  (Ball (x,r)) \/ (Sphere (x,r)) = cl_Ball (x,r) by A2, XBOOLE_0:def_10; ::_thesis: verum
end;

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 & 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 & 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
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X st seq is constant holds
seq is Cauchy
let seq be sequence of X; ::_thesis: ( seq is constant implies seq is Cauchy )
assume A1: seq is constant ; ::_thesis: seq is Cauchy
let r be Real; :: according to CLVECT_2:def_8 ::_thesis: ( r > 0 implies ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
dist ((seq . n),(seq . m)) < r )
assume A2: r > 0 ; ::_thesis: ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
dist ((seq . n),(seq . m)) < r
take k = 0 ; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds
dist ((seq . n),(seq . m)) < r
let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies dist ((seq . n),(seq . m)) < r )
assume that
 n >= k and
 m >= k ; ::_thesis: dist ((seq . n),(seq . m)) < r
dist ((seq . n),(seq . m)) = dist ((seq . n),(seq . n)) by A1, VALUED_0:23
.= 0 by CSSPACE:50 ;
hence  dist ((seq . n),(seq . m)) < r by A2; ::_thesis: verum
end;

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 & m >= k holds
||.((seq . n) - (seq . m)).|| < r )
proof
let X be ComplexUnitarySpace; ::_thesis: 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 & m >= k holds
||.((seq . n) - (seq . m)).|| < r )
let seq be sequence of X; ::_thesis: ( 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 & m >= k holds
||.((seq . n) - (seq . m)).|| < r )
thus  ( seq is Cauchy implies 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 & m >= k holds
||.((seq . n) - (seq . m)).|| < r ) ::_thesis: ( ( 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 & m >= k holds
||.((seq . n) - (seq . m)).|| < r ) implies seq is Cauchy )
proof
assume A1: seq is Cauchy ; ::_thesis: 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 & m >= k holds
||.((seq . n) - (seq . m)).|| < r
let r be Real; ::_thesis: ( r > 0 implies ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r )
assume  r > 0 ; ::_thesis: ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r
then consider l being Element of NAT  such that
A2: for n, m being Element of NAT st n >= l & m >= l holds
dist ((seq . n),(seq . m)) < r by A1, Def8;
take k = l; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r
let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies ||.((seq . n) - (seq . m)).|| < r )
assume  ( n >= k & m >= k ) ; ::_thesis: ||.((seq . n) - (seq . m)).|| < r
then  dist ((seq . n),(seq . m)) < r by A2;
hence  ||.((seq . n) - (seq . m)).|| < r by CSSPACE:def_16; ::_thesis: verum
end;
 ( ( 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 & m >= k holds
||.((seq . n) - (seq . m)).|| < r ) implies seq is Cauchy )
proof
assume A3: 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 & m >= k holds
||.((seq . n) - (seq . m)).|| < r ; ::_thesis: seq is Cauchy
let r be Real; :: according to CLVECT_2:def_8 ::_thesis: ( r > 0 implies ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
dist ((seq . n),(seq . m)) < r )
assume  r > 0 ; ::_thesis: ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
dist ((seq . n),(seq . m)) < r
then consider l being Element of NAT  such that
A4: for n, m being Element of NAT st n >= l & m >= l holds
||.((seq . n) - (seq . m)).|| < r by A3;
take k = l; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds
dist ((seq . n),(seq . m)) < r
let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies dist ((seq . n),(seq . m)) < r )
assume  ( n >= k & m >= k ) ; ::_thesis: dist ((seq . n),(seq . m)) < r
then  ||.((seq . n) - (seq . m)).|| < r by A4;
hence  dist ((seq . n),(seq . m)) < r by CSSPACE:def_16; ::_thesis: verum
end;
hence  ( ( 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 & m >= k holds
||.((seq . n) - (seq . m)).|| < r ) implies seq is Cauchy ) ; ::_thesis: verum
end;

theorem :: CLVECT_2:59
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is Cauchy & seq2 is Cauchy holds
seq1 + seq2 is Cauchy
proof
let X be ComplexUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X st seq1 is Cauchy & seq2 is Cauchy holds
seq1 + seq2 is Cauchy
let seq1, seq2 be sequence of X; ::_thesis: ( seq1 is Cauchy & seq2 is Cauchy implies seq1 + seq2 is Cauchy )
assume that
A1: seq1 is Cauchy and
A2: seq2 is Cauchy ; ::_thesis: seq1 + seq2 is Cauchy
let r be Real; :: according to CLVECT_2:def_8 ::_thesis: ( r > 0 implies ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
dist (((seq1 + seq2) . n),((seq1 + seq2) . m)) < r )
assume  r > 0 ; ::_thesis: ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
dist (((seq1 + seq2) . n),((seq1 + seq2) . m)) < r
then A3: r / 2 > 0 by XREAL_1:215;
then consider m1 being Element of NAT  such that
A4: for n, m being Element of NAT st n >= m1 & m >= m1 holds
dist ((seq1 . n),(seq1 . m)) < r / 2 by A1, Def8;
consider m2 being Element of NAT  such that
A5: for n, m being Element of NAT st n >= m2 & m >= m2 holds
dist ((seq2 . n),(seq2 . m)) < r / 2 by A2, A3, Def8;
take k = m1 + m2; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds
dist (((seq1 + seq2) . n),((seq1 + seq2) . m)) < r
let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies dist (((seq1 + seq2) . n),((seq1 + seq2) . m)) < r )
assume A6: ( n >= k & m >= k ) ; ::_thesis: dist (((seq1 + seq2) . n),((seq1 + seq2) . m)) < r
 k >= m2 by NAT_1:12;
then  ( n >= m2 & m >= m2 ) by A6, XXREAL_0:2;
then A7: dist ((seq2 . n),(seq2 . m)) < r / 2 by A5;
dist (((seq1 + seq2) . n),((seq1 + seq2) . m)) = dist (((seq1 . n) + (seq2 . n)),((seq1 + seq2) . m)) by NORMSP_1:def_2
.= dist (((seq1 . n) + (seq2 . n)),((seq1 . m) + (seq2 . m))) by NORMSP_1:def_2 ;
then A8: dist (((seq1 + seq2) . n),((seq1 + seq2) . m)) <= (dist ((seq1 . n),(seq1 . m))) + (dist ((seq2 . n),(seq2 . m))) by CSSPACE:56;
 m1 + m2 >= m1 by NAT_1:12;
then  ( n >= m1 & m >= m1 ) by A6, XXREAL_0:2;
then  dist ((seq1 . n),(seq1 . m)) < r / 2 by A4;
then  (dist ((seq1 . n),(seq1 . m))) + (dist ((seq2 . n),(seq2 . m))) < (r / 2) + (r / 2) by A7, XREAL_1:8;
hence  dist (((seq1 + seq2) . n),((seq1 + seq2) . m)) < r by A8, XXREAL_0:2; ::_thesis: verum
end;

theorem :: CLVECT_2:60
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is Cauchy & seq2 is Cauchy holds
seq1 - seq2 is Cauchy
proof
let X be ComplexUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X st seq1 is Cauchy & seq2 is Cauchy holds
seq1 - seq2 is Cauchy
let seq1, seq2 be sequence of X; ::_thesis: ( seq1 is Cauchy & seq2 is Cauchy implies seq1 - seq2 is Cauchy )
assume that
A1: seq1 is Cauchy and
A2: seq2 is Cauchy ; ::_thesis: seq1 - seq2 is Cauchy
let r be Real; :: according to CLVECT_2:def_8 ::_thesis: ( r > 0 implies ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
dist (((seq1 - seq2) . n),((seq1 - seq2) . m)) < r )
assume  r > 0 ; ::_thesis: ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
dist (((seq1 - seq2) . n),((seq1 - seq2) . m)) < r
then A3: r / 2 > 0 by XREAL_1:215;
then consider m1 being Element of NAT  such that
A4: for n, m being Element of NAT st n >= m1 & m >= m1 holds
dist ((seq1 . n),(seq1 . m)) < r / 2 by A1, Def8;
consider m2 being Element of NAT  such that
A5: for n, m being Element of NAT st n >= m2 & m >= m2 holds
dist ((seq2 . n),(seq2 . m)) < r / 2 by A2, A3, Def8;
take k = m1 + m2; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds
dist (((seq1 - seq2) . n),((seq1 - seq2) . m)) < r
let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies dist (((seq1 - seq2) . n),((seq1 - seq2) . m)) < r )
assume A6: ( n >= k & m >= k ) ; ::_thesis: dist (((seq1 - seq2) . n),((seq1 - seq2) . m)) < r
 k >= m2 by NAT_1:12;
then  ( n >= m2 & m >= m2 ) by A6, XXREAL_0:2;
then A7: dist ((seq2 . n),(seq2 . m)) < r / 2 by A5;
dist (((seq1 - seq2) . n),((seq1 - seq2) . m)) = dist (((seq1 . n) - (seq2 . n)),((seq1 - seq2) . m)) by NORMSP_1:def_3
.= dist (((seq1 . n) - (seq2 . n)),((seq1 . m) - (seq2 . m))) by NORMSP_1:def_3 ;
then A8: dist (((seq1 - seq2) . n),((seq1 - seq2) . m)) <= (dist ((seq1 . n),(seq1 . m))) + (dist ((seq2 . n),(seq2 . m))) by CSSPACE:57;
 m1 + m2 >= m1 by NAT_1:12;
then  ( n >= m1 & m >= m1 ) by A6, XXREAL_0:2;
then  dist ((seq1 . n),(seq1 . m)) < r / 2 by A4;
then  (dist ((seq1 . n),(seq1 . m))) + (dist ((seq2 . n),(seq2 . m))) < (r / 2) + (r / 2) by A7, XREAL_1:8;
hence  dist (((seq1 - seq2) . n),((seq1 - seq2) . m)) < r by A8, XXREAL_0:2; ::_thesis: verum
end;

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
proof
let X be ComplexUnitarySpace; ::_thesis: for z being Complex
for seq being sequence of X st seq is Cauchy holds
z * seq is Cauchy
let z be Complex; ::_thesis: for seq being sequence of X st seq is Cauchy holds
z * seq is Cauchy
let seq be sequence of X; ::_thesis: ( seq is Cauchy implies z * seq is Cauchy )
assume A1: seq is Cauchy ; ::_thesis: z * seq is Cauchy
A2: now__::_thesis:_(_z_<>_0_implies_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_&_m_>=_k_holds_
dist_(((z_*_seq)_._n),((z_*_seq)_._m))_<_r_)
A3: 0 / |.z.| = 0 ;
assume A4: z <> 0 ; ::_thesis: 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 & m >= k holds
dist (((z * seq) . n),((z * seq) . m)) < r
then A5: |.z.| > 0 by COMPLEX1:47;
let r be Real; ::_thesis: ( r > 0 implies ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
dist (((z * seq) . n),((z * seq) . m)) < r )
assume  r > 0 ; ::_thesis: ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
dist (((z * seq) . n),((z * seq) . m)) < r
then  r / |.z.| > 0 by A5, A3, XREAL_1:74;
then consider m1 being Element of NAT  such that
A6: for n, m being Element of NAT st n >= m1 & m >= m1 holds
dist ((seq . n),(seq . m)) < r / |.z.| by A1, Def8;
take k = m1; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds
dist (((z * seq) . n),((z * seq) . m)) < r
let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies dist (((z * seq) . n),((z * seq) . m)) < r )
assume  ( n >= k & m >= k ) ; ::_thesis: dist (((z * seq) . n),((z * seq) . m)) < r
then A7: dist ((seq . n),(seq . m)) < r / |.z.| by A6;
A8: |.z.| <> 0 by A4, COMPLEX1:47;
A9: |.z.| * (r / |.z.|) = |.z.| * ((|.z.| ") * r) by XCMPLX_0:def_9
.= (|.z.| * (|.z.| ")) * r
.= 1 * r by A8, XCMPLX_0:def_7
.= r ;
dist ((z * (seq . n)),(z * (seq . m))) = ||.((z * (seq . n)) - (z * (seq . m))).|| by CSSPACE:def_16
.= ||.(z * ((seq . n) - (seq . m))).|| by CLVECT_1:9
.= |.z.| * ||.((seq . n) - (seq . m)).|| by CSSPACE:43
.= |.z.| * (dist ((seq . n),(seq . m))) by CSSPACE:def_16 ;
then  dist ((z * (seq . n)),(z * (seq . m))) < r by A5, A7, A9, XREAL_1:68;
then  dist (((z * seq) . n),(z * (seq . m))) < r by CLVECT_1:def_14;
hence  dist (((z * seq) . n),((z * seq) . m)) < r by CLVECT_1:def_14; ::_thesis: verum
end;
now__::_thesis:_(_z_=_0_implies_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_&_m_>=_k_holds_
dist_(((z_*_seq)_._n),((z_*_seq)_._m))_<_r_)
assume A10: z = 0 ; ::_thesis: 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 & m >= k holds
dist (((z * seq) . n),((z * seq) . m)) < r
let r be Real; ::_thesis: ( r > 0 implies ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
dist (((z * seq) . n),((z * seq) . m)) < r )
assume  r > 0 ; ::_thesis: ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
dist (((z * seq) . n),((z * seq) . m)) < r
then consider m1 being Element of NAT  such that
A11: for n, m being Element of NAT st n >= m1 & m >= m1 holds
dist ((seq . n),(seq . m)) < r by A1, Def8;
take k = m1; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds
dist (((z * seq) . n),((z * seq) . m)) < r
let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies dist (((z * seq) . n),((z * seq) . m)) < r )
assume  ( n >= k & m >= k ) ; ::_thesis: dist (((z * seq) . n),((z * seq) . m)) < r
then A12: dist ((seq . n),(seq . m)) < r by A11;
dist ((z * (seq . n)),(z * (seq . m))) = dist (H2(X),(0c * (seq . m))) by A10, CLVECT_1:1
.= dist (H2(X),H2(X)) by CLVECT_1:1
.= 0 by CSSPACE:50 ;
then  dist ((z * (seq . n)),(z * (seq . m))) < r by A12, CSSPACE:53;
then  dist (((z * seq) . n),(z * (seq . m))) < r by CLVECT_1:def_14;
hence  dist (((z * seq) . n),((z * seq) . m)) < r by CLVECT_1:def_14; ::_thesis: verum
end;
hence  z * seq is Cauchy by A2, Def8; ::_thesis: verum
end;

theorem :: CLVECT_2:62
for X being ComplexUnitarySpace
for seq being sequence of X st seq is Cauchy holds
- seq is Cauchy
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X st seq is Cauchy holds
- seq is Cauchy
let seq be sequence of X; ::_thesis: ( seq is Cauchy implies - seq is Cauchy )
assume  seq is Cauchy ; ::_thesis: - seq is Cauchy
then  (- 1r) * seq is Cauchy by Th61;
hence  - seq is Cauchy by CSSPACE:70; ::_thesis: verum
end;

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
proof
let X be ComplexUnitarySpace; ::_thesis: for x being Point of X
for seq being sequence of X st seq is Cauchy holds
seq + x is Cauchy
let x be Point of X; ::_thesis: for seq being sequence of X st seq is Cauchy holds
seq + x is Cauchy
let seq be sequence of X; ::_thesis: ( seq is Cauchy implies seq + x is Cauchy )
assume A1: seq is Cauchy ; ::_thesis: seq + x is Cauchy
let r be Real; :: according to CLVECT_2:def_8 ::_thesis: ( r > 0 implies ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
dist (((seq + x) . n),((seq + x) . m)) < r )
assume  r > 0 ; ::_thesis: ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
dist (((seq + x) . n),((seq + x) . m)) < r
then consider m1 being Element of NAT  such that
A2: for n, m being Element of NAT st n >= m1 & m >= m1 holds
dist ((seq . n),(seq . m)) < r by A1, Def8;
take k = m1; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds
dist (((seq + x) . n),((seq + x) . m)) < r
let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies dist (((seq + x) . n),((seq + x) . m)) < r )
 dist (((seq . n) + x),((seq . m) + x)) <= (dist ((seq . n),(seq . m))) + (dist (x,x)) by CSSPACE:56;
then A3: dist (((seq . n) + x),((seq . m) + x)) <= (dist ((seq . n),(seq . m))) + 0 by CSSPACE:50;
assume  ( n >= k & m >= k ) ; ::_thesis: dist (((seq + x) . n),((seq + x) . m)) < r
then  dist ((seq . n),(seq . m)) < r by A2;
then  dist (((seq . n) + x),((seq . m) + x)) < r by A3, XXREAL_0:2;
then  dist (((seq + x) . n),((seq . m) + x)) < r by BHSP_1:def_6;
hence  dist (((seq + x) . n),((seq + x) . m)) < r by BHSP_1:def_6; ::_thesis: verum
end;

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
proof
let X be ComplexUnitarySpace; ::_thesis: for x being Point of X
for seq being sequence of X st seq is Cauchy holds
seq - x is Cauchy
let x be Point of X; ::_thesis: for seq being sequence of X st seq is Cauchy holds
seq - x is Cauchy
let seq be sequence of X; ::_thesis: ( seq is Cauchy implies seq - x is Cauchy )
assume  seq is Cauchy ; ::_thesis: seq - x is Cauchy
then  seq + (- x) is Cauchy by Th63;
hence  seq - x is Cauchy by CSSPACE:71; ::_thesis: verum
end;

theorem :: CLVECT_2:65
for X being ComplexUnitarySpace
for seq being sequence of X st seq is convergent holds
seq is Cauchy
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X st seq is convergent holds
seq is Cauchy
let seq be sequence of X; ::_thesis: ( seq is convergent implies seq is Cauchy )
assume  seq is convergent ; ::_thesis: seq is Cauchy
then consider h being Point of X such that
A1: for r being Real st r > 0 holds
ex k being Element of NAT st
for n being Element of NAT st n >= k holds
dist ((seq . n),h) < r by Def1;
let r be Real; :: according to CLVECT_2:def_8 ::_thesis: ( r > 0 implies ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
dist ((seq . n),(seq . m)) < r )
assume  r > 0 ; ::_thesis: ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
dist ((seq . n),(seq . m)) < r
then consider m1 being Element of NAT  such that
A2: for n being Element of NAT st n >= m1 holds
dist ((seq . n),h) < r / 2 by A1, XREAL_1:215;
take k = m1; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds
dist ((seq . n),(seq . m)) < r
let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies dist ((seq . n),(seq . m)) < r )
assume  ( n >= k & m >= k ) ; ::_thesis: dist ((seq . n),(seq . m)) < r
then  ( dist ((seq . n),h) < r / 2 & dist ((seq . m),h) < r / 2 ) by A2;
then  ( dist ((seq . n),(seq . m)) <= (dist ((seq . n),h)) + (dist (h,(seq . m))) & (dist ((seq . n),h)) + (dist (h,(seq . m))) < (r / 2) + (r / 2) ) by CSSPACE:51, XREAL_1:8;
hence  dist ((seq . n),(seq . m)) < r by XXREAL_0:2; ::_thesis: verum
end;

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
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X holds seq is_compared_to seq
let seq be sequence of X; ::_thesis: seq is_compared_to seq
let r be Real; :: according to CLVECT_2:def_9 ::_thesis: ( r > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq . n),(seq . n)) < r )
assume A1: r > 0 ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq . n),(seq . n)) < r
take m = 0 ; ::_thesis: for n being Element of NAT st n >= m holds
dist ((seq . n),(seq . n)) < r
let n be Element of NAT ; ::_thesis: ( n >= m implies dist ((seq . n),(seq . n)) < r )
assume  n >= m ; ::_thesis: dist ((seq . n),(seq . n)) < r
thus  dist ((seq . n),(seq . n)) < r by A1, CSSPACE:50; ::_thesis: verum
end;

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
proof
let X be ComplexUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X st seq1 is_compared_to seq2 holds
seq2 is_compared_to seq1
let seq1, seq2 be sequence of X; ::_thesis: ( seq1 is_compared_to seq2 implies seq2 is_compared_to seq1 )
assume A1: seq1 is_compared_to seq2 ; ::_thesis: seq2 is_compared_to seq1
let r be Real; :: according to CLVECT_2:def_9 ::_thesis: ( r > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq2 . n),(seq1 . n)) < r )
assume  r > 0 ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq2 . n),(seq1 . n)) < r
then consider k being Element of NAT  such that
A2: for n being Element of NAT st n >= k holds
dist ((seq1 . n),(seq2 . n)) < r by A1, Def9;
take m = k; ::_thesis: for n being Element of NAT st n >= m holds
dist ((seq2 . n),(seq1 . n)) < r
let n be Element of NAT ; ::_thesis: ( n >= m implies dist ((seq2 . n),(seq1 . n)) < r )
assume  n >= m ; ::_thesis: dist ((seq2 . n),(seq1 . n)) < r
hence  dist ((seq2 . n),(seq1 . n)) < r by A2; ::_thesis: verum
end;

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 & seq2 is_compared_to seq3 holds
seq1 is_compared_to seq3
proof
let X be ComplexUnitarySpace; ::_thesis: for seq1, seq2, seq3 being sequence of X st seq1 is_compared_to seq2 & seq2 is_compared_to seq3 holds
seq1 is_compared_to seq3
let seq1, seq2, seq3 be sequence of X; ::_thesis: ( seq1 is_compared_to seq2 & seq2 is_compared_to seq3 implies seq1 is_compared_to seq3 )
assume that
A1: seq1 is_compared_to seq2 and
A2: seq2 is_compared_to seq3 ; ::_thesis: seq1 is_compared_to seq3
let r be Real; :: according to CLVECT_2:def_9 ::_thesis: ( r > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq1 . n),(seq3 . n)) < r )
assume  r > 0 ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq1 . n),(seq3 . n)) < r
then A3: r / 2 > 0 by XREAL_1:215;
then consider m1 being Element of NAT  such that
A4: for n being Element of NAT st n >= m1 holds
dist ((seq1 . n),(seq2 . n)) < r / 2 by A1, Def9;
consider m2 being Element of NAT  such that
A5: for n being Element of NAT st n >= m2 holds
dist ((seq2 . n),(seq3 . n)) < r / 2 by A2, A3, Def9;
take m = m1 + m2; ::_thesis: for n being Element of NAT st n >= m holds
dist ((seq1 . n),(seq3 . n)) < r
let n be Element of NAT ; ::_thesis: ( n >= m implies dist ((seq1 . n),(seq3 . n)) < r )
assume A6: n >= m ; ::_thesis: dist ((seq1 . n),(seq3 . n)) < r
 m >= m2 by NAT_1:12;
then  n >= m2 by A6, XXREAL_0:2;
then A7: dist ((seq2 . n),(seq3 . n)) < r / 2 by A5;
A8: dist ((seq1 . n),(seq3 . n)) <= (dist ((seq1 . n),(seq2 . n))) + (dist ((seq2 . n),(seq3 . n))) by CSSPACE:51;
 m1 + m2 >= m1 by NAT_1:12;
then  n >= m1 by A6, XXREAL_0:2;
then  dist ((seq1 . n),(seq2 . n)) < r / 2 by A4;
then  (dist ((seq1 . n),(seq2 . n))) + (dist ((seq2 . n),(seq3 . n))) < (r / 2) + (r / 2) by A7, XREAL_1:8;
hence  dist ((seq1 . n),(seq3 . n)) < r by A8, XXREAL_0:2; ::_thesis: verum
end;

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 )
proof
let X be ComplexUnitarySpace; ::_thesis: 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 )
let seq1, seq2 be sequence of X; ::_thesis: ( 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 )
thus  ( seq1 is_compared_to seq2 implies 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 ) ::_thesis: ( ( 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 ) implies seq1 is_compared_to seq2 )
proof
assume A1: seq1 is_compared_to seq2 ; ::_thesis: 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
let r be Real; ::_thesis: ( r > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((seq1 . n) - (seq2 . n)).|| < r )
assume  r > 0 ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((seq1 . n) - (seq2 . n)).|| < r
then consider m1 being Element of NAT  such that
A2: for n being Element of NAT st n >= m1 holds
dist ((seq1 . n),(seq2 . n)) < r by A1, Def9;
take m = m1; ::_thesis: for n being Element of NAT st n >= m holds
||.((seq1 . n) - (seq2 . n)).|| < r
let n be Element of NAT ; ::_thesis: ( n >= m implies ||.((seq1 . n) - (seq2 . n)).|| < r )
assume  n >= m ; ::_thesis: ||.((seq1 . n) - (seq2 . n)).|| < r
then  dist ((seq1 . n),(seq2 . n)) < r by A2;
hence  ||.((seq1 . n) - (seq2 . n)).|| < r by CSSPACE:def_16; ::_thesis: verum
end;
 ( ( 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 ) implies seq1 is_compared_to seq2 )
proof
assume A3: 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 ; ::_thesis: seq1 is_compared_to seq2
let r be Real; :: according to CLVECT_2:def_9 ::_thesis: ( r > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq1 . n),(seq2 . n)) < r )
assume  r > 0 ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq1 . n),(seq2 . n)) < r
then consider m1 being Element of NAT  such that
A4: for n being Element of NAT st n >= m1 holds
||.((seq1 . n) - (seq2 . n)).|| < r by A3;
take m = m1; ::_thesis: for n being Element of NAT st n >= m holds
dist ((seq1 . n),(seq2 . n)) < r
let n be Element of NAT ; ::_thesis: ( n >= m implies dist ((seq1 . n),(seq2 . n)) < r )
assume  n >= m ; ::_thesis: dist ((seq1 . n),(seq2 . n)) < r
then  ||.((seq1 . n) - (seq2 . n)).|| < r by A4;
hence  dist ((seq1 . n),(seq2 . n)) < r by CSSPACE:def_16; ::_thesis: verum
end;
hence  ( ( 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 ) implies seq1 is_compared_to seq2 ) ; ::_thesis: verum
end;

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
proof
let X be ComplexUnitarySpace; ::_thesis: 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
let seq1, seq2 be sequence of X; ::_thesis: ( ex k being Element of NAT st
for n being Element of NAT st n >= k holds
seq1 . n = seq2 . n implies seq1 is_compared_to seq2 )
assume  ex k being Element of NAT st
for n being Element of NAT st n >= k holds
seq1 . n = seq2 . n ; ::_thesis: seq1 is_compared_to seq2
then consider m being Element of NAT  such that
A1: for n being Element of NAT st n >= m holds
seq1 . n = seq2 . n ;
let r be Real; :: according to CLVECT_2:def_9 ::_thesis: ( r > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq1 . n),(seq2 . n)) < r )
assume A2: r > 0 ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq1 . n),(seq2 . n)) < r
take k = m; ::_thesis: for n being Element of NAT st n >= k holds
dist ((seq1 . n),(seq2 . n)) < r
let n be Element of NAT ; ::_thesis: ( n >= k implies dist ((seq1 . n),(seq2 . n)) < r )
assume  n >= k ; ::_thesis: dist ((seq1 . n),(seq2 . n)) < r
then  dist ((seq1 . n),(seq2 . n)) = dist ((seq1 . n),(seq1 . n)) by A1
.= 0 by CSSPACE:50 ;
hence  dist ((seq1 . n),(seq2 . n)) < r by A2; ::_thesis: verum
end;

theorem :: CLVECT_2:71
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is Cauchy & seq1 is_compared_to seq2 holds
seq2 is Cauchy
proof
let X be ComplexUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X st seq1 is Cauchy & seq1 is_compared_to seq2 holds
seq2 is Cauchy
let seq1, seq2 be sequence of X; ::_thesis: ( seq1 is Cauchy & seq1 is_compared_to seq2 implies seq2 is Cauchy )
assume that
A1: seq1 is Cauchy and
A2: seq1 is_compared_to seq2 ; ::_thesis: seq2 is Cauchy
let r be Real; :: according to CLVECT_2:def_8 ::_thesis: ( r > 0 implies ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
dist ((seq2 . n),(seq2 . m)) < r )
assume  r > 0 ; ::_thesis: ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
dist ((seq2 . n),(seq2 . m)) < r
then A3: r / 3 > 0 by XREAL_1:222;
then consider m1 being Element of NAT  such that
A4: for n, m being Element of NAT st n >= m1 & m >= m1 holds
dist ((seq1 . n),(seq1 . m)) < r / 3 by A1, Def8;
consider m2 being Element of NAT  such that
A5: for n being Element of NAT st n >= m2 holds
dist ((seq1 . n),(seq2 . n)) < r / 3 by A2, A3, Def9;
take k = m1 + m2; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds
dist ((seq2 . n),(seq2 . m)) < r
let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies dist ((seq2 . n),(seq2 . m)) < r )
assume that
A6: n >= k and
A7: m >= k ; ::_thesis: dist ((seq2 . n),(seq2 . m)) < r
 m1 + m2 >= m1 by NAT_1:12;
then  ( n >= m1 & m >= m1 ) by A6, A7, XXREAL_0:2;
then A8: dist ((seq1 . n),(seq1 . m)) < r / 3 by A4;
A9: dist ((seq2 . n),(seq1 . m)) <= (dist ((seq2 . n),(seq1 . n))) + (dist ((seq1 . n),(seq1 . m))) by CSSPACE:51;
A10: k >= m2 by NAT_1:12;
then  n >= m2 by A6, XXREAL_0:2;
then  dist ((seq1 . n),(seq2 . n)) < r / 3 by A5;
then  (dist ((seq2 . n),(seq1 . n))) + (dist ((seq1 . n),(seq1 . m))) < (r / 3) + (r / 3) by A8, XREAL_1:8;
then A11: dist ((seq2 . n),(seq1 . m)) < (r / 3) + (r / 3) by A9, XXREAL_0:2;
A12: dist ((seq2 . n),(seq2 . m)) <= (dist ((seq2 . n),(seq1 . m))) + (dist ((seq1 . m),(seq2 . m))) by CSSPACE:51;
 m >= m2 by A7, A10, XXREAL_0:2;
then  dist ((seq1 . m),(seq2 . m)) < r / 3 by A5;
then  (dist ((seq2 . n),(seq1 . m))) + (dist ((seq1 . m),(seq2 . m))) < ((r / 3) + (r / 3)) + (r / 3) by A11, XREAL_1:8;
hence  dist ((seq2 . n),(seq2 . m)) < r by A12, XXREAL_0:2; ::_thesis: verum
end;

theorem :: CLVECT_2:72
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is convergent & seq1 is_compared_to seq2 holds
seq2 is convergent
proof
let X be ComplexUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X st seq1 is convergent & seq1 is_compared_to seq2 holds
seq2 is convergent
let seq1, seq2 be sequence of X; ::_thesis: ( seq1 is convergent & seq1 is_compared_to seq2 implies seq2 is convergent )
assume that
A1: seq1 is convergent and
A2: seq1 is_compared_to seq2 ; ::_thesis: seq2 is convergent
now__::_thesis:_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_((seq2_._n),(lim_seq1))_<_r
let r be Real; ::_thesis: ( r > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq2 . n),(lim seq1)) < r )
assume  r > 0 ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq2 . n),(lim seq1)) < r
then A3: r / 2 > 0 by XREAL_1:215;
then consider m1 being Element of NAT  such that
A4: for n being Element of NAT st n >= m1 holds
dist ((seq1 . n),(lim seq1)) < r / 2 by A1, Def2;
consider m2 being Element of NAT  such that
A5: for n being Element of NAT st n >= m2 holds
dist ((seq1 . n),(seq2 . n)) < r / 2 by A2, A3, Def9;
take m = m1 + m2; ::_thesis: for n being Element of NAT st n >= m holds
dist ((seq2 . n),(lim seq1)) < r
let n be Element of NAT ; ::_thesis: ( n >= m implies dist ((seq2 . n),(lim seq1)) < r )
assume A6: n >= m ; ::_thesis: dist ((seq2 . n),(lim seq1)) < r
 m >= m2 by NAT_1:12;
then  n >= m2 by A6, XXREAL_0:2;
then A7: dist ((seq1 . n),(seq2 . n)) < r / 2 by A5;
A8: dist ((seq2 . n),(lim seq1)) <= (dist ((seq2 . n),(seq1 . n))) + (dist ((seq1 . n),(lim seq1))) by CSSPACE:51;
 m1 + m2 >= m1 by NAT_1:12;
then  n >= m1 by A6, XXREAL_0:2;
then  dist ((seq1 . n),(lim seq1)) < r / 2 by A4;
then  (dist ((seq2 . n),(seq1 . n))) + (dist ((seq1 . n),(lim seq1))) < (r / 2) + (r / 2) by A7, XREAL_1:8;
hence  dist ((seq2 . n),(lim seq1)) < r by A8, XXREAL_0:2; ::_thesis: verum
end;
hence  seq2 is convergent by Def1; ::_thesis: verum
end;

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 & lim seq1 = g & seq1 is_compared_to seq2 holds
( seq2 is convergent & lim seq2 = g )
proof
let X be ComplexUnitarySpace; ::_thesis: for g being Point of X
for seq1, seq2 being sequence of X st seq1 is convergent & lim seq1 = g & seq1 is_compared_to seq2 holds
( seq2 is convergent & lim seq2 = g )
let g be Point of X; ::_thesis: for seq1, seq2 being sequence of X st seq1 is convergent & lim seq1 = g & seq1 is_compared_to seq2 holds
( seq2 is convergent & lim seq2 = g )
let seq1, seq2 be sequence of X; ::_thesis: ( seq1 is convergent & lim seq1 = g & seq1 is_compared_to seq2 implies ( seq2 is convergent & lim seq2 = g ) )
assume that
A1: ( seq1 is convergent & lim seq1 = g ) and
A2: seq1 is_compared_to seq2 ; ::_thesis: ( seq2 is convergent & lim seq2 = g )
A3: now__::_thesis:_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_((seq2_._n),g)_<_r
let r be Real; ::_thesis: ( r > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq2 . n),g) < r )
assume  r > 0 ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq2 . n),g) < r
then A4: r / 2 > 0 by XREAL_1:215;
then consider m1 being Element of NAT  such that
A5: for n being Element of NAT st n >= m1 holds
dist ((seq1 . n),g) < r / 2 by A1, Def2;
consider m2 being Element of NAT  such that
A6: for n being Element of NAT st n >= m2 holds
dist ((seq1 . n),(seq2 . n)) < r / 2 by A2, A4, Def9;
take m = m1 + m2; ::_thesis: for n being Element of NAT st n >= m holds
dist ((seq2 . n),g) < r
let n be Element of NAT ; ::_thesis: ( n >= m implies dist ((seq2 . n),g) < r )
assume A7: n >= m ; ::_thesis: dist ((seq2 . n),g) < r
 m >= m2 by NAT_1:12;
then  n >= m2 by A7, XXREAL_0:2;
then A8: dist ((seq1 . n),(seq2 . n)) < r / 2 by A6;
A9: dist ((seq2 . n),g) <= (dist ((seq2 . n),(seq1 . n))) + (dist ((seq1 . n),g)) by CSSPACE:51;
 m1 + m2 >= m1 by NAT_1:12;
then  n >= m1 by A7, XXREAL_0:2;
then  dist ((seq1 . n),g) < r / 2 by A5;
then  (dist ((seq2 . n),(seq1 . n))) + (dist ((seq1 . n),g)) < (r / 2) + (r / 2) by A8, XREAL_1:8;
hence  dist ((seq2 . n),g) < r by A9, XXREAL_0:2; ::_thesis: verum
end;
then  seq2 is convergent by Def1;
hence  ( seq2 is convergent & lim seq2 = g ) by A3, Def2; ::_thesis: verum
end;

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 & ( 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 & ( 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 & seq2 is bounded holds
seq1 + seq2 is bounded
proof
let X be ComplexUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X st seq1 is bounded & seq2 is bounded holds
seq1 + seq2 is bounded
let seq1, seq2 be sequence of X; ::_thesis: ( seq1 is bounded & seq2 is bounded implies seq1 + seq2 is bounded )
assume that
A1: seq1 is bounded and
A2: seq2 is bounded ; ::_thesis: seq1 + seq2 is bounded
consider M2 being Real such that
A3: M2 > 0 and
A4: for n being Element of NAT holds ||.(seq2 . n).|| <= M2 by A2, Def10;
consider M1 being Real such that
A5: M1 > 0 and
A6: for n being Element of NAT holds ||.(seq1 . n).|| <= M1 by A1, Def10;
now__::_thesis:_for_n_being_Element_of_NAT_holds_||.((seq1_+_seq2)_._n).||_<=_M1_+_M2
let n be Element of NAT ; ::_thesis: ||.((seq1 + seq2) . n).|| <= M1 + M2
 ||.((seq1 + seq2) . n).|| = ||.((seq1 . n) + (seq2 . n)).|| by NORMSP_1:def_2;
then A7: ||.((seq1 + seq2) . n).|| <= ||.(seq1 . n).|| + ||.(seq2 . n).|| by CSSPACE:46;
 ( ||.(seq1 . n).|| <= M1 & ||.(seq2 . n).|| <= M2 ) by A6, A4;
then  ||.(seq1 . n).|| + ||.(seq2 . n).|| <= M1 + M2 by XREAL_1:7;
hence  ||.((seq1 + seq2) . n).|| <= M1 + M2 by A7, XXREAL_0:2; ::_thesis: verum
end;
hence  seq1 + seq2 is bounded by A5, A3, Def10; ::_thesis: verum
end;

theorem Th75: :: CLVECT_2:75
for X being ComplexUnitarySpace
for seq being sequence of X st seq is bounded holds
- seq is bounded
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X st seq is bounded holds
- seq is bounded
let seq be sequence of X; ::_thesis: ( seq is bounded implies - seq is bounded )
assume  seq is bounded ; ::_thesis: - seq is bounded
then consider M being Real such that
A1: M > 0 and
A2: for n being Element of NAT holds ||.(seq . n).|| <= M by Def10;
now__::_thesis:_for_n_being_Element_of_NAT_holds_||.((-_seq)_._n).||_<=_M
let n be Element of NAT ; ::_thesis: ||.((- seq) . n).|| <= M
||.((- seq) . n).|| = ||.(- (seq . n)).|| by BHSP_1:44
.= ||.(seq . n).|| by CSSPACE:47 ;
hence  ||.((- seq) . n).|| <= M by A2; ::_thesis: verum
end;
hence  - seq is bounded by A1, Def10; ::_thesis: verum
end;

theorem :: CLVECT_2:76
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is bounded & seq2 is bounded holds
seq1 - seq2 is bounded
proof
let X be ComplexUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X st seq1 is bounded & seq2 is bounded holds
seq1 - seq2 is bounded
let seq1, seq2 be sequence of X; ::_thesis: ( seq1 is bounded & seq2 is bounded implies seq1 - seq2 is bounded )
assume that
A1: seq1 is bounded and
A2: seq2 is bounded ; ::_thesis: seq1 - seq2 is bounded
A3: seq1 - seq2 = seq1 + (- seq2) by CSSPACE:64;
 - seq2 is bounded by A2, Th75;
hence  seq1 - seq2 is bounded by A1, A3, Th74; ::_thesis: verum
end;

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
proof
let X be ComplexUnitarySpace; ::_thesis: for z being Complex
for seq being sequence of X st seq is bounded holds
z * seq is bounded
let z be Complex; ::_thesis: for seq being sequence of X st seq is bounded holds
z * seq is bounded
let seq be sequence of X; ::_thesis: ( seq is bounded implies z * seq is bounded )
assume  seq is bounded ; ::_thesis: z * seq is bounded
then consider M being Real such that
A1: M > 0 and
A2: for n being Element of NAT holds ||.(seq . n).|| <= M by Def10;
A3: ( z <> 0 implies z * seq is bounded )
proof
A4: now__::_thesis:_for_n_being_Element_of_NAT_holds_||.((z_*_seq)_._n).||_<=_|.z.|_*_M
let n be Element of NAT ; ::_thesis: ||.((z * seq) . n).|| <= |.z.| * M
A5: |.z.| >= 0 by COMPLEX1:46;
||.((z * seq) . n).|| = ||.(z * (seq . n)).|| by CLVECT_1:def_14
.= |.z.| * ||.(seq . n).|| by CSSPACE:43 ;
hence  ||.((z * seq) . n).|| <= |.z.| * M by A2, A5, XREAL_1:64; ::_thesis: verum
end;
assume  z <> 0 ; ::_thesis: z * seq is bounded
then  |.z.| > 0 by COMPLEX1:47;
then  |.z.| * M > 0 by A1, XREAL_1:129;
hence  z * seq is bounded by A4, Def10; ::_thesis: verum
end;
 ( z = 0 implies z * seq is bounded )
proof
assume A6: z = 0 ; ::_thesis: z * seq is bounded
now__::_thesis:_for_n_being_Element_of_NAT_holds_||.((z_*_seq)_._n).||_<=_M
let n be Element of NAT ; ::_thesis: ||.((z * seq) . n).|| <= M
||.((z * seq) . n).|| = ||.(0c * (seq . n)).|| by A6, CLVECT_1:def_14
.= ||.H2(X).|| by CLVECT_1:1
.= 0 by CSSPACE:42 ;
hence  ||.((z * seq) . n).|| <= M by A1; ::_thesis: verum
end;
hence  z * seq is bounded by A1, Def10; ::_thesis: verum
end;
hence  z * seq is bounded by A3; ::_thesis: verum
end;

theorem :: CLVECT_2:78
for X being ComplexUnitarySpace
for seq being sequence of X st seq is constant holds
seq is bounded
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X st seq is constant holds
seq is bounded
let seq be sequence of X; ::_thesis: ( seq is constant implies seq is bounded )
assume  seq is constant ; ::_thesis: seq is bounded
then consider x being Point of X such that
A1: for n being Nat holds seq . n = x by VALUED_0:def_18;
A2: ( x = H2(X) implies seq is bounded )
proof
consider M being real number  such that
A3: M > 0 by XREAL_1:1;
reconsider M = M as Real by XREAL_0:def_1;
assume A4: x = H2(X) ; ::_thesis: seq is bounded
now__::_thesis:_for_n_being_Element_of_NAT_holds_||.(seq_._n).||_<=_M
let n be Element of NAT ; ::_thesis: ||.(seq . n).|| <= M
 seq . n = H2(X) by A1, A4;
hence  ||.(seq . n).|| <= M by A3, CSSPACE:42; ::_thesis: verum
end;
hence  seq is bounded by A3, Def10; ::_thesis: verum
end;
 ( x <> H2(X) implies seq is bounded )
proof
assume  x <> H2(X) ; ::_thesis: seq is bounded
consider M being real number  such that
A5: ||.x.|| < M by XREAL_1:1;
reconsider M = M as Real by XREAL_0:def_1;
 ( ||.x.|| >= 0 & ( for n being Element of NAT holds ||.(seq . n).|| <= M ) ) by A1, A5, CSSPACE:44;
hence  seq is bounded by A5, Def10; ::_thesis: verum
end;
hence  seq is bounded by A2; ::_thesis: verum
end;

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 & ( for n being Element of NAT st n <= m holds
||.(seq . n).|| < M ) )
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X
for m being Element of NAT ex M being Real st
( M > 0 & ( for n being Element of NAT st n <= m holds
||.(seq . n).|| < M ) )
let seq be sequence of X; ::_thesis: for m being Element of NAT ex M being Real st
( M > 0 & ( for n being Element of NAT st n <= m holds
||.(seq . n).|| < M ) )
defpred S1[ Element of NAT ] means  ex M being Real st
( M > 0 & ( for n being Element of NAT st n <= $1 holds
||.(seq . n).|| < M ) );
A1: for m being Element of NAT st S1[m] holds
S1[m + 1]
proof
let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] )
given M1 being Real such that A2: M1 > 0 and
A3: for n being Element of NAT st n <= m holds
||.(seq . n).|| < M1 ; ::_thesis: S1[m + 1]
A4: now__::_thesis:_(_||.(seq_._(m_+_1)).||_>=_M1_implies_ex_M_being_Element_of_REAL_st_
(_M_>_0_&_(_for_n_being_Element_of_NAT_st_n_<=_m_+_1_holds_
||.(seq_._n).||_<_M_)_)_)
assume A5: ||.(seq . (m + 1)).|| >= M1 ; ::_thesis: ex M being Element of REAL st
( M > 0 & ( for n being Element of NAT st n <= m + 1 holds
||.(seq . n).|| < M ) )
take M = ||.(seq . (m + 1)).|| + 1; ::_thesis: ( M > 0 & ( for n being Element of NAT st n <= m + 1 holds
||.(seq . n).|| < M ) )
 M > 0 + 0 by CSSPACE:44, XREAL_1:8;
hence  M > 0 ; ::_thesis: for n being Element of NAT st n <= m + 1 holds
||.(seq . n).|| < M
let n be Element of NAT ; ::_thesis: ( n <= m + 1 implies ||.(seq . n).|| < M )
assume A6: n <= m + 1 ; ::_thesis: ||.(seq . n).|| < M
A7: now__::_thesis:_(_m_>=_n_implies_||.(seq_._n).||_<_M_)
assume  m >= n ; ::_thesis: ||.(seq . n).|| < M
then  ||.(seq . n).|| < M1 by A3;
then  ||.(seq . n).|| < ||.(seq . (m + 1)).|| by A5, XXREAL_0:2;
then  ||.(seq . n).|| + 0 < M by XREAL_1:8;
hence  ||.(seq . n).|| < M ; ::_thesis: verum
end;
now__::_thesis:_(_n_=_m_+_1_implies_||.(seq_._n).||_<_M_)
assume  n = m + 1 ; ::_thesis: ||.(seq . n).|| < M
then  ||.(seq . n).|| + 0 < M by XREAL_1:8;
hence  ||.(seq . n).|| < M ; ::_thesis: verum
end;
hence  ||.(seq . n).|| < M by A6, A7, NAT_1:8; ::_thesis: verum
end;
now__::_thesis:_(_||.(seq_._(m_+_1)).||_<=_M1_implies_ex_M_being_Element_of_REAL_st_
(_M_>_0_&_(_for_n_being_Element_of_NAT_st_n_<=_m_+_1_holds_
||.(seq_._n).||_<_M_)_)_)
assume A8: ||.(seq . (m + 1)).|| <= M1 ; ::_thesis: ex M being Element of REAL st
( M > 0 & ( for n being Element of NAT st n <= m + 1 holds
||.(seq . n).|| < M ) )
take M = M1 + 1; ::_thesis: ( M > 0 & ( for n being Element of NAT st n <= m + 1 holds
||.(seq . n).|| < M ) )
thus  M > 0 by A2; ::_thesis: for n being Element of NAT st n <= m + 1 holds
||.(seq . n).|| < M
let n be Element of NAT ; ::_thesis: ( n <= m + 1 implies ||.(seq . n).|| < M )
assume A9: n <= m + 1 ; ::_thesis: ||.(seq . n).|| < M
A10: now__::_thesis:_(_m_>=_n_implies_||.(seq_._n).||_<_M_)
assume  m >= n ; ::_thesis: ||.(seq . n).|| < M
then A11: ||.(seq . n).|| < M1 by A3;
 M > M1 + 0 by XREAL_1:8;
hence  ||.(seq . n).|| < M by A11, XXREAL_0:2; ::_thesis: verum
end;
now__::_thesis:_(_n_=_m_+_1_implies_||.(seq_._n).||_<_M_)
A12: M > M1 + 0 by XREAL_1:8;
assume  n = m + 1 ; ::_thesis: ||.(seq . n).|| < M
hence  ||.(seq . n).|| < M by A8, A12, XXREAL_0:2; ::_thesis: verum
end;
hence  ||.(seq . n).|| < M by A9, A10, NAT_1:8; ::_thesis: verum
end;
hence  S1[m + 1] by A4; ::_thesis: verum
end;
A13: S1[ 0 ]
proof
take M = ||.(seq . 0).|| + 1; ::_thesis: ( M > 0 & ( for n being Element of NAT st n <= 0 holds
||.(seq . n).|| < M ) )
 ||.(seq . 0).|| + 1 > 0 + 0 by CSSPACE:44, XREAL_1:8;
hence  M > 0 ; ::_thesis: for n being Element of NAT st n <= 0 holds
||.(seq . n).|| < M
let n be Element of NAT ; ::_thesis: ( n <= 0 implies ||.(seq . n).|| < M )
assume  n <= 0 ; ::_thesis: ||.(seq . n).|| < M
then  n = 0 ;
then  ||.(seq . n).|| + 0 < M by XREAL_1:8;
hence  ||.(seq . n).|| < M ; ::_thesis: verum
end;
thus  for m being Element of NAT holds S1[m] from NAT_1:sch_1(A13, A1); ::_thesis: verum
end;

theorem Th80: :: CLVECT_2:80
for X being ComplexUnitarySpace
for seq being sequence of X st seq is convergent holds
seq is bounded
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X st seq is convergent holds
seq is bounded
let seq be sequence of X; ::_thesis: ( seq is convergent implies seq is bounded )
assume  seq is convergent ; ::_thesis: seq is bounded
then consider g being Point of X such that
A1: 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 by Th9;
consider m1 being Element of NAT  such that
A2: for n being Element of NAT st n >= m1 holds
||.((seq . n) - g).|| < 1 by A1;
A3: now__::_thesis:_ex_p_being_Element_of_REAL_st_
(_p_>_0_&_(_for_n_being_Element_of_NAT_st_n_>=_m1_holds_
||.(seq_._n).||_<_p_)_)
take p = ||.g.|| + 1; ::_thesis: ( p > 0 & ( for n being Element of NAT st n >= m1 holds
||.(seq . n).|| < p ) )
 0 + 0 < p by CSSPACE:44, XREAL_1:8;
hence  p > 0 ; ::_thesis: for n being Element of NAT st n >= m1 holds
||.(seq . n).|| < p
let n be Element of NAT ; ::_thesis: ( n >= m1 implies ||.(seq . n).|| < p )
assume  n >= m1 ; ::_thesis: ||.(seq . n).|| < p
then A4: ||.((seq . n) - g).|| < 1 by A2;
 ||.(seq . n).|| - ||.g.|| <= ||.((seq . n) - g).|| by CSSPACE:48;
then  ||.(seq . n).|| - ||.g.|| < 1 by A4, XXREAL_0:2;
hence  ||.(seq . n).|| < p by XREAL_1:19; ::_thesis: verum
end;
now__::_thesis:_ex_M_being_Element_of_REAL_st_
(_M_>_0_&_(_for_n_being_Element_of_NAT_holds_||.(seq_._n).||_<=_M_)_)
consider M2 being Real such that
A5: M2 > 0 and
A6: for n being Element of NAT st n <= m1 holds
||.(seq . n).|| < M2 by Th79;
consider M1 being Real such that
A7: M1 > 0 and
A8: for n being Element of NAT st n >= m1 holds
||.(seq . n).|| < M1 by A3;
take M = M1 + M2; ::_thesis: ( M > 0 & ( for n being Element of NAT holds ||.(seq . n).|| <= M ) )
thus  M > 0 by A7, A5; ::_thesis: for n being Element of NAT holds ||.(seq . n).|| <= M
let n be Element of NAT ; ::_thesis: ||.(seq . n).|| <= M
A9: M > 0 + M2 by A7, XREAL_1:8;
A10: now__::_thesis:_(_n_<=_m1_implies_||.(seq_._n).||_<=_M_)
assume  n <= m1 ; ::_thesis: ||.(seq . n).|| <= M
then  ||.(seq . n).|| < M2 by A6;
hence  ||.(seq . n).|| <= M by A9, XXREAL_0:2; ::_thesis: verum
end;
A11: M > M1 + 0 by A5, XREAL_1:8;
now__::_thesis:_(_n_>=_m1_implies_||.(seq_._n).||_<=_M_)
assume  n >= m1 ; ::_thesis: ||.(seq . n).|| <= M
then  ||.(seq . n).|| < M1 by A8;
hence  ||.(seq . n).|| <= M by A11, XXREAL_0:2; ::_thesis: verum
end;
hence  ||.(seq . n).|| <= M by A10; ::_thesis: verum
end;
hence  seq is bounded by Def10; ::_thesis: verum
end;

theorem :: CLVECT_2:81
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is bounded & seq1 is_compared_to seq2 holds
seq2 is bounded
proof
let X be ComplexUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X st seq1 is bounded & seq1 is_compared_to seq2 holds
seq2 is bounded
let seq1, seq2 be sequence of X; ::_thesis: ( seq1 is bounded & seq1 is_compared_to seq2 implies seq2 is bounded )
assume that
A1: seq1 is bounded and
A2: seq1 is_compared_to seq2 ; ::_thesis: seq2 is bounded
consider m1 being Element of NAT  such that
A3: for n being Element of NAT st n >= m1 holds
dist ((seq1 . n),(seq2 . n)) < 1 by A2, Def9;
consider p being Real such that
A4: p > 0 and
A5: for n being Element of NAT holds ||.(seq1 . n).|| <= p by A1, Def10;
A6: ex M being Real st
( M > 0 & ( for n being Element of NAT st n >= m1 holds
||.(seq2 . n).|| < M ) )
proof
take M = p + 1; ::_thesis: ( M > 0 & ( for n being Element of NAT st n >= m1 holds
||.(seq2 . n).|| < M ) )
now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_m1_holds_
||.(seq2_._n).||_<_M
let n be Element of NAT ; ::_thesis: ( n >= m1 implies ||.(seq2 . n).|| < M )
assume  n >= m1 ; ::_thesis: ||.(seq2 . n).|| < M
then  dist ((seq1 . n),(seq2 . n)) < 1 by A3;
then A7: ||.((seq2 . n) - (seq1 . n)).|| < 1 by CSSPACE:def_16;
 ||.(seq2 . n).|| - ||.(seq1 . n).|| <= ||.((seq2 . n) - (seq1 . n)).|| by CSSPACE:48;
then  ||.(seq2 . n).|| - ||.(seq1 . n).|| < 1 by A7, XXREAL_0:2;
then A8: ||.(seq2 . n).|| < ||.(seq1 . n).|| + 1 by XREAL_1:19;
 ||.(seq1 . n).|| <= p by A5;
then  ||.(seq1 . n).|| + 1 <= p + 1 by XREAL_1:6;
hence  ||.(seq2 . n).|| < M by A8, XXREAL_0:2; ::_thesis: verum
end;
hence  ( M > 0 & ( for n being Element of NAT st n >= m1 holds
||.(seq2 . n).|| < M ) ) by A4; ::_thesis: verum
end;
now__::_thesis:_ex_M_being_Element_of_REAL_st_
(_M_>_0_&_(_for_n_being_Element_of_NAT_holds_||.(seq2_._n).||_<=_M_)_)
consider M2 being Real such that
A9: M2 > 0 and
A10: for n being Element of NAT st n <= m1 holds
||.(seq2 . n).|| < M2 by Th79;
consider M1 being Real such that
A11: M1 > 0 and
A12: for n being Element of NAT st n >= m1 holds
||.(seq2 . n).|| < M1 by A6;
take M = M1 + M2; ::_thesis: ( M > 0 & ( for n being Element of NAT holds ||.(seq2 . n).|| <= M ) )
thus  M > 0 by A11, A9; ::_thesis: for n being Element of NAT holds ||.(seq2 . n).|| <= M
let n be Element of NAT ; ::_thesis: ||.(seq2 . n).|| <= M
A13: M > 0 + M2 by A11, XREAL_1:8;
A14: now__::_thesis:_(_n_<=_m1_implies_||.(seq2_._n).||_<=_M_)
assume  n <= m1 ; ::_thesis: ||.(seq2 . n).|| <= M
then  ||.(seq2 . n).|| < M2 by A10;
hence  ||.(seq2 . n).|| <= M by A13, XXREAL_0:2; ::_thesis: verum
end;
A15: M > M1 + 0 by A9, XREAL_1:8;
now__::_thesis:_(_n_>=_m1_implies_||.(seq2_._n).||_<=_M_)
assume  n >= m1 ; ::_thesis: ||.(seq2 . n).|| <= M
then  ||.(seq2 . n).|| < M1 by A12;
hence  ||.(seq2 . n).|| <= M by A15, XXREAL_0:2; ::_thesis: verum
end;
hence  ||.(seq2 . n).|| <= M by A14; ::_thesis: verum
end;
hence  seq2 is bounded by Def10; ::_thesis: verum
end;

theorem Th82: :: CLVECT_2:82
for X being ComplexUnitarySpace
for seq, seq1 being sequence of X st seq is bounded & seq1 is subsequence of seq holds
seq1 is bounded
proof
let X be ComplexUnitarySpace; ::_thesis: for seq, seq1 being sequence of X st seq is bounded & seq1 is subsequence of seq holds
seq1 is bounded
let seq, seq1 be sequence of X; ::_thesis: ( seq is bounded & seq1 is subsequence of seq implies seq1 is bounded )
assume that
A1: seq is bounded and
A2: seq1 is subsequence of seq ; ::_thesis: seq1 is bounded
consider Nseq being increasing sequence of NAT such that
A3: seq1 = seq * Nseq by A2, VALUED_0:def_17;
consider M1 being Real such that
A4: M1 > 0 and
A5: for n being Element of NAT holds ||.(seq . n).|| <= M1 by A1, Def10;
take M = M1; :: according to CLVECT_2:def_10 ::_thesis: ( M > 0 & ( for n being Element of NAT holds ||.(seq1 . n).|| <= M ) )
now__::_thesis:_for_n_being_Element_of_NAT_holds_||.(seq1_._n).||_<=_M
let n be Element of NAT ; ::_thesis: ||.(seq1 . n).|| <= M
 seq1 . n = seq . (Nseq . n) by A3, FUNCT_2:15;
hence  ||.(seq1 . n).|| <= M by A5; ::_thesis: verum
end;
hence  ( M > 0 & ( for n being Element of NAT holds ||.(seq1 . n).|| <= M ) ) by A4; ::_thesis: verum
end;

theorem Th83: :: CLVECT_2:83
for X being ComplexUnitarySpace
for seq, seq1 being sequence of X st seq is convergent & seq1 is subsequence of seq holds
seq1 is convergent
proof
let X be ComplexUnitarySpace; ::_thesis: for seq, seq1 being sequence of X st seq is convergent & seq1 is subsequence of seq holds
seq1 is convergent
let seq, seq1 be sequence of X; ::_thesis: ( seq is convergent & seq1 is subsequence of seq implies seq1 is convergent )
assume that
A1: seq is convergent and
A2: seq1 is subsequence of seq ; ::_thesis: seq1 is convergent
consider Nseq being increasing sequence of NAT such that
A3: seq1 = seq * Nseq by A2, VALUED_0:def_17;
consider g1 being Point of X such that
A4: 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) - g1).|| < r by A1, Th9;
now__::_thesis:_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)_-_g1).||_<_r
let r be Real; ::_thesis: ( r > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((seq1 . n) - g1).|| < r )
assume  r > 0 ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((seq1 . n) - g1).|| < r
then consider m1 being Element of NAT  such that
A5: for n being Element of NAT st n >= m1 holds
||.((seq . n) - g1).|| < r by A4;
take m = m1; ::_thesis: for n being Element of NAT st n >= m holds
||.((seq1 . n) - g1).|| < r
let n be Element of NAT ; ::_thesis: ( n >= m implies ||.((seq1 . n) - g1).|| < r )
assume A6: n >= m ; ::_thesis: ||.((seq1 . n) - g1).|| < r
 Nseq . n >= n by SEQM_3:14;
then A7: Nseq . n >= m by A6, XXREAL_0:2;
 seq1 . n = seq . (Nseq . n) by A3, FUNCT_2:15;
hence  ||.((seq1 . n) - g1).|| < r by A5, A7; ::_thesis: verum
end;
hence  seq1 is convergent by Th9; ::_thesis: verum
end;

theorem Th84: :: CLVECT_2:84
for X being ComplexUnitarySpace
for seq1, seq being sequence of X st seq1 is subsequence of seq & seq is convergent holds
lim seq1 = lim seq
proof
let X be ComplexUnitarySpace; ::_thesis: for seq1, seq being sequence of X st seq1 is subsequence of seq & seq is convergent holds
lim seq1 = lim seq
let seq1, seq be sequence of X; ::_thesis: ( seq1 is subsequence of seq & seq is convergent implies lim seq1 = lim seq )
assume that
A1: seq1 is subsequence of seq and
A2: seq is convergent ; ::_thesis: lim seq1 = lim seq
consider Nseq being increasing sequence of NAT such that
A3: seq1 = seq * Nseq by A1, VALUED_0:def_17;
A4: now__::_thesis:_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),(lim_seq))_<_r
let r be Real; ::_thesis: ( r > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq1 . n),(lim seq)) < r )
assume  r > 0 ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq1 . n),(lim seq)) < r
then consider m1 being Element of NAT  such that
A5: for n being Element of NAT st n >= m1 holds
dist ((seq . n),(lim seq)) < r by A2, Def2;
take m = m1; ::_thesis: for n being Element of NAT st n >= m holds
dist ((seq1 . n),(lim seq)) < r
let n be Element of NAT ; ::_thesis: ( n >= m implies dist ((seq1 . n),(lim seq)) < r )
assume A6: n >= m ; ::_thesis: dist ((seq1 . n),(lim seq)) < r
 Nseq . n >= n by SEQM_3:14;
then A7: Nseq . n >= m by A6, XXREAL_0:2;
 seq1 . n = seq . (Nseq . n) by A3, FUNCT_2:15;
hence  dist ((seq1 . n),(lim seq)) < r by A5, A7; ::_thesis: verum
end;
 seq1 is convergent by A1, A2, Th83;
hence  lim seq1 = lim seq by A4, Def2; ::_thesis: verum
end;

theorem Th85: :: CLVECT_2:85
for X being ComplexUnitarySpace
for seq, seq1 being sequence of X st seq is Cauchy & seq1 is subsequence of seq holds
seq1 is Cauchy
proof
let X be ComplexUnitarySpace; ::_thesis: for seq, seq1 being sequence of X st seq is Cauchy & seq1 is subsequence of seq holds
seq1 is Cauchy
let seq, seq1 be sequence of X; ::_thesis: ( seq is Cauchy & seq1 is subsequence of seq implies seq1 is Cauchy )
assume that
A1: seq is Cauchy and
A2: seq1 is subsequence of seq ; ::_thesis: seq1 is Cauchy
consider Nseq being increasing sequence of NAT such that
A3: seq1 = seq * Nseq by A2, VALUED_0:def_17;
now__::_thesis:_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_&_m_>=_k_holds_
dist_((seq1_._n),(seq1_._m))_<_r
let r be Real; ::_thesis: ( r > 0 implies ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
dist ((seq1 . n),(seq1 . m)) < r )
assume  r > 0 ; ::_thesis: ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
dist ((seq1 . n),(seq1 . m)) < r
then consider l being Element of NAT  such that
A4: for n, m being Element of NAT st n >= l & m >= l holds
dist ((seq . n),(seq . m)) < r by A1, Def8;
take k = l; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds
dist ((seq1 . n),(seq1 . m)) < r
let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies dist ((seq1 . n),(seq1 . m)) < r )
assume that
A5: n >= k and
A6: m >= k ; ::_thesis: dist ((seq1 . n),(seq1 . m)) < r
 Nseq . n >= n by SEQM_3:14;
then A7: Nseq . n >= k by A5, XXREAL_0:2;
 Nseq . m >= m by SEQM_3:14;
then A8: Nseq . m >= k by A6, XXREAL_0:2;
 ( seq1 . n = seq . (Nseq . n) & seq1 . m = seq . (Nseq . m) ) by A3, FUNCT_2:15;
hence  dist ((seq1 . n),(seq1 . m)) < r by A4, A7, A8; ::_thesis: verum
end;
hence  seq1 is Cauchy by Def8; ::_thesis: verum
end;

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)
proof
let X be ComplexUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X
for k being Element of NAT holds (seq1 + seq2) ^\ k = (seq1 ^\ k) + (seq2 ^\ k)
let seq1, seq2 be sequence of X; ::_thesis: for k being Element of NAT holds (seq1 + seq2) ^\ k = (seq1 ^\ k) + (seq2 ^\ k)
let k be Element of NAT ; ::_thesis: (seq1 + seq2) ^\ k = (seq1 ^\ k) + (seq2 ^\ k)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq1_+_seq2)_^\_k)_._n_=_((seq1_^\_k)_+_(seq2_^\_k))_._n
let n be Element of NAT ; ::_thesis: ((seq1 + seq2) ^\ k) . n = ((seq1 ^\ k) + (seq2 ^\ k)) . n
thus ((seq1 + seq2) ^\ k) . n = (seq1 + seq2) . (n + k) by NAT_1:def_3
.= (seq1 . (n + k)) + (seq2 . (n + k)) by NORMSP_1:def_2
.= ((seq1 ^\ k) . n) + (seq2 . (n + k)) by NAT_1:def_3
.= ((seq1 ^\ k) . n) + ((seq2 ^\ k) . n) by NAT_1:def_3
.= ((seq1 ^\ k) + (seq2 ^\ k)) . n by NORMSP_1:def_2 ; ::_thesis: verum
end;
hence  (seq1 + seq2) ^\ k = (seq1 ^\ k) + (seq2 ^\ k) by FUNCT_2:63; ::_thesis: verum
end;

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)
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X
for k being Element of NAT holds (- seq) ^\ k = - (seq ^\ k)
let seq be sequence of X; ::_thesis: for k being Element of NAT holds (- seq) ^\ k = - (seq ^\ k)
let k be Element of NAT ; ::_thesis: (- seq) ^\ k = - (seq ^\ k)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((-_seq)_^\_k)_._n_=_(-_(seq_^\_k))_._n
let n be Element of NAT ; ::_thesis: ((- seq) ^\ k) . n = (- (seq ^\ k)) . n
thus ((- seq) ^\ k) . n = (- seq) . (n + k) by NAT_1:def_3
.= - (seq . (n + k)) by BHSP_1:44
.= - ((seq ^\ k) . n) by NAT_1:def_3
.= (- (seq ^\ k)) . n by BHSP_1:44 ; ::_thesis: verum
end;
hence  (- seq) ^\ k = - (seq ^\ k) by FUNCT_2:63; ::_thesis: verum
end;

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)
proof
let X be ComplexUnitarySpace; ::_thesis: for seq1, seq2 being sequence of X
for k being Element of NAT holds (seq1 - seq2) ^\ k = (seq1 ^\ k) - (seq2 ^\ k)
let seq1, seq2 be sequence of X; ::_thesis: for k being Element of NAT holds (seq1 - seq2) ^\ k = (seq1 ^\ k) - (seq2 ^\ k)
let k be Element of NAT ; ::_thesis: (seq1 - seq2) ^\ k = (seq1 ^\ k) - (seq2 ^\ k)
thus (seq1 - seq2) ^\ k = (seq1 + (- seq2)) ^\ k by CSSPACE:64
.= (seq1 ^\ k) + ((- seq2) ^\ k) by Th86
.= (seq1 ^\ k) + (- (seq2 ^\ k)) by Th87
.= (seq1 ^\ k) - (seq2 ^\ k) by CSSPACE:64 ; ::_thesis: verum
end;

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)
proof
let X be ComplexUnitarySpace; ::_thesis: for z being Complex
for seq being sequence of X
for k being Element of NAT holds (z * seq) ^\ k = z * (seq ^\ k)
let z be Complex; ::_thesis: for seq being sequence of X
for k being Element of NAT holds (z * seq) ^\ k = z * (seq ^\ k)
let seq be sequence of X; ::_thesis: for k being Element of NAT holds (z * seq) ^\ k = z * (seq ^\ k)
let k be Element of NAT ; ::_thesis: (z * seq) ^\ k = z * (seq ^\ k)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((z_*_seq)_^\_k)_._n_=_(z_*_(seq_^\_k))_._n
let n be Element of NAT ; ::_thesis: ((z * seq) ^\ k) . n = (z * (seq ^\ k)) . n
thus ((z * seq) ^\ k) . n = (z * seq) . (n + k) by NAT_1:def_3
.= z * (seq . (n + k)) by CLVECT_1:def_14
.= z * ((seq ^\ k) . n) by NAT_1:def_3
.= (z * (seq ^\ k)) . n by CLVECT_1:def_14 ; ::_thesis: verum
end;
hence  (z * seq) ^\ k = z * (seq ^\ k) by FUNCT_2:63; ::_thesis: verum
end;

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 & 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 & ex k being Element of NAT st seq = seq1 ^\ k holds
seq1 is convergent
proof
let X be ComplexUnitarySpace; ::_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 Point of X such that
A4: 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) - 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_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_n_>=_m_holds_
||.((seq1_._n)_-_g).||_<_r
take g = g1; ::_thesis: 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) - g).|| < r
let r be Real; ::_thesis: ( r > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((seq1 . n) - g).|| < r )
assume  r > 0 ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((seq1 . n) - g).|| < r
then consider m1 being Element of NAT  such that
A5: for n being Element of NAT st n >= m1 holds
||.((seq . n) - g).|| < r by A4;
take m = m1 + k; ::_thesis: for n being Element of NAT st n >= m holds
||.((seq1 . n) - g).|| < r
let n be Element of 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 Element of NAT by ORDINAL1:def_12;
 n - k = m1 + m2 by A7;
then consider l being Element of 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
end;

theorem :: CLVECT_2:92
for X being ComplexUnitarySpace
for seq, seq1 being sequence of X st seq is Cauchy & ex k being Element of NAT st seq = seq1 ^\ k holds
seq1 is Cauchy
proof
let X be ComplexUnitarySpace; ::_thesis: for seq, seq1 being sequence of X st seq is Cauchy & ex k being Element of NAT st seq = seq1 ^\ k holds
seq1 is Cauchy
let seq, seq1 be sequence of X; ::_thesis: ( seq is Cauchy & ex k being Element of NAT st seq = seq1 ^\ k implies seq1 is Cauchy )
assume that
A1: seq is Cauchy and
A2: ex k being Element of NAT st seq = seq1 ^\ k ; ::_thesis: seq1 is Cauchy
consider k being Element of NAT  such that
A3: seq = seq1 ^\ k by A2;
let r be Real; :: according to CLVECT_2:def_8 ::_thesis: ( r > 0 implies ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
dist ((seq1 . n),(seq1 . m)) < r )
assume  r > 0 ; ::_thesis: ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
dist ((seq1 . n),(seq1 . m)) < r
then consider l1 being Element of NAT  such that
A4: for n, m being Element of NAT st n >= l1 & m >= l1 holds
dist ((seq . n),(seq . m)) < r by A1, Def8;
take l = l1 + k; ::_thesis: for n, m being Element of NAT st n >= l & m >= l holds
dist ((seq1 . n),(seq1 . m)) < r
let n, m be Element of NAT ; ::_thesis: ( n >= l & m >= l implies dist ((seq1 . n),(seq1 . m)) < r )
assume that
A5: n >= l and
A6: m >= l ; ::_thesis: dist ((seq1 . n),(seq1 . m)) < r
consider m1 being Nat such that
A7: n = (l1 + k) + m1 by A5, NAT_1:10;
reconsider m1 = m1 as Element of NAT by ORDINAL1:def_12;
 n - k = l1 + m1 by A7;
then consider l2 being Element of NAT  such that
A8: l2 = n - k ;
consider m2 being Nat such that
A9: m = (l1 + k) + m2 by A6, NAT_1:10;
reconsider m2 = m2 as Element of NAT by ORDINAL1:def_12;
 m - k = l1 + m2 by A9;
then consider l3 being Element of NAT  such that
A10: l3 = m - k ;
A11: now__::_thesis:_not_l2_<_l1
assume  l2 < l1 ; ::_thesis: contradiction
then  l2 + k < l1 + k by XREAL_1:6;
hence  contradiction by A5, A8; ::_thesis: verum
end;
A12: l2 + k = n by A8;
now__::_thesis:_not_l3_<_l1
assume  l3 < l1 ; ::_thesis: contradiction
then  l3 + k < l1 + k by XREAL_1:6;
hence  contradiction by A6, A10; ::_thesis: verum
end;
then  dist ((seq . l2),(seq . l3)) < r by A4, A11;
then A13: dist ((seq1 . n),(seq . l3)) < r by A3, A12, NAT_1:def_3;
 l3 + k = m by A10;
hence  dist ((seq1 . n),(seq1 . m)) < r by A3, A13, NAT_1:def_3; ::_thesis: verum
end;

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
proof
let X be ComplexUnitarySpace; ::_thesis: 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
let seq1, seq2 be sequence of X; ::_thesis: for k being Element of NAT st seq1 is_compared_to seq2 holds
seq1 ^\ k is_compared_to seq2 ^\ k
let k be Element of NAT ; ::_thesis: ( seq1 is_compared_to seq2 implies seq1 ^\ k is_compared_to seq2 ^\ k )
assume A1: seq1 is_compared_to seq2 ; ::_thesis: seq1 ^\ k is_compared_to seq2 ^\ k
let r be Real; :: according to CLVECT_2:def_9 ::_thesis: ( r > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist (((seq1 ^\ k) . n),((seq2 ^\ k) . n)) < r )
assume  r > 0 ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist (((seq1 ^\ k) . n),((seq2 ^\ k) . n)) < r
then consider m1 being Element of NAT  such that
A2: for n being Element of NAT st n >= m1 holds
dist ((seq1 . n),(seq2 . n)) < r by A1, Def9;
take m = m1; ::_thesis: for n being Element of NAT st n >= m holds
dist (((seq1 ^\ k) . n),((seq2 ^\ k) . n)) < r
let n be Element of NAT ; ::_thesis: ( n >= m implies dist (((seq1 ^\ k) . n),((seq2 ^\ k) . n)) < r )
assume A3: n >= m ; ::_thesis: dist (((seq1 ^\ k) . n),((seq2 ^\ k) . n)) < r
 n + k >= n by NAT_1:11;
then  n + k >= m by A3, XXREAL_0:2;
then  dist ((seq1 . (n + k)),(seq2 . (n + k))) < r by A2;
then  dist (((seq1 ^\ k) . n),(seq2 . (n + k))) < r by NAT_1:def_3;
hence  dist (((seq1 ^\ k) . n),((seq2 ^\ k) . n)) < r by NAT_1:def_3; ::_thesis: verum
end;

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 & seq is Cauchy holds
seq is bounded
proof
let X be ComplexUnitarySpace; ::_thesis: for seq being sequence of X st X is complete & seq is Cauchy holds
seq is bounded
let seq be sequence of X; ::_thesis: ( X is complete & seq is Cauchy implies seq is bounded )
assume  ( X is complete & seq is Cauchy ) ; ::_thesis: seq is bounded
then  seq is convergent by Def11;
hence  seq is bounded by Th80; ::_thesis: verum
end;