:: deftheorem Def7 defines sequence_of_dist METRIC_6:def 7 :
for X being non empty MetrSpace
for S, T being sequence of X
for b₄ being Real_Sequence holds
( b₄ = sequence_of_dist (S,T) iff for n being Nat holds b₄ . n = dist ((S . n),(T . n)) );