:: 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;