for n being Nat
for x being Point of (REAL-NS n)
for xs being Element of REAL n
for seq being sequence of (REAL-NS n)
for xseq being sequence of (REAL n) st xs = x & xseq = seq holds
( ( seq is convergent & lim seq = x ) iff for i being Nat st i in Seg n holds
ex rseqi being Real_Sequence st
for k being Nat holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) )