let a, b be Real; :: thesis: for S1 being sequence of ()
for S being sequence of RealSpace st S = S1 & a <= b holds
( ( S is convergent implies S1 is convergent ) & ( S1 is convergent implies S is convergent ) & ( S is convergent implies lim S = lim S1 ) )

let S1 be sequence of (); :: thesis: for S being sequence of RealSpace st S = S1 & a <= b holds
( ( S is convergent implies S1 is convergent ) & ( S1 is convergent implies S is convergent ) & ( S is convergent implies lim S = lim S1 ) )

let S be sequence of RealSpace; :: thesis: ( S = S1 & a <= b implies ( ( S is convergent implies S1 is convergent ) & ( S1 is convergent implies S is convergent ) & ( S is convergent implies lim S = lim S1 ) ) )
assume that
A1: S = S1 and
A2: a <= b ; :: thesis: ( ( S is convergent implies S1 is convergent ) & ( S1 is convergent implies S is convergent ) & ( S is convergent implies lim S = lim S1 ) )
reconsider P = [.a,b.] as Subset of R^1 by TOPMETR:17;
A3: the carrier of () = [.a,b.] by ;
A4: ( S is convergent implies S1 is convergent )
proof
A5: for m being Nat holds S . m in [.a,b.]
proof
let m be Nat; :: thesis: S . m in [.a,b.]
A6: m in NAT by ORDINAL1:def 12;
dom S1 = NAT by FUNCT_2:def 1;
then S1 . m in rng S1 by ;
hence S . m in [.a,b.] by A1, A3; :: thesis: verum
end;
A7: P is closed by TREAL_1:1;
assume A8: S is convergent ; :: thesis: S1 is convergent
then consider x0 being Element of RealSpace such that
A9: for r being Real st r > 0 holds
ex n being Nat st
for m being Nat st n <= m holds
dist ((S . m),x0) < r by TBSP_1:def 2;
x0 = lim S by ;
then reconsider x1 = x0 as Element of () by ;
for r being Real st r > 0 holds
ex n being Nat st
for m being Nat st n <= m holds
dist ((S1 . m),x1) < r
proof
let r be Real; :: thesis: ( r > 0 implies ex n being Nat st
for m being Nat st n <= m holds
dist ((S1 . m),x1) < r )

assume r > 0 ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
dist ((S1 . m),x1) < r

then consider n0 being Nat such that
A10: for m being Nat st n0 <= m holds
dist ((S . m),x0) < r by A9;
for m being Nat st n0 <= m holds
dist ((S1 . m),x1) < r
proof
let m be Nat; :: thesis: ( n0 <= m implies dist ((S1 . m),x1) < r )
assume A11: n0 <= m ; :: thesis: dist ((S1 . m),x1) < r
dist ((S1 . m),x1) = the distance of () . ((S1 . m),x1) by METRIC_1:def 1
.= the distance of RealSpace . ((S1 . m),x1) by TOPMETR:def 1
.= dist ((S . m),x0) by ;
hence dist ((S1 . m),x1) < r by ; :: thesis: verum
end;
hence ex n being Nat st
for m being Nat st n <= m holds
dist ((S1 . m),x1) < r ; :: thesis: verum
end;
hence S1 is convergent by TBSP_1:def 2; :: thesis: verum
end;
( S1 is convergent implies S is convergent )
proof
assume S1 is convergent ; :: thesis: S is convergent
then consider x0 being Element of () such that
A12: for r being Real st r > 0 holds
ex n being Nat st
for m being Nat st n <= m holds
dist ((S1 . m),x0) < r by TBSP_1:def 2;
x0 in [.a,b.] by A3;
then reconsider x1 = x0 as Element of RealSpace by METRIC_1:def 13;
for r being Real st r > 0 holds
ex n being Nat st
for m being Nat st n <= m holds
dist ((S . m),x1) < r
proof
let r be Real; :: thesis: ( r > 0 implies ex n being Nat st
for m being Nat st n <= m holds
dist ((S . m),x1) < r )

assume r > 0 ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
dist ((S . m),x1) < r

then consider n0 being Nat such that
A13: for m being Nat st n0 <= m holds
dist ((S1 . m),x0) < r by A12;
for m being Nat st n0 <= m holds
dist ((S . m),x1) < r
proof
let m be Nat; :: thesis: ( n0 <= m implies dist ((S . m),x1) < r )
assume A14: n0 <= m ; :: thesis: dist ((S . m),x1) < r
dist ((S1 . m),x0) = the distance of () . ((S1 . m),x0) by METRIC_1:def 1
.= the distance of RealSpace . ((S1 . m),x0) by TOPMETR:def 1
.= dist ((S . m),x1) by ;
hence dist ((S . m),x1) < r by ; :: thesis: verum
end;
hence ex n being Nat st
for m being Nat st n <= m holds
dist ((S . m),x1) < r ; :: thesis: verum
end;
hence S is convergent by TBSP_1:def 2; :: thesis: verum
end;
hence ( S is convergent iff S1 is convergent ) by A4; :: thesis: ( S is convergent implies lim S = lim S1 )
thus ( S is convergent implies lim S = lim S1 ) :: thesis: verum
proof
lim S1 in the carrier of () ;
then reconsider t0 = lim S1 as Point of RealSpace by ;
assume A15: S is convergent ; :: thesis: lim S = lim S1
for r1 being Real st 0 < r1 holds
ex m1 being Nat st
for n1 being Nat st m1 <= n1 holds
dist ((S . n1),t0) < r1
proof
let r1 be Real; :: thesis: ( 0 < r1 implies ex m1 being Nat st
for n1 being Nat st m1 <= n1 holds
dist ((S . n1),t0) < r1 )

assume 0 < r1 ; :: thesis: ex m1 being Nat st
for n1 being Nat st m1 <= n1 holds
dist ((S . n1),t0) < r1

then consider m1 being Nat such that
A16: for n1 being Nat st m1 <= n1 holds
dist ((S1 . n1),(lim S1)) < r1 by ;
for n1 being Nat st m1 <= n1 holds
dist ((S . n1),t0) < r1
proof
let n1 be Nat; :: thesis: ( m1 <= n1 implies dist ((S . n1),t0) < r1 )
assume A17: m1 <= n1 ; :: thesis: dist ((S . n1),t0) < r1
dist ((S1 . n1),(lim S1)) = the distance of () . ((S1 . n1),(lim S1)) by METRIC_1:def 1
.= the distance of RealSpace . ((S1 . n1),(lim S1)) by TOPMETR:def 1
.= dist ((S . n1),t0) by ;
hence dist ((S . n1),t0) < r1 by ; :: thesis: verum
end;
hence ex m1 being Nat st
for n1 being Nat st m1 <= n1 holds
dist ((S . n1),t0) < r1 ; :: thesis: verum
end;
hence lim S = lim S1 by ; :: thesis: verum
end;