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, Th28;
consider y being Element of X such that
A5: T is_convergent_in_metrspace_to y and
A6: lim T = y by A2, Th28;
A7: 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 (((sequence_of_dist S,T) . n) - (dist x,y)) < 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 (((sequence_of_dist S,T) . n) - (dist x,y)) < r )
assume A8: 0 < r ; :: thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
abs (((sequence_of_dist S,T) . n) - (dist x,y)) < r
reconsider r = r as Real by XREAL_0:def 1;
A9: 0 < r / 2 by A8, XREAL_1:217;
then consider m1 being Element of NAT such that
A10: for n being Element of NAT st m1 <= n holds
dist (S . n),x < r / 2 by A3, Def8;
consider m2 being Element of NAT such that
A11: for n being Element of NAT st m2 <= n holds
dist (T . n),y < r / 2 by A5, A9, Def8;
take k = m1 + m2; :: thesis: for n being Element of NAT st k <= n holds
abs (((sequence_of_dist S,T) . n) - (dist x,y)) < r
let n be Element of NAT ; :: thesis: ( k <= n implies abs (((sequence_of_dist S,T) . n) - (dist x,y)) < r )
assume A12: k <= n ; :: thesis: abs (((sequence_of_dist S,T) . n) - (dist x,y)) < r
( abs ((dist (S . n),(T . n)) - (dist x,(T . n))) <= dist (S . n),x & abs ((dist (T . n),x) - (dist y,x)) <= dist (T . n),y ) by Th1;
then A13: (abs ((dist (S . n),(T . n)) - (dist (T . n),x))) + (abs ((dist (T . n),x) - (dist x,y))) <= (dist (S . n),x) + (dist (T . n),y) by XREAL_1:9;
abs (((sequence_of_dist S,T) . n) - (dist (lim S),(lim T))) = abs ((dist (S . n),(T . n)) - (dist x,y)) by A4, A6, Def15
.= abs (((dist (S . n),(T . n)) - (dist (T . n),x)) + ((dist (T . n),x) - (dist x,y))) ;
then abs (((sequence_of_dist S,T) . n) - (dist (lim S),(lim T))) <= (abs ((dist (S . n),(T . n)) - (dist (T . n),x))) + (abs ((dist (T . n),x) - (dist x,y))) by COMPLEX1:142;
then A14: abs (((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:10;
hence abs (((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