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