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 )

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

( ( 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

( S is convergent implies s is convergent )
assume
s is convergent
; :: thesis: S is convergent

then consider g being Real such that

A3: for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((s . m) - g).| < p by SEQ_2:def 6;

reconsider g0 = g as Real ;

reconsider x0 = g as Point of RealSpace by METRIC_1:def 13, XREAL_0:def 1;

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

end;then consider g being Real such that

A3: for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((s . m) - g).| < p by SEQ_2:def 6;

reconsider g0 = g as Real ;

reconsider x0 = g as Point of RealSpace by METRIC_1:def 13, XREAL_0:def 1;

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

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),x0) < r )

assume r > 0 ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

dist ((S . m),x0) < r

then consider n0 being Nat such that

A4: for m being Nat st n0 <= m holds

|.((s . m) - g).| < r by A3;

for m being Nat st n0 <= m holds

dist ((S . m),x0) < r

for m being Nat st n <= m holds

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

end;for m being Nat st n <= m holds

dist ((S . m),x0) < r )

assume r > 0 ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

dist ((S . m),x0) < r

then consider n0 being Nat such that

A4: for m being Nat st n0 <= m holds

|.((s . m) - g).| < r by A3;

for m being Nat st n0 <= m holds

dist ((S . m),x0) < r

proof

hence
ex n being Nat st
let m be 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 13

.= |.(t - g0).| by METRIC_1:def 12 ;

hence dist ((S . m),x0) < r by A4, A5; :: thesis: verum

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

.= |.(t - g0).| by METRIC_1:def 12 ;

hence dist ((S . m),x0) < r by A4, A5; :: thesis: verum

for m being Nat st n <= m holds

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

proof

hence
( s is convergent iff S is convergent )
by A2; :: thesis: ( s is convergent implies lim s = lim S )
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 Nat st

for m being Nat st n <= m holds

dist ((S . m),x) < r by TBSP_1:def 2;

reconsider g0 = x as Real ;

for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((s . m) - g0).| < p

end;then consider x being Element of RealSpace such that

A6: for r being Real st r > 0 holds

ex n being Nat st

for m being Nat st n <= m holds

dist ((S . m),x) < r by TBSP_1:def 2;

reconsider g0 = x as Real ;

for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((s . m) - g0).| < p

proof

hence
s is convergent
by SEQ_2:def 6; :: thesis: verum
let p be Real; :: thesis: ( 0 < p implies ex n being Nat st

for m being Nat st n <= m holds

|.((s . m) - g0).| < p )

reconsider p0 = p as Real ;

assume 0 < p ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

|.((s . m) - g0).| < p

then consider n0 being Nat such that

A7: for m being Nat st n0 <= m holds

dist ((S . m),x) < p0 by A6;

for m being Nat st n0 <= m holds

|.((s . m) - g0).| < p

for m being Nat st n <= m holds

|.((s . m) - g0).| < p ; :: thesis: verum

end;for m being Nat st n <= m holds

|.((s . m) - g0).| < p )

reconsider p0 = p as Real ;

assume 0 < p ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

|.((s . m) - g0).| < p

then consider n0 being Nat such that

A7: for m being Nat st n0 <= m holds

dist ((S . m),x) < p0 by A6;

for m being Nat st n0 <= m holds

|.((s . m) - g0).| < p

proof

hence
ex n being Nat st
let m be Nat; :: thesis: ( n0 <= m implies |.((s . m) - g0).| < p )

assume A8: n0 <= m ; :: thesis: |.((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 13

.= |.(t - g0).| by METRIC_1:def 12 ;

hence |.((s . m) - g0).| < p by A7, A8; :: thesis: verum

end;assume A8: n0 <= m ; :: thesis: |.((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 13

.= |.(t - g0).| by METRIC_1:def 12 ;

hence |.((s . m) - g0).| < p by A7, A8; :: thesis: verum

for m being Nat st n <= m holds

|.((s . m) - g0).| < p ; :: thesis: verum

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

proof

reconsider g0 = lim S as Real ;

assume A9: s is convergent ; :: thesis: lim s = lim S

for r being Real st 0 < r holds

ex m being Nat st

for n being Nat st m <= n holds

|.((s . n) - g0).| < r

end;assume A9: s is convergent ; :: thesis: lim s = lim S

for r being Real st 0 < r holds

ex m being Nat st

for n being Nat st m <= n holds

|.((s . n) - g0).| < r

proof

hence
lim s = lim S
by A9, SEQ_2:def 7; :: thesis: verum
let r be Real; :: thesis: ( 0 < r implies ex m being Nat st

for n being Nat st m <= n holds

|.((s . n) - g0).| < r )

reconsider r0 = r as Real ;

assume 0 < r ; :: thesis: ex m being Nat st

for n being Nat st m <= n holds

|.((s . n) - g0).| < r

then consider m0 being Nat such that

A10: for n being Nat st m0 <= n holds

dist ((S . n),(lim S)) < r0 by A2, A9, TBSP_1:def 3;

for n being Nat st m0 <= n holds

|.((s . n) - g0).| < r

for n being Nat st m <= n holds

|.((s . n) - g0).| < r ; :: thesis: verum

end;for n being Nat st m <= n holds

|.((s . n) - g0).| < r )

reconsider r0 = r as Real ;

assume 0 < r ; :: thesis: ex m being Nat st

for n being Nat st m <= n holds

|.((s . n) - g0).| < r

then consider m0 being Nat such that

A10: for n being Nat st m0 <= n holds

dist ((S . n),(lim S)) < r0 by A2, A9, TBSP_1:def 3;

for n being Nat st m0 <= n holds

|.((s . n) - g0).| < r

proof

hence
ex m being Nat st
let n be Nat; :: thesis: ( m0 <= n implies |.((s . n) - g0).| < r )

assume A11: m0 <= n ; :: thesis: |.((s . n) - g0).| < r

dist ((S . n),(lim S)) = real_dist . ((s . n),g0) by A1, METRIC_1:def 1, METRIC_1:def 13

.= |.((s . n) - g0).| by METRIC_1:def 12 ;

hence |.((s . n) - g0).| < r by A10, A11; :: thesis: verum

end;assume A11: m0 <= n ; :: thesis: |.((s . n) - g0).| < r

dist ((S . n),(lim S)) = real_dist . ((s . n),g0) by A1, METRIC_1:def 1, METRIC_1:def 13

.= |.((s . n) - g0).| by METRIC_1:def 12 ;

hence |.((s . n) - g0).| < r by A10, A11; :: thesis: verum

for n being Nat st m <= n holds

|.((s . n) - g0).| < r ; :: thesis: verum