let a, b be Real; 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)); 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; ( 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
; ( ( 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.]
A7:
P is
closed
by TREAL_1:1;
assume A8:
S is
convergent
;
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;
( r > 0 implies ex n being Nat st
for m being Nat st n <= m holds
dist ((S1 . m),x1) < r )
assume
r > 0
;
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;
( n0 <= m implies dist ((S1 . m),x1) < r )
assume A11:
n0 <= m
;
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;
verum
end;
hence
ex
n being
Nat st
for
m being
Nat st
n <= m holds
dist (
(S1 . m),
x1)
< r
;
verum
end;
hence
S1 is
convergent
by TBSP_1:def 2;
verum
end;
( S1 is convergent implies S is convergent )
proof
assume
S1 is
convergent
;
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;
( r > 0 implies ex n being Nat st
for m being Nat st n <= m holds
dist ((S . m),x1) < r )
assume
r > 0
;
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;
( n0 <= m implies dist ((S . m),x1) < r )
assume A14:
n0 <= m
;
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;
verum
end;
hence
ex
n being
Nat st
for
m being
Nat st
n <= m holds
dist (
(S . m),
x1)
< r
;
verum
end;
hence
S is
convergent
by TBSP_1:def 2;
verum
end;
hence
( S is convergent iff S1 is convergent )
by A4; ( S is convergent implies lim S = lim S1 )
thus
( S is convergent implies lim S = lim S1 )
verumproof
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
;
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;
( 0 < r1 implies ex m1 being Nat st
for n1 being Nat st m1 <= n1 holds
dist ((S . n1),t0) < r1 )
assume
0 < r1
;
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;
( m1 <= n1 implies dist ((S . n1),t0) < r1 )
assume A17:
m1 <= n1
;
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;
verum
end;
hence
ex
m1 being
Nat st
for
n1 being
Nat st
m1 <= n1 holds
dist (
(S . n1),
t0)
< r1
;
verum
end;
hence
lim S = lim S1
by A15, TBSP_1:def 3;
verum
end;