theorem Th23: :: TOPMETR4:20

for S1 being sequence of RealSpace
for seq being Real_Sequence
for g being Real
for g1 being Element of RealSpace st S1 = seq & g = g1 holds
( ( for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - g).| < p ) iff for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
dist ((S1 . m),g1) < p )