let s be Real_Sequence; :: thesis: for S being sequence of RealSpace st s = S holds
( ( s is convergent implies S is convergent ) & ( S is convergent implies s is convergent ) & ( s is convergent implies lim s = lim S ) )
let S be sequence of RealSpace; :: thesis: ( s = S implies ( ( s is convergent implies S is convergent ) & ( S is convergent implies s is convergent ) & ( s is convergent implies lim s = lim S ) ) )
assume A1: s = S ; :: thesis: ( ( s is convergent implies S is convergent ) & ( S is convergent implies s is convergent ) & ( s is convergent implies lim s = lim S ) )
A2: ( s is convergent implies S is convergent )

proof

assume s is convergent ; :: thesis: S is convergent
then consider g being real number such that
A3: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((s . m) - g) < p by SEQ_2:def 6;
reconsider g0 = g as Real by XREAL_0:def 1;
reconsider x0 = g as Point of RealSpace by METRIC_1:def 14, XREAL_0:def 1;
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

proof

let r be Real; :: thesis: ( r > 0 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist ((S . m),x0) < r )
assume r > 0 ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist ((S . m),x0) < r
then consider n0 being Element of NAT such that
A4: for m being Element of NAT st n0 <= m holds
abs ((s . m) - g) < r by A3;
for m being Element of NAT st n0 <= m holds
dist ((S . m),x0) < r

proof

let m be Element of NAT ; :: thesis: ( n0 <= m implies dist ((S . m),x0) < r )
assume A5: n0 <= m ; :: thesis: dist ((S . m),x0) < r
reconsider t = s . m as Real ;
dist ((S . m),x0) = real_dist . (t,g) by A1, METRIC_1:def 1, METRIC_1:def 14
.= abs (t - g0) by METRIC_1:def 13 ;
hence dist ((S . m),x0) < r by A4, A5; :: thesis: verum

end;

hence ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist ((S . m),x0) < r ; :: thesis: verum

end;

hence S is convergent by TBSP_1:def 3; :: thesis: verum

end;

( S is convergent implies s is convergent )

proof

assume S is convergent ; :: thesis: s is convergent
then consider x being Element of RealSpace such that
A6: 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),x) < r by TBSP_1:def 3;
reconsider g0 = x as Real by METRIC_1:def 14;
for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((s . m) - g0) < p

proof

let p be real number ; :: thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((s . m) - g0) < p )
reconsider p0 = p as Real by XREAL_0:def 1;
assume 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((s . m) - g0) < p
then consider n0 being Element of NAT such that
A7: for m being Element of NAT st n0 <= m holds
dist ((S . m),x) < p0 by A6;
for m being Element of NAT st n0 <= m holds
abs ((s . m) - g0) < p

proof

let m be Element of NAT ; :: thesis: ( n0 <= m implies abs ((s . m) - g0) < p )
assume A8: n0 <= m ; :: thesis: abs ((s . m) - g0) < p
reconsider t = s . m as Real ;
dist ((S . m),x) = real_dist . (t,g0) by A1, METRIC_1:def 1, METRIC_1:def 14
.= abs (t - g0) by METRIC_1:def 13 ;
hence abs ((s . m) - g0) < p by A7, A8; :: thesis: verum

end;

hence ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((s . m) - g0) < p ; :: thesis: verum

end;

hence s is convergent by SEQ_2:def 6; :: thesis: verum

end;

hence ( s is convergent iff S is convergent ) by A2; :: thesis: ( s is convergent implies lim s = lim S )
thus ( s is convergent implies lim s = lim S ) :: thesis: verum

proof

reconsider g0 = lim S as Real by METRIC_1:def 14;
assume A9: s is convergent ; :: thesis: lim s = lim S
for r being real number st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
abs ((s . n) - g0) < r

proof

let r be real number ; :: thesis: ( 0 < r implies ex m being Element of NAT st
for n being Element of NAT st m <= n holds
abs ((s . n) - g0) < r )
reconsider r0 = r as Real by XREAL_0:def 1;
assume 0 < r ; :: thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
abs ((s . n) - g0) < r
then consider m0 being Element of NAT such that
A10: for n being Element of NAT st m0 <= n holds
dist ((S . n),(lim S)) < r0 by A2, A9, TBSP_1:def 4;
for n being Element of NAT st m0 <= n holds
abs ((s . n) - g0) < r

proof

let n be Element of NAT ; :: thesis: ( m0 <= n implies abs ((s . n) - g0) < r )
assume A11: m0 <= n ; :: thesis: abs ((s . n) - g0) < r
dist ((S . n),(lim S)) = real_dist . ((s . n),g0) by A1, METRIC_1:def 1, METRIC_1:def 14
.= abs ((s . n) - g0) by METRIC_1:def 13 ;
hence abs ((s . n) - g0) < r by A10, A11; :: thesis: verum

end;

hence ex m being Element of NAT st
for n being Element of NAT st m <= n holds
abs ((s . n) - g0) < r ; :: thesis: verum

end;

hence lim s = lim S by A9, SEQ_2:def 7; :: thesis: verum

end;