let n be Nat; :: thesis: for seq1 being sequence of (REAL-NS n)

for seq2 being sequence of (REAL-US n) st seq1 = seq2 holds

( ( seq1 is convergent implies ( seq2 is convergent & lim seq1 = lim seq2 ) ) & ( seq2 is convergent implies ( seq1 is convergent & lim seq1 = lim seq2 ) ) )

let seq1 be sequence of (REAL-NS n); :: thesis: for seq2 being sequence of (REAL-US n) st seq1 = seq2 holds

( ( seq1 is convergent implies ( seq2 is convergent & lim seq1 = lim seq2 ) ) & ( seq2 is convergent implies ( seq1 is convergent & lim seq1 = lim seq2 ) ) )

let seq2 be sequence of (REAL-US n); :: thesis: ( seq1 = seq2 implies ( ( seq1 is convergent implies ( seq2 is convergent & lim seq1 = lim seq2 ) ) & ( seq2 is convergent implies ( seq1 is convergent & lim seq1 = lim seq2 ) ) ) )

assume A1: seq1 = seq2 ; :: thesis: ( ( seq1 is convergent implies ( seq2 is convergent & lim seq1 = lim seq2 ) ) & ( seq2 is convergent implies ( seq1 is convergent & lim seq1 = lim seq2 ) ) )

A2: the carrier of (REAL-NS n) = REAL n by Def4

.= the carrier of (REAL-US n) by Def6 ;

for seq2 being sequence of (REAL-US n) st seq1 = seq2 holds

( ( seq1 is convergent implies ( seq2 is convergent & lim seq1 = lim seq2 ) ) & ( seq2 is convergent implies ( seq1 is convergent & lim seq1 = lim seq2 ) ) )

let seq1 be sequence of (REAL-NS n); :: thesis: for seq2 being sequence of (REAL-US n) st seq1 = seq2 holds

( ( seq1 is convergent implies ( seq2 is convergent & lim seq1 = lim seq2 ) ) & ( seq2 is convergent implies ( seq1 is convergent & lim seq1 = lim seq2 ) ) )

let seq2 be sequence of (REAL-US n); :: thesis: ( seq1 = seq2 implies ( ( seq1 is convergent implies ( seq2 is convergent & lim seq1 = lim seq2 ) ) & ( seq2 is convergent implies ( seq1 is convergent & lim seq1 = lim seq2 ) ) ) )

assume A1: seq1 = seq2 ; :: thesis: ( ( seq1 is convergent implies ( seq2 is convergent & lim seq1 = lim seq2 ) ) & ( seq2 is convergent implies ( seq1 is convergent & lim seq1 = lim seq2 ) ) )

A2: the carrier of (REAL-NS n) = REAL n by Def4

.= the carrier of (REAL-US n) by Def6 ;

now :: thesis: ( seq1 is convergent implies ( seq2 is convergent & lim seq2 = lim seq1 ) )

hence
( seq1 is convergent implies ( seq2 is convergent & lim seq1 = lim seq2 ) )
; :: thesis: ( seq2 is convergent implies ( seq1 is convergent & lim seq1 = lim seq2 ) )reconsider LIMIT = lim seq1 as Point of (REAL-US n) by A2;

assume A3: seq1 is convergent ; :: thesis: ( seq2 is convergent & lim seq2 = lim seq1 )

then consider RNg being Point of (REAL-NS n) such that

A4: for r being Real st 0 < r holds

ex m being Nat st

for k being Nat st m <= k holds

||.((seq1 . k) - RNg).|| < r by NORMSP_1:def 6;

reconsider RUg = RNg as Point of (REAL-US n) by A2;

for r being Real st 0 < r holds

ex m being Nat st

for k being Nat st m <= k holds

dist ((seq2 . k),RUg) < r

for r being Real st r > 0 holds

ex m being Nat st

for k being Nat st k >= m holds

dist ((seq2 . k),LIMIT) < r

end;assume A3: seq1 is convergent ; :: thesis: ( seq2 is convergent & lim seq2 = lim seq1 )

then consider RNg being Point of (REAL-NS n) such that

A4: for r being Real st 0 < r holds

ex m being Nat st

for k being Nat st m <= k holds

||.((seq1 . k) - RNg).|| < r by NORMSP_1:def 6;

reconsider RUg = RNg as Point of (REAL-US n) by A2;

for r being Real st 0 < r holds

ex m being Nat st

for k being Nat st m <= k holds

dist ((seq2 . k),RUg) < r

proof

hence A8:
seq2 is convergent
by BHSP_2:def 1; :: thesis: lim seq2 = lim seq1
let r be Real; :: thesis: ( 0 < r implies ex m being Nat st

for k being Nat st m <= k holds

dist ((seq2 . k),RUg) < r )

assume 0 < r ; :: thesis: ex m being Nat st

for k being Nat st m <= k holds

dist ((seq2 . k),RUg) < r

then consider m being Nat such that

A5: for k being Nat st m <= k holds

||.((seq1 . k) - RNg).|| < r by A4;

take m ; :: thesis: for k being Nat st m <= k holds

dist ((seq2 . k),RUg) < r

let k be Nat; :: thesis: ( m <= k implies dist ((seq2 . k),RUg) < r )

reconsider p = (seq1 . k) - RNg as Element of REAL n by Def4;

assume A6: m <= k ; :: thesis: dist ((seq2 . k),RUg) < r

- RNg = - RUg by Th13;

then A7: p = (seq2 . k) - RUg by A1, Th13;

||.((seq1 . k) - RNg).|| = |.p.| by Th1

.= sqrt |(p,p)| by EUCLID_2:5

.= sqrt (Sum (mlt (p,p))) by RVSUM_1:def 16

.= sqrt ((Euclid_scalar n) . (p,p)) by Def5

.= ||.((seq2 . k) - RUg).|| by A7, Def6 ;

hence dist ((seq2 . k),RUg) < r by A5, A6; :: thesis: verum

end;for k being Nat st m <= k holds

dist ((seq2 . k),RUg) < r )

assume 0 < r ; :: thesis: ex m being Nat st

for k being Nat st m <= k holds

dist ((seq2 . k),RUg) < r

then consider m being Nat such that

A5: for k being Nat st m <= k holds

||.((seq1 . k) - RNg).|| < r by A4;

take m ; :: thesis: for k being Nat st m <= k holds

dist ((seq2 . k),RUg) < r

let k be Nat; :: thesis: ( m <= k implies dist ((seq2 . k),RUg) < r )

reconsider p = (seq1 . k) - RNg as Element of REAL n by Def4;

assume A6: m <= k ; :: thesis: dist ((seq2 . k),RUg) < r

- RNg = - RUg by Th13;

then A7: p = (seq2 . k) - RUg by A1, Th13;

||.((seq1 . k) - RNg).|| = |.p.| by Th1

.= sqrt |(p,p)| by EUCLID_2:5

.= sqrt (Sum (mlt (p,p))) by RVSUM_1:def 16

.= sqrt ((Euclid_scalar n) . (p,p)) by Def5

.= ||.((seq2 . k) - RUg).|| by A7, Def6 ;

hence dist ((seq2 . k),RUg) < r by A5, A6; :: thesis: verum

for r being Real st r > 0 holds

ex m being Nat st

for k being Nat st k >= m holds

dist ((seq2 . k),LIMIT) < r

proof

hence
lim seq2 = lim seq1
by A8, BHSP_2:def 2; :: thesis: verum
let r be Real; :: thesis: ( r > 0 implies ex m being Nat st

for k being Nat st k >= m holds

dist ((seq2 . k),LIMIT) < r )

assume r > 0 ; :: thesis: ex m being Nat st

for k being Nat st k >= m holds

dist ((seq2 . k),LIMIT) < r

then consider m being Nat such that

A9: for k being Nat st m <= k holds

||.((seq1 . k) - (lim seq1)).|| < r by A3, NORMSP_1:def 7;

take m ; :: thesis: for k being Nat st k >= m holds

dist ((seq2 . k),LIMIT) < r

let k be Nat; :: thesis: ( k >= m implies dist ((seq2 . k),LIMIT) < r )

reconsider p = (seq1 . k) - (lim seq1) as Element of REAL n by Def4;

assume A10: m <= k ; :: thesis: dist ((seq2 . k),LIMIT) < r

- (lim seq1) = - LIMIT by Th13;

then A11: p = (seq2 . k) - LIMIT by A1, Th13;

||.((seq1 . k) - (lim seq1)).|| = |.p.| by Th1

.= sqrt |(p,p)| by EUCLID_2:5

.= sqrt (Sum (mlt (p,p))) by RVSUM_1:def 16

.= sqrt ((Euclid_scalar n) . (p,p)) by Def5

.= ||.((seq2 . k) - LIMIT).|| by A11, Def6 ;

hence dist ((seq2 . k),LIMIT) < r by A9, A10; :: thesis: verum

end;for k being Nat st k >= m holds

dist ((seq2 . k),LIMIT) < r )

assume r > 0 ; :: thesis: ex m being Nat st

for k being Nat st k >= m holds

dist ((seq2 . k),LIMIT) < r

then consider m being Nat such that

A9: for k being Nat st m <= k holds

||.((seq1 . k) - (lim seq1)).|| < r by A3, NORMSP_1:def 7;

take m ; :: thesis: for k being Nat st k >= m holds

dist ((seq2 . k),LIMIT) < r

let k be Nat; :: thesis: ( k >= m implies dist ((seq2 . k),LIMIT) < r )

reconsider p = (seq1 . k) - (lim seq1) as Element of REAL n by Def4;

assume A10: m <= k ; :: thesis: dist ((seq2 . k),LIMIT) < r

- (lim seq1) = - LIMIT by Th13;

then A11: p = (seq2 . k) - LIMIT by A1, Th13;

||.((seq1 . k) - (lim seq1)).|| = |.p.| by Th1

.= sqrt |(p,p)| by EUCLID_2:5

.= sqrt (Sum (mlt (p,p))) by RVSUM_1:def 16

.= sqrt ((Euclid_scalar n) . (p,p)) by Def5

.= ||.((seq2 . k) - LIMIT).|| by A11, Def6 ;

hence dist ((seq2 . k),LIMIT) < r by A9, A10; :: thesis: verum

now :: thesis: ( seq2 is convergent implies ( seq1 is convergent & lim seq1 = lim seq2 ) )

hence
( seq2 is convergent implies ( seq1 is convergent & lim seq1 = lim seq2 ) )
; :: thesis: verumreconsider LIMIT = lim seq2 as Point of (REAL-NS n) by A2;

assume A12: seq2 is convergent ; :: thesis: ( seq1 is convergent & lim seq1 = lim seq2 )

then consider RUg being Point of (REAL-US n) such that

A13: for r being Real st 0 < r holds

ex m being Nat st

for k being Nat st m <= k holds

dist ((seq2 . k),RUg) < r by BHSP_2:def 1;

reconsider RNg = RUg as Point of (REAL-NS n) by A2;

for r being Real st 0 < r holds

ex m being Nat st

for k being Nat st m <= k holds

||.((seq1 . k) - RNg).|| < r

for r being Real st r > 0 holds

ex m being Nat st

for k being Nat st k >= m holds

||.((seq1 . k) - LIMIT).|| < r

end;assume A12: seq2 is convergent ; :: thesis: ( seq1 is convergent & lim seq1 = lim seq2 )

then consider RUg being Point of (REAL-US n) such that

A13: for r being Real st 0 < r holds

ex m being Nat st

for k being Nat st m <= k holds

dist ((seq2 . k),RUg) < r by BHSP_2:def 1;

reconsider RNg = RUg as Point of (REAL-NS n) by A2;

for r being Real st 0 < r holds

ex m being Nat st

for k being Nat st m <= k holds

||.((seq1 . k) - RNg).|| < r

proof

hence A17:
seq1 is convergent
by NORMSP_1:def 6; :: thesis: lim seq1 = lim seq2
let r be Real; :: thesis: ( 0 < r implies ex m being Nat st

for k being Nat st m <= k holds

||.((seq1 . k) - RNg).|| < r )

assume 0 < r ; :: thesis: ex m being Nat st

for k being Nat st m <= k holds

||.((seq1 . k) - RNg).|| < r

then consider m being Nat such that

A14: for k being Nat st m <= k holds

dist ((seq2 . k),RUg) < r by A13;

take m ; :: thesis: for k being Nat st m <= k holds

||.((seq1 . k) - RNg).|| < r

for k being Nat st m <= k holds

||.((seq1 . k) - RNg).|| < r

||.((seq1 . k) - RNg).|| < r ; :: thesis: verum

end;for k being Nat st m <= k holds

||.((seq1 . k) - RNg).|| < r )

assume 0 < r ; :: thesis: ex m being Nat st

for k being Nat st m <= k holds

||.((seq1 . k) - RNg).|| < r

then consider m being Nat such that

A14: for k being Nat st m <= k holds

dist ((seq2 . k),RUg) < r by A13;

take m ; :: thesis: for k being Nat st m <= k holds

||.((seq1 . k) - RNg).|| < r

for k being Nat st m <= k holds

||.((seq1 . k) - RNg).|| < r

proof

hence
for k being Nat st m <= k holds
let k be Nat; :: thesis: ( m <= k implies ||.((seq1 . k) - RNg).|| < r )

reconsider p = (seq2 . k) - RUg as Element of REAL n by Def6;

assume m <= k ; :: thesis: ||.((seq1 . k) - RNg).|| < r

then A15: dist ((seq2 . k),RUg) < r by A14;

- RNg = - RUg by Th13;

then A16: p = (seq1 . k) - RNg by A1, Th13;

dist ((seq2 . k),RUg) = sqrt ((Euclid_scalar n) . (p,p)) by Def6

.= sqrt (Sum (mlt (p,p))) by Def5

.= sqrt |(p,p)| by RVSUM_1:def 16

.= |.p.| by EUCLID_2:5 ;

hence ||.((seq1 . k) - RNg).|| < r by A15, A16, Th1; :: thesis: verum

end;reconsider p = (seq2 . k) - RUg as Element of REAL n by Def6;

assume m <= k ; :: thesis: ||.((seq1 . k) - RNg).|| < r

then A15: dist ((seq2 . k),RUg) < r by A14;

- RNg = - RUg by Th13;

then A16: p = (seq1 . k) - RNg by A1, Th13;

dist ((seq2 . k),RUg) = sqrt ((Euclid_scalar n) . (p,p)) by Def6

.= sqrt (Sum (mlt (p,p))) by Def5

.= sqrt |(p,p)| by RVSUM_1:def 16

.= |.p.| by EUCLID_2:5 ;

hence ||.((seq1 . k) - RNg).|| < r by A15, A16, Th1; :: thesis: verum

||.((seq1 . k) - RNg).|| < r ; :: thesis: verum

for r being Real st r > 0 holds

ex m being Nat st

for k being Nat st k >= m holds

||.((seq1 . k) - LIMIT).|| < r

proof

hence
lim seq1 = lim seq2
by A17, NORMSP_1:def 7; :: thesis: verum
let r be Real; :: thesis: ( r > 0 implies ex m being Nat st

for k being Nat st k >= m holds

||.((seq1 . k) - LIMIT).|| < r )

assume r > 0 ; :: thesis: ex m being Nat st

for k being Nat st k >= m holds

||.((seq1 . k) - LIMIT).|| < r

then consider m being Nat such that

A18: for k being Nat st k >= m holds

dist ((seq2 . k),(lim seq2)) < r by A12, BHSP_2:def 2;

take m ; :: thesis: for k being Nat st k >= m holds

||.((seq1 . k) - LIMIT).|| < r

let k be Nat; :: thesis: ( k >= m implies ||.((seq1 . k) - LIMIT).|| < r )

assume k >= m ; :: thesis: ||.((seq1 . k) - LIMIT).|| < r

then A19: dist ((seq2 . k),(lim seq2)) < r by A18;

reconsider p = (seq2 . k) - (lim seq2) as Element of REAL n by Def6;

- (lim seq2) = - LIMIT by Th13;

then A20: p = (seq1 . k) - LIMIT by A1, Th13;

dist ((seq2 . k),(lim seq2)) = sqrt ((Euclid_scalar n) . (p,p)) by Def6

.= sqrt (Sum (mlt (p,p))) by Def5

.= sqrt |(p,p)| by RVSUM_1:def 16

.= |.p.| by EUCLID_2:5 ;

hence ||.((seq1 . k) - LIMIT).|| < r by A19, A20, Th1; :: thesis: verum

end;for k being Nat st k >= m holds

||.((seq1 . k) - LIMIT).|| < r )

assume r > 0 ; :: thesis: ex m being Nat st

for k being Nat st k >= m holds

||.((seq1 . k) - LIMIT).|| < r

then consider m being Nat such that

A18: for k being Nat st k >= m holds

dist ((seq2 . k),(lim seq2)) < r by A12, BHSP_2:def 2;

take m ; :: thesis: for k being Nat st k >= m holds

||.((seq1 . k) - LIMIT).|| < r

let k be Nat; :: thesis: ( k >= m implies ||.((seq1 . k) - LIMIT).|| < r )

assume k >= m ; :: thesis: ||.((seq1 . k) - LIMIT).|| < r

then A19: dist ((seq2 . k),(lim seq2)) < r by A18;

reconsider p = (seq2 . k) - (lim seq2) as Element of REAL n by Def6;

- (lim seq2) = - LIMIT by Th13;

then A20: p = (seq1 . k) - LIMIT by A1, Th13;

dist ((seq2 . k),(lim seq2)) = sqrt ((Euclid_scalar n) . (p,p)) by Def6

.= sqrt (Sum (mlt (p,p))) by Def5

.= sqrt |(p,p)| by RVSUM_1:def 16

.= |.p.| by EUCLID_2:5 ;

hence ||.((seq1 . k) - LIMIT).|| < r by A19, A20, Th1; :: thesis: verum