for M being non empty MetrSpace
for s being sequence of the carrier of (TopSpaceMetr M)
for x being Point of (TopSpaceMetr M) holds
( x in lim_f s iff x in Lim s )