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 ;

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

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

proof

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;

hence A8: seq2 is convergent by BHSP_2:def 1; :: thesis: lim seq2 = lim seq1
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

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;

hence lim seq2 = lim seq1 by A8, BHSP_2:def 2; :: thesis: verum

end;

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

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

reconsider 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

proof

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

proof

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;

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

end;

hence A17: seq1 is convergent by NORMSP_1:def 6; :: thesis: lim seq1 = lim seq2
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

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;

hence lim seq1 = lim seq2 by A17, NORMSP_1:def 7; :: thesis: verum

end;

hence ( seq2 is convergent implies ( seq1 is convergent & lim seq1 = lim seq2 ) ) ; :: thesis: verum