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 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
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
proof
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;
hence ex n being Nat st
for m being Nat st n <= m holds
dist ((S . m),x0) < r ; :: thesis: verum
end;
hence S is convergent by TBSP_1:def 2; :: 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 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
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
proof
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;
hence ex n being Nat st
for m being Nat st n <= m holds
|.((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 ;
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
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
proof
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;
hence ex m being Nat st
for n being Nat st m <= n holds
|.((s . n) - g0).| < r ; :: thesis: verum
end;
hence lim s = lim S by A9, SEQ_2:def 7; :: thesis: verum
end;