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 A1: ( S is convergent & T is convergent ) ; :: thesis: dist (lim S),(lim T) = lim (sequence_of_dist S,T)
then consider x being Element of X such that
A2: ( S is_convergent_in_metrspace_to x & lim S = x ) by Th28;
consider y being Element of X such that
A3: ( T is_convergent_in_metrspace_to y & lim T = y ) by A1, Th28;
A4: 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 A5: 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;
A6: 0 < r / 2 by A5, XREAL_1:217;
then consider m1 being Element of NAT such that
A7: for n being Element of NAT st m1 <= n holds
dist (S . n),x < r / 2 by A2, Def8;
consider m2 being Element of NAT such that
A8: for n being Element of NAT st m2 <= n holds
dist (T . n),y < r / 2 by A3, A6, 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 A9: k <= n ; :: thesis: abs (((sequence_of_dist S,T) . n) - (dist x,y)) < r
m1 <= k by NAT_1:11;
then m1 <= n by A9, XXREAL_0:2;
then A10: dist (S . n),x < r / 2 by A7;
m2 <= k by NAT_1:12;
then m2 <= n by A9, XXREAL_0:2;
then A11: dist (T . n),y < r / 2 by A8;
abs (((sequence_of_dist S,T) . n) - (dist (lim S),(lim T))) = abs ((dist (S . n),(T . n)) - (dist x,y)) by A2, A3, Def15
.= abs (((dist (S . n),(T . n)) - (dist (T . n),x)) + ((dist (T . n),x) - (dist x,y))) ;
then A12: 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;
A13: abs ((dist (S . n),(T . n)) - (dist x,(T . n))) <= dist (S . n),x by Th1;
abs ((dist (T . n),x) - (dist y,x)) <= dist (T . n),y by Th1;
then A14: (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 A13, XREAL_1:9;
A15: (dist (S . n),x) + (dist (T . n),y) < (r / 2) + (r / 2) by A10, A11, XREAL_1:10;
abs (((sequence_of_dist S,T) . n) - (dist (lim S),(lim T))) <= (dist (S . n),x) + (dist (T . n),y) by A12, A14, XXREAL_0:2;
then abs (((sequence_of_dist S,T) . n) - (dist (lim S),(lim T))) < r by A15, XXREAL_0:2;
hence abs (((sequence_of_dist S,T) . n) - (dist x,y)) < r by A2, A3; :: 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 A2, A3, A4, SEQ_2:def 7; :: thesis: verum