theorem Th4: :: RUSUB_7:4

for X being RealUnitarySpace
for S being sequence of X
for St being sequence of (MetricSpaceNorm (RUSp2RNSp X))
for x being Point of X
for xt being Point of (MetricSpaceNorm (RUSp2RNSp X)) st S = St & x = xt holds
( St is_convergent_in_metrspace_to xt iff for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((S . n) - x).|| < r )