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 )

thus ( S is convergent implies lim S = lim S1 ) :: thesis: verum

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

( S1 is convergent implies S is convergent )
A5:
for m being Nat holds S . m in [.a,b.]

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

end;proof

A7:
P is closed
by TREAL_1:1;
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;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

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

hence
S1 is convergent
by TBSP_1:def 2; :: thesis: verum
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

for m being Nat st n <= m holds

dist ((S1 . m),x1) < r ; :: thesis: verum

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

hence
ex n being Nat st
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;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

for m being Nat st n <= m holds

dist ((S1 . m),x1) < r ; :: thesis: verum

proof

hence
( S is convergent iff S1 is convergent )
by A4; :: thesis: ( S is convergent implies lim S = lim S1 )
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

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

hence
S is convergent
by TBSP_1:def 2; :: thesis: verum
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

for m being Nat st n <= m holds

dist ((S . m),x1) < r ; :: thesis: verum

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

hence
ex n being Nat st
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;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

for m being Nat st n <= m holds

dist ((S . m),x1) < r ; :: thesis: verum

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

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

hence
lim S = lim S1
by A15, TBSP_1:def 3; :: thesis: verum
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

for n1 being Nat st m1 <= n1 holds

dist ((S . n1),t0) < r1 ; :: thesis: verum

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

hence
ex m1 being Nat st
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;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

for n1 being Nat st m1 <= n1 holds

dist ((S . n1),t0) < r1 ; :: thesis: verum