:: BHSP_3 semantic presentation

begin

                         deffunc H1( RealUnitarySpace) ->  Element of the U1 of $1 = 0. $1;

definition
let X be RealUnitarySpace;
let seq be sequence of X;
attrseq is Cauchy  means :Def1: :: BHSP_3:def 1
 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 Def1 defines Cauchy BHSP_3:def_1_:_
 for X being RealUnitarySpace
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 :: BHSP_3:1
for X being RealUnitarySpace
for seq being sequence of X st seq is constant holds
seq is Cauchy
proof
let X be RealUnitarySpace; ::_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 BHSP_3:def_1 ::_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 BHSP_1:34 ;
hence  dist ((seq . n),(seq . m)) < r by A2; ::_thesis: verum
end;

theorem :: BHSP_3:2
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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, Def1;
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 BHSP_1:def_5; ::_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 BHSP_3:def_1 ::_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 BHSP_1:def_5; ::_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 :: BHSP_3:3
for X being RealUnitarySpace
for seq1, seq2 being sequence of X st seq1 is Cauchy & seq2 is Cauchy holds
seq1 + seq2 is Cauchy
proof
let X be RealUnitarySpace; ::_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 BHSP_3:def_1 ::_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, Def1;
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, Def1;
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 BHSP_1:40;
 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 :: BHSP_3:4
for X being RealUnitarySpace
for seq1, seq2 being sequence of X st seq1 is Cauchy & seq2 is Cauchy holds
seq1 - seq2 is Cauchy
proof
let X be RealUnitarySpace; ::_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 BHSP_3:def_1 ::_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, Def1;
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, Def1;
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 BHSP_1:41;
 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 Th5: :: BHSP_3:5
for X being RealUnitarySpace
for a being Real
for seq being sequence of X st seq is Cauchy holds
a * seq is Cauchy
proof
let X be RealUnitarySpace; ::_thesis: for a being Real
for seq being sequence of X st seq is Cauchy holds
a * seq is Cauchy
let a be Real; ::_thesis: for seq being sequence of X st seq is Cauchy holds
a * seq is Cauchy
let seq be sequence of X; ::_thesis: ( seq is Cauchy implies a * seq is Cauchy )
assume A1: seq is Cauchy ; ::_thesis: a * seq is Cauchy
A2: now__::_thesis:_(_a_<>_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_(((a_*_seq)_._n),((a_*_seq)_._m))_<_r_)
A3: 0 / (abs a) = 0 ;
assume A4: a <> 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 (((a * seq) . n),((a * seq) . m)) < r
then A5: abs a > 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 (((a * seq) . n),((a * 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 (((a * seq) . n),((a * seq) . m)) < r
then  r / (abs a) > 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 / (abs a) by A1, Def1;
take k = m1; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds
dist (((a * seq) . n),((a * seq) . m)) < r
let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies dist (((a * seq) . n),((a * seq) . m)) < r )
assume  ( n >= k & m >= k ) ; ::_thesis: dist (((a * seq) . n),((a * seq) . m)) < r
then A7: dist ((seq . n),(seq . m)) < r / (abs a) by A6;
A8: abs a <> 0 by A4, COMPLEX1:47;
A9: (abs a) * (r / (abs a)) = (abs a) * (((abs a) ") * r) by XCMPLX_0:def_9
.= ((abs a) * ((abs a) ")) * r
.= 1 * r by A8, XCMPLX_0:def_7
.= r ;
dist ((a * (seq . n)),(a * (seq . m))) = ||.((a * (seq . n)) - (a * (seq . m))).|| by BHSP_1:def_5
.= ||.(a * ((seq . n) - (seq . m))).|| by RLVECT_1:34
.= (abs a) * ||.((seq . n) - (seq . m)).|| by BHSP_1:27
.= (abs a) * (dist ((seq . n),(seq . m))) by BHSP_1:def_5 ;
then  dist ((a * (seq . n)),(a * (seq . m))) < r by A5, A7, A9, XREAL_1:68;
then  dist (((a * seq) . n),(a * (seq . m))) < r by NORMSP_1:def_5;
hence  dist (((a * seq) . n),((a * seq) . m)) < r by NORMSP_1:def_5; ::_thesis: verum
end;
now__::_thesis:_(_a_=_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_(((a_*_seq)_._n),((a_*_seq)_._m))_<_r_)
assume A10: a = 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 (((a * seq) . n),((a * 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 (((a * seq) . n),((a * 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 (((a * seq) . n),((a * 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, Def1;
take k = m1; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds
dist (((a * seq) . n),((a * seq) . m)) < r
let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies dist (((a * seq) . n),((a * seq) . m)) < r )
assume  ( n >= k & m >= k ) ; ::_thesis: dist (((a * seq) . n),((a * seq) . m)) < r
then A12: dist ((seq . n),(seq . m)) < r by A11;
dist ((a * (seq . n)),(a * (seq . m))) = dist (H1(X),(0 * (seq . m))) by A10, RLVECT_1:10
.= dist (H1(X),H1(X)) by RLVECT_1:10
.= 0 by BHSP_1:34 ;
then  dist ((a * (seq . n)),(a * (seq . m))) < r by A12, BHSP_1:37;
then  dist (((a * seq) . n),(a * (seq . m))) < r by NORMSP_1:def_5;
hence  dist (((a * seq) . n),((a * seq) . m)) < r by NORMSP_1:def_5; ::_thesis: verum
end;
hence  a * seq is Cauchy by A2, Def1; ::_thesis: verum
end;

theorem :: BHSP_3:6
for X being RealUnitarySpace
for seq being sequence of X st seq is Cauchy holds
- seq is Cauchy
proof
let X be RealUnitarySpace; ::_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  (- 1) * seq is Cauchy by Th5;
hence  - seq is Cauchy by BHSP_1:55; ::_thesis: verum
end;

theorem Th7: :: BHSP_3:7
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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 BHSP_3:def_1 ::_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, Def1;
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 BHSP_1:40;
then A3: dist (((seq . n) + x),((seq . m) + x)) <= (dist ((seq . n),(seq . m))) + 0 by BHSP_1:34;
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 :: BHSP_3:8
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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 Th7;
hence  seq - x is Cauchy by BHSP_1:56; ::_thesis: verum
end;

theorem :: BHSP_3:9
for X being RealUnitarySpace
for seq being sequence of X st seq is convergent holds
seq is Cauchy
proof
let X be RealUnitarySpace; ::_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 BHSP_2:def_1;
let r be Real; :: according to BHSP_3:def_1 ::_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 BHSP_1:35, XREAL_1:8;
hence  dist ((seq . n),(seq . m)) < r by XXREAL_0:2; ::_thesis: verum
end;

definition
let X be RealUnitarySpace;
let seq1, seq2 be sequence of X;
predseq1 is_compared_to seq2 means :Def2: :: BHSP_3: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 ((seq1 . n),(seq2 . n)) < r;
end;

:: deftheorem Def2 defines is_compared_to BHSP_3:def_2_:_
 for X being RealUnitarySpace
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 Th10: :: BHSP_3:10
for X being RealUnitarySpace
for seq being sequence of X holds seq is_compared_to seq
proof
let X be RealUnitarySpace; ::_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 BHSP_3:def_2 ::_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, BHSP_1:34; ::_thesis: verum
end;

theorem Th11: :: BHSP_3:11
for X being RealUnitarySpace
for seq1, seq2 being sequence of X st seq1 is_compared_to seq2 holds
seq2 is_compared_to seq1
proof
let X be RealUnitarySpace; ::_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 BHSP_3:def_2 ::_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, Def2;
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 RealUnitarySpace;
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 Th10;
symmetry
 for seq1, seq2 being sequence of X st (X,b1,b2) holds
(X,b2,b1) by Th11;
end;

theorem :: BHSP_3:12
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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 BHSP_3:def_2 ::_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, Def2;
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, Def2;
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 BHSP_1:35;
 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 :: BHSP_3:13
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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, Def2;
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 BHSP_1:def_5; ::_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 BHSP_3:def_2 ::_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 BHSP_1:def_5; ::_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 :: BHSP_3:14
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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 BHSP_3:def_2 ::_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 BHSP_1:34 ;
hence  dist ((seq1 . n),(seq2 . n)) < r by A2; ::_thesis: verum
end;

theorem :: BHSP_3:15
for X being RealUnitarySpace
for seq1, seq2 being sequence of X st seq1 is Cauchy & seq1 is_compared_to seq2 holds
seq2 is Cauchy
proof
let X be RealUnitarySpace; ::_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 BHSP_3:def_1 ::_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, Def1;
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, Def2;
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 BHSP_1:35;
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 BHSP_1:35;
 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 :: BHSP_3:16
for X being RealUnitarySpace
for seq1, seq2 being sequence of X st seq1 is convergent & seq1 is_compared_to seq2 holds
seq2 is convergent
proof
let X be RealUnitarySpace; ::_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, BHSP_2:def_2;
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, Def2;
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 BHSP_1:35;
 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 BHSP_2:def_1; ::_thesis: verum
end;

theorem :: BHSP_3:17
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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, BHSP_2:def_2;
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, Def2;
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 BHSP_1:35;
 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 BHSP_2:def_1;
hence  ( seq2 is convergent & lim seq2 = g ) by A3, BHSP_2:def_2; ::_thesis: verum
end;

definition
let X be RealUnitarySpace;
let seq be sequence of X;
attrseq is bounded  means :Def3: :: BHSP_3:def 3
 ex M being Real st
( M > 0 & ( for n being Element of NAT holds ||.(seq . n).|| <= M ) );
end;

:: deftheorem Def3 defines bounded BHSP_3:def_3_:_
 for X being RealUnitarySpace
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 Th18: :: BHSP_3:18
for X being RealUnitarySpace
for seq1, seq2 being sequence of X st seq1 is bounded & seq2 is bounded holds
seq1 + seq2 is bounded
proof
let X be RealUnitarySpace; ::_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, Def3;
consider M1 being Real such that
A5: M1 > 0 and
A6: for n being Element of NAT holds ||.(seq1 . n).|| <= M1 by A1, Def3;
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 BHSP_1:30;
 ( ||.(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, Def3; ::_thesis: verum
end;

theorem Th19: :: BHSP_3:19
for X being RealUnitarySpace
for seq being sequence of X st seq is bounded holds
- seq is bounded
proof
let X be RealUnitarySpace; ::_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 Def3;
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 BHSP_1:31 ;
hence  ||.((- seq) . n).|| <= M by A2; ::_thesis: verum
end;
hence  - seq is bounded by A1, Def3; ::_thesis: verum
end;

theorem :: BHSP_3:20
for X being RealUnitarySpace
for seq1, seq2 being sequence of X st seq1 is bounded & seq2 is bounded holds
seq1 - seq2 is bounded
proof
let X be RealUnitarySpace; ::_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 BHSP_1:49;
 - seq2 is bounded by A2, Th19;
hence  seq1 - seq2 is bounded by A1, A3, Th18; ::_thesis: verum
end;

theorem :: BHSP_3:21
for X being RealUnitarySpace
for a being Real
for seq being sequence of X st seq is bounded holds
a * seq is bounded
proof
let X be RealUnitarySpace; ::_thesis: for a being Real
for seq being sequence of X st seq is bounded holds
a * seq is bounded
let a be Real; ::_thesis: for seq being sequence of X st seq is bounded holds
a * seq is bounded
let seq be sequence of X; ::_thesis: ( seq is bounded implies a * seq is bounded )
assume  seq is bounded ; ::_thesis: a * 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 Def3;
A3: ( a <> 0 implies a * seq is bounded )
proof
A4: now__::_thesis:_for_n_being_Element_of_NAT_holds_||.((a_*_seq)_._n).||_<=_(abs_a)_*_M
let n be Element of NAT ; ::_thesis: ||.((a * seq) . n).|| <= (abs a) * M
A5: abs a >= 0 by COMPLEX1:46;
||.((a * seq) . n).|| = ||.(a * (seq . n)).|| by NORMSP_1:def_5
.= (abs a) * ||.(seq . n).|| by BHSP_1:27 ;
hence  ||.((a * seq) . n).|| <= (abs a) * M by A2, A5, XREAL_1:64; ::_thesis: verum
end;
assume  a <> 0 ; ::_thesis: a * seq is bounded
then  abs a > 0 by COMPLEX1:47;
then  (abs a) * M > 0 by A1, XREAL_1:129;
hence  a * seq is bounded by A4, Def3; ::_thesis: verum
end;
 ( a = 0 implies a * seq is bounded )
proof
assume A6: a = 0 ; ::_thesis: a * seq is bounded
now__::_thesis:_for_n_being_Element_of_NAT_holds_||.((a_*_seq)_._n).||_<=_M
let n be Element of NAT ; ::_thesis: ||.((a * seq) . n).|| <= M
||.((a * seq) . n).|| = ||.(0 * (seq . n)).|| by A6, NORMSP_1:def_5
.= ||.H1(X).|| by RLVECT_1:10
.= 0 by BHSP_1:26 ;
hence  ||.((a * seq) . n).|| <= M by A1; ::_thesis: verum
end;
hence  a * seq is bounded by A1, Def3; ::_thesis: verum
end;
hence  a * seq is bounded by A3; ::_thesis: verum
end;

theorem :: BHSP_3:22
for X being RealUnitarySpace
for seq being sequence of X st seq is constant holds
seq is bounded
proof
let X be RealUnitarySpace; ::_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 = H1(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 = H1(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 = H1(X) by A1, A4;
hence  ||.(seq . n).|| <= M by A3, BHSP_1:26; ::_thesis: verum
end;
hence  seq is bounded by A3, Def3; ::_thesis: verum
end;
 ( x <> H1(X) implies seq is bounded )
proof
assume  x <> H1(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, BHSP_1:28;
hence  seq is bounded by A5, Def3; ::_thesis: verum
end;
hence  seq is bounded by A2; ::_thesis: verum
end;

theorem Th23: :: BHSP_3:23
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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 BHSP_1:28, 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 BHSP_1:28, 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 Th24: :: BHSP_3:24
for X being RealUnitarySpace
for seq being sequence of X st seq is convergent holds
seq is bounded
proof
let X be RealUnitarySpace; ::_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 BHSP_2:9;
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 BHSP_1:28, 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 BHSP_1:32;
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 Th23;
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 Def3; ::_thesis: verum
end;

theorem :: BHSP_3:25
for X being RealUnitarySpace
for seq1, seq2 being sequence of X st seq1 is bounded & seq1 is_compared_to seq2 holds
seq2 is bounded
proof
let X be RealUnitarySpace; ::_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, Def2;
consider p being Real such that
A4: p > 0 and
A5: for n being Element of NAT holds ||.(seq1 . n).|| <= p by A1, Def3;
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 BHSP_1:def_5;
 ||.(seq2 . n).|| - ||.(seq1 . n).|| <= ||.((seq2 . n) - (seq1 . n)).|| by BHSP_1:32;
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 Th23;
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 Def3; ::_thesis: verum
end;

theorem Th26: :: BHSP_3:26
for X being RealUnitarySpace
for seq, seq1 being sequence of X st seq is bounded & seq1 is subsequence of seq holds
seq1 is bounded
proof
let X be RealUnitarySpace; ::_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, Def3;
take M = M1; :: according to BHSP_3:def_3 ::_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 Th27: :: BHSP_3:27
for X being RealUnitarySpace
for seq, seq1 being sequence of X st seq is convergent & seq1 is subsequence of seq holds
seq1 is convergent
proof
let X be RealUnitarySpace; ::_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 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
||.((seq . n) - g1).|| < r by A1, BHSP_2:9;
consider Nseq being increasing sequence of NAT such that
A4: seq1 = seq * Nseq by A2, VALUED_0:def_17;
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 A3;
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 A4, FUNCT_2:15;
hence  ||.((seq1 . n) - g1).|| < r by A5, A7; ::_thesis: verum
end;
hence  seq1 is convergent by BHSP_2:9; ::_thesis: verum
end;

theorem Th28: :: BHSP_3:28
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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, BHSP_2:def_2;
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, Th27;
hence  lim seq1 = lim seq by A4, BHSP_2:def_2; ::_thesis: verum
end;

theorem Th29: :: BHSP_3:29
for X being RealUnitarySpace
for seq, seq1 being sequence of X st seq is Cauchy & seq1 is subsequence of seq holds
seq1 is Cauchy
proof
let X be RealUnitarySpace; ::_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, Def1;
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 Def1; ::_thesis: verum
end;

theorem :: BHSP_3:30
for X being RealUnitarySpace
for seq being sequence of X
for k, m being Element of NAT holds (seq ^\ k) ^\ m = (seq ^\ m) ^\ k
proof
let X be RealUnitarySpace; ::_thesis: for seq being sequence of X
for k, m being Element of NAT holds (seq ^\ k) ^\ m = (seq ^\ m) ^\ k
let seq be sequence of X; ::_thesis: for k, m being Element of NAT holds (seq ^\ k) ^\ m = (seq ^\ m) ^\ k
let k, m be Element of NAT ; ::_thesis: (seq ^\ k) ^\ m = (seq ^\ m) ^\ k
now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq_^\_k)_^\_m)_._n_=_((seq_^\_m)_^\_k)_._n
let n be Element of NAT ; ::_thesis: ((seq ^\ k) ^\ m) . n = ((seq ^\ m) ^\ k) . n
thus ((seq ^\ k) ^\ m) . n = (seq ^\ k) . (n + m) by NAT_1:def_3
.= seq . ((n + m) + k) by NAT_1:def_3
.= seq . ((n + k) + m)
.= (seq ^\ m) . (n + k) by NAT_1:def_3
.= ((seq ^\ m) ^\ k) . n by NAT_1:def_3 ; ::_thesis: verum
end;
hence  (seq ^\ k) ^\ m = (seq ^\ m) ^\ k by FUNCT_2:63; ::_thesis: verum
end;

theorem :: BHSP_3:31
for X being RealUnitarySpace
for seq being sequence of X
for k, m being Element of NAT holds (seq ^\ k) ^\ m = seq ^\ (k + m)
proof
let X be RealUnitarySpace; ::_thesis: for seq being sequence of X
for k, m being Element of NAT holds (seq ^\ k) ^\ m = seq ^\ (k + m)
let seq be sequence of X; ::_thesis: for k, m being Element of NAT holds (seq ^\ k) ^\ m = seq ^\ (k + m)
let k, m be Element of NAT ; ::_thesis: (seq ^\ k) ^\ m = seq ^\ (k + m)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq_^\_k)_^\_m)_._n_=_(seq_^\_(k_+_m))_._n
let n be Element of NAT ; ::_thesis: ((seq ^\ k) ^\ m) . n = (seq ^\ (k + m)) . n
thus ((seq ^\ k) ^\ m) . n = (seq ^\ k) . (n + m) by NAT_1:def_3
.= seq . ((n + m) + k) by NAT_1:def_3
.= seq . (n + (k + m))
.= (seq ^\ (k + m)) . n by NAT_1:def_3 ; ::_thesis: verum
end;
hence  (seq ^\ k) ^\ m = seq ^\ (k + m) by FUNCT_2:63; ::_thesis: verum
end;

theorem Th32: :: BHSP_3:32
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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 Th33: :: BHSP_3:33
for X being RealUnitarySpace
for seq being sequence of X
for k being Element of NAT holds (- seq) ^\ k = - (seq ^\ k)
proof
let X be RealUnitarySpace; ::_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 :: BHSP_3:34
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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 BHSP_1:49
.= (seq1 ^\ k) + ((- seq2) ^\ k) by Th32
.= (seq1 ^\ k) + (- (seq2 ^\ k)) by Th33
.= (seq1 ^\ k) - (seq2 ^\ k) by BHSP_1:49 ; ::_thesis: verum
end;

theorem :: BHSP_3:35
for X being RealUnitarySpace
for a being Real
for seq being sequence of X
for k being Element of NAT holds (a * seq) ^\ k = a * (seq ^\ k)
proof
let X be RealUnitarySpace; ::_thesis: for a being Real
for seq being sequence of X
for k being Element of NAT holds (a * seq) ^\ k = a * (seq ^\ k)
let a be Real; ::_thesis: for seq being sequence of X
for k being Element of NAT holds (a * seq) ^\ k = a * (seq ^\ k)
let seq be sequence of X; ::_thesis: for k being Element of NAT holds (a * seq) ^\ k = a * (seq ^\ k)
let k be Element of NAT ; ::_thesis: (a * seq) ^\ k = a * (seq ^\ k)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((a_*_seq)_^\_k)_._n_=_(a_*_(seq_^\_k))_._n
let n be Element of NAT ; ::_thesis: ((a * seq) ^\ k) . n = (a * (seq ^\ k)) . n
thus ((a * seq) ^\ k) . n = (a * seq) . (n + k) by NAT_1:def_3
.= a * (seq . (n + k)) by NORMSP_1:def_5
.= a * ((seq ^\ k) . n) by NAT_1:def_3
.= (a * (seq ^\ k)) . n by NORMSP_1:def_5 ; ::_thesis: verum
end;
hence  (a * seq) ^\ k = a * (seq ^\ k) by FUNCT_2:63; ::_thesis: verum
end;

theorem :: BHSP_3:36
for X being RealUnitarySpace
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 Th27, Th28;

theorem :: BHSP_3:37
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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, BHSP_2:9;
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 BHSP_2:9; ::_thesis: verum
end;

theorem :: BHSP_3:38
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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 BHSP_3:def_1 ::_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, Def1;
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 :: BHSP_3:39
for X being RealUnitarySpace
for seq being sequence of X
for k being Element of NAT st seq is Cauchy holds
seq ^\ k is Cauchy by Th29;

theorem :: BHSP_3:40
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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 BHSP_3:def_2 ::_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, Def2;
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 :: BHSP_3:41
for X being RealUnitarySpace
for seq being sequence of X
for k being Element of NAT st seq is bounded holds
seq ^\ k is bounded by Th26;

theorem :: BHSP_3:42
for X being RealUnitarySpace
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 RealUnitarySpace;
attrX is complete  means :Def4: :: BHSP_3:def 4
 for seq being sequence of X st seq is Cauchy holds
seq is convergent ;
end;

:: deftheorem Def4 defines complete BHSP_3:def_4_:_
 for X being RealUnitarySpace holds
( X is complete iff for seq being sequence of X st seq is Cauchy holds
seq is convergent );

theorem :: BHSP_3:43
for X being RealUnitarySpace
for seq being sequence of X st X is complete & seq is Cauchy holds
seq is bounded
proof
let X be RealUnitarySpace; ::_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 Def4;
hence  seq is bounded by Th24; ::_thesis: verum
end;