:: BHSP_2 semantic presentation

begin

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

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

theorem Th2: :: BHSP_2:2
for X being RealUnitarySpace
for seq, seq9 being sequence of X st seq is convergent & ex k being Element of NAT st
for n being Element of NAT st k <= n holds
seq9 . n = seq . n holds
seq9 is convergent
proof
let X be RealUnitarySpace; ::_thesis: for seq, seq9 being sequence of X st seq is convergent & ex k being Element of NAT st
for n being Element of NAT st k <= n holds
seq9 . n = seq . n holds
seq9 is convergent
let seq, seq9 be sequence of X; ::_thesis: ( seq is convergent & ex k being Element of NAT st
for n being Element of NAT st k <= n holds
seq9 . n = seq . n implies seq9 is convergent )
assume that
A1: seq is convergent and
A2: ex k being Element of NAT st
for n being Element of NAT st k <= n holds
seq9 . n = seq . n ; ::_thesis: seq9 is convergent
consider k being Element of NAT  such that
A3: for n being Element of NAT st n >= k holds
seq9 . n = seq . 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 ((seq . n),g) < r by A1, Def1;
take h = g; :: according to BHSP_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 ((seq9 . 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 ((seq9 . 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 ((seq9 . n),h) < r
then consider m1 being Element of NAT  such that
A5: for n being Element of NAT st n >= m1 holds
dist ((seq . 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_((seq9_._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 ((seq9 . n),h) < r
take m = k; ::_thesis: for n being Element of NAT st n >= m holds
dist ((seq9 . n),h) < r
let n be Element of NAT ; ::_thesis: ( n >= m implies dist ((seq9 . n),h) < r )
assume A8: n >= m ; ::_thesis: dist ((seq9 . n),h) < r
then  n >= m1 by A7, XXREAL_0:2;
then  dist ((seq . n),g) < r by A5;
hence  dist ((seq9 . 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_((seq9_._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 ((seq9 . n),h) < r
take m = m1; ::_thesis: for n being Element of NAT st n >= m holds
dist ((seq9 . n),h) < r
let n be Element of NAT ; ::_thesis: ( n >= m implies dist ((seq9 . n),h) < r )
assume A10: n >= m ; ::_thesis: dist ((seq9 . n),h) < r
then  seq9 . n = seq . n by A3, A9, XXREAL_0:2;
hence  dist ((seq9 . 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 ((seq9 . n),h) < r by A6; ::_thesis: verum
end;

theorem Th3: :: BHSP_2:3
for X being RealUnitarySpace
for seq1, seq2 being sequence of X st seq1 is convergent & seq2 is convergent holds
seq1 + seq2 is convergent
proof
let X be RealUnitarySpace; ::_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 BHSP_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 BHSP_1:40;
 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: :: BHSP_2:4
for X being RealUnitarySpace
for seq1, seq2 being sequence of X st seq1 is convergent & seq2 is convergent holds
seq1 - seq2 is convergent
proof
let X be RealUnitarySpace; ::_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 BHSP_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 BHSP_1:41;
 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: :: BHSP_2:5
for X being RealUnitarySpace
for a being Real
for seq being sequence of X st seq is convergent holds
a * seq is convergent
proof
let X be RealUnitarySpace; ::_thesis: for a being Real
for seq being sequence of X st seq is convergent holds
a * seq is convergent
let a be Real; ::_thesis: for seq being sequence of X st seq is convergent holds
a * seq is convergent
let seq be sequence of X; ::_thesis: ( seq is convergent implies a * seq is convergent )
assume  seq is convergent ; ::_thesis: a * 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 = a * g; :: according to BHSP_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 (((a * seq) . n),h) < r
A2: now__::_thesis:_(_a_<>_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_(((a_*_seq)_._n),h)_<_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 being Element of NAT st n >= k holds
dist (((a * seq) . n),h) < 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 being Element of NAT st n >= k holds
dist (((a * 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 (((a * 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 / (abs a) by A1, A5, A3, XREAL_1:74;
take k = m1; ::_thesis: for n being Element of NAT st n >= k holds
dist (((a * seq) . n),h) < r
let n be Element of NAT ; ::_thesis: ( n >= k implies dist (((a * seq) . n),h) < r )
assume  n >= k ; ::_thesis: dist (((a * seq) . n),h) < r
then A7: dist ((seq . n),g) < 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 * g)) = ||.((a * (seq . n)) - (a * g)).|| by BHSP_1:def_5
.= ||.(a * ((seq . n) - g)).|| by RLVECT_1:34
.= (abs a) * ||.((seq . n) - g).|| by BHSP_1:27
.= (abs a) * (dist ((seq . n),g)) by BHSP_1:def_5 ;
then  dist ((a * (seq . n)),h) < r by A5, A7, A9, XREAL_1:68;
hence  dist (((a * seq) . n),h) < 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_being_Element_of_NAT_st_n_>=_k_holds_
dist_(((a_*_seq)_._n),h)_<_r_)
assume A10: a = 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 (((a * 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 (((a * 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 (((a * 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 (((a * seq) . n),h) < r
let n be Element of NAT ; ::_thesis: ( n >= k implies dist (((a * seq) . n),h) < r )
assume  n >= k ; ::_thesis: dist (((a * seq) . n),h) < r
then A12: dist ((seq . n),g) < r by A11;
dist ((a * (seq . n)),(a * g)) = dist ((0 * (seq . n)),H1(X)) by A10, RLVECT_1:10
.= dist (H1(X),H1(X)) by RLVECT_1:10
.= 0 by BHSP_1:34 ;
then  dist ((a * (seq . n)),h) < r by A12, BHSP_1:37;
hence  dist (((a * seq) . n),h) < r by NORMSP_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
dist (((a * seq) . n),h) < r by A2; ::_thesis: verum
end;

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

theorem Th7: :: BHSP_2:7
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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 BHSP_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 BHSP_1:40;
then A3: dist (((seq . n) + x),(g + x)) <= (dist ((seq . n),g)) + 0 by BHSP_1:34;
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: :: BHSP_2:8
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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 BHSP_1:56; ::_thesis: verum
end;

theorem Th9: :: BHSP_2:9
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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 BHSP_1:def_5; ::_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 BHSP_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 BHSP_1:def_5; ::_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 RealUnitarySpace;
let seq be sequence of X;
assume A1: seq is convergent ;
func lim seq ->  Point of X means :Def2: :: BHSP_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, BHSP_1:38;
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 BHSP_1:42;
then A11: dist (x,y) <= (dist ((seq . m1),x)) + (dist ((seq . m1),y)) by BHSP_1:43;
 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 BHSP_1:42;
then A13: dist (x,y) <= (dist ((seq . m2),x)) + (dist ((seq . m2),y)) by BHSP_1:43;
 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 BHSP_2:def_2_:_
 for X being RealUnitarySpace
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: :: BHSP_2:10
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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 z being Point of X such that
A4: for n being Nat holds seq . n = z 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  z in rng seq by A4;
then  z = x by A3, A5, TARSKI:def_1;
then  seq . n = x by A4;
hence  dist ((seq . n),x) < r by A7, BHSP_1:34; ::_thesis: verum
end;
 seq is convergent by A1, Th1;
hence  lim seq = x by A6, Def2; ::_thesis: verum
end;

theorem :: BHSP_2:11
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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 :: BHSP_2:12
for X being RealUnitarySpace
for seq, seq9 being sequence of X st seq is convergent & ex k being Element of NAT st
for n being Element of NAT st n >= k holds
seq9 . n = seq . n holds
lim seq = lim seq9
proof
let X be RealUnitarySpace; ::_thesis: for seq, seq9 being sequence of X st seq is convergent & ex k being Element of NAT st
for n being Element of NAT st n >= k holds
seq9 . n = seq . n holds
lim seq = lim seq9
let seq, seq9 be sequence of X; ::_thesis: ( seq is convergent & ex k being Element of NAT st
for n being Element of NAT st n >= k holds
seq9 . n = seq . n implies lim seq = lim seq9 )
assume that
A1: seq is convergent and
A2: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
seq9 . n = seq . n ; ::_thesis: lim seq = lim seq9
consider k being Element of NAT  such that
A3: for n being Element of NAT st n >= k holds
seq9 . n = seq . 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_((seq9_._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 ((seq9 . 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 ((seq9 . 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 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_((seq9_._n),(lim_seq))_<_r_)
assume A7: m1 <= k ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq9 . n),(lim seq)) < r
take m = k; ::_thesis: for n being Element of NAT st n >= m holds
dist ((seq9 . n),(lim seq)) < r
let n be Element of NAT ; ::_thesis: ( n >= m implies dist ((seq9 . n),(lim seq)) < r )
assume A8: n >= m ; ::_thesis: dist ((seq9 . n),(lim seq)) < r
then  n >= m1 by A7, XXREAL_0:2;
then  dist ((seq . n),(lim seq)) < r by A5;
hence  dist ((seq9 . n),(lim seq)) < 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_((seq9_._n),(lim_seq))_<_r_)
assume A9: k <= m1 ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq9 . n),(lim seq)) < r
take m = m1; ::_thesis: for n being Element of NAT st n >= m holds
dist ((seq9 . n),(lim seq)) < r
let n be Element of NAT ; ::_thesis: ( n >= m implies dist ((seq9 . n),(lim seq)) < r )
assume A10: n >= m ; ::_thesis: dist ((seq9 . n),(lim seq)) < r
then  seq9 . n = seq . n by A3, A9, XXREAL_0:2;
hence  dist ((seq9 . n),(lim seq)) < 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 ((seq9 . n),(lim seq)) < r by A6; ::_thesis: verum
end;
 seq9 is convergent by A1, A2, Th2;
hence  lim seq = lim seq9 by A4, Def2; ::_thesis: verum
end;

theorem Th13: :: BHSP_2:13
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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 BHSP_1:40;
 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: :: BHSP_2:14
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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 BHSP_1:41;
 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: :: BHSP_2:15
for X being RealUnitarySpace
for a being Real
for seq being sequence of X st seq is convergent holds
lim (a * seq) = a * (lim seq)
proof
let X be RealUnitarySpace; ::_thesis: for a being Real
for seq being sequence of X st seq is convergent holds
lim (a * seq) = a * (lim seq)
let a be Real; ::_thesis: for seq being sequence of X st seq is convergent holds
lim (a * seq) = a * (lim seq)
let seq be sequence of X; ::_thesis: ( seq is convergent implies lim (a * seq) = a * (lim seq) )
set g = lim seq;
set h = a * (lim seq);
assume A1: seq is convergent ; ::_thesis: lim (a * seq) = a * (lim seq)
A2: now__::_thesis:_(_a_=_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_(((a_*_seq)_._n),(a_*_(lim_seq)))_<_r_)
assume A3: a = 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 (((a * seq) . n),(a * (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 (((a * seq) . n),(a * (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 (((a * seq) . n),(a * (lim seq))) < r
then consider m1 being Element of NAT  such that
A4: 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 (((a * seq) . n),(a * (lim seq))) < r
let n be Element of NAT ; ::_thesis: ( n >= k implies dist (((a * seq) . n),(a * (lim seq))) < r )
assume  n >= k ; ::_thesis: dist (((a * seq) . n),(a * (lim seq))) < r
then A5: dist ((seq . n),(lim seq)) < r by A4;
dist ((a * (seq . n)),(a * (lim seq))) = dist ((0 * (seq . n)),H1(X)) by A3, RLVECT_1:10
.= dist (H1(X),H1(X)) by RLVECT_1:10
.= 0 by BHSP_1:34 ;
then  dist ((a * (seq . n)),(a * (lim seq))) < r by A5, BHSP_1:37;
hence  dist (((a * seq) . n),(a * (lim seq))) < r by NORMSP_1:def_5; ::_thesis: verum
end;
A6: now__::_thesis:_(_a_<>_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_(((a_*_seq)_._n),(a_*_(lim_seq)))_<_r_)
A7: 0 / (abs a) = 0 ;
assume A8: a <> 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 (((a * seq) . n),(a * (lim seq))) < r
then A9: abs a > 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 (((a * seq) . n),(a * (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 (((a * seq) . n),(a * (lim seq))) < r
then  r / (abs a) > 0 by A9, A7, XREAL_1:74;
then consider m1 being Element of NAT  such that
A10: for n being Element of NAT st n >= m1 holds
dist ((seq . n),(lim seq)) < r / (abs a) by A1, Def2;
take k = m1; ::_thesis: for n being Element of NAT st n >= k holds
dist (((a * seq) . n),(a * (lim seq))) < r
let n be Element of NAT ; ::_thesis: ( n >= k implies dist (((a * seq) . n),(a * (lim seq))) < r )
assume  n >= k ; ::_thesis: dist (((a * seq) . n),(a * (lim seq))) < r
then A11: dist ((seq . n),(lim seq)) < r / (abs a) by A10;
A12: abs a <> 0 by A8, COMPLEX1:47;
A13: (abs a) * (r / (abs a)) = (abs a) * (((abs a) ") * r) by XCMPLX_0:def_9
.= ((abs a) * ((abs a) ")) * r
.= 1 * r by A12, XCMPLX_0:def_7
.= r ;
dist ((a * (seq . n)),(a * (lim seq))) = ||.((a * (seq . n)) - (a * (lim seq))).|| by BHSP_1:def_5
.= ||.(a * ((seq . n) - (lim seq))).|| by RLVECT_1:34
.= (abs a) * ||.((seq . n) - (lim seq)).|| by BHSP_1:27
.= (abs a) * (dist ((seq . n),(lim seq))) by BHSP_1:def_5 ;
then  dist ((a * (seq . n)),(a * (lim seq))) < r by A9, A11, A13, XREAL_1:68;
hence  dist (((a * seq) . n),(a * (lim seq))) < r by NORMSP_1:def_5; ::_thesis: verum
end;
 a * seq is convergent by A1, Th5;
hence  lim (a * seq) = a * (lim seq) by A2, A6, Def2; ::_thesis: verum
end;

theorem Th16: :: BHSP_2:16
for X being RealUnitarySpace
for seq being sequence of X st seq is convergent holds
lim (- seq) = - (lim seq)
proof
let X be RealUnitarySpace; ::_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 ((- 1) * seq) = (- 1) * (lim seq) by Th15;
then  lim (- seq) = (- 1) * (lim seq) by BHSP_1:55;
hence  lim (- seq) = - (lim seq) by RLVECT_1:16; ::_thesis: verum
end;

theorem Th17: :: BHSP_2:17
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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 BHSP_1:42
.= 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 :: BHSP_2:18
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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 BHSP_1:56;
hence  lim (seq - x) = (lim seq) - x by RLVECT_1:def_11; ::_thesis: verum
end;

theorem Th19: :: BHSP_2:19
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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 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
||.((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 BHSP_1:def_5; ::_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 RealUnitarySpace;
let seq be sequence of X;
func||.seq.|| ->  Real_Sequence means :Def3: :: BHSP_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 ||. BHSP_2:def_3_:_
 for X being RealUnitarySpace
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: :: BHSP_2:20
for X being RealUnitarySpace
for seq being sequence of X st seq is convergent holds
||.seq.|| is convergent
proof
let X be RealUnitarySpace; ::_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 BHSP_1:33;
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: :: BHSP_2:21
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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 BHSP_1:33;
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: :: BHSP_2:22
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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 BHSP_1:33;
then  abs (||.((seq . n) - g).|| - ||.H1(X).||) < r by A6, XXREAL_0:2;
then  abs (||.((seq . n) - g).|| - 0) < r by BHSP_1:26;
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 RealUnitarySpace;
let seq be sequence of X;
let x be Point of X;
func dist (seq,x) ->  Real_Sequence means :Def4: :: BHSP_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 BHSP_2:def_4_:_
 for X being RealUnitarySpace
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: :: BHSP_2:23
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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 BHSP_1:37;
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: :: BHSP_2:24
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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 BHSP_1:37;
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 :: BHSP_2:25
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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 :: BHSP_2:26
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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 :: BHSP_2:27
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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 :: BHSP_2:28
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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 :: BHSP_2:29
for X being RealUnitarySpace
for g being Point of X
for a being Real
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.(a * seq).|| is convergent & lim ||.(a * seq).|| = ||.(a * g).|| )
proof
let X be RealUnitarySpace; ::_thesis: for g being Point of X
for a being Real
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.(a * seq).|| is convergent & lim ||.(a * seq).|| = ||.(a * g).|| )
let g be Point of X; ::_thesis: for a being Real
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.(a * seq).|| is convergent & lim ||.(a * seq).|| = ||.(a * g).|| )
let a be Real; ::_thesis: for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.(a * seq).|| is convergent & lim ||.(a * seq).|| = ||.(a * g).|| )
let seq be sequence of X; ::_thesis: ( seq is convergent & lim seq = g implies ( ||.(a * seq).|| is convergent & lim ||.(a * seq).|| = ||.(a * g).|| ) )
assume  ( seq is convergent & lim seq = g ) ; ::_thesis: ( ||.(a * seq).|| is convergent & lim ||.(a * seq).|| = ||.(a * g).|| )
then  ( a * seq is convergent & lim (a * seq) = a * g ) by Th5, Th15;
hence  ( ||.(a * seq).|| is convergent & lim ||.(a * seq).|| = ||.(a * g).|| ) by Th21; ::_thesis: verum
end;

theorem :: BHSP_2:30
for X being RealUnitarySpace
for g being Point of X
for a being Real
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.((a * seq) - (a * g)).|| is convergent & lim ||.((a * seq) - (a * g)).|| = 0 )
proof
let X be RealUnitarySpace; ::_thesis: for g being Point of X
for a being Real
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.((a * seq) - (a * g)).|| is convergent & lim ||.((a * seq) - (a * g)).|| = 0 )
let g be Point of X; ::_thesis: for a being Real
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.((a * seq) - (a * g)).|| is convergent & lim ||.((a * seq) - (a * g)).|| = 0 )
let a be Real; ::_thesis: for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.((a * seq) - (a * g)).|| is convergent & lim ||.((a * seq) - (a * g)).|| = 0 )
let seq be sequence of X; ::_thesis: ( seq is convergent & lim seq = g implies ( ||.((a * seq) - (a * g)).|| is convergent & lim ||.((a * seq) - (a * g)).|| = 0 ) )
assume  ( seq is convergent & lim seq = g ) ; ::_thesis: ( ||.((a * seq) - (a * g)).|| is convergent & lim ||.((a * seq) - (a * g)).|| = 0 )
then  ( a * seq is convergent & lim (a * seq) = a * g ) by Th5, Th15;
hence  ( ||.((a * seq) - (a * g)).|| is convergent & lim ||.((a * seq) - (a * g)).|| = 0 ) by Th22; ::_thesis: verum
end;

theorem :: BHSP_2:31
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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 :: BHSP_2:32
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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 RealUnitarySpace
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 RealUnitarySpace; ::_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: :: BHSP_2:33
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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 :: BHSP_2:34
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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 BHSP_1:56;
 ||.(seq + (- x)).|| is convergent by A1, Lm1;
hence  ( ||.(seq - x).|| is convergent & lim ||.(seq - x).|| = ||.(g - x).|| ) by A2, BHSP_1:56, RLVECT_1:def_11; ::_thesis: verum
end;

theorem :: BHSP_2:35
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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 BHSP_1:56;
 ||.((seq + (- x)) - (g + (- x))).|| is convergent by A1, Th33;
then  ||.((seq - x) - (g + (- x))).|| is convergent by BHSP_1:56;
hence  ( ||.((seq - x) - (g - x)).|| is convergent & lim ||.((seq - x) - (g - x)).|| = 0 ) by A2, RLVECT_1:def_11; ::_thesis: verum
end;

theorem :: BHSP_2:36
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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 :: BHSP_2:37
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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 :: BHSP_2:38
for X being RealUnitarySpace
for g being Point of X
for a being Real
for seq being sequence of X st seq is convergent & lim seq = g holds
( dist ((a * seq),(a * g)) is convergent & lim (dist ((a * seq),(a * g))) = 0 )
proof
let X be RealUnitarySpace; ::_thesis: for g being Point of X
for a being Real
for seq being sequence of X st seq is convergent & lim seq = g holds
( dist ((a * seq),(a * g)) is convergent & lim (dist ((a * seq),(a * g))) = 0 )
let g be Point of X; ::_thesis: for a being Real
for seq being sequence of X st seq is convergent & lim seq = g holds
( dist ((a * seq),(a * g)) is convergent & lim (dist ((a * seq),(a * g))) = 0 )
let a be Real; ::_thesis: for seq being sequence of X st seq is convergent & lim seq = g holds
( dist ((a * seq),(a * g)) is convergent & lim (dist ((a * seq),(a * g))) = 0 )
let seq be sequence of X; ::_thesis: ( seq is convergent & lim seq = g implies ( dist ((a * seq),(a * g)) is convergent & lim (dist ((a * seq),(a * g))) = 0 ) )
assume  ( seq is convergent & lim seq = g ) ; ::_thesis: ( dist ((a * seq),(a * g)) is convergent & lim (dist ((a * seq),(a * g))) = 0 )
then  ( a * seq is convergent & lim (a * seq) = a * g ) by Th5, Th15;
hence  ( dist ((a * seq),(a * g)) is convergent & lim (dist ((a * seq),(a * g))) = 0 ) by Th24; ::_thesis: verum
end;

theorem :: BHSP_2:39
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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 RealUnitarySpace;
let x be Point of X;
let r be Real;
func Ball (x,r) ->  Subset of X equals :: BHSP_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 :: BHSP_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 :: BHSP_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 BHSP_2:def_5_:_
 for X being RealUnitarySpace
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 BHSP_2:def_6_:_
 for X being RealUnitarySpace
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 BHSP_2:def_7_:_
 for X being RealUnitarySpace
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: :: BHSP_2:40
for X being RealUnitarySpace
for z, x being Point of X
for r being Real holds
( z in Ball (x,r) iff ||.(x - z).|| < r )
proof
let X be RealUnitarySpace; ::_thesis: for z, x being Point of X
for r being Real holds
( z in Ball (x,r) iff ||.(x - z).|| < r )
let z, x be Point of X; ::_thesis: for r being Real holds
( z in Ball (x,r) iff ||.(x - z).|| < r )
let r be Real; ::_thesis: ( z in Ball (x,r) iff ||.(x - z).|| < r )
thus  ( z in Ball (x,r) implies ||.(x - z).|| < r ) ::_thesis: ( ||.(x - z).|| < r implies z in Ball (x,r) )
proof
assume  z in Ball (x,r) ; ::_thesis: ||.(x - z).|| < r
then  ex y being Point of X st
( z = y & ||.(x - y).|| < r ) ;
hence  ||.(x - z).|| < r ; ::_thesis: verum
end;
thus  ( ||.(x - z).|| < r implies z in Ball (x,r) ) ; ::_thesis: verum
end;

theorem Th41: :: BHSP_2:41
for X being RealUnitarySpace
for z, x being Point of X
for r being Real holds
( z in Ball (x,r) iff dist (x,z) < r )
proof
let X be RealUnitarySpace; ::_thesis: for z, x being Point of X
for r being Real holds
( z in Ball (x,r) iff dist (x,z) < r )
let z, x be Point of X; ::_thesis: for r being Real holds
( z in Ball (x,r) iff dist (x,z) < r )
let r be Real; ::_thesis: ( z in Ball (x,r) iff dist (x,z) < r )
thus  ( z in Ball (x,r) implies dist (x,z) < r ) ::_thesis: ( dist (x,z) < r implies z in Ball (x,r) )
proof
assume  z in Ball (x,r) ; ::_thesis: dist (x,z) < r
then  ||.(x - z).|| < r by Th40;
hence  dist (x,z) < r by BHSP_1:def_5; ::_thesis: verum
end;
assume  dist (x,z) < r ; ::_thesis: z in Ball (x,r)
then  ||.(x - z).|| < r by BHSP_1:def_5;
hence  z in Ball (x,r) ; ::_thesis: verum
end;

theorem :: BHSP_2:42
for X being RealUnitarySpace
for x being Point of X
for r being Real st r > 0 holds
x in Ball (x,r)
proof
let X be RealUnitarySpace; ::_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 BHSP_1:34;
assume  r > 0 ; ::_thesis: x in Ball (x,r)
hence  x in Ball (x,r) by A1, Th41; ::_thesis: verum
end;

theorem :: BHSP_2:43
for X being RealUnitarySpace
for y, x, z being Point of X
for r being Real st y in Ball (x,r) & z in Ball (x,r) holds
dist (y,z) < 2 * r
proof
let X be RealUnitarySpace; ::_thesis: for y, x, z being Point of X
for r being Real st y in Ball (x,r) & z in Ball (x,r) holds
dist (y,z) < 2 * r
let y, x, z be Point of X; ::_thesis: for r being Real st y in Ball (x,r) & z in Ball (x,r) holds
dist (y,z) < 2 * r
let r be Real; ::_thesis: ( y in Ball (x,r) & z in Ball (x,r) implies dist (y,z) < 2 * r )
assume that
A1: y in Ball (x,r) and
A2: z in Ball (x,r) ; ::_thesis: dist (y,z) < 2 * r
 dist (x,z) < r by A2, Th41;
then A3: r + (dist (x,z)) < r + r by XREAL_1:6;
A4: dist (y,z) <= (dist (y,x)) + (dist (x,z)) by BHSP_1:35;
 dist (x,y) < r by A1, Th41;
then  (dist (x,y)) + (dist (x,z)) < r + (dist (x,z)) by XREAL_1:6;
then  (dist (x,y)) + (dist (x,z)) < 2 * r by A3, XXREAL_0:2;
hence  dist (y,z) < 2 * r by A4, XXREAL_0:2; ::_thesis: verum
end;

theorem :: BHSP_2:44
for X being RealUnitarySpace
for y, x, z being Point of X
for r being Real st y in Ball (x,r) holds
y - z in Ball ((x - z),r)
proof
let X be RealUnitarySpace; ::_thesis: for y, x, z being Point of X
for r being Real st y in Ball (x,r) holds
y - z in Ball ((x - z),r)
let y, x, z be Point of X; ::_thesis: for r being Real st y in Ball (x,r) holds
y - z in Ball ((x - z),r)
let r be Real; ::_thesis: ( y in Ball (x,r) implies y - z in Ball ((x - z),r) )
assume  y in Ball (x,r) ; ::_thesis: y - z in Ball ((x - z),r)
then A1: dist (x,y) < r by Th41;
 dist ((x - z),(y - z)) = dist (x,y) by BHSP_1:42;
hence  y - z in Ball ((x - z),r) by A1, Th41; ::_thesis: verum
end;

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

theorem Th48: :: BHSP_2:48
for X being RealUnitarySpace
for z, x being Point of X
for r being Real holds
( z in cl_Ball (x,r) iff dist (x,z) <= r )
proof
let X be RealUnitarySpace; ::_thesis: for z, x being Point of X
for r being Real holds
( z in cl_Ball (x,r) iff dist (x,z) <= r )
let z, x be Point of X; ::_thesis: for r being Real holds
( z in cl_Ball (x,r) iff dist (x,z) <= r )
let r be Real; ::_thesis: ( z in cl_Ball (x,r) iff dist (x,z) <= r )
thus  ( z in cl_Ball (x,r) implies dist (x,z) <= r ) ::_thesis: ( dist (x,z) <= r implies z in cl_Ball (x,r) )
proof
assume  z in cl_Ball (x,r) ; ::_thesis: dist (x,z) <= r
then  ||.(x - z).|| <= r by Th47;
hence  dist (x,z) <= r by BHSP_1:def_5; ::_thesis: verum
end;
assume  dist (x,z) <= r ; ::_thesis: z in cl_Ball (x,r)
then  ||.(x - z).|| <= r by BHSP_1:def_5;
hence  z in cl_Ball (x,r) ; ::_thesis: verum
end;

theorem :: BHSP_2:49
for X being RealUnitarySpace
for x being Point of X
for r being Real st r >= 0 holds
x in cl_Ball (x,r)
proof
let X be RealUnitarySpace; ::_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 BHSP_1:34;
hence  x in cl_Ball (x,r) by Th48; ::_thesis: verum
end;

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

theorem :: BHSP_2:52
for X being RealUnitarySpace
for z, x being Point of X
for r being Real holds
( z in Sphere (x,r) iff dist (x,z) = r )
proof
let X be RealUnitarySpace; ::_thesis: for z, x being Point of X
for r being Real holds
( z in Sphere (x,r) iff dist (x,z) = r )
let z, x be Point of X; ::_thesis: for r being Real holds
( z in Sphere (x,r) iff dist (x,z) = r )
let r be Real; ::_thesis: ( z in Sphere (x,r) iff dist (x,z) = r )
thus  ( z in Sphere (x,r) implies dist (x,z) = r ) ::_thesis: ( dist (x,z) = r implies z in Sphere (x,r) )
proof
assume  z in Sphere (x,r) ; ::_thesis: dist (x,z) = r
then  ||.(x - z).|| = r by Th51;
hence  dist (x,z) = r by BHSP_1:def_5; ::_thesis: verum
end;
assume  dist (x,z) = r ; ::_thesis: z in Sphere (x,r)
then  ||.(x - z).|| = r by BHSP_1:def_5;
hence  z in Sphere (x,r) ; ::_thesis: verum
end;

theorem :: BHSP_2:53
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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: :: BHSP_2:54
for X being RealUnitarySpace
for x being Point of X
for r being Real holds Ball (x,r) c= cl_Ball (x,r)
proof
let X be RealUnitarySpace; ::_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: :: BHSP_2:55
for X being RealUnitarySpace
for x being Point of X
for r being Real holds Sphere (x,r) c= cl_Ball (x,r)
proof
let X be RealUnitarySpace; ::_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 :: BHSP_2:56
for X being RealUnitarySpace
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 RealUnitarySpace; ::_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;