let a, b be real number ; 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:24;
A3:
the carrier of (Closed-Interval-MSpace a,b) = [.a,b.]
by A2, TOPMETR:14;
A4:
( S is convergent implies S1 is convergent )
proof
A5:
for
m being
Element of
NAT holds
S . m in [.a,b.]
A6:
P is
closed
by TREAL_1:4;
assume A7:
S is
convergent
;
S1 is convergent
then consider x0 being
Element of
RealSpace such that A8:
for
r being
Real st
r > 0 holds
ex
n being
Element of
NAT st
for
m being
Element of
NAT st
n <= m holds
dist (S . m),
x0 < r
by TBSP_1:def 3;
x0 = lim S
by A7, A8, TBSP_1:def 4;
then reconsider x1 =
x0 as
Element of
(Closed-Interval-MSpace a,b) by A3, A7, A5, A6, Th2, TOPMETR:def 7;
for
r being
Real st
r > 0 holds
ex
n being
Element of
NAT st
for
m being
Element of
NAT st
n <= m holds
dist (S1 . m),
x1 < r
proof
let r be
Real;
( r > 0 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist (S1 . m),x1 < r )
assume
r > 0
;
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist (S1 . m),x1 < r
then consider n0 being
Element of
NAT such that A9:
for
m being
Element of
NAT st
n0 <= m holds
dist (S . m),
x0 < r
by A8;
for
m being
Element of
NAT st
n0 <= m holds
dist (S1 . m),
x1 < r
proof
let m be
Element of
NAT ;
( n0 <= m implies dist (S1 . m),x1 < r )
assume A10:
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 A9, A10;
verum
end;
hence
ex
n being
Element of
NAT st
for
m being
Element of
NAT st
n <= m holds
dist (S1 . m),
x1 < r
;
verum
end;
hence
S1 is
convergent
by TBSP_1:def 3;
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 A11:
for
r being
Real st
r > 0 holds
ex
n being
Element of
NAT st
for
m being
Element of
NAT st
n <= m holds
dist (S1 . m),
x0 < r
by TBSP_1:def 3;
x0 in [.a,b.]
by A3;
then reconsider x1 =
x0 as
Element of
RealSpace by METRIC_1:def 14;
for
r being
Real st
r > 0 holds
ex
n being
Element of
NAT st
for
m being
Element of
NAT st
n <= m holds
dist (S . m),
x1 < r
proof
let r be
Real;
( r > 0 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist (S . m),x1 < r )
assume
r > 0
;
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist (S . m),x1 < r
then consider n0 being
Element of
NAT such that A12:
for
m being
Element of
NAT st
n0 <= m holds
dist (S1 . m),
x0 < r
by A11;
for
m being
Element of
NAT st
n0 <= m holds
dist (S . m),
x1 < r
proof
let m be
Element of
NAT ;
( n0 <= m implies dist (S . m),x1 < r )
assume A13:
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 A12, A13;
verum
end;
hence
ex
n being
Element of
NAT st
for
m being
Element of
NAT st
n <= m holds
dist (S . m),
x1 < r
;
verum
end;
hence
S is
convergent
by TBSP_1:def 3;
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 14;
assume A14:
S is
convergent
;
lim S = lim S1
for
r1 being
Real st
0 < r1 holds
ex
m1 being
Element of
NAT st
for
n1 being
Element of
NAT st
m1 <= n1 holds
dist (S . n1),
t0 < r1
proof
let r1 be
Real;
( 0 < r1 implies ex m1 being Element of NAT st
for n1 being Element of NAT st m1 <= n1 holds
dist (S . n1),t0 < r1 )
assume
0 < r1
;
ex m1 being Element of NAT st
for n1 being Element of NAT st m1 <= n1 holds
dist (S . n1),t0 < r1
then consider m1 being
Element of
NAT such that A15:
for
n1 being
Element of
NAT st
m1 <= n1 holds
dist (S1 . n1),
(lim S1) < r1
by A4, A14, TBSP_1:def 4;
for
n1 being
Element of
NAT st
m1 <= n1 holds
dist (S . n1),
t0 < r1
proof
let n1 be
Element of
NAT ;
( m1 <= n1 implies dist (S . n1),t0 < r1 )
assume A16:
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 A15, A16;
verum
end;
hence
ex
m1 being
Element of
NAT st
for
n1 being
Element of
NAT st
m1 <= n1 holds
dist (S . n1),
t0 < r1
;
verum
end;
hence
lim S = lim S1
by A14, TBSP_1:def 4;
verum
end;