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:215;
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:7;
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:56;
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:8;
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