let a, b be Real; :: thesis: for S1 being sequence of (Closed-Interval-MSpace (a,b))
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 (Closed-Interval-MSpace (a,b)); :: 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 (Closed-Interval-MSpace (a,b)) = [.a,b.] by A2, TOPMETR:10;
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 FUNCT_1:def 3, A6;
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 A8, A9, TBSP_1:def 3;
then reconsider x1 = x0 as Element of (Closed-Interval-MSpace (a,b)) by A3, A8, A5, A7, Th1, TOPMETR:def 6;
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 (Closed-Interval-MSpace (a,b)) . ((S1 . m),x1) by METRIC_1:def 1
.= the distance of RealSpace . ((S1 . m),x1) by TOPMETR:def 1
.= dist ((S . m),x0) by A1, METRIC_1:def 1 ;
hence dist ((S1 . m),x1) < r by A10, A11; :: 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 (Closed-Interval-MSpace (a,b)) 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 (Closed-Interval-MSpace (a,b)) . ((S1 . m),x0) by METRIC_1:def 1
.= the distance of RealSpace . ((S1 . m),x0) by TOPMETR:def 1
.= dist ((S . m),x1) by A1, METRIC_1:def 1 ;
hence dist ((S . m),x1) < r by A13, A14; :: 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 (Closed-Interval-MSpace (a,b)) ;
then reconsider t0 = lim S1 as Point of RealSpace by A3, METRIC_1:def 13;
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 A4, A15, TBSP_1:def 3;
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 (Closed-Interval-MSpace (a,b)) . ((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 A1, METRIC_1:def 1 ;
hence dist ((S . n1),t0) < r1 by A16, A17; :: 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 A15, TBSP_1:def 3; :: thesis: verum

end;