let X be non empty MetrSpace; :: thesis: for S, T being sequence of X st S is convergent & T is convergent holds
dist ((lim S),(lim T)) = lim (sequence_of_dist (S,T))
let S, T be sequence of X; :: thesis: ( S is convergent & T is convergent implies dist ((lim S),(lim T)) = lim (sequence_of_dist (S,T)) )
assume that
A1: S is convergent and
A2: T is convergent ; :: thesis: dist ((lim S),(lim T)) = lim (sequence_of_dist (S,T))
consider x being Element of X such that
A3: S is_convergent_in_metrspace_to x and
A4: lim S = x by A1, Th13;
consider y being Element of X such that
A5: T is_convergent_in_metrspace_to y and
A6: lim T = y by A2, Th13;
A7: for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
|.(((sequence_of_dist (S,T)) . n) - (dist (x,y))).| < r

proof

let r be Real; :: thesis: ( 0 < r implies ex m being Nat st
for n being Nat st m <= n holds
|.(((sequence_of_dist (S,T)) . n) - (dist (x,y))).| < r )
assume A8: 0 < r ; :: thesis: ex m being Nat st
for n being Nat st m <= n holds
|.(((sequence_of_dist (S,T)) . n) - (dist (x,y))).| < r
reconsider r = r as Real ;
A9: 0 < r / 2 by A8, XREAL_1:215;
then consider m1 being Nat such that
A10: for n being Nat st m1 <= n holds
dist ((S . n),x) < r / 2 by A3;
consider m2 being Nat such that
A11: for n being Nat st m2 <= n holds
dist ((T . n),y) < r / 2 by A5, A9;
reconsider k = m1 + m2 as Nat ;
take k ; :: thesis: for n being Nat st k <= n holds
|.(((sequence_of_dist (S,T)) . n) - (dist (x,y))).| < r
let n be Nat; :: thesis: ( k <= n implies |.(((sequence_of_dist (S,T)) . n) - (dist (x,y))).| < r )
assume A12: k <= n ; :: thesis: |.(((sequence_of_dist (S,T)) . n) - (dist (x,y))).| < r
( |.((dist ((S . n),(T . n))) - (dist (x,(T . n)))).| <= dist ((S . n),x) & |.((dist ((T . n),x)) - (dist (y,x))).| <= dist ((T . n),y) ) by Th1;
then A13: |.((dist ((S . n),(T . n))) - (dist ((T . n),x))).| + |.((dist ((T . n),x)) - (dist (x,y))).| <= (dist ((S . n),x)) + (dist ((T . n),y)) by XREAL_1:7;
|.(((sequence_of_dist (S,T)) . n) - (dist ((lim S),(lim T)))).| = |.((dist ((S . n),(T . n))) - (dist (x,y))).| by A4, A6, Def7
.= |.(((dist ((S . n),(T . n))) - (dist ((T . n),x))) + ((dist ((T . n),x)) - (dist (x,y)))).| ;
then |.(((sequence_of_dist (S,T)) . n) - (dist ((lim S),(lim T)))).| <= |.((dist ((S . n),(T . n))) - (dist ((T . n),x))).| + |.((dist ((T . n),x)) - (dist (x,y))).| by COMPLEX1:56;
then A14: |.(((sequence_of_dist (S,T)) . n) - (dist ((lim S),(lim T)))).| <= (dist ((S . n),x)) + (dist ((T . n),y)) by A13, XXREAL_0:2;
m2 <= k by NAT_1:12;
then m2 <= n by A12, XXREAL_0:2;
then A15: dist ((T . n),y) < r / 2 by A11;
m1 <= k by NAT_1:11;
then m1 <= n by A12, XXREAL_0:2;
then dist ((S . n),x) < r / 2 by A10;
then (dist ((S . n),x)) + (dist ((T . n),y)) < (r / 2) + (r / 2) by A15, XREAL_1:8;
hence |.(((sequence_of_dist (S,T)) . n) - (dist (x,y))).| < r by A4, A6, A14, XXREAL_0:2; :: thesis: verum

end;

then sequence_of_dist (S,T) is convergent by SEQ_2:def 6;
hence dist ((lim S),(lim T)) = lim (sequence_of_dist (S,T)) by A4, A6, A7, SEQ_2:def 7; :: thesis: verum