theorem Th65: :: LPSPACE2:65

for X being RealNormSpace
for Sq being sequence of X st Sq is Cauchy_sequence_by_Norm holds
ex N being increasing sequence of NAT st
for i, j being Nat st j >= N . i holds
||.((Sq . j) - (Sq . (N . i))).|| < 2 to_power (- i)